Metamath Proof Explorer

Theorem tgaaddcpbl2

Description: The angular addition is compatible with angle congruence: by adding congruent angles together, we obtain congruent angles. Compared with tgaaddcpbl , this version handles cases where U , V and W are aligned. (Contributed by Thierry Arnoux, 23-Aug-2026)

Ref Expression
Hypotheses tgaaddcpbl2.p 
|- P = ( Base ` G )
tgaaddcpbl2.i 
|- I = ( Itv ` G )
tgaaddcpbl2.l 
|- L = ( LineG ` G )
tgaaddcpbl2.c 
|- .~ = ( cgrA ` G )
tgaaddcpbl2.1 
|- ( ph -> G e. TarskiG )
tgaaddcpbl2.s 
|- ( ph -> S e. P )
tgaaddcpbl2.t 
|- ( ph -> T e. P )
tgaaddcpbl2.u 
|- ( ph -> U e. P )
tgaaddcpbl2.v 
|- ( ph -> V e. P )
tgaaddcpbl2.w 
|- ( ph -> W e. P )
tgaaddcpbl2.x 
|- ( ph -> X e. P )
tgaaddcpbl2.y 
|- ( ph -> Y e. P )
tgaaddcpbl2.z 
|- ( ph -> Z e. P )
tgaaddcpbl2.2 
|- ( ph -> Y =/= S )
tgaaddcpbl2.3 
|- ( ph -> V =/= T )
tgaaddcpbl2.4 
|- ( ph -> ( ( Y L S ) i^i ( X I Z ) ) =/= (/) )
tgaaddcpbl2.5 
|- ( ph -> ( ( V L T ) i^i ( U I W ) ) =/= (/) )
tgaaddcpbl2.6 
|- ( ph -> <" X Y S "> .~ <" U V T "> )
tgaaddcpbl2.7 
|- ( ph -> <" S Y Z "> .~ <" T V W "> )
Assertion tgaaddcpbl2 
|- ( ph -> <" X Y Z "> .~ <" U V W "> )

Proof

Step Hyp Ref Expression
1 tgaaddcpbl2.p 
 |-  P = ( Base ` G )
2 tgaaddcpbl2.i 
 |-  I = ( Itv ` G )
3 tgaaddcpbl2.l 
 |-  L = ( LineG ` G )
4 tgaaddcpbl2.c 
 |-  .~ = ( cgrA ` G )
5 tgaaddcpbl2.1 
 |-  ( ph -> G e. TarskiG )
6 tgaaddcpbl2.s 
 |-  ( ph -> S e. P )
7 tgaaddcpbl2.t 
 |-  ( ph -> T e. P )
8 tgaaddcpbl2.u 
 |-  ( ph -> U e. P )
9 tgaaddcpbl2.v 
 |-  ( ph -> V e. P )
10 tgaaddcpbl2.w 
 |-  ( ph -> W e. P )
11 tgaaddcpbl2.x 
 |-  ( ph -> X e. P )
12 tgaaddcpbl2.y 
 |-  ( ph -> Y e. P )
13 tgaaddcpbl2.z 
 |-  ( ph -> Z e. P )
14 tgaaddcpbl2.2 
 |-  ( ph -> Y =/= S )
15 tgaaddcpbl2.3 
 |-  ( ph -> V =/= T )
16 tgaaddcpbl2.4 
 |-  ( ph -> ( ( Y L S ) i^i ( X I Z ) ) =/= (/) )
17 tgaaddcpbl2.5 
 |-  ( ph -> ( ( V L T ) i^i ( U I W ) ) =/= (/) )
18 tgaaddcpbl2.6 
 |-  ( ph -> <" X Y S "> .~ <" U V T "> )
19 tgaaddcpbl2.7 
 |-  ( ph -> <" S Y Z "> .~ <" T V W "> )
20 4 a1i 
 |-  ( ph -> .~ = ( cgrA ` G ) )
21 20 eqcomd 
 |-  ( ph -> ( cgrA ` G ) = .~ )
22 5 adantr 
 |-  ( ( ph /\ S ( ( hlG ` G ) ` Y ) X ) -> G e. TarskiG )
23 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
24 8 adantr 
 |-  ( ( ph /\ S ( ( hlG ` G ) ` Y ) X ) -> U e. P )
25 9 adantr 
 |-  ( ( ph /\ S ( ( hlG ` G ) ` Y ) X ) -> V e. P )
26 10 adantr 
 |-  ( ( ph /\ S ( ( hlG ` G ) ` Y ) X ) -> W e. P )
27 11 adantr 
 |-  ( ( ph /\ S ( ( hlG ` G ) ` Y ) X ) -> X e. P )
28 12 adantr 
 |-  ( ( ph /\ S ( ( hlG ` G ) ` Y ) X ) -> Y e. P )
29 13 adantr 
 |-  ( ( ph /\ S ( ( hlG ` G ) ` Y ) X ) -> Z e. P )
30 6 adantr 
 |-  ( ( ph /\ S ( ( hlG ` G ) ` Y ) X ) -> S e. P )
31 7 adantr 
 |-  ( ( ph /\ S ( ( hlG ` G ) ` Y ) X ) -> T e. P )
32 20 19 breqdi 
 |-  ( ph -> <" S Y Z "> ( cgrA ` G ) <" T V W "> )
33 32 adantr 
 |-  ( ( ph /\ S ( ( hlG ` G ) ` Y ) X ) -> <" S Y Z "> ( cgrA ` G ) <" T V W "> )
34 eqid 
 |-  ( dist ` G ) = ( dist ` G )
35 20 18 breqdi 
 |-  ( ph -> <" X Y S "> ( cgrA ` G ) <" U V T "> )
36 35 adantr 
 |-  ( ( ph /\ S ( ( hlG ` G ) ` Y ) X ) -> <" X Y S "> ( cgrA ` G ) <" U V T "> )
37 simpr 
 |-  ( ( ph /\ S ( ( hlG ` G ) ` Y ) X ) -> S ( ( hlG ` G ) ` Y ) X )
38 1 2 23 30 27 28 22 37 hlcomd 
 |-  ( ( ph /\ S ( ( hlG ` G ) ` Y ) X ) -> X ( ( hlG ` G ) ` Y ) S )
39 1 2 34 22 27 28 30 24 25 31 36 23 38 cgrahl 
 |-  ( ( ph /\ S ( ( hlG ` G ) ` Y ) X ) -> U ( ( hlG ` G ) ` V ) T )
40 1 2 23 22 30 28 29 31 25 26 33 24 39 cgrahl1 
 |-  ( ( ph /\ S ( ( hlG ` G ) ` Y ) X ) -> <" S Y Z "> ( cgrA ` G ) <" U V W "> )
41 1 2 22 23 30 28 29 24 25 26 40 cgracom 
 |-  ( ( ph /\ S ( ( hlG ` G ) ` Y ) X ) -> <" U V W "> ( cgrA ` G ) <" S Y Z "> )
42 1 2 23 22 24 25 26 30 28 29 41 27 38 cgrahl1 
 |-  ( ( ph /\ S ( ( hlG ` G ) ` Y ) X ) -> <" U V W "> ( cgrA ` G ) <" X Y Z "> )
43 1 2 22 23 24 25 26 27 28 29 42 cgracom 
 |-  ( ( ph /\ S ( ( hlG ` G ) ` Y ) X ) -> <" X Y Z "> ( cgrA ` G ) <" U V W "> )
44 43 adantlr 
 |-  ( ( ( ph /\ X e. ( Y L S ) ) /\ S ( ( hlG ` G ) ` Y ) X ) -> <" X Y Z "> ( cgrA ` G ) <" U V W "> )
45 5 adantr 
 |-  ( ( ph /\ Y e. ( X I S ) ) -> G e. TarskiG )
46 6 adantr 
 |-  ( ( ph /\ Y e. ( X I S ) ) -> S e. P )
47 12 adantr 
 |-  ( ( ph /\ Y e. ( X I S ) ) -> Y e. P )
48 13 adantr 
 |-  ( ( ph /\ Y e. ( X I S ) ) -> Z e. P )
49 7 adantr 
 |-  ( ( ph /\ Y e. ( X I S ) ) -> T e. P )
50 9 adantr 
 |-  ( ( ph /\ Y e. ( X I S ) ) -> V e. P )
51 10 adantr 
 |-  ( ( ph /\ Y e. ( X I S ) ) -> W e. P )
52 11 adantr 
 |-  ( ( ph /\ Y e. ( X I S ) ) -> X e. P )
53 8 adantr 
 |-  ( ( ph /\ Y e. ( X I S ) ) -> U e. P )
54 32 adantr 
 |-  ( ( ph /\ Y e. ( X I S ) ) -> <" S Y Z "> ( cgrA ` G ) <" T V W "> )
55 simpr 
 |-  ( ( ph /\ Y e. ( X I S ) ) -> Y e. ( X I S ) )
56 1 34 2 45 52 47 46 55 tgbtwncom 
 |-  ( ( ph /\ Y e. ( X I S ) ) -> Y e. ( S I X ) )
57 35 adantr 
 |-  ( ( ph /\ Y e. ( X I S ) ) -> <" X Y S "> ( cgrA ` G ) <" U V T "> )
58 1 2 34 45 52 47 46 53 50 49 57 55 cgrabtwn 
 |-  ( ( ph /\ Y e. ( X I S ) ) -> V e. ( U I T ) )
59 1 34 2 45 53 50 49 58 tgbtwncom 
 |-  ( ( ph /\ Y e. ( X I S ) ) -> V e. ( T I U ) )
60 1 2 23 5 11 12 6 8 9 7 35 cgrane1 
 |-  ( ph -> X =/= Y )
61 60 necomd 
 |-  ( ph -> Y =/= X )
62 61 adantr 
 |-  ( ( ph /\ Y e. ( X I S ) ) -> Y =/= X )
63 1 2 5 23 11 12 6 8 9 7 35 cgracom 
 |-  ( ph -> <" U V T "> ( cgrA ` G ) <" X Y S "> )
64 1 2 23 5 8 9 7 11 12 6 63 cgrane1 
 |-  ( ph -> U =/= V )
65 64 necomd 
 |-  ( ph -> V =/= U )
66 65 adantr 
 |-  ( ( ph /\ Y e. ( X I S ) ) -> V =/= U )
67 1 2 34 45 46 47 48 49 50 51 52 53 54 56 59 62 66 sacgr 
 |-  ( ( ph /\ Y e. ( X I S ) ) -> <" X Y Z "> ( cgrA ` G ) <" U V W "> )
68 67 adantlr 
 |-  ( ( ( ph /\ X e. ( Y L S ) ) /\ Y e. ( X I S ) ) -> <" X Y Z "> ( cgrA ` G ) <" U V W "> )
69 11 adantr 
 |-  ( ( ph /\ X e. ( Y L S ) ) -> X e. P )
70 12 adantr 
 |-  ( ( ph /\ X e. ( Y L S ) ) -> Y e. P )
71 6 adantr 
 |-  ( ( ph /\ X e. ( Y L S ) ) -> S e. P )
72 5 adantr 
 |-  ( ( ph /\ X e. ( Y L S ) ) -> G e. TarskiG )
73 60 adantr 
 |-  ( ( ph /\ X e. ( Y L S ) ) -> X =/= Y )
74 simpr 
 |-  ( ( ph /\ X e. ( Y L S ) ) -> X e. ( Y L S ) )
75 14 adantr 
 |-  ( ( ph /\ X e. ( Y L S ) ) -> Y =/= S )
76 1 2 3 72 69 70 71 73 74 75 lnrot2 
 |-  ( ( ph /\ X e. ( Y L S ) ) -> S e. ( X L Y ) )
77 1 2 23 69 70 71 72 69 3 76 lnhl 
 |-  ( ( ph /\ X e. ( Y L S ) ) -> ( S ( ( hlG ` G ) ` Y ) X \/ Y e. ( X I S ) ) )
78 44 68 77 mpjaodan 
 |-  ( ( ph /\ X e. ( Y L S ) ) -> <" X Y Z "> ( cgrA ` G ) <" U V W "> )
79 5 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ S ( ( hlG ` G ) ` Y ) Z ) -> G e. TarskiG )
80 11 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ S ( ( hlG ` G ) ` Y ) Z ) -> X e. P )
81 12 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ S ( ( hlG ` G ) ` Y ) Z ) -> Y e. P )
82 13 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ S ( ( hlG ` G ) ` Y ) Z ) -> Z e. P )
83 8 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ S ( ( hlG ` G ) ` Y ) Z ) -> U e. P )
84 9 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ S ( ( hlG ` G ) ` Y ) Z ) -> V e. P )
85 7 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ S ( ( hlG ` G ) ` Y ) Z ) -> T e. P )
86 6 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ S ( ( hlG ` G ) ` Y ) Z ) -> S e. P )
87 63 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ S ( ( hlG ` G ) ` Y ) Z ) -> <" U V T "> ( cgrA ` G ) <" X Y S "> )
88 simpr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ S ( ( hlG ` G ) ` Y ) Z ) -> S ( ( hlG ` G ) ` Y ) Z )
89 1 2 23 86 82 81 79 88 hlcomd 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ S ( ( hlG ` G ) ` Y ) Z ) -> Z ( ( hlG ` G ) ` Y ) S )
90 1 2 23 79 83 84 85 80 81 86 87 82 89 cgrahl2 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ S ( ( hlG ` G ) ` Y ) Z ) -> <" U V T "> ( cgrA ` G ) <" X Y Z "> )
91 1 2 79 23 83 84 85 80 81 82 90 cgracom 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ S ( ( hlG ` G ) ` Y ) Z ) -> <" X Y Z "> ( cgrA ` G ) <" U V T "> )
92 10 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ S ( ( hlG ` G ) ` Y ) Z ) -> W e. P )
93 32 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ S ( ( hlG ` G ) ` Y ) Z ) -> <" S Y Z "> ( cgrA ` G ) <" T V W "> )
94 1 2 34 79 86 81 82 85 84 92 93 23 88 cgrahl 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ S ( ( hlG ` G ) ` Y ) Z ) -> T ( ( hlG ` G ) ` V ) W )
95 1 2 23 85 92 84 79 94 hlcomd 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ S ( ( hlG ` G ) ` Y ) Z ) -> W ( ( hlG ` G ) ` V ) T )
96 1 2 23 79 80 81 82 83 84 85 91 92 95 cgrahl2 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ S ( ( hlG ` G ) ` Y ) Z ) -> <" X Y Z "> ( cgrA ` G ) <" U V W "> )
97 96 adantlr 
 |-  ( ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Z e. ( Y L S ) ) /\ S ( ( hlG ` G ) ` Y ) Z ) -> <" X Y Z "> ( cgrA ` G ) <" U V W "> )
98 5 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Y e. ( Z I S ) ) -> G e. TarskiG )
99 13 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Y e. ( Z I S ) ) -> Z e. P )
100 12 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Y e. ( Z I S ) ) -> Y e. P )
101 11 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Y e. ( Z I S ) ) -> X e. P )
102 10 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Y e. ( Z I S ) ) -> W e. P )
103 9 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Y e. ( Z I S ) ) -> V e. P )
104 8 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Y e. ( Z I S ) ) -> U e. P )
105 6 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Y e. ( Z I S ) ) -> S e. P )
106 7 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Y e. ( Z I S ) ) -> T e. P )
107 1 2 34 5 11 12 6 8 9 7 35 cgraswaplr 
 |-  ( ph -> <" S Y X "> ( cgrA ` G ) <" T V U "> )
108 107 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Y e. ( Z I S ) ) -> <" S Y X "> ( cgrA ` G ) <" T V U "> )
109 simpr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Y e. ( Z I S ) ) -> Y e. ( Z I S ) )
110 1 34 2 98 99 100 105 109 tgbtwncom 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Y e. ( Z I S ) ) -> Y e. ( S I Z ) )
111 32 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Y e. ( Z I S ) ) -> <" S Y Z "> ( cgrA ` G ) <" T V W "> )
112 1 2 34 98 105 100 99 106 103 102 111 110 cgrabtwn 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Y e. ( Z I S ) ) -> V e. ( T I W ) )
113 1 2 23 5 6 12 13 7 9 10 32 cgrane2 
 |-  ( ph -> Y =/= Z )
114 113 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Y e. ( Z I S ) ) -> Y =/= Z )
115 1 2 5 23 6 12 13 7 9 10 32 cgracom 
 |-  ( ph -> <" T V W "> ( cgrA ` G ) <" S Y Z "> )
116 1 2 23 5 7 9 10 6 12 13 115 cgrane2 
 |-  ( ph -> V =/= W )
117 116 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Y e. ( Z I S ) ) -> V =/= W )
118 1 2 34 98 105 100 101 106 103 104 99 102 108 110 112 114 117 sacgr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Y e. ( Z I S ) ) -> <" Z Y X "> ( cgrA ` G ) <" W V U "> )
119 1 2 34 98 99 100 101 102 103 104 118 cgraswaplr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Y e. ( Z I S ) ) -> <" X Y Z "> ( cgrA ` G ) <" U V W "> )
120 119 adantlr 
 |-  ( ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Z e. ( Y L S ) ) /\ Y e. ( Z I S ) ) -> <" X Y Z "> ( cgrA ` G ) <" U V W "> )
121 13 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Z e. ( Y L S ) ) -> Z e. P )
122 12 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Z e. ( Y L S ) ) -> Y e. P )
123 6 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Z e. ( Y L S ) ) -> S e. P )
124 5 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Z e. ( Y L S ) ) -> G e. TarskiG )
125 113 necomd 
 |-  ( ph -> Z =/= Y )
126 125 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Z e. ( Y L S ) ) -> Z =/= Y )
127 simpr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Z e. ( Y L S ) ) -> Z e. ( Y L S ) )
128 14 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Z e. ( Y L S ) ) -> Y =/= S )
129 1 2 3 124 121 122 123 126 127 128 lnrot2 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Z e. ( Y L S ) ) -> S e. ( Z L Y ) )
130 1 2 23 121 122 123 124 122 3 129 lnhl 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Z e. ( Y L S ) ) -> ( S ( ( hlG ` G ) ` Y ) Z \/ Y e. ( Z I S ) ) )
131 97 120 130 mpjaodan 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ Z e. ( Y L S ) ) -> <" X Y Z "> ( cgrA ` G ) <" U V W "> )
132 eqid 
 |-  ( cgrA ` G ) = ( cgrA ` G )
133 eleq1 
 |-  ( a = c -> ( a e. ( P \ ( Y L S ) ) <-> c e. ( P \ ( Y L S ) ) ) )
134 133 adantr 
 |-  ( ( a = c /\ b = d ) -> ( a e. ( P \ ( Y L S ) ) <-> c e. ( P \ ( Y L S ) ) ) )
135 eleq1 
 |-  ( b = d -> ( b e. ( P \ ( Y L S ) ) <-> d e. ( P \ ( Y L S ) ) ) )
136 135 adantl 
 |-  ( ( a = c /\ b = d ) -> ( b e. ( P \ ( Y L S ) ) <-> d e. ( P \ ( Y L S ) ) ) )
137 134 136 anbi12d 
 |-  ( ( a = c /\ b = d ) -> ( ( a e. ( P \ ( Y L S ) ) /\ b e. ( P \ ( Y L S ) ) ) <-> ( c e. ( P \ ( Y L S ) ) /\ d e. ( P \ ( Y L S ) ) ) ) )
138 oveq12 
 |-  ( ( a = c /\ b = d ) -> ( a I b ) = ( c I d ) )
139 138 eleq2d 
 |-  ( ( a = c /\ b = d ) -> ( s e. ( a I b ) <-> s e. ( c I d ) ) )
140 139 rexbidv 
 |-  ( ( a = c /\ b = d ) -> ( E. s e. ( Y L S ) s e. ( a I b ) <-> E. s e. ( Y L S ) s e. ( c I d ) ) )
141 eleq1 
 |-  ( s = t -> ( s e. ( c I d ) <-> t e. ( c I d ) ) )
142 141 cbvrexvw 
 |-  ( E. s e. ( Y L S ) s e. ( c I d ) <-> E. t e. ( Y L S ) t e. ( c I d ) )
143 140 142 bitrdi 
 |-  ( ( a = c /\ b = d ) -> ( E. s e. ( Y L S ) s e. ( a I b ) <-> E. t e. ( Y L S ) t e. ( c I d ) ) )
144 137 143 anbi12d 
 |-  ( ( a = c /\ b = d ) -> ( ( ( a e. ( P \ ( Y L S ) ) /\ b e. ( P \ ( Y L S ) ) ) /\ E. s e. ( Y L S ) s e. ( a I b ) ) <-> ( ( c e. ( P \ ( Y L S ) ) /\ d e. ( P \ ( Y L S ) ) ) /\ E. t e. ( Y L S ) t e. ( c I d ) ) ) )
145 144 cbvopabv 
 |-  { <. a , b >. | ( ( a e. ( P \ ( Y L S ) ) /\ b e. ( P \ ( Y L S ) ) ) /\ E. s e. ( Y L S ) s e. ( a I b ) ) } = { <. c , d >. | ( ( c e. ( P \ ( Y L S ) ) /\ d e. ( P \ ( Y L S ) ) ) /\ E. t e. ( Y L S ) t e. ( c I d ) ) }
146 eleq1 
 |-  ( e = g -> ( e e. ( P \ ( V L T ) ) <-> g e. ( P \ ( V L T ) ) ) )
147 146 adantr 
 |-  ( ( e = g /\ f = h ) -> ( e e. ( P \ ( V L T ) ) <-> g e. ( P \ ( V L T ) ) ) )
148 eleq1 
 |-  ( f = h -> ( f e. ( P \ ( V L T ) ) <-> h e. ( P \ ( V L T ) ) ) )
149 148 adantl 
 |-  ( ( e = g /\ f = h ) -> ( f e. ( P \ ( V L T ) ) <-> h e. ( P \ ( V L T ) ) ) )
150 147 149 anbi12d 
 |-  ( ( e = g /\ f = h ) -> ( ( e e. ( P \ ( V L T ) ) /\ f e. ( P \ ( V L T ) ) ) <-> ( g e. ( P \ ( V L T ) ) /\ h e. ( P \ ( V L T ) ) ) ) )
151 oveq12 
 |-  ( ( e = g /\ f = h ) -> ( e I f ) = ( g I h ) )
152 151 eleq2d 
 |-  ( ( e = g /\ f = h ) -> ( u e. ( e I f ) <-> u e. ( g I h ) ) )
153 152 rexbidv 
 |-  ( ( e = g /\ f = h ) -> ( E. u e. ( V L T ) u e. ( e I f ) <-> E. u e. ( V L T ) u e. ( g I h ) ) )
154 eleq1 
 |-  ( u = v -> ( u e. ( g I h ) <-> v e. ( g I h ) ) )
155 154 cbvrexvw 
 |-  ( E. u e. ( V L T ) u e. ( g I h ) <-> E. v e. ( V L T ) v e. ( g I h ) )
156 153 155 bitrdi 
 |-  ( ( e = g /\ f = h ) -> ( E. u e. ( V L T ) u e. ( e I f ) <-> E. v e. ( V L T ) v e. ( g I h ) ) )
157 150 156 anbi12d 
 |-  ( ( e = g /\ f = h ) -> ( ( ( e e. ( P \ ( V L T ) ) /\ f e. ( P \ ( V L T ) ) ) /\ E. u e. ( V L T ) u e. ( e I f ) ) <-> ( ( g e. ( P \ ( V L T ) ) /\ h e. ( P \ ( V L T ) ) ) /\ E. v e. ( V L T ) v e. ( g I h ) ) ) )
158 157 cbvopabv 
 |-  { <. e , f >. | ( ( e e. ( P \ ( V L T ) ) /\ f e. ( P \ ( V L T ) ) ) /\ E. u e. ( V L T ) u e. ( e I f ) ) } = { <. g , h >. | ( ( g e. ( P \ ( V L T ) ) /\ h e. ( P \ ( V L T ) ) ) /\ E. v e. ( V L T ) v e. ( g I h ) ) }
159 5 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> G e. TarskiG )
160 6 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> S e. P )
161 7 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> T e. P )
162 8 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> U e. P )
163 9 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> V e. P )
164 10 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> W e. P )
165 11 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> X e. P )
166 12 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> Y e. P )
167 13 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> Z e. P )
168 14 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> Y =/= S )
169 15 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> V =/= T )
170 simplr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> -. X e. ( Y L S ) )
171 165 170 eldifd 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> X e. ( P \ ( Y L S ) ) )
172 simpr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> -. Z e. ( Y L S ) )
173 167 172 eldifd 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> Z e. ( P \ ( Y L S ) ) )
174 171 173 jca 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> ( X e. ( P \ ( Y L S ) ) /\ Z e. ( P \ ( Y L S ) ) ) )
175 inn0 
 |-  ( ( ( Y L S ) i^i ( X I Z ) ) =/= (/) <-> E. t e. ( Y L S ) t e. ( X I Z ) )
176 16 175 sylib 
 |-  ( ph -> E. t e. ( Y L S ) t e. ( X I Z ) )
177 176 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> E. t e. ( Y L S ) t e. ( X I Z ) )
178 174 177 jca 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> ( ( X e. ( P \ ( Y L S ) ) /\ Z e. ( P \ ( Y L S ) ) ) /\ E. t e. ( Y L S ) t e. ( X I Z ) ) )
179 145 a1i 
 |-  ( ph -> { <. a , b >. | ( ( a e. ( P \ ( Y L S ) ) /\ b e. ( P \ ( Y L S ) ) ) /\ E. s e. ( Y L S ) s e. ( a I b ) ) } = { <. c , d >. | ( ( c e. ( P \ ( Y L S ) ) /\ d e. ( P \ ( Y L S ) ) ) /\ E. t e. ( Y L S ) t e. ( c I d ) ) } )
180 oveq12 
 |-  ( ( c = X /\ d = Z ) -> ( c I d ) = ( X I Z ) )
181 180 eleq2d 
 |-  ( ( c = X /\ d = Z ) -> ( t e. ( c I d ) <-> t e. ( X I Z ) ) )
182 181 adantl 
 |-  ( ( ph /\ ( c = X /\ d = Z ) ) -> ( t e. ( c I d ) <-> t e. ( X I Z ) ) )
183 182 rexbidv 
 |-  ( ( ph /\ ( c = X /\ d = Z ) ) -> ( E. t e. ( Y L S ) t e. ( c I d ) <-> E. t e. ( Y L S ) t e. ( X I Z ) ) )
184 179 183 brab2d 
 |-  ( ph -> ( X { <. a , b >. | ( ( a e. ( P \ ( Y L S ) ) /\ b e. ( P \ ( Y L S ) ) ) /\ E. s e. ( Y L S ) s e. ( a I b ) ) } Z <-> ( ( X e. ( P \ ( Y L S ) ) /\ Z e. ( P \ ( Y L S ) ) ) /\ E. t e. ( Y L S ) t e. ( X I Z ) ) ) )
185 184 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> ( X { <. a , b >. | ( ( a e. ( P \ ( Y L S ) ) /\ b e. ( P \ ( Y L S ) ) ) /\ E. s e. ( Y L S ) s e. ( a I b ) ) } Z <-> ( ( X e. ( P \ ( Y L S ) ) /\ Z e. ( P \ ( Y L S ) ) ) /\ E. t e. ( Y L S ) t e. ( X I Z ) ) ) )
186 178 185 mpbird 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> X { <. a , b >. | ( ( a e. ( P \ ( Y L S ) ) /\ b e. ( P \ ( Y L S ) ) ) /\ E. s e. ( Y L S ) s e. ( a I b ) ) } Z )
187 simpr 
 |-  ( ( ph /\ -. X e. ( Y L S ) ) -> -. X e. ( Y L S ) )
188 5 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ U e. ( V L T ) ) -> G e. TarskiG )
189 12 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ U e. ( V L T ) ) -> Y e. P )
190 6 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ U e. ( V L T ) ) -> S e. P )
191 11 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ U e. ( V L T ) ) -> X e. P )
192 14 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ U e. ( V L T ) ) -> Y =/= S )
193 8 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ U e. ( V L T ) ) -> U e. P )
194 9 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ U e. ( V L T ) ) -> V e. P )
195 7 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ U e. ( V L T ) ) -> T e. P )
196 63 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ U e. ( V L T ) ) -> <" U V T "> ( cgrA ` G ) <" X Y S "> )
197 animorrl 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ U e. ( V L T ) ) -> ( U e. ( V L T ) \/ V = T ) )
198 1 3 2 188 194 195 193 197 colrot2 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ U e. ( V L T ) ) -> ( T e. ( U L V ) \/ U = V ) )
199 1 2 34 188 193 194 195 191 189 190 196 3 198 cgracol 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ U e. ( V L T ) ) -> ( S e. ( X L Y ) \/ X = Y ) )
200 60 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ U e. ( V L T ) ) -> X =/= Y )
201 200 neneqd 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ U e. ( V L T ) ) -> -. X = Y )
202 199 201 olcnd 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ U e. ( V L T ) ) -> S e. ( X L Y ) )
203 1 2 3 188 189 190 191 192 202 200 lnrot1 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ U e. ( V L T ) ) -> X e. ( Y L S ) )
204 187 203 mtand 
 |-  ( ( ph /\ -. X e. ( Y L S ) ) -> -. U e. ( V L T ) )
205 204 adantr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> -. U e. ( V L T ) )
206 162 205 eldifd 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> U e. ( P \ ( V L T ) ) )
207 simpr 
 |-  ( ( ph /\ -. Z e. ( Y L S ) ) -> -. Z e. ( Y L S ) )
208 5 ad2antrr 
 |-  ( ( ( ph /\ -. Z e. ( Y L S ) ) /\ W e. ( V L T ) ) -> G e. TarskiG )
209 12 ad2antrr 
 |-  ( ( ( ph /\ -. Z e. ( Y L S ) ) /\ W e. ( V L T ) ) -> Y e. P )
210 6 ad2antrr 
 |-  ( ( ( ph /\ -. Z e. ( Y L S ) ) /\ W e. ( V L T ) ) -> S e. P )
211 13 ad2antrr 
 |-  ( ( ( ph /\ -. Z e. ( Y L S ) ) /\ W e. ( V L T ) ) -> Z e. P )
212 14 ad2antrr 
 |-  ( ( ( ph /\ -. Z e. ( Y L S ) ) /\ W e. ( V L T ) ) -> Y =/= S )
213 7 ad2antrr 
 |-  ( ( ( ph /\ -. Z e. ( Y L S ) ) /\ W e. ( V L T ) ) -> T e. P )
214 9 ad2antrr 
 |-  ( ( ( ph /\ -. Z e. ( Y L S ) ) /\ W e. ( V L T ) ) -> V e. P )
215 10 ad2antrr 
 |-  ( ( ( ph /\ -. Z e. ( Y L S ) ) /\ W e. ( V L T ) ) -> W e. P )
216 115 ad2antrr 
 |-  ( ( ( ph /\ -. Z e. ( Y L S ) ) /\ W e. ( V L T ) ) -> <" T V W "> ( cgrA ` G ) <" S Y Z "> )
217 animorrl 
 |-  ( ( ( ph /\ -. Z e. ( Y L S ) ) /\ W e. ( V L T ) ) -> ( W e. ( V L T ) \/ V = T ) )
218 1 3 2 208 214 213 215 217 colcom 
 |-  ( ( ( ph /\ -. Z e. ( Y L S ) ) /\ W e. ( V L T ) ) -> ( W e. ( T L V ) \/ T = V ) )
219 1 2 34 208 213 214 215 210 209 211 216 3 218 cgracol 
 |-  ( ( ( ph /\ -. Z e. ( Y L S ) ) /\ W e. ( V L T ) ) -> ( Z e. ( S L Y ) \/ S = Y ) )
220 14 necomd 
 |-  ( ph -> S =/= Y )
221 220 neneqd 
 |-  ( ph -> -. S = Y )
222 221 ad2antrr 
 |-  ( ( ( ph /\ -. Z e. ( Y L S ) ) /\ W e. ( V L T ) ) -> -. S = Y )
223 219 222 olcnd 
 |-  ( ( ( ph /\ -. Z e. ( Y L S ) ) /\ W e. ( V L T ) ) -> Z e. ( S L Y ) )
224 1 2 3 208 209 210 211 212 223 lncom 
 |-  ( ( ( ph /\ -. Z e. ( Y L S ) ) /\ W e. ( V L T ) ) -> Z e. ( Y L S ) )
225 207 224 mtand 
 |-  ( ( ph /\ -. Z e. ( Y L S ) ) -> -. W e. ( V L T ) )
226 225 adantlr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> -. W e. ( V L T ) )
227 164 226 eldifd 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> W e. ( P \ ( V L T ) ) )
228 206 227 jca 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> ( U e. ( P \ ( V L T ) ) /\ W e. ( P \ ( V L T ) ) ) )
229 inn0 
 |-  ( ( ( V L T ) i^i ( U I W ) ) =/= (/) <-> E. v e. ( V L T ) v e. ( U I W ) )
230 17 229 sylib 
 |-  ( ph -> E. v e. ( V L T ) v e. ( U I W ) )
231 230 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> E. v e. ( V L T ) v e. ( U I W ) )
232 228 231 jca 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> ( ( U e. ( P \ ( V L T ) ) /\ W e. ( P \ ( V L T ) ) ) /\ E. v e. ( V L T ) v e. ( U I W ) ) )
233 158 a1i 
 |-  ( ph -> { <. e , f >. | ( ( e e. ( P \ ( V L T ) ) /\ f e. ( P \ ( V L T ) ) ) /\ E. u e. ( V L T ) u e. ( e I f ) ) } = { <. g , h >. | ( ( g e. ( P \ ( V L T ) ) /\ h e. ( P \ ( V L T ) ) ) /\ E. v e. ( V L T ) v e. ( g I h ) ) } )
234 oveq12 
 |-  ( ( g = U /\ h = W ) -> ( g I h ) = ( U I W ) )
235 234 eleq2d 
 |-  ( ( g = U /\ h = W ) -> ( v e. ( g I h ) <-> v e. ( U I W ) ) )
236 235 adantl 
 |-  ( ( ph /\ ( g = U /\ h = W ) ) -> ( v e. ( g I h ) <-> v e. ( U I W ) ) )
237 236 rexbidv 
 |-  ( ( ph /\ ( g = U /\ h = W ) ) -> ( E. v e. ( V L T ) v e. ( g I h ) <-> E. v e. ( V L T ) v e. ( U I W ) ) )
238 233 237 brab2d 
 |-  ( ph -> ( U { <. e , f >. | ( ( e e. ( P \ ( V L T ) ) /\ f e. ( P \ ( V L T ) ) ) /\ E. u e. ( V L T ) u e. ( e I f ) ) } W <-> ( ( U e. ( P \ ( V L T ) ) /\ W e. ( P \ ( V L T ) ) ) /\ E. v e. ( V L T ) v e. ( U I W ) ) ) )
239 238 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> ( U { <. e , f >. | ( ( e e. ( P \ ( V L T ) ) /\ f e. ( P \ ( V L T ) ) ) /\ E. u e. ( V L T ) u e. ( e I f ) ) } W <-> ( ( U e. ( P \ ( V L T ) ) /\ W e. ( P \ ( V L T ) ) ) /\ E. v e. ( V L T ) v e. ( U I W ) ) ) )
240 232 239 mpbird 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> U { <. e , f >. | ( ( e e. ( P \ ( V L T ) ) /\ f e. ( P \ ( V L T ) ) ) /\ E. u e. ( V L T ) u e. ( e I f ) ) } W )
241 35 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> <" X Y S "> ( cgrA ` G ) <" U V T "> )
242 32 ad2antrr 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> <" S Y Z "> ( cgrA ` G ) <" T V W "> )
243 1 2 3 132 145 158 159 160 161 162 163 164 165 166 167 168 169 186 240 241 242 tgaaddcpbl 
 |-  ( ( ( ph /\ -. X e. ( Y L S ) ) /\ -. Z e. ( Y L S ) ) -> <" X Y Z "> ( cgrA ` G ) <" U V W "> )
244 exmidd 
 |-  ( ( ph /\ -. X e. ( Y L S ) ) -> ( Z e. ( Y L S ) \/ -. Z e. ( Y L S ) ) )
245 131 243 244 mpjaodan 
 |-  ( ( ph /\ -. X e. ( Y L S ) ) -> <" X Y Z "> ( cgrA ` G ) <" U V W "> )
246 exmidd 
 |-  ( ph -> ( X e. ( Y L S ) \/ -. X e. ( Y L S ) ) )
247 78 245 246 mpjaodan 
 |-  ( ph -> <" X Y Z "> ( cgrA ` G ) <" U V W "> )
248 21 247 breqdi 
 |-  ( ph -> <" X Y Z "> .~ <" U V W "> )