Metamath Proof Explorer

Theorem footexlem2

Description: Lemma for footex . (Contributed by Thierry Arnoux, 19-Oct-2019) (Revised by Thierry Arnoux, 1-Jul-2023)

Ref Expression
Hypotheses isperp.p 
|- P = ( Base ` G )
isperp.d 
|- .- = ( dist ` G )
isperp.i 
|- I = ( Itv ` G )
isperp.l 
|- L = ( LineG ` G )
isperp.g 
|- ( ph -> G e. TarskiG )
isperp.a 
|- ( ph -> A e. ran L )
foot.x 
|- ( ph -> C e. P )
foot.y 
|- ( ph -> -. C e. A )
footexlem.e 
|- ( ph -> E e. P )
footexlem.f 
|- ( ph -> F e. P )
footexlem.r 
|- ( ph -> R e. P )
footexlem.x 
|- ( ph -> X e. P )
footexlem.y 
|- ( ph -> Y e. P )
footexlem.z 
|- ( ph -> Z e. P )
footexlem.d 
|- ( ph -> D e. P )
footexlem.1 
|- ( ph -> A = ( E L F ) )
footexlem.2 
|- ( ph -> E =/= F )
footexlem.3 
|- ( ph -> E e. ( F I Y ) )
footexlem.4 
|- ( ph -> ( E .- Y ) = ( E .- C ) )
footexlem.5 
|- ( ph -> C = ( ( ( pInvG ` G ) ` R ) ` Y ) )
footexlem.6 
|- ( ph -> Y e. ( E I Z ) )
footexlem.7 
|- ( ph -> ( Y .- Z ) = ( Y .- R ) )
footexlem.q 
|- ( ph -> Q e. P )
footexlem.8 
|- ( ph -> Y e. ( R I Q ) )
footexlem.9 
|- ( ph -> ( Y .- Q ) = ( Y .- E ) )
footexlem.10 
|- ( ph -> Y e. ( ( ( ( pInvG ` G ) ` Z ) ` Q ) I D ) )
footexlem.11 
|- ( ph -> ( Y .- D ) = ( Y .- C ) )
footexlem.12 
|- ( ph -> D = ( ( ( pInvG ` G ) ` X ) ` C ) )
Assertion footexlem2 
|- ( ph -> ( C L X ) ( perpG ` G ) A )

Proof

Step Hyp Ref Expression
1 isperp.p 
 |-  P = ( Base ` G )
2 isperp.d 
 |-  .- = ( dist ` G )
3 isperp.i 
 |-  I = ( Itv ` G )
4 isperp.l 
 |-  L = ( LineG ` G )
5 isperp.g 
 |-  ( ph -> G e. TarskiG )
6 isperp.a 
 |-  ( ph -> A e. ran L )
7 foot.x 
 |-  ( ph -> C e. P )
8 foot.y 
 |-  ( ph -> -. C e. A )
9 footexlem.e 
 |-  ( ph -> E e. P )
10 footexlem.f 
 |-  ( ph -> F e. P )
11 footexlem.r 
 |-  ( ph -> R e. P )
12 footexlem.x 
 |-  ( ph -> X e. P )
13 footexlem.y 
 |-  ( ph -> Y e. P )
14 footexlem.z 
 |-  ( ph -> Z e. P )
15 footexlem.d 
 |-  ( ph -> D e. P )
16 footexlem.1 
 |-  ( ph -> A = ( E L F ) )
17 footexlem.2 
 |-  ( ph -> E =/= F )
18 footexlem.3 
 |-  ( ph -> E e. ( F I Y ) )
19 footexlem.4 
 |-  ( ph -> ( E .- Y ) = ( E .- C ) )
20 footexlem.5 
 |-  ( ph -> C = ( ( ( pInvG ` G ) ` R ) ` Y ) )
21 footexlem.6 
 |-  ( ph -> Y e. ( E I Z ) )
22 footexlem.7 
 |-  ( ph -> ( Y .- Z ) = ( Y .- R ) )
23 footexlem.q 
 |-  ( ph -> Q e. P )
24 footexlem.8 
 |-  ( ph -> Y e. ( R I Q ) )
25 footexlem.9 
 |-  ( ph -> ( Y .- Q ) = ( Y .- E ) )
26 footexlem.10 
 |-  ( ph -> Y e. ( ( ( ( pInvG ` G ) ` Z ) ` Q ) I D ) )
27 footexlem.11 
 |-  ( ph -> ( Y .- D ) = ( Y .- C ) )
28 footexlem.12 
 |-  ( ph -> D = ( ( ( pInvG ` G ) ` X ) ` C ) )
29 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 footexlem1 
 |-  ( ph -> X e. A )
30 nelne2 
 |-  ( ( X e. A /\ -. C e. A ) -> X =/= C )
31 29 8 30 syl2anc 
 |-  ( ph -> X =/= C )
32 31 necomd 
 |-  ( ph -> C =/= X )
33 1 3 4 5 7 12 32 tgelrnln 
 |-  ( ph -> ( C L X ) e. ran L )
34 1 3 4 5 7 12 32 tglinerflx2 
 |-  ( ph -> X e. ( C L X ) )
35 34 29 elind 
 |-  ( ph -> X e. ( ( C L X ) i^i A ) )
36 1 3 4 5 7 12 32 tglinerflx1 
 |-  ( ph -> C e. ( C L X ) )
37 17 necomd 
 |-  ( ph -> F =/= E )
38 1 3 4 5 10 9 13 37 18 btwnlng3 
 |-  ( ph -> Y e. ( F L E ) )
39 1 3 4 5 9 10 13 17 38 lncom 
 |-  ( ph -> Y e. ( E L F ) )
40 39 16 eleqtrrd 
 |-  ( ph -> Y e. A )
41 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
42 5 adantr 
 |-  ( ( ph /\ Y = X ) -> G e. TarskiG )
43 9 adantr 
 |-  ( ( ph /\ Y = X ) -> E e. P )
44 13 adantr 
 |-  ( ( ph /\ Y = X ) -> Y e. P )
45 11 adantr 
 |-  ( ( ph /\ Y = X ) -> R e. P )
46 7 adantr 
 |-  ( ( ph /\ Y = X ) -> C e. P )
47 eqidd 
 |-  ( ( ph /\ Y = X ) -> C = C )
48 simpr 
 |-  ( ( ph /\ Y = X ) -> Y = X )
49 eqidd 
 |-  ( ( ph /\ Y = X ) -> E = E )
50 47 48 49 s3eqd 
 |-  ( ( ph /\ Y = X ) -> <" C Y E "> = <" C X E "> )
51 12 adantr 
 |-  ( ( ph /\ Y = X ) -> X e. P )
52 14 adantr 
 |-  ( ( ph /\ Y = X ) -> Z e. P )
53 eqid 
 |-  ( ( pInvG ` G ) ` Z ) = ( ( pInvG ` G ) ` Z )
54 1 2 3 4 41 5 14 53 23 mircl 
 |-  ( ph -> ( ( ( pInvG ` G ) ` Z ) ` Q ) e. P )
55 1 2 3 5 9 13 9 7 19 tgcgrcomlr 
 |-  ( ph -> ( Y .- E ) = ( C .- E ) )
56 25 55 eqtr2d 
 |-  ( ph -> ( C .- E ) = ( Y .- Q ) )
57 1 3 4 5 9 10 17 tglinerflx1 
 |-  ( ph -> E e. ( E L F ) )
58 57 16 eleqtrrd 
 |-  ( ph -> E e. A )
59 nelne2 
 |-  ( ( E e. A /\ -. C e. A ) -> E =/= C )
60 58 8 59 syl2anc 
 |-  ( ph -> E =/= C )
61 60 necomd 
 |-  ( ph -> C =/= E )
62 1 2 3 5 7 9 13 23 56 61 tgcgrneq 
 |-  ( ph -> Y =/= Q )
63 62 necomd 
 |-  ( ph -> Q =/= Y )
64 nelne2 
 |-  ( ( Y e. A /\ -. C e. A ) -> Y =/= C )
65 40 8 64 syl2anc 
 |-  ( ph -> Y =/= C )
66 65 necomd 
 |-  ( ph -> C =/= Y )
67 20 66 eqnetrrd 
 |-  ( ph -> ( ( ( pInvG ` G ) ` R ) ` Y ) =/= Y )
68 eqid 
 |-  ( ( pInvG ` G ) ` R ) = ( ( pInvG ` G ) ` R )
69 1 2 3 4 41 5 11 68 13 mirinv 
 |-  ( ph -> ( ( ( ( pInvG ` G ) ` R ) ` Y ) = Y <-> R = Y ) )
70 69 necon3bid 
 |-  ( ph -> ( ( ( ( pInvG ` G ) ` R ) ` Y ) =/= Y <-> R =/= Y ) )
71 67 70 mpbid 
 |-  ( ph -> R =/= Y )
72 1 2 3 4 41 5 11 68 13 mirbtwn 
 |-  ( ph -> R e. ( ( ( ( pInvG ` G ) ` R ) ` Y ) I Y ) )
73 20 oveq1d 
 |-  ( ph -> ( C I Y ) = ( ( ( ( pInvG ` G ) ` R ) ` Y ) I Y ) )
74 72 73 eleqtrrd 
 |-  ( ph -> R e. ( C I Y ) )
75 1 2 3 5 7 11 13 23 71 74 24 tgbtwnouttr2 
 |-  ( ph -> Y e. ( C I Q ) )
76 1 2 3 5 7 13 23 75 tgbtwncom 
 |-  ( ph -> Y e. ( Q I C ) )
77 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
78 20 oveq2d 
 |-  ( ph -> ( E .- C ) = ( E .- ( ( ( pInvG ` G ) ` R ) ` Y ) ) )
79 19 78 eqtrd 
 |-  ( ph -> ( E .- Y ) = ( E .- ( ( ( pInvG ` G ) ` R ) ` Y ) ) )
80 1 2 3 4 41 5 9 11 13 israg 
 |-  ( ph -> ( <" E R Y "> e. ( raG ` G ) <-> ( E .- Y ) = ( E .- ( ( ( pInvG ` G ) ` R ) ` Y ) ) ) )
81 79 80 mpbird 
 |-  ( ph -> <" E R Y "> e. ( raG ` G ) )
82 1 2 3 5 11 13 23 24 tgbtwncom 
 |-  ( ph -> Y e. ( Q I R ) )
83 1 2 3 5 13 23 13 9 25 tgcgrcomlr 
 |-  ( ph -> ( Q .- Y ) = ( E .- Y ) )
84 22 eqcomd 
 |-  ( ph -> ( Y .- R ) = ( Y .- Z ) )
85 1 2 3 5 23 9 axtgcgrrflx 
 |-  ( ph -> ( Q .- E ) = ( E .- Q ) )
86 25 eqcomd 
 |-  ( ph -> ( Y .- E ) = ( Y .- Q ) )
87 1 2 3 5 23 13 11 9 13 14 9 23 63 82 21 83 84 85 86 axtg5seg 
 |-  ( ph -> ( R .- E ) = ( Z .- Q ) )
88 1 2 3 5 11 9 14 23 87 tgcgrcomlr 
 |-  ( ph -> ( E .- R ) = ( Q .- Z ) )
89 1 2 3 5 13 11 13 14 84 tgcgrcomlr 
 |-  ( ph -> ( R .- Y ) = ( Z .- Y ) )
90 1 2 77 5 9 11 13 23 14 13 88 89 86 trgcgr 
 |-  ( ph -> <" E R Y "> ( cgrG ` G ) <" Q Z Y "> )
91 1 2 3 4 41 5 9 11 13 77 23 14 13 81 90 ragcgr 
 |-  ( ph -> <" Q Z Y "> e. ( raG ` G ) )
92 1 2 3 4 41 5 23 14 13 91 ragcom 
 |-  ( ph -> <" Y Z Q "> e. ( raG ` G ) )
93 1 2 3 4 41 5 13 14 23 israg 
 |-  ( ph -> ( <" Y Z Q "> e. ( raG ` G ) <-> ( Y .- Q ) = ( Y .- ( ( ( pInvG ` G ) ` Z ) ` Q ) ) ) )
94 92 93 mpbid 
 |-  ( ph -> ( Y .- Q ) = ( Y .- ( ( ( pInvG ` G ) ` Z ) ` Q ) ) )
95 1 2 3 5 13 23 13 54 94 tgcgrcomlr 
 |-  ( ph -> ( Q .- Y ) = ( ( ( ( pInvG ` G ) ` Z ) ` Q ) .- Y ) )
96 27 eqcomd 
 |-  ( ph -> ( Y .- C ) = ( Y .- D ) )
97 1 2 3 4 41 5 14 53 23 mircgr 
 |-  ( ph -> ( Z .- ( ( ( pInvG ` G ) ` Z ) ` Q ) ) = ( Z .- Q ) )
98 97 eqcomd 
 |-  ( ph -> ( Z .- Q ) = ( Z .- ( ( ( pInvG ` G ) ` Z ) ` Q ) ) )
99 1 2 3 5 14 23 14 54 98 tgcgrcomlr 
 |-  ( ph -> ( Q .- Z ) = ( ( ( ( pInvG ` G ) ` Z ) ` Q ) .- Z ) )
100 eqidd 
 |-  ( ph -> ( Y .- Z ) = ( Y .- Z ) )
101 1 2 3 5 23 13 7 54 13 15 14 14 63 76 26 95 96 99 100 axtg5seg 
 |-  ( ph -> ( C .- Z ) = ( D .- Z ) )
102 1 2 3 5 7 14 15 14 101 tgcgrcomlr 
 |-  ( ph -> ( Z .- C ) = ( Z .- D ) )
103 28 oveq2d 
 |-  ( ph -> ( Z .- D ) = ( Z .- ( ( ( pInvG ` G ) ` X ) ` C ) ) )
104 102 103 eqtrd 
 |-  ( ph -> ( Z .- C ) = ( Z .- ( ( ( pInvG ` G ) ` X ) ` C ) ) )
105 1 2 3 4 41 5 14 12 7 israg 
 |-  ( ph -> ( <" Z X C "> e. ( raG ` G ) <-> ( Z .- C ) = ( Z .- ( ( ( pInvG ` G ) ` X ) ` C ) ) ) )
106 104 105 mpbird 
 |-  ( ph -> <" Z X C "> e. ( raG ` G ) )
107 106 adantr 
 |-  ( ( ph /\ Y = X ) -> <" Z X C "> e. ( raG ` G ) )
108 71 necomd 
 |-  ( ph -> Y =/= R )
109 1 2 3 5 13 11 13 14 84 108 tgcgrneq 
 |-  ( ph -> Y =/= Z )
110 109 necomd 
 |-  ( ph -> Z =/= Y )
111 110 adantr 
 |-  ( ( ph /\ Y = X ) -> Z =/= Y )
112 111 48 neeqtrd 
 |-  ( ( ph /\ Y = X ) -> Z =/= X )
113 19 eqcomd 
 |-  ( ph -> ( E .- C ) = ( E .- Y ) )
114 113 adantr 
 |-  ( ( ph /\ Y = X ) -> ( E .- C ) = ( E .- Y ) )
115 60 adantr 
 |-  ( ( ph /\ Y = X ) -> E =/= C )
116 1 2 3 42 43 46 43 44 114 115 tgcgrneq 
 |-  ( ( ph /\ Y = X ) -> E =/= Y )
117 116 necomd 
 |-  ( ( ph /\ Y = X ) -> Y =/= E )
118 1 2 3 5 9 7 9 13 113 60 tgcgrneq 
 |-  ( ph -> E =/= Y )
119 1 3 4 5 9 13 14 118 21 btwnlng3 
 |-  ( ph -> Z e. ( E L Y ) )
120 119 adantr 
 |-  ( ( ph /\ Y = X ) -> Z e. ( E L Y ) )
121 1 3 4 42 44 43 52 117 120 lncom 
 |-  ( ( ph /\ Y = X ) -> Z e. ( Y L E ) )
122 48 oveq1d 
 |-  ( ( ph /\ Y = X ) -> ( Y L E ) = ( X L E ) )
123 121 122 eleqtrd 
 |-  ( ( ph /\ Y = X ) -> Z e. ( X L E ) )
124 123 orcd 
 |-  ( ( ph /\ Y = X ) -> ( Z e. ( X L E ) \/ X = E ) )
125 1 2 3 4 41 42 52 51 46 43 107 112 124 ragcol 
 |-  ( ( ph /\ Y = X ) -> <" E X C "> e. ( raG ` G ) )
126 1 2 3 4 41 42 43 51 46 125 ragcom 
 |-  ( ( ph /\ Y = X ) -> <" C X E "> e. ( raG ` G ) )
127 50 126 eqeltrd 
 |-  ( ( ph /\ Y = X ) -> <" C Y E "> e. ( raG ` G ) )
128 66 adantr 
 |-  ( ( ph /\ Y = X ) -> C =/= Y )
129 1 2 3 5 7 11 13 74 tgbtwncom 
 |-  ( ph -> R e. ( Y I C ) )
130 1 4 3 5 13 11 7 129 btwncolg3 
 |-  ( ph -> ( C e. ( Y L R ) \/ Y = R ) )
131 130 adantr 
 |-  ( ( ph /\ Y = X ) -> ( C e. ( Y L R ) \/ Y = R ) )
132 1 2 3 4 41 42 46 44 43 45 127 128 131 ragcol 
 |-  ( ( ph /\ Y = X ) -> <" R Y E "> e. ( raG ` G ) )
133 1 2 3 4 41 42 45 44 43 132 ragcom 
 |-  ( ( ph /\ Y = X ) -> <" E Y R "> e. ( raG ` G ) )
134 81 adantr 
 |-  ( ( ph /\ Y = X ) -> <" E R Y "> e. ( raG ` G ) )
135 1 2 3 4 41 42 43 44 45 133 134 ragflat 
 |-  ( ( ph /\ Y = X ) -> Y = R )
136 108 adantr 
 |-  ( ( ph /\ Y = X ) -> Y =/= R )
137 136 neneqd 
 |-  ( ( ph /\ Y = X ) -> -. Y = R )
138 135 137 pm2.65da 
 |-  ( ph -> -. Y = X )
139 138 neqned 
 |-  ( ph -> Y =/= X )
140 28 oveq2d 
 |-  ( ph -> ( Y .- D ) = ( Y .- ( ( ( pInvG ` G ) ` X ) ` C ) ) )
141 96 140 eqtrd 
 |-  ( ph -> ( Y .- C ) = ( Y .- ( ( ( pInvG ` G ) ` X ) ` C ) ) )
142 1 2 3 4 41 5 13 12 7 israg 
 |-  ( ph -> ( <" Y X C "> e. ( raG ` G ) <-> ( Y .- C ) = ( Y .- ( ( ( pInvG ` G ) ` X ) ` C ) ) ) )
143 141 142 mpbird 
 |-  ( ph -> <" Y X C "> e. ( raG ` G ) )
144 1 2 3 4 41 5 13 12 7 143 ragcom 
 |-  ( ph -> <" C X Y "> e. ( raG ` G ) )
145 1 2 3 4 5 33 6 35 36 40 32 139 144 ragperp 
 |-  ( ph -> ( C L X ) ( perpG ` G ) A )