Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  footex Structured version   Visualization version   Unicode version

Theorem footex 24842
 Description: Lemma for foot 24843: existence part. (Contributed by Thierry Arnoux, 19-Oct-2019.)
Hypotheses
Ref Expression
isperp.p
isperp.d
isperp.i Itv
isperp.l LineG
isperp.g TarskiG
isperp.a
foot.x
foot.y
Assertion
Ref Expression
footex ⟂G
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,

Proof of Theorem footex
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isperp.p . . . . . . . . 9
2 isperp.d . . . . . . . . 9
3 isperp.i . . . . . . . . 9 Itv
4 isperp.l . . . . . . . . 9 LineG
5 eqid 2471 . . . . . . . . 9 pInvG pInvG
6 isperp.g . . . . . . . . . . . . . . 15 TarskiG
76ad3antrrr 744 . . . . . . . . . . . . . 14 TarskiG
87ad2antrr 740 . . . . . . . . . . . . 13 TarskiG
98ad2antrr 740 . . . . . . . . . . . 12 pInvG TarskiG
109ad2antrr 740 . . . . . . . . . . 11 pInvG TarskiG
1110ad2antrr 740 . . . . . . . . . 10 pInvG TarskiG
1211ad2antrr 740 . . . . . . . . 9 pInvG pInvG TarskiG
13 eqid 2471 . . . . . . . . 9 pInvG pInvG
14 foot.x . . . . . . . . . . . . 13
1514ad3antrrr 744 . . . . . . . . . . . 12
1615ad2antrr 740 . . . . . . . . . . 11
1716ad6antr 750 . . . . . . . . . 10 pInvG
1817ad2antrr 740 . . . . . . . . 9 pInvG pInvG
19 simplr 770 . . . . . . . . 9 pInvG pInvG
20 simp-4r 785 . . . . . . . . . . . 12 pInvG
2120ad2antrr 740 . . . . . . . . . . 11 pInvG
2221ad2antrr 740 . . . . . . . . . 10 pInvG
2322ad2antrr 740 . . . . . . . . 9 pInvG pInvG
24 simprr 774 . . . . . . . . . 10 pInvG pInvG
2524eqcomd 2477 . . . . . . . . 9 pInvG pInvG
261, 2, 3, 4, 5, 12, 13, 18, 19, 23, 25midexlem 24816 . . . . . . . 8 pInvG pInvG pInvG
2712adantr 472 . . . . . . . . . . . . 13 pInvG pInvG pInvG TarskiG
2823adantr 472 . . . . . . . . . . . . 13 pInvG pInvG pInvG
29 simp-6r 789 . . . . . . . . . . . . . 14 pInvG pInvG
3029adantr 472 . . . . . . . . . . . . 13 pInvG pInvG pInvG
31 simprl 772 . . . . . . . . . . . . 13 pInvG pInvG pInvG
32 simp-4r 785 . . . . . . . . . . . . . . . 16 pInvG
3332ad4antr 746 . . . . . . . . . . . . . . 15 pInvG pInvG
3433adantr 472 . . . . . . . . . . . . . 14 pInvG pInvG pInvG
35 simp-5r 787 . . . . . . . . . . . . . . . . 17 pInvG pInvG
3635simprd 470 . . . . . . . . . . . . . . . 16 pInvG pInvG
3736eqcomd 2477 . . . . . . . . . . . . . . 15 pInvG pInvG
3837adantr 472 . . . . . . . . . . . . . 14 pInvG pInvG pInvG
39 simp-7r 791 . . . . . . . . . . . . . . . . . 18 pInvG pInvG pInvG
4039adantr 472 . . . . . . . . . . . . . . . . 17 pInvG pInvG pInvG pInvG
41 simpllr 777 . . . . . . . . . . . . . . . . . . . . . . . . . 26
4241ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . 25
4342ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . 24 pInvG
4443ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . 23 pInvG
4544ad4antr 746 . . . . . . . . . . . . . . . . . . . . . 22 pInvG pInvG
46 simplr 770 . . . . . . . . . . . . . . . . . . . . . . 23
4746ad10antr 758 . . . . . . . . . . . . . . . . . . . . . 22 pInvG pInvG
48 simp-11r 799 . . . . . . . . . . . . . . . . . . . . . . 23 pInvG pInvG
4948simprd 470 . . . . . . . . . . . . . . . . . . . . . 22 pInvG pInvG
5049necomd 2698 . . . . . . . . . . . . . . . . . . . . . . 23 pInvG pInvG
51 simp-9r 795 . . . . . . . . . . . . . . . . . . . . . . . 24 pInvG pInvG
5251simpld 466 . . . . . . . . . . . . . . . . . . . . . . 23 pInvG pInvG
531, 3, 4, 12, 47, 45, 23, 50, 52btwnlng3 24745 . . . . . . . . . . . . . . . . . . . . . 22 pInvG pInvG
541, 3, 4, 12, 45, 47, 23, 49, 53lncom 24746 . . . . . . . . . . . . . . . . . . . . 21 pInvG pInvG
5548simpld 466 . . . . . . . . . . . . . . . . . . . . 21 pInvG pInvG
5654, 55eleqtrrd 2552 . . . . . . . . . . . . . . . . . . . 20 pInvG pInvG
5756adantr 472 . . . . . . . . . . . . . . . . . . 19 pInvG pInvG pInvG
58 foot.y . . . . . . . . . . . . . . . . . . . . . 22
5958ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . 21
6059ad10antr 758 . . . . . . . . . . . . . . . . . . . 20 pInvG pInvG
6160adantr 472 . . . . . . . . . . . . . . . . . . 19 pInvG pInvG pInvG
62 nelne2 2740 . . . . . . . . . . . . . . . . . . 19
6357, 61, 62syl2anc 673 . . . . . . . . . . . . . . . . . 18 pInvG pInvG pInvG
6463necomd 2698 . . . . . . . . . . . . . . . . 17 pInvG pInvG pInvG
6540, 64eqnetrrd 2711 . . . . . . . . . . . . . . . 16 pInvG pInvG pInvG pInvG
66 eqid 2471 . . . . . . . . . . . . . . . . . 18 pInvG pInvG
671, 2, 3, 4, 5, 27, 34, 66, 28mirinv 24790 . . . . . . . . . . . . . . . . 17 pInvG pInvG pInvG pInvG
6867necon3bid 2687 . . . . . . . . . . . . . . . 16 pInvG pInvG pInvG pInvG
6965, 68mpbid 215 . . . . . . . . . . . . . . 15 pInvG pInvG pInvG
7069necomd 2698 . . . . . . . . . . . . . 14 pInvG pInvG pInvG
711, 2, 3, 27, 28, 34, 28, 30, 38, 70tgcgrneq 24606 . . . . . . . . . . . . 13 pInvG pInvG pInvG
7271necomd 2698 . . . . . . . . . . . . . 14 pInvG pInvG pInvG
73 eqid 2471 . . . . . . . . . . . . . . 15 pInvG pInvG
74 simp-4r 785 . . . . . . . . . . . . . . . 16 pInvG pInvG
7574adantr 472 . . . . . . . . . . . . . . 15 pInvG pInvG pInvG
76 simp-4r 785 . . . . . . . . . . . . . . . . 17 pInvG
77 simplr 770 . . . . . . . . . . . . . . . . 17 pInvG
781, 2, 3, 4, 5, 11, 76, 73, 77mircl 24785 . . . . . . . . . . . . . . . 16 pInvG pInvG
7978ad3antrrr 744 . . . . . . . . . . . . . . 15 pInvG pInvG pInvG pInvG
8018adantr 472 . . . . . . . . . . . . . . 15 pInvG pInvG pInvG
81 simpllr 777 . . . . . . . . . . . . . . 15 pInvG pInvG pInvG
821, 2, 3, 4, 5, 27, 34, 66, 28mirbtwn 24782 . . . . . . . . . . . . . . . . . 18 pInvG pInvG pInvG pInvG
8340oveq1d 6323 . . . . . . . . . . . . . . . . . 18 pInvG pInvG pInvG pInvG
8482, 83eleqtrrd 2552 . . . . . . . . . . . . . . . . 17 pInvG pInvG pInvG
85 simpllr 777 . . . . . . . . . . . . . . . . . . 19 pInvG pInvG
8685simpld 466 . . . . . . . . . . . . . . . . . 18 pInvG pInvG
8786adantr 472 . . . . . . . . . . . . . . . . 17 pInvG pInvG pInvG
881, 2, 3, 27, 80, 34, 28, 75, 69, 84, 87tgbtwnouttr2 24618 . . . . . . . . . . . . . . . 16 pInvG pInvG pInvG
891, 2, 3, 27, 80, 28, 75, 88tgbtwncom 24611 . . . . . . . . . . . . . . 15 pInvG pInvG pInvG
90 simplrl 778 . . . . . . . . . . . . . . 15 pInvG pInvG pInvG pInvG
91 eqid 2471 . . . . . . . . . . . . . . . . . . 19 cgrG cgrG
9251simprd 470 . . . . . . . . . . . . . . . . . . . . 21 pInvG pInvG
9339oveq2d 6324 . . . . . . . . . . . . . . . . . . . . 21 pInvG pInvG pInvG
9492, 93eqtrd 2505 . . . . . . . . . . . . . . . . . . . 20 pInvG pInvG pInvG
951, 2, 3, 4, 5, 12, 45, 33, 23israg 24821 . . . . . . . . . . . . . . . . . . . 20 pInvG pInvG ∟G pInvG
9694, 95mpbird 240 . . . . . . . . . . . . . . . . . . 19 pInvG pInvG ∟G
9785simprd 470 . . . . . . . . . . . . . . . . . . . . . . . . 25 pInvG pInvG
981, 2, 3, 12, 45, 23, 45, 18, 92tgcgrcomlr 24603 . . . . . . . . . . . . . . . . . . . . . . . . 25 pInvG pInvG
9997, 98eqtr2d 2506 . . . . . . . . . . . . . . . . . . . . . . . 24 pInvG pInvG
1001, 3, 4, 12, 45, 47, 49tglinerflx1 24757 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 pInvG pInvG
101100, 55eleqtrrd 2552 . . . . . . . . . . . . . . . . . . . . . . . . . 26 pInvG pInvG
102 nelne2 2740 . . . . . . . . . . . . . . . . . . . . . . . . . 26
103101, 60, 102syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . 25 pInvG pInvG
104103necomd 2698 . . . . . . . . . . . . . . . . . . . . . . . 24 pInvG pInvG
1051, 2, 3, 12, 18, 45, 23, 74, 99, 104tgcgrneq 24606 . . . . . . . . . . . . . . . . . . . . . . 23 pInvG pInvG
106105necomd 2698 . . . . . . . . . . . . . . . . . . . . . 22 pInvG pInvG
1071, 2, 3, 12, 33, 23, 74, 86tgbtwncom 24611 . . . . . . . . . . . . . . . . . . . . . 22 pInvG pInvG
10835simpld 466 . . . . . . . . . . . . . . . . . . . . . 22 pInvG pInvG
1091, 2, 3, 12, 23, 74, 23, 45, 97tgcgrcomlr 24603 . . . . . . . . . . . . . . . . . . . . . 22 pInvG pInvG
1101, 2, 3, 12, 74, 45axtgcgrrflx 24589 . . . . . . . . . . . . . . . . . . . . . 22 pInvG