Metamath Proof Explorer

Theorem prlngmid2

Description: If the midpoints of two segments ( X I Z ) and ( Y I W ) coincide, the points X , Y , Z and W form a parallelogram, i.e. the lines ( X L Y ) and ( Z L W ) are parallel. Theorem 12.17 of Schwabhauser p. 125. (Contributed by Thierry Arnoux, 13-Jul-2026)

Ref Expression
Hypotheses prlngmid2.b 
|- P = ( Base ` G )
prlngmid2.l 
|- L = ( LineG ` G )
prlngmid2.e 
|- E = ( PlnG ` G )
prlngmid2.p 
|- .|| = ( parlnG ` G )
prlngmid2.m 
|- M = ( midG ` G )
prlngmid2.g 
|- ( ph -> G e. TarskiG )
prlngmid2.1 
|- ( ph -> G e. TarskiGE )
prlngmid2.x 
|- ( ph -> X e. P )
prlngmid2.y 
|- ( ph -> Y e. P )
prlngmid2.z 
|- ( ph -> Z e. ( P \ ( X L Y ) ) )
prlngmid2.w 
|- ( ph -> W e. P )
prlngmid2.2 
|- ( ph -> ( X M Z ) = ( Y M W ) )
prlngmid2.3 
|- ( ph -> X =/= Y )
Assertion prlngmid2 
|- ( ph -> ( X L Y ) .|| ( Z L W ) )

Proof

Step Hyp Ref Expression
1 prlngmid2.b 
 |-  P = ( Base ` G )
2 prlngmid2.l 
 |-  L = ( LineG ` G )
3 prlngmid2.e 
 |-  E = ( PlnG ` G )
4 prlngmid2.p 
 |-  .|| = ( parlnG ` G )
5 prlngmid2.m 
 |-  M = ( midG ` G )
6 prlngmid2.g 
 |-  ( ph -> G e. TarskiG )
7 prlngmid2.1 
 |-  ( ph -> G e. TarskiGE )
8 prlngmid2.x 
 |-  ( ph -> X e. P )
9 prlngmid2.y 
 |-  ( ph -> Y e. P )
10 prlngmid2.z 
 |-  ( ph -> Z e. ( P \ ( X L Y ) ) )
11 prlngmid2.w 
 |-  ( ph -> W e. P )
12 prlngmid2.2 
 |-  ( ph -> ( X M Z ) = ( Y M W ) )
13 prlngmid2.3 
 |-  ( ph -> X =/= Y )
14 6 ad2antrr 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> G e. TarskiG )
15 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
16 1 15 2 6 8 9 13 tgelrnln 
 |-  ( ph -> ( X L Y ) e. ran L )
17 1 2 3 6 16 10 tgelrnpln 
 |-  ( ph -> ( ( X L Y ) E Z ) e. ran E )
18 17 ad2antrr 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( ( X L Y ) E Z ) e. ran E )
19 1 15 2 3 6 16 10 elplnglnid 
 |-  ( ph -> ( X L Y ) C_ ( ( X L Y ) E Z ) )
20 19 ad2antrr 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( X L Y ) C_ ( ( X L Y ) E Z ) )
21 1 15 2 3 6 16 10 elplngid 
 |-  ( ph -> Z e. ( ( X L Y ) E Z ) )
22 12 fveq2d 
 |-  ( ph -> ( ( pInvG ` G ) ` ( X M Z ) ) = ( ( pInvG ` G ) ` ( Y M W ) ) )
23 22 fveq1d 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( X M Z ) ) ` Y ) = ( ( ( pInvG ` G ) ` ( Y M W ) ) ` Y ) )
24 5 oveqi 
 |-  ( Y M W ) = ( Y ( midG ` G ) W )
25 24 eqcomi 
 |-  ( Y ( midG ` G ) W ) = ( Y M W )
26 eqid 
 |-  ( dist ` G ) = ( dist ` G )
27 10 eldifad 
 |-  ( ph -> Z e. P )
28 10 eldifbd 
 |-  ( ph -> -. Z e. ( X L Y ) )
29 13 neneqd 
 |-  ( ph -> -. X = Y )
30 ioran 
 |-  ( -. ( Z e. ( X L Y ) \/ X = Y ) <-> ( -. Z e. ( X L Y ) /\ -. X = Y ) )
31 28 29 30 sylanbrc 
 |-  ( ph -> -. ( Z e. ( X L Y ) \/ X = Y ) )
32 1 2 15 6 8 9 27 31 ncoltgdim2 
 |-  ( ph -> G TarskiGDim>= 2 )
33 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
34 5 oveqi 
 |-  ( X M Z ) = ( X ( midG ` G ) Z )
35 1 26 15 6 32 8 27 midcl 
 |-  ( ph -> ( X ( midG ` G ) Z ) e. P )
36 34 35 eqeltrid 
 |-  ( ph -> ( X M Z ) e. P )
37 12 36 eqeltrrd 
 |-  ( ph -> ( Y M W ) e. P )
38 1 26 15 6 32 9 11 33 37 ismidb 
 |-  ( ph -> ( W = ( ( ( pInvG ` G ) ` ( Y M W ) ) ` Y ) <-> ( Y ( midG ` G ) W ) = ( Y M W ) ) )
39 25 38 mpbiri 
 |-  ( ph -> W = ( ( ( pInvG ` G ) ` ( Y M W ) ) ` Y ) )
40 23 39 eqtr4d 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( X M Z ) ) ` Y ) = W )
41 eqid 
 |-  ( ( pInvG ` G ) ` ( X M Z ) ) = ( ( pInvG ` G ) ` ( X M Z ) )
42 1 15 2 6 8 9 13 tglinerflx1 
 |-  ( ph -> X e. ( X L Y ) )
43 19 42 sseldd 
 |-  ( ph -> X e. ( ( X L Y ) E Z ) )
44 nelne2 
 |-  ( ( X e. ( X L Y ) /\ -. Z e. ( X L Y ) ) -> X =/= Z )
45 42 28 44 syl2anc 
 |-  ( ph -> X =/= Z )
46 1 15 2 3 6 17 43 21 45 lnssplng1 
 |-  ( ph -> ( X L Z ) C_ ( ( X L Y ) E Z ) )
47 1 26 15 6 32 8 27 midbtwn 
 |-  ( ph -> ( X ( midG ` G ) Z ) e. ( X ( Itv ` G ) Z ) )
48 34 47 eqeltrid 
 |-  ( ph -> ( X M Z ) e. ( X ( Itv ` G ) Z ) )
49 1 15 2 6 8 27 36 45 48 btwnlng1 
 |-  ( ph -> ( X M Z ) e. ( X L Z ) )
50 46 49 sseldd 
 |-  ( ph -> ( X M Z ) e. ( ( X L Y ) E Z ) )
51 1 15 2 6 8 9 13 tglinerflx2 
 |-  ( ph -> Y e. ( X L Y ) )
52 19 51 sseldd 
 |-  ( ph -> Y e. ( ( X L Y ) E Z ) )
53 1 3 33 41 6 17 50 52 mirplncl 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( X M Z ) ) ` Y ) e. ( ( X L Y ) E Z ) )
54 40 53 eqeltrrd 
 |-  ( ph -> W e. ( ( X L Y ) E Z ) )
55 6 adantr 
 |-  ( ( ph /\ Z = W ) -> G e. TarskiG )
56 36 adantr 
 |-  ( ( ph /\ Z = W ) -> ( X M Z ) e. P )
57 8 adantr 
 |-  ( ( ph /\ Z = W ) -> X e. P )
58 9 adantr 
 |-  ( ( ph /\ Z = W ) -> Y e. P )
59 34 eqcomi 
 |-  ( X ( midG ` G ) Z ) = ( X M Z )
60 1 26 15 6 32 8 27 33 36 ismidb 
 |-  ( ph -> ( Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` X ) <-> ( X ( midG ` G ) Z ) = ( X M Z ) ) )
61 59 60 mpbiri 
 |-  ( ph -> Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` X ) )
62 61 eqcomd 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( X M Z ) ) ` X ) = Z )
63 62 adantr 
 |-  ( ( ph /\ Z = W ) -> ( ( ( pInvG ` G ) ` ( X M Z ) ) ` X ) = Z )
64 simpr 
 |-  ( ( ph /\ Z = W ) -> Z = W )
65 40 eqcomd 
 |-  ( ph -> W = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` Y ) )
66 65 adantr 
 |-  ( ( ph /\ Z = W ) -> W = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` Y ) )
67 63 64 66 3eqtrd 
 |-  ( ( ph /\ Z = W ) -> ( ( ( pInvG ` G ) ` ( X M Z ) ) ` X ) = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` Y ) )
68 1 26 15 2 33 55 56 41 57 58 67 mireq 
 |-  ( ( ph /\ Z = W ) -> X = Y )
69 13 68 mteqand 
 |-  ( ph -> Z =/= W )
70 1 15 2 3 6 17 21 54 69 lnssplng1 
 |-  ( ph -> ( Z L W ) C_ ( ( X L Y ) E Z ) )
71 70 ad2antrr 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( Z L W ) C_ ( ( X L Y ) E Z ) )
72 42 ad2antrr 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> X e. ( X L Y ) )
73 20 72 sseldd 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> X e. ( ( X L Y ) E Z ) )
74 21 ad2antrr 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> Z e. ( ( X L Y ) E Z ) )
75 45 ad2antrr 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> X =/= Z )
76 1 15 2 3 14 18 73 74 75 lnssplng1 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( X L Z ) C_ ( ( X L Y ) E Z ) )
77 49 ad2antrr 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( X M Z ) e. ( X L Z ) )
78 76 77 sseldd 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( X M Z ) e. ( ( X L Y ) E Z ) )
79 simplr 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> e e. ( X L Y ) )
80 20 79 sseldd 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> e e. ( ( X L Y ) E Z ) )
81 6 adantr 
 |-  ( ( ph /\ ( X M Z ) e. ( X L Y ) ) -> G e. TarskiG )
82 8 adantr 
 |-  ( ( ph /\ ( X M Z ) e. ( X L Y ) ) -> X e. P )
83 36 adantr 
 |-  ( ( ph /\ ( X M Z ) e. ( X L Y ) ) -> ( X M Z ) e. P )
84 27 adantr 
 |-  ( ( ph /\ ( X M Z ) e. ( X L Y ) ) -> Z e. P )
85 simpr 
 |-  ( ( ph /\ X = ( X M Z ) ) -> X = ( X M Z ) )
86 85 34 eqtr2di 
 |-  ( ( ph /\ X = ( X M Z ) ) -> ( X ( midG ` G ) Z ) = X )
87 1 26 15 6 32 8 27 33 8 ismidb 
 |-  ( ph -> ( Z = ( ( ( pInvG ` G ) ` X ) ` X ) <-> ( X ( midG ` G ) Z ) = X ) )
88 87 adantr 
 |-  ( ( ph /\ X = ( X M Z ) ) -> ( Z = ( ( ( pInvG ` G ) ` X ) ` X ) <-> ( X ( midG ` G ) Z ) = X ) )
89 86 88 mpbird 
 |-  ( ( ph /\ X = ( X M Z ) ) -> Z = ( ( ( pInvG ` G ) ` X ) ` X ) )
90 eqid 
 |-  ( ( pInvG ` G ) ` X ) = ( ( pInvG ` G ) ` X )
91 1 26 15 2 33 6 8 90 mircinv 
 |-  ( ph -> ( ( ( pInvG ` G ) ` X ) ` X ) = X )
92 91 adantr 
 |-  ( ( ph /\ X = ( X M Z ) ) -> ( ( ( pInvG ` G ) ` X ) ` X ) = X )
93 89 92 eqtr2d 
 |-  ( ( ph /\ X = ( X M Z ) ) -> X = Z )
94 42 adantr 
 |-  ( ( ph /\ X = ( X M Z ) ) -> X e. ( X L Y ) )
95 93 94 eqeltrrd 
 |-  ( ( ph /\ X = ( X M Z ) ) -> Z e. ( X L Y ) )
96 28 95 mtand 
 |-  ( ph -> -. X = ( X M Z ) )
97 96 neqned 
 |-  ( ph -> X =/= ( X M Z ) )
98 97 adantr 
 |-  ( ( ph /\ ( X M Z ) e. ( X L Y ) ) -> X =/= ( X M Z ) )
99 1 15 2 6 8 27 45 tglinecom 
 |-  ( ph -> ( X L Z ) = ( Z L X ) )
100 49 99 eleqtrd 
 |-  ( ph -> ( X M Z ) e. ( Z L X ) )
101 100 adantr 
 |-  ( ( ph /\ ( X M Z ) e. ( X L Y ) ) -> ( X M Z ) e. ( Z L X ) )
102 45 adantr 
 |-  ( ( ph /\ ( X M Z ) e. ( X L Y ) ) -> X =/= Z )
103 102 necomd 
 |-  ( ( ph /\ ( X M Z ) e. ( X L Y ) ) -> Z =/= X )
104 1 15 2 81 82 83 84 98 101 103 lnrot1 
 |-  ( ( ph /\ ( X M Z ) e. ( X L Y ) ) -> Z e. ( X L ( X M Z ) ) )
105 16 adantr 
 |-  ( ( ph /\ ( X M Z ) e. ( X L Y ) ) -> ( X L Y ) e. ran L )
106 42 adantr 
 |-  ( ( ph /\ ( X M Z ) e. ( X L Y ) ) -> X e. ( X L Y ) )
107 simpr 
 |-  ( ( ph /\ ( X M Z ) e. ( X L Y ) ) -> ( X M Z ) e. ( X L Y ) )
108 1 15 2 81 82 83 98 98 105 106 107 tglinethru 
 |-  ( ( ph /\ ( X M Z ) e. ( X L Y ) ) -> ( X L Y ) = ( X L ( X M Z ) ) )
109 104 108 eleqtrrd 
 |-  ( ( ph /\ ( X M Z ) e. ( X L Y ) ) -> Z e. ( X L Y ) )
110 28 109 mtand 
 |-  ( ph -> -. ( X M Z ) e. ( X L Y ) )
111 110 ad2antrr 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> -. ( X M Z ) e. ( X L Y ) )
112 nelne2 
 |-  ( ( e e. ( X L Y ) /\ -. ( X M Z ) e. ( X L Y ) ) -> e =/= ( X M Z ) )
113 79 111 112 syl2anc 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> e =/= ( X M Z ) )
114 113 necomd 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( X M Z ) =/= e )
115 1 15 2 3 14 18 78 80 114 lnssplng1 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( ( X M Z ) L e ) C_ ( ( X L Y ) E Z ) )
116 16 ad2antrr 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( X L Y ) e. ran L )
117 1 2 15 14 116 79 tglnpt 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> e e. P )
118 36 ad2antrr 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( X M Z ) e. P )
119 1 15 2 14 117 118 113 tglinecom 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( e L ( X M Z ) ) = ( ( X M Z ) L e ) )
120 1 15 2 14 117 118 113 tgelrnln 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( e L ( X M Z ) ) e. ran L )
121 simpr 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) )
122 119 121 eqbrtrd 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( e L ( X M Z ) ) ( perpG ` G ) ( X L Y ) )
123 1 26 15 2 14 120 116 122 perpcom 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( X L Y ) ( perpG ` G ) ( e L ( X M Z ) ) )
124 119 123 breq2dd 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( X L Y ) ( perpG ` G ) ( ( X M Z ) L e ) )
125 14 adantr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> G e. TarskiG )
126 1 15 2 6 27 11 69 tgelrnln 
 |-  ( ph -> ( Z L W ) e. ran L )
127 126 ad2antrr 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( Z L W ) e. ran L )
128 127 adantr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( Z L W ) e. ran L )
129 119 120 eqeltrrd 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( ( X M Z ) L e ) e. ran L )
130 129 adantr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( ( X M Z ) L e ) e. ran L )
131 simpr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) )
132 8 ad2antrr 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> X e. P )
133 9 ad2antrr 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> Y e. P )
134 13 necomd 
 |-  ( ph -> Y =/= X )
135 134 ad2antrr 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> Y =/= X )
136 1 2 33 41 14 118 117 132 133 135 79 mirlni 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) e. ( ( ( ( pInvG ` G ) ` ( X M Z ) ) ` X ) L ( ( ( pInvG ` G ) ` ( X M Z ) ) ` Y ) ) )
137 62 40 oveq12d 
 |-  ( ph -> ( ( ( ( pInvG ` G ) ` ( X M Z ) ) ` X ) L ( ( ( pInvG ` G ) ` ( X M Z ) ) ` Y ) ) = ( Z L W ) )
138 137 ad2antrr 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( ( ( ( pInvG ` G ) ` ( X M Z ) ) ` X ) L ( ( ( pInvG ` G ) ` ( X M Z ) ) ` Y ) ) = ( Z L W ) )
139 136 138 eleqtrd 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) e. ( Z L W ) )
140 1 15 2 14 118 117 114 tglinerflx1 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( X M Z ) e. ( ( X M Z ) L e ) )
141 1 15 2 14 118 117 114 tglinerflx2 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> e e. ( ( X M Z ) L e ) )
142 1 26 15 2 33 14 41 129 140 141 mirln 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) e. ( ( X M Z ) L e ) )
143 139 142 elind 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) e. ( ( Z L W ) i^i ( ( X M Z ) L e ) ) )
144 143 adantr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) e. ( ( Z L W ) i^i ( ( X M Z ) L e ) ) )
145 131 144 eqeltrd 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> Z e. ( ( Z L W ) i^i ( ( X M Z ) L e ) ) )
146 1 15 2 6 27 11 69 tglinerflx2 
 |-  ( ph -> W e. ( Z L W ) )
147 146 ad3antrrr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> W e. ( Z L W ) )
148 140 adantr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( X M Z ) e. ( ( X M Z ) L e ) )
149 69 necomd 
 |-  ( ph -> W =/= Z )
150 149 ad3antrrr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> W =/= Z )
151 1 26 15 2 33 14 118 41 117 113 mirne 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) =/= ( X M Z ) )
152 151 necomd 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( X M Z ) =/= ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) )
153 152 adantr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( X M Z ) =/= ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) )
154 153 131 neeqtrrd 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( X M Z ) =/= Z )
155 40 ad3antrrr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( ( ( pInvG ` G ) ` ( X M Z ) ) ` Y ) = W )
156 131 eqcomd 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) = Z )
157 1 26 15 2 33 6 36 41 mircinv 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( X M Z ) ) ` ( X M Z ) ) = ( X M Z ) )
158 157 ad2antrr 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( ( ( pInvG ` G ) ` ( X M Z ) ) ` ( X M Z ) ) = ( X M Z ) )
159 158 adantr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( ( ( pInvG ` G ) ` ( X M Z ) ) ` ( X M Z ) ) = ( X M Z ) )
160 155 156 159 s3eqd 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> <" ( ( ( pInvG ` G ) ` ( X M Z ) ) ` Y ) ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ( ( ( pInvG ` G ) ` ( X M Z ) ) ` ( X M Z ) ) "> = <" W Z ( X M Z ) "> )
161 133 adantr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> Y e. P )
162 117 adantr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> e e. P )
163 118 adantr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( X M Z ) e. P )
164 132 adantr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> X e. P )
165 1 15 2 14 133 132 117 135 79 lncom 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> e e. ( Y L X ) )
166 165 adantr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> e e. ( Y L X ) )
167 1 15 2 6 8 9 13 tglinecom 
 |-  ( ph -> ( X L Y ) = ( Y L X ) )
168 167 ad3antrrr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( X L Y ) = ( Y L X ) )
169 116 adantr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( X L Y ) e. ran L )
170 simplr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) )
171 1 26 15 2 125 130 169 170 perpcom 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( X L Y ) ( perpG ` G ) ( ( X M Z ) L e ) )
172 168 171 eqbrtrrd 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( Y L X ) ( perpG ` G ) ( ( X M Z ) L e ) )
173 119 adantr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( e L ( X M Z ) ) = ( ( X M Z ) L e ) )
174 172 173 breqtrrd 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( Y L X ) ( perpG ` G ) ( e L ( X M Z ) ) )
175 1 26 15 2 125 161 164 166 163 174 perprag 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> <" Y e ( X M Z ) "> e. ( raG ` G ) )
176 1 26 15 2 33 125 161 162 163 175 41 163 mirrag 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> <" ( ( ( pInvG ` G ) ` ( X M Z ) ) ` Y ) ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ( ( ( pInvG ` G ) ` ( X M Z ) ) ` ( X M Z ) ) "> e. ( raG ` G ) )
177 160 176 eqeltrrd 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> <" W Z ( X M Z ) "> e. ( raG ` G ) )
178 1 26 15 2 125 128 130 145 147 148 150 154 177 ragperp 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( Z L W ) ( perpG ` G ) ( ( X M Z ) L e ) )
179 14 adantr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z =/= ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> G e. TarskiG )
180 127 adantr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z =/= ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( Z L W ) e. ran L )
181 129 adantr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z =/= ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( ( X M Z ) L e ) e. ran L )
182 143 adantr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z =/= ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) e. ( ( Z L W ) i^i ( ( X M Z ) L e ) ) )
183 1 15 2 6 27 11 69 tglinerflx1 
 |-  ( ph -> Z e. ( Z L W ) )
184 183 ad2antrr 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> Z e. ( Z L W ) )
185 184 adantr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z =/= ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> Z e. ( Z L W ) )
186 140 adantr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z =/= ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( X M Z ) e. ( ( X M Z ) L e ) )
187 simpr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z =/= ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> Z =/= ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) )
188 152 adantr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z =/= ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( X M Z ) =/= ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) )
189 62 ad2antrr 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( ( ( pInvG ` G ) ` ( X M Z ) ) ` X ) = Z )
190 eqidd 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) = ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) )
191 189 190 158 s3eqd 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> <" ( ( ( pInvG ` G ) ` ( X M Z ) ) ` X ) ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ( ( ( pInvG ` G ) ` ( X M Z ) ) ` ( X M Z ) ) "> = <" Z ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ( X M Z ) "> )
192 1 26 15 2 14 132 133 79 118 123 perprag 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> <" X e ( X M Z ) "> e. ( raG ` G ) )
193 1 26 15 2 33 14 132 117 118 192 41 118 mirrag 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> <" ( ( ( pInvG ` G ) ` ( X M Z ) ) ` X ) ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ( ( ( pInvG ` G ) ` ( X M Z ) ) ` ( X M Z ) ) "> e. ( raG ` G ) )
194 191 193 eqeltrrd 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> <" Z ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ( X M Z ) "> e. ( raG ` G ) )
195 194 adantr 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z =/= ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> <" Z ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ( X M Z ) "> e. ( raG ` G ) )
196 1 26 15 2 179 180 181 182 185 186 187 188 195 ragperp 
 |-  ( ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) /\ Z =/= ( ( ( pInvG ` G ) ` ( X M Z ) ) ` e ) ) -> ( Z L W ) ( perpG ` G ) ( ( X M Z ) L e ) )
197 178 196 pm2.61dane 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( Z L W ) ( perpG ` G ) ( ( X M Z ) L e ) )
198 1 2 3 4 14 18 20 71 115 124 197 perpprlng 
 |-  ( ( ( ph /\ e e. ( X L Y ) ) /\ ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) ) -> ( X L Y ) .|| ( Z L W ) )
199 1 26 15 2 6 16 36 110 footex 
 |-  ( ph -> E. e e. ( X L Y ) ( ( X M Z ) L e ) ( perpG ` G ) ( X L Y ) )
200 198 199 r19.29a 
 |-  ( ph -> ( X L Y ) .|| ( Z L W ) )