Metamath Proof Explorer

Theorem quadcgrprlng

Description: Nontrivial quadrilaterals with congruent and parallel opposite sides are parallelograms. Theorem 12.20 of Schwabhauser p. 126. (Contributed by Thierry Arnoux, 20-Jul-2026)

Ref Expression
Hypotheses quadcgrprlng.p 
|- P = ( Base ` G )
quadcgrprlng.d 
|- .- = ( dist ` G )
quadcgrprlng.i 
|- I = ( Itv ` G )
quadcgrprlng.l 
|- L = ( LineG ` G )
quadcgrprlng.r 
|- .|| = ( parlnG ` G )
quadcgrprlng.o 
|- O = { <. a , b >. | ( ( a e. ( P \ ( X L Z ) ) /\ b e. ( P \ ( X L Z ) ) ) /\ E. t e. ( X L Z ) t e. ( a I b ) ) }
quadcgrprlng.g 
|- ( ph -> G e. TarskiG )
quadcgrprlng.1 
|- ( ph -> G e. TarskiGE )
quadcgrprlng.x 
|- ( ph -> X e. P )
quadcgrprlng.y 
|- ( ph -> Y e. P )
quadcgrprlng.z 
|- ( ph -> Z e. P )
quadcgrprlng.w 
|- ( ph -> W e. P )
quadcgrprlng.2 
|- ( ph -> -. ( X e. ( Y L Z ) \/ Y = Z ) )
quadcgrprlng.3 
|- ( ph -> ( X L Y ) .|| ( Z L W ) )
quadcgrprlng.4 
|- ( ph -> ( X .- Y ) = ( Z .- W ) )
quadcgrprlng.5 
|- ( ph -> Y O W )
Assertion quadcgrprlng 
|- ( ph -> ( ( Y L Z ) .|| ( W L X ) /\ ( Y .- Z ) = ( W .- X ) ) )

Proof

Step Hyp Ref Expression
1 quadcgrprlng.p 
 |-  P = ( Base ` G )
2 quadcgrprlng.d 
 |-  .- = ( dist ` G )
3 quadcgrprlng.i 
 |-  I = ( Itv ` G )
4 quadcgrprlng.l 
 |-  L = ( LineG ` G )
5 quadcgrprlng.r 
 |-  .|| = ( parlnG ` G )
6 quadcgrprlng.o 
 |-  O = { <. a , b >. | ( ( a e. ( P \ ( X L Z ) ) /\ b e. ( P \ ( X L Z ) ) ) /\ E. t e. ( X L Z ) t e. ( a I b ) ) }
7 quadcgrprlng.g 
 |-  ( ph -> G e. TarskiG )
8 quadcgrprlng.1 
 |-  ( ph -> G e. TarskiGE )
9 quadcgrprlng.x 
 |-  ( ph -> X e. P )
10 quadcgrprlng.y 
 |-  ( ph -> Y e. P )
11 quadcgrprlng.z 
 |-  ( ph -> Z e. P )
12 quadcgrprlng.w 
 |-  ( ph -> W e. P )
13 quadcgrprlng.2 
 |-  ( ph -> -. ( X e. ( Y L Z ) \/ Y = Z ) )
14 quadcgrprlng.3 
 |-  ( ph -> ( X L Y ) .|| ( Z L W ) )
15 quadcgrprlng.4 
 |-  ( ph -> ( X .- Y ) = ( Z .- W ) )
16 quadcgrprlng.5 
 |-  ( ph -> Y O W )
17 eqid 
 |-  ( PlnG ` G ) = ( PlnG ` G )
18 7 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) -> G e. TarskiG )
19 8 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) -> G e. TarskiGE )
20 1 4 3 7 10 11 9 13 ncolrot2 
 |-  ( ph -> -. ( Z e. ( X L Y ) \/ X = Y ) )
21 1 3 4 7 11 9 10 20 ncolne2 
 |-  ( ph -> Z =/= Y )
22 21 necomd 
 |-  ( ph -> Y =/= Z )
23 1 3 4 7 10 11 22 tgelrnln 
 |-  ( ph -> ( Y L Z ) e. ran L )
24 23 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) -> ( Y L Z ) e. ran L )
25 13 orsild 
 |-  ( ph -> -. X e. ( Y L Z ) )
26 9 25 eldifd 
 |-  ( ph -> X e. ( P \ ( Y L Z ) ) )
27 26 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) -> X e. ( P \ ( Y L Z ) ) )
28 1 4 17 18 24 27 tgelrnpln 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) -> ( ( Y L Z ) ( PlnG ` G ) X ) e. ran ( PlnG ` G ) )
29 4 5 7 14 prlngrcl2 
 |-  ( ph -> ( Z L W ) e. ran L )
30 29 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) -> ( Z L W ) e. ran L )
31 1 3 4 7 10 11 22 tglinerflx2 
 |-  ( ph -> Z e. ( Y L Z ) )
32 1 3 4 7 11 12 29 tglnne 
 |-  ( ph -> Z =/= W )
33 1 3 4 7 11 12 32 tglinerflx1 
 |-  ( ph -> Z e. ( Z L W ) )
34 31 33 elind 
 |-  ( ph -> Z e. ( ( Y L Z ) i^i ( Z L W ) ) )
35 34 ne0d 
 |-  ( ph -> ( ( Y L Z ) i^i ( Z L W ) ) =/= (/) )
36 35 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) -> ( ( Y L Z ) i^i ( Z L W ) ) =/= (/) )
37 20 orsild 
 |-  ( ph -> -. Z e. ( X L Y ) )
38 31 adantr 
 |-  ( ( ph /\ ( Y L Z ) = ( Z L W ) ) -> Z e. ( Y L Z ) )
39 7 adantr 
 |-  ( ( ph /\ ( Y L Z ) = ( Z L W ) ) -> G e. TarskiG )
40 8 adantr 
 |-  ( ( ph /\ ( Y L Z ) = ( Z L W ) ) -> G e. TarskiGE )
41 4 17 5 7 14 prlngsym 
 |-  ( ph -> ( Z L W ) .|| ( X L Y ) )
42 41 adantr 
 |-  ( ( ph /\ ( Y L Z ) = ( Z L W ) ) -> ( Z L W ) .|| ( X L Y ) )
43 29 adantr 
 |-  ( ( ph /\ ( Y L Z ) = ( Z L W ) ) -> ( Z L W ) e. ran L )
44 4 17 5 39 43 prlngref 
 |-  ( ( ph /\ ( Y L Z ) = ( Z L W ) ) -> ( Z L W ) .|| ( Z L W ) )
45 simpr 
 |-  ( ( ph /\ ( Y L Z ) = ( Z L W ) ) -> ( Y L Z ) = ( Z L W ) )
46 44 45 breqtrrd 
 |-  ( ( ph /\ ( Y L Z ) = ( Z L W ) ) -> ( Z L W ) .|| ( Y L Z ) )
47 1 3 4 7 9 10 11 13 ncolne1 
 |-  ( ph -> X =/= Y )
48 1 3 4 7 9 10 47 tglinerflx2 
 |-  ( ph -> Y e. ( X L Y ) )
49 48 adantr 
 |-  ( ( ph /\ ( Y L Z ) = ( Z L W ) ) -> Y e. ( X L Y ) )
50 1 3 4 7 10 11 22 tglinerflx1 
 |-  ( ph -> Y e. ( Y L Z ) )
51 50 adantr 
 |-  ( ( ph /\ ( Y L Z ) = ( Z L W ) ) -> Y e. ( Y L Z ) )
52 1 5 39 40 42 46 49 51 prlngeq 
 |-  ( ( ph /\ ( Y L Z ) = ( Z L W ) ) -> ( X L Y ) = ( Y L Z ) )
53 38 52 eleqtrrd 
 |-  ( ( ph /\ ( Y L Z ) = ( Z L W ) ) -> Z e. ( X L Y ) )
54 37 53 mtand 
 |-  ( ph -> -. ( Y L Z ) = ( Z L W ) )
55 54 neqned 
 |-  ( ph -> ( Y L Z ) =/= ( Z L W ) )
56 55 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) -> ( Y L Z ) =/= ( Z L W ) )
57 simplr 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) -> ( Y L Z ) .|| a )
58 1 3 4 17 18 24 27 elplnglnid 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) -> ( Y L Z ) C_ ( ( Y L Z ) ( PlnG ` G ) X ) )
59 simpr 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) -> X e. a )
60 25 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) -> -. X e. ( Y L Z ) )
61 nelne1 
 |-  ( ( X e. a /\ -. X e. ( Y L Z ) ) -> a =/= ( Y L Z ) )
62 59 60 61 syl2anc 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) -> a =/= ( Y L Z ) )
63 62 necomd 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) -> ( Y L Z ) =/= a )
64 4 17 5 18 57 63 59 prlngpln3 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) -> a C_ ( ( Y L Z ) ( PlnG ` G ) X ) )
65 1 3 4 7 9 10 11 12 13 tglineneq 
 |-  ( ph -> ( X L Y ) =/= ( Z L W ) )
66 4 17 5 7 14 65 33 prlngpln3 
 |-  ( ph -> ( Z L W ) C_ ( ( X L Y ) ( PlnG ` G ) Z ) )
67 1 4 3 7 10 11 9 13 ncolcom 
 |-  ( ph -> -. ( X e. ( Z L Y ) \/ Z = Y ) )
68 67 orsild 
 |-  ( ph -> -. X e. ( Z L Y ) )
69 9 68 eldifd 
 |-  ( ph -> X e. ( P \ ( Z L Y ) ) )
70 11 37 eldifd 
 |-  ( ph -> Z e. ( P \ ( X L Y ) ) )
71 1 3 4 17 7 69 10 70 47 plngrot 
 |-  ( ph -> ( ( X L Y ) ( PlnG ` G ) Z ) = ( ( Z L Y ) ( PlnG ` G ) X ) )
72 1 3 4 7 11 10 21 tglinecom 
 |-  ( ph -> ( Z L Y ) = ( Y L Z ) )
73 72 oveq1d 
 |-  ( ph -> ( ( Z L Y ) ( PlnG ` G ) X ) = ( ( Y L Z ) ( PlnG ` G ) X ) )
74 71 73 eqtr2d 
 |-  ( ph -> ( ( Y L Z ) ( PlnG ` G ) X ) = ( ( X L Y ) ( PlnG ` G ) Z ) )
75 66 74 sseqtrrd 
 |-  ( ph -> ( Z L W ) C_ ( ( Y L Z ) ( PlnG ` G ) X ) )
76 75 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) -> ( Z L W ) C_ ( ( Y L Z ) ( PlnG ` G ) X ) )
77 4 17 5 18 19 28 30 36 56 57 58 64 76 prlnginn0 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) -> ( a i^i ( Z L W ) ) =/= (/) )
78 simpllr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> ( Y L Z ) .|| a )
79 18 adantr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> G e. TarskiG )
80 30 adantr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> ( Z L W ) e. ran L )
81 simpr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> w e. ( a i^i ( Z L W ) ) )
82 81 elin2d 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> w e. ( Z L W ) )
83 1 4 3 79 80 82 tglnpt 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> w e. P )
84 9 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> X e. P )
85 33 adantr 
 |-  ( ( ph /\ X e. ( Z L W ) ) -> Z e. ( Z L W ) )
86 7 adantr 
 |-  ( ( ph /\ X e. ( Z L W ) ) -> G e. TarskiG )
87 8 adantr 
 |-  ( ( ph /\ X e. ( Z L W ) ) -> G e. TarskiGE )
88 1 3 4 7 9 10 47 tgelrnln 
 |-  ( ph -> ( X L Y ) e. ran L )
89 88 adantr 
 |-  ( ( ph /\ X e. ( Z L W ) ) -> ( X L Y ) e. ran L )
90 4 17 5 86 89 prlngref 
 |-  ( ( ph /\ X e. ( Z L W ) ) -> ( X L Y ) .|| ( X L Y ) )
91 14 adantr 
 |-  ( ( ph /\ X e. ( Z L W ) ) -> ( X L Y ) .|| ( Z L W ) )
92 1 3 4 7 9 10 47 tglinerflx1 
 |-  ( ph -> X e. ( X L Y ) )
93 92 adantr 
 |-  ( ( ph /\ X e. ( Z L W ) ) -> X e. ( X L Y ) )
94 simpr 
 |-  ( ( ph /\ X e. ( Z L W ) ) -> X e. ( Z L W ) )
95 1 5 86 87 90 91 93 94 prlngeq 
 |-  ( ( ph /\ X e. ( Z L W ) ) -> ( X L Y ) = ( Z L W ) )
96 85 95 eleqtrrd 
 |-  ( ( ph /\ X e. ( Z L W ) ) -> Z e. ( X L Y ) )
97 37 96 mtand 
 |-  ( ph -> -. X e. ( Z L W ) )
98 97 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> -. X e. ( Z L W ) )
99 nelne2 
 |-  ( ( w e. ( Z L W ) /\ -. X e. ( Z L W ) ) -> w =/= X )
100 82 98 99 syl2anc 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> w =/= X )
101 simp-4r 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> a e. ran L )
102 81 elin1d 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> w e. a )
103 simplr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> X e. a )
104 1 3 4 79 83 84 100 100 101 102 103 tglinethru 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> a = ( w L X ) )
105 78 104 breqtrd 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> ( Y L Z ) .|| ( w L X ) )
106 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
107 11 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> Z e. P )
108 10 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> Y e. P )
109 12 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> W e. P )
110 32 necomd 
 |-  ( ph -> W =/= Z )
111 110 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> W =/= Z )
112 47 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> X =/= Y )
113 1 3 4 7 9 10 11 13 ncolne2 
 |-  ( ph -> X =/= Z )
114 1 3 4 7 9 11 113 tgelrnln 
 |-  ( ph -> ( X L Z ) e. ran L )
115 114 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> ( X L Z ) e. ran L )
116 1 2 3 6 4 114 7 10 12 16 oppcom 
 |-  ( ph -> W O Y )
117 116 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> W O Y )
118 1 3 4 7 9 11 113 tglinerflx2 
 |-  ( ph -> Z e. ( X L Z ) )
119 118 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> Z e. ( X L Z ) )
120 19 adantr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> G e. TarskiGE )
121 13 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> -. ( X e. ( Y L Z ) \/ Y = Z ) )
122 14 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> ( X L Y ) .|| ( Z L W ) )
123 25 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> -. X e. ( Y L Z ) )
124 simpllr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) /\ Z = w ) -> X e. a )
125 79 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) /\ Z = w ) -> G e. TarskiG )
126 120 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) /\ Z = w ) -> G e. TarskiGE )
127 4 17 5 7 23 prlngref 
 |-  ( ph -> ( Y L Z ) .|| ( Y L Z ) )
128 127 ad5antr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) /\ Z = w ) -> ( Y L Z ) .|| ( Y L Z ) )
129 simp-4r 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) /\ Z = w ) -> ( Y L Z ) .|| a )
130 31 ad5antr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) /\ Z = w ) -> Z e. ( Y L Z ) )
131 simpr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) /\ Z = w ) -> Z = w )
132 102 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) /\ Z = w ) -> w e. a )
133 131 132 eqeltrd 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) /\ Z = w ) -> Z e. a )
134 1 5 125 126 128 129 130 133 prlngeq 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) /\ Z = w ) -> ( Y L Z ) = a )
135 124 134 eleqtrrd 
 |-  ( ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) /\ Z = w ) -> X e. ( Y L Z ) )
136 123 135 mtand 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> -. Z = w )
137 136 neqned 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> Z =/= w )
138 33 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> Z e. ( Z L W ) )
139 1 3 4 79 107 83 137 137 80 138 82 tglinethru 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> ( Z L W ) = ( Z L w ) )
140 122 139 breqtrd 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> ( X L Y ) .|| ( Z L w ) )
141 1 2 4 5 79 120 84 108 107 83 121 140 105 6 3 prlngsymquadopp 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> w O Y )
142 1 3 4 7 11 12 32 tglinecom 
 |-  ( ph -> ( Z L W ) = ( W L Z ) )
143 142 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> ( Z L W ) = ( W L Z ) )
144 82 143 eleqtrd 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> w e. ( W L Z ) )
145 1 3 4 6 106 79 115 109 108 117 119 141 144 hlopp 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> w ( ( hlG ` G ) ` Z ) W )
146 1 3 106 12 9 11 7 110 hlid 
 |-  ( ph -> W ( ( hlG ` G ) ` Z ) W )
147 146 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> W ( ( hlG ` G ) ` Z ) W )
148 1 2 4 5 79 120 84 108 107 83 121 140 105 prlngsymquad 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> ( ( X .- Y ) = ( Z .- w ) /\ ( Y .- Z ) = ( w .- X ) ) )
149 148 simpld 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> ( X .- Y ) = ( Z .- w ) )
150 149 eqcomd 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> ( Z .- w ) = ( X .- Y ) )
151 15 eqcomd 
 |-  ( ph -> ( Z .- W ) = ( X .- Y ) )
152 151 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> ( Z .- W ) = ( X .- Y ) )
153 1 2 106 107 84 108 79 109 111 112 145 147 150 152 hlcgreq 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> w = W )
154 153 oveq1d 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> ( w L X ) = ( W L X ) )
155 105 154 breqtrd 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> ( Y L Z ) .|| ( W L X ) )
156 148 simprd 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> ( Y .- Z ) = ( w .- X ) )
157 153 oveq1d 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> ( w .- X ) = ( W .- X ) )
158 156 157 eqtrd 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> ( Y .- Z ) = ( W .- X ) )
159 155 158 jca 
 |-  ( ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) /\ w e. ( a i^i ( Z L W ) ) ) -> ( ( Y L Z ) .|| ( W L X ) /\ ( Y .- Z ) = ( W .- X ) ) )
160 77 159 n0limd 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .|| a ) /\ X e. a ) -> ( ( Y L Z ) .|| ( W L X ) /\ ( Y .- Z ) = ( W .- X ) ) )
161 160 anasss 
 |-  ( ( ( ph /\ a e. ran L ) /\ ( ( Y L Z ) .|| a /\ X e. a ) ) -> ( ( Y L Z ) .|| ( W L X ) /\ ( Y .- Z ) = ( W .- X ) ) )
162 1 4 5 7 23 9 prlngex 
 |-  ( ph -> E. a e. ran L ( ( Y L Z ) .|| a /\ X e. a ) )
163 161 162 r19.29a 
 |-  ( ph -> ( ( Y L Z ) .|| ( W L X ) /\ ( Y .- Z ) = ( W .- X ) ) )