Skip to content

Commit bf5b11c

Browse files
tirixtirix
authored
Split ~ footex (#3275)
* Split `~ footex`
1 parent 82f8fc5 commit bf5b11c

File tree

2 files changed

+132
-3
lines changed

2 files changed

+132
-3
lines changed

‎discouraged‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15412,6 +15412,7 @@ New usage of "flddivrng" is discouraged (2 uses).
1541215412
New usage of "fldhmsubcALTV" is discouraged (0 uses).
1541315413
New usage of "fnexALT" is discouraged (0 uses).
1541415414
New usage of "fnmpt2ovdOLD" is discouraged (0 uses).
15415+
New usage of "footexALT" is discouraged (0 uses).
1541515416
New usage of "fresisonOLD" is discouraged (0 uses).
1541615417
New usage of "frgrwopreglem5ALT" is discouraged (0 uses).
1541715418
New usage of "funadj" is discouraged (4 uses).
@@ -18896,6 +18897,7 @@ Proof modification of "fimaxreOLD" is discouraged (172 steps).
1889618897
Proof modification of "fiminreOLD" is discouraged (312 steps).
1889718898
Proof modification of "fnexALT" is discouraged (111 steps).
1889818899
Proof modification of "fnmpt2ovdOLD" is discouraged (219 steps).
18900+
Proof modification of "footexALT" is discouraged (2161 steps).
1889918901
Proof modification of "frege10" is discouraged (27 steps).
1890018902
Proof modification of "frege100" is discouraged (31 steps).
1890118903
Proof modification of "frege101" is discouraged (49 steps).

‎set.mm‎

Lines changed: 130 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -387516,9 +387516,10 @@ are congruent (CPCTC), focusing on a specific segment. (Contributed
387516387516
$d a b d p ph q x y z $.
387517387517
foot.x $e |- ( ph -> C e. P ) $.
387518387518
foot.y $e |- ( ph -> -. C e. A ) $.
387519-
$( Lemma for ~ foot : existence part. (Contributed by Thierry Arnoux,
387520-
19-Oct-2019.) $)
387521-
footex $p |- ( ph -> E. x e. A ( C L x ) ( perpG ` G ) A ) $=
387519+
$( Alternative version of ~ footex which minimization requires a notably
387520+
long time. (Contributed by Thierry Arnoux, 19-Oct-2019.)
387521+
(New usage is discouraged.) (Proof modification is discouraged.) $)
387522+
footexALT $p |- ( ph -> E. x e. A ( C L x ) ( perpG ` G ) A ) $=
387522387523
( co wcel adantr va vb vy vp vz vq vd wceq wne cperpg cfv wbr wrex cmir
387523387524
cv eqid cstrkg ad3antrrr ad2antrr ad6antr simplr simprr eqcomd midexlem
387524387525
simp-4r simp-6r simprl ad4antr simp-5r simprd simp-7r ad10antr simp-11r
@@ -387600,6 +387601,132 @@ are congruent (CPCTC), focusing on a specific segment. (Contributed
387600387601
VIUVHVAYOYPUVCUDUUODYTEUVEFGHUVFIJKLMUXDUXGVUOUUNUVAUUTVAUXOVUAUVBUUPUU
387601387602
SVBVDYPUUNUCYTDEFGIUUAYTJKLUXFVUEUYTUYTUXNYOYPAUAUBCEFGHJLMNOYQYR $.
387602387603

387604+
${
387605+
footexlem.e $e |- ( ph -> E e. P ) $.
387606+
footexlem.f $e |- ( ph -> F e. P ) $.
387607+
footexlem.r $e |- ( ph -> R e. P ) $.
387608+
footexlem.x $e |- ( ph -> X e. P ) $.
387609+
footexlem.y $e |- ( ph -> Y e. P ) $.
387610+
footexlem.z $e |- ( ph -> Z e. P ) $.
387611+
footexlem.d $e |- ( ph -> D e. P ) $.
387612+
footexlem.1 $e |- ( ph -> A = ( E L F ) ) $.
387613+
footexlem.2 $e |- ( ph -> E =/= F ) $.
387614+
footexlem.3 $e |- ( ph -> E e. ( F I Y ) ) $.
387615+
footexlem.4 $e |- ( ph -> ( E .- Y ) = ( E .- C ) ) $.
387616+
footexlem.5 $e |- ( ph -> C = ( ( ( pInvG ` G ) ` R ) ` Y ) ) $.
387617+
footexlem.6 $e |- ( ph -> Y e. ( E I Z ) ) $.
387618+
footexlem.7 $e |- ( ph -> ( Y .- Z ) = ( Y .- R ) ) $.
387619+
footexlem.q $e |- ( ph -> Q e. P ) $.
387620+
footexlem.8 $e |- ( ph -> Y e. ( R I Q ) ) $.
387621+
footexlem.9 $e |- ( ph -> ( Y .- Q ) = ( Y .- E ) ) $.
387622+
footexlem.10 $e |- ( ph -> Y e. ( ( ( ( pInvG ` G ) ` Z ) ` Q ) I D ) )
387623+
$.
387624+
footexlem.11 $e |- ( ph -> ( Y .- D ) = ( Y .- C ) ) $.
387625+
footexlem.12 $e |- ( ph -> D = ( ( ( pInvG ` G ) ` X ) ` C ) ) $.
387626+
$( Lemma for ~ footex (Contributed by Thierry Arnoux, 19-Oct-2019.)
387627+
(Revised by Thierry Arnoux, 1-Jul-2023.) $)
387628+
footexlem1 $p |- ( ph -> X e. A ) $=
387629+
( co eqcomd cmir cfv wne wcel wn necomd btwnlng3 lncom nelne2 syl2anc
387630+
eleqtrrd eqnetrrd eqid mirinv necon3bid mpbid tgcgrneq mirbtwn oveq1d
387631+
mircl tgbtwnouttr2 tgbtwncom cs3 crag ccgrg oveq2d eqtrd israg mpbird
387632+
wceq tgcgrcomlr eqtr2d tglinerflx1 axtgcgrrflx axtg5seg trgcgr ragcgr
387633+
ragcom eqidd krippen tglinethru ) ANOPLVEBAEJKLOPNQSTUAUIUJUHAOGOPEJK
387634+
MQRSUAUIUGUIUJAOPMVEOGMVEURVFZAGOAOGJVGVHZVHZVHZOVIGOVIACXKOUPAOCAOBV
387635+
JCBVJVKZOCVIAOHILVEZBAEJKLHIOQSTUAUEUFUIUMAEJKLIHOQSTUAUFUEUIAHIUMVLU
387636+
NVMVNULVQZUDOCBVOVPVLVRAXKOGOAGOEXIJKLXJMQRSTXIVSZUAUGXJVSZUIVTWAWBZV
387637+
LWCZAEJKLPONQSTUAUJUIUHAOPXRVLAFFPXIVHZVHZOEXICDJKLXSMNXIVHZPNQRSTXOU
387638+
AXSVSZYAVSUSAPEXIJKLXSMFQRSTXOUAUJYBUSWFUIUCUKUJUHACOFEJKMQRSUAUCUIUS
387639+
ACGOFEJKMQRSUAUCUGUIUSXQAGXKOKVECOKVEAGOEXIJKLXJMQRSTXOUAUGXPUIWDACXK
387640+
OKUPWEVQUTWGWHVBAOPFWIJWJVHZVJOFMVEZOXTMVEWPAFPOEXIJKLMQRSTXOUAUSUJUI
387641+
AHGOFEJWKVHZXIPOJKLMQRSTXOUAUEUGUIYEVSZUSUJUIAHGOWIYCVJHOMVEZHXKMVEZW
387642+
PAYGHCMVEZYHUOACXKHMUPWLWMAHGOEXIJKLMQRSTXOUAUEUGUIWNWOAHGOFEYEPOJMQR
387643+
YFUAUEUGUIUSUJUIAGHPFEJKMQRSUAUGUEUJUSAHOPEHJKMFFOGQRSUAUSUIUGUEUIUJU
387644+
EUSAOFACHOFEJKMQRSUAUCUEUIUSAYDOHMVEZCHMVEVAAHOHCEJKMQRSUAUEUIUEUCUOW
387645+
QWRAHCAHBVJXLHCVIAHXMBAEHIJKLQSTUAUEUFUMWSULVQZUDHCBVOVPZVLWCVLAGOFEJ
387646+
KMQRSUAUGUIUSUTWHUQAOFOHEJKMQRSUAUIUSUIUEVAWQXHAEJKMFHQRSUAUSUEWTAYDY
387647+
JVAVFZXAWQAOGOPEJKMQRSUAUIUGUIUJXHWQYMXBXCXDAOPFEXIJKLMQRSTXOUAUIUJUS
387648+
WNWBAODMVEOCMVEVCVFAXTXEVDXFVMVNABEOPJKLQSTUAUIUJXRXRUBXNAPHOLVEBAEJK
387649+
LHOPQSTUAUEUIUJAHCHOEJKMQRSUAUEUCUEUIAYGYIUOVFYLWCZUQVMABEHOJKLQSTUAU
387650+
EUIYNYNUBYKXNXGVQXGVQ $.
387651+
387652+
$( Lemma for ~ footex (Contributed by Thierry Arnoux, 19-Oct-2019.)
387653+
(Revised by Thierry Arnoux, 1-Jul-2023.) $)
387654+
footexlem2 $p |- ( ph -> ( C L X ) ( perpG ` G ) A ) $=
387655+
( co wcel wn wne footexlem1 nelne2 syl2anc tgelrnln tglinerflx2 elind
387656+
necomd tglinerflx1 btwnlng3 lncom eleqtrrd wceq wa cmir cstrkg adantr
387657+
eqid crag eqidd simpr s3eqd mircl tgcgrcomlr eqtr2d tgcgrneq eqnetrrd
387658+
cfv cs3 mirinv necon3bid mirbtwn oveq1d tgbtwnouttr2 tgbtwncom oveq2d
387659+
mpbid ccgrg eqtrd mpbird eqcomd axtg5seg trgcgr ragcgr ragcom neeqtrd
387660+
israg axtgcgrrflx mircgr eleqtrd orcd ragcol eqeltrd btwncolg3 neneqd
387661+
wo ragflat pm2.65da neqned ragperp ) ACNLVEZBECJKLMONQRSTUAAEJKLCNQST
387662+
UAUCUHANCANBVFCBVFVGZNCVHABCDEFGHIJKLMNOPQRSTUAUBUCUDUEUFUGUHUIUJUKUL
387663+
UMUNUOUPUQURUSUTVAVBVCVDVIZUDNCBVJVKVOZVLUBAYHBNAECNJKLQSTUAUCUHYKVMY
387664+
JVNAECNJKLQSTUAUCUHYKVPAOHILVEZBAEJKLHIOQSTUAUEUFUIUMAEJKLIHOQSTUAUFU
387665+
EUIAHIUMVOUNVQVRULVSZYKAONAONVTZOGVTZAYNWAZHOGEJWBWOZJKLMQRSTYQWEZAJW
387666+
CVFYNUAWDZAHEVFYNUEWDZAOEVFYNUIWDZAGEVFYNUGWDZYPGOHEYQJKLMQRSTYRYSUUB
387667+
UUAYTYPCOHGEYQJKLMQRSTYRYSACEVFYNUCWDZUUAYTUUBYPCOHWPCNHWPJWFWOZYPCOH
387668+
HCNYPCWGAYNWHZYPHWGWIYPHNCEYQJKLMQRSTYRYSYTANEVFYNUHWDZUUCYPPNCHEYQJK
387669+
LMQRSTYRYSAPEVFYNUJWDZUUFUUCYTAPNCWPUUDVFZYNAUUHPCMVEZPCNYQWOWOZMVEZV
387670+
TAUUIPDMVEUUKACPDPEJKMQRSUAUCUJUKUJAFPYQWOZWOZODEPJKMPFOCQRSUAUSUIUCA
387671+
PEYQJKLUULMFQRSTYRUAUJUULWEZUSWJZUIUKUJUJAOFACHOFEJKMQRSUAUCUEUIUSAOF
387672+
MVEZOHMVEZCHMVEVAAHOHCEJKMQRSUAUEUIUEUCUOWKWLAHCAHBVFYIHCVHZAHYLBAEHI
387673+
JKLQSTUAUEUFUMVPULVSUDHCBVJVKZVOWMVOZACOFEJKMQRSUAUCUIUSACGOFEJKMQRSU
387674+
AUCUGUIUSAOGYQWOZWOZOVHGOVHACUVBOUPAOCAOBVFYIOCVHYMUDOCBVJVKVOZWNAUVB
387675+
OGOAGOEYQJKLUVAMQRSTYRUAUGUVAWEZUIWQWRXDZAGUVBOKVECOKVEAGOEYQJKLUVAMQ
387676+
RSTYRUAUGUVDUIWSACUVBOKUPWTVSZUTXAXBVBAOFOUUMEJKMQRSUAUIUSUIUUOAOPFWP
387677+
UUDVFUUPOUUMMVEVTAFPOEYQJKLMQRSTYRUAUSUJUIAHGOFEJXEWOZYQPOJKLMQRSTYRU
387678+
AUEUGUIUVGWEZUSUJUIAHGOWPUUDVFZHOMVEZHUVBMVEZVTAUVJHCMVEZUVKUOACUVBHM
387679+
UPXCXFAHGOEYQJKLMQRSTYRUAUEUGUIXNXGZAHGOFEUVGPOJMQRUVHUAUEUGUIUSUJUIA
387680+
GHPFEJKMQRSUAUGUEUJUSAHOPEHJKMFFOGQRSUAUSUIUGUEUIUJUEUSUUTAGOFEJKMQRS
387681+
UAUGUIUSUTXBUQAOFOHEJKMQRSUAUIUSUIUEVAWKAOPMVEZOGMVEURXHZAEJKMFHQRSUA
387682+
USUEXOAUUPUUQVAXHZXIWKAOGOPEJKMQRSUAUIUGUIUJUVOWKUVPXJXKXLAOPFEYQJKLM
387683+
QRSTYRUAUIUJUSXNXDWKAODMVEZOCMVEZVCXHZAPFPUUMEJKMQRSUAUJUSUJUUOAPUUMM
387684+
VEPFMVEAPFEYQJKLUULMQRSTYRUAUJUUNUSXPXHWKAUVNWGXIWKADUUJPMVDXCXFAPNCE
387685+
YQJKLMQRSTYRUAUJUHUCXNXGWDYPPONAPOVHYNAOPAOGOPEJKMQRSUAUIUGUIUJUVOAGO
387686+
UVEVOZWMVOWDUUEXMYPPNHLVEZVFNHVTYPPOHLVEUWAYPEJKLOHPQSTYSUUAYTUUGYPHO
387687+
YPHCHOEJKMQRSYSYTUUCYTUUAAUVLUVJVTYNAUVJUVLUOXHZWDAUURYNUUSWDWMVOAPHO
387688+
LVEVFYNAEJKLHOPQSTUAUEUIUJAHCHOEJKMQRSUAUEUCUEUIUWBUUSWMUQVQWDVRYPONH
387689+
LUUEWTXQXRXSXLXTACOVHYNUVCWDACOGLVEVFYOYCYNAEJKLOGCQTSUAUIUGUCACGOEJK
387690+
MQRSUAUCUGUIUVFXBYAWDXSXLAUVIYNUVMWDYDYPOGAOGVHYNUVTWDYBYEYFAONCEYQJK
387691+
LMQRSTYRUAUIUHUCAONCWPUUDVFUVROUUJMVEZVTAUVRUVQUWCUVSADUUJOMVDXCXFAON
387692+
CEYQJKLMQRSTYRUAUIUHUCXNXGXLYG $.
387693+
$}
387694+
387695+
$( From a point ` C ` outside of a line ` A ` , there exists a point
387696+
` x ` on ` A ` such that ` ( C L x ) ` is perpendicular to ` A ` .
387697+
This point is unique, see ~ foot . (Contributed by Thierry Arnoux,
387698+
19-Oct-2019.) (Revised by Thierry Arnoux, 1-Jul-2023.) $)
387699+
footex $p |- ( ph -> E. x e. A ( C L x ) ( perpG ` G ) A ) $=
387700+
( co wa wcel va vb vy vp vz vq vd cv wceq wne cperpg cfv wrex cmir eqid
387701+
wbr cstrkg ad5antr ad2antrr ad6antr simplr simp-4r midexlem crn ad9antr
387702+
simprr eqcomd adantr ad3antrrr ad10antr simp-7r simprl simpllr simp-11r
387703+
wn simpld simp-9r simp-5r simplrl footexlem1 footexlem2 reximssdv mircl
387704+
simprd axtgsegcon r19.29a tgisline r19.29vva ) ACUAUHZUBUHZHRUIZWIWJUJZ
387705+
SZDBUHZHRCFUKULUPZBCUMZUAUBEEAWIETZSZWJETZSZWMSZWIWJUCUHZGRTZWIXBIRWIDI
387706+
RUIZSZWPUCEXAXBETZSZXESZDXBUDUHZFUNULZULZULUIZWPUDEXHXIETZSZXLSZXBWIUEU
387707+
HZGRTZXBXPIRXBXIIRUIZSZWPUEEXOXPETZSZXSSZXBXIUFUHZGRTZXBYCIRXBWIIRUIZSZ
387708+
WPUFEYBYCETZSZYFSZXBYCXPXJULZULZUGUHZGRTZXBYLIRZXBDIRZUIZSZWPUGEYIYLETZ
387709+
SZYQSZYLDWNXJULZULUIZWOBCEYTBDYLXBEXJFGHUUAIJKLMXJUOZYIFUQTZYRYQYBUUDYG
387710+
YFXOUUDXTXSXHUUDXMXLAUUDWQWSWMXFXENURZUSZUSZUSZUSUUAUOYIDETZYRYQXHUUIXM
387711+
XLXTXSYGYFAUUIWQWSWMXFXEPURZUTZUSZYIYRYQVAYIXFYRYQYBXFYGYFXOXFXTXSXAXFX
387712+
EXMXLVBZUSZUSZUSYTYNYOYSYMYPVFZVGVCYTWNETZUUBSZSZCDYLEYCXIWIWJFGHIWNXBX
387713+
PJKLMYBUUDYGYFYRYQUURUUGURZXHCHVDTZXMXLXTXSYGYFYRYQUURAUVAWQWSWMXFXEOUR
387714+
VEZYTUUIUURUULVHZYTDCTVOZUURXAUVDXFXEXMXLXTXSYGYFYRYQAUVDWQWSWMQVIVJVHZ
387715+
YBWQYGYFYRYQUURXOWQXTXSAWQWSWMXFXEXMXLVKZUSZURZYTWSUURXAWSXFXEXMXLXTXSY
387716+
GYFYRYQWRWSWMVAZVJVHZYBXMYGYFYRYQUURXHXMXLXTXSVBZURZYTUUQUUBVLZYBXFYGYF
387717+
YRYQUURUUNURZXOXTXSYGYFYRYQUURVKZYIYRYQUURVMZYTWKUURYTWKWLWTWMXFXEXMXLX
387718+
TXSYGYFYRYQVNZVPVHZYTWLUURYTWKWLUVQWDVHZYTXCUURYTXCXDXGXEXMXLXTXSYGYFYR
387719+
YQVQZVPVHZYTXDUURYTXCXDUVTWDVHZYTXLUURXNXLXTXSYGYFYRYQVKVHZYTXQUURYTXQX
387720+
RYAXSYGYFYRYQVRZVPVHZYTXRUURYTXQXRUWDWDVHZYBYGYFYRYQUURVRZYTYDUURYTYDYE
387721+
YHYFYRYQVMZVPVHZYTYEUURYTYDYEUWHWDVHZYSYMYPUURVSZYTYPUURUUPVHZYTUUQUUBV
387722+
FZVTUUSCDYLEYCXIWIWJFGHIWNXBXPJKLMUUTUVBUVCUVEUVHUVJUVLUVMUVNUVOUVPUVRU
387723+
VSUWAUWBUWCUWEUWFUWGUWIUWJUWKUWLUWMWAWBYIUGXBDEFGIYKXBJKLUUHYIXPEXJFGHY
387724+
JIYCJKLMUUCUUHXOXTXSYGYFVBYJUOYBYGYFVAWCUUOUUOUUKWEWFYBUFXBWIEFGIXIXBJK
387725+
LUUGUVKUUNUUNUVGWEWFXOUEXBXIEFGIWIXBJKLUUFUVFUUMUUMXHXMXLVAWEWFXHUDXBDW
387726+
IEXJFGHXKIJKLMUUCUUEXKUOXAXFXEVAUUJAWQWSWMXFXEVRXGXCXDVFVCWFXAUCWIDEFGI
387727+
WJWIJKLAUUDWQWSWMNVIUVIAWQWSWMVMZUWNAUUIWQWSWMPVIWEWFAUAUBCEFGHJLMNOWGW
387728+
H $.
387729+
387603387730
$( From a point ` C ` outside of a line ` A ` , there exists a unique
387604387731
point ` x ` on ` A ` such that ` ( C L x ) ` is perpendicular to
387605387732
` A ` . That point is called the foot from ` C ` on ` A ` . Theorem

0 commit comments

Comments
 (0)