Metamath Proof Explorer

Theorem tgaaddcpbllem3

Description: Lemma for tgaaddcpbl . (Contributed by Thierry Arnoux, 2-Aug-2026)

Ref Expression
Hypotheses tgaaddcpbl.p 
|- P = ( Base ` G )
tgaaddcpbl.i 
|- I = ( Itv ` G )
tgaaddcpbl.l 
|- L = ( LineG ` G )
tgaaddcpbl.c 
|- .~ = ( cgrA ` G )
tgaaddcpbl.o 
|- O = { <. 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 ) ) }
tgaaddcpbl.q 
|- Q = { <. c , d >. | ( ( c e. ( P \ ( V L T ) ) /\ d e. ( P \ ( V L T ) ) ) /\ E. t e. ( V L T ) t e. ( c I d ) ) }
tgaaddcpbl.1 
|- ( ph -> G e. TarskiG )
tgaaddcpbl.s 
|- ( ph -> S e. P )
tgaaddcpbl.t 
|- ( ph -> T e. P )
tgaaddcpbl.u 
|- ( ph -> U e. P )
tgaaddcpbl.v 
|- ( ph -> V e. P )
tgaaddcpbl.w 
|- ( ph -> W e. P )
tgaaddcpbl.x 
|- ( ph -> X e. P )
tgaaddcpbl.y 
|- ( ph -> Y e. P )
tgaaddcpbl.z 
|- ( ph -> Z e. P )
tgaaddcpbl.2 
|- ( ph -> Y =/= S )
tgaaddcpbl.3 
|- ( ph -> V =/= T )
tgaaddcpbl.4 
|- ( ph -> X O Z )
tgaaddcpbl.5 
|- ( ph -> U Q W )
tgaaddcpbl.6 
|- ( ph -> <" X Y S "> .~ <" U V T "> )
tgaaddcpbl.7 
|- ( ph -> <" S Y Z "> .~ <" T V W "> )
tgaaddcpbllem3.1 
|- ( ph -> -. Y e. ( X I Z ) )
Assertion tgaaddcpbllem3 
|- ( ph -> <" X Y Z "> .~ <" U V W "> )

Proof

Step Hyp Ref Expression
1 tgaaddcpbl.p 
 |-  P = ( Base ` G )
2 tgaaddcpbl.i 
 |-  I = ( Itv ` G )
3 tgaaddcpbl.l 
 |-  L = ( LineG ` G )
4 tgaaddcpbl.c 
 |-  .~ = ( cgrA ` G )
5 tgaaddcpbl.o 
 |-  O = { <. 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 ) ) }
6 tgaaddcpbl.q 
 |-  Q = { <. c , d >. | ( ( c e. ( P \ ( V L T ) ) /\ d e. ( P \ ( V L T ) ) ) /\ E. t e. ( V L T ) t e. ( c I d ) ) }
7 tgaaddcpbl.1 
 |-  ( ph -> G e. TarskiG )
8 tgaaddcpbl.s 
 |-  ( ph -> S e. P )
9 tgaaddcpbl.t 
 |-  ( ph -> T e. P )
10 tgaaddcpbl.u 
 |-  ( ph -> U e. P )
11 tgaaddcpbl.v 
 |-  ( ph -> V e. P )
12 tgaaddcpbl.w 
 |-  ( ph -> W e. P )
13 tgaaddcpbl.x 
 |-  ( ph -> X e. P )
14 tgaaddcpbl.y 
 |-  ( ph -> Y e. P )
15 tgaaddcpbl.z 
 |-  ( ph -> Z e. P )
16 tgaaddcpbl.2 
 |-  ( ph -> Y =/= S )
17 tgaaddcpbl.3 
 |-  ( ph -> V =/= T )
18 tgaaddcpbl.4 
 |-  ( ph -> X O Z )
19 tgaaddcpbl.5 
 |-  ( ph -> U Q W )
20 tgaaddcpbl.6 
 |-  ( ph -> <" X Y S "> .~ <" U V T "> )
21 tgaaddcpbl.7 
 |-  ( ph -> <" S Y Z "> .~ <" T V W "> )
22 tgaaddcpbllem3.1 
 |-  ( ph -> -. Y e. ( X I Z ) )
23 eleq1w 
 |-  ( s = r -> ( s e. ( a I b ) <-> r e. ( a I b ) ) )
24 23 cbvrexvw 
 |-  ( E. s e. ( Y L S ) s e. ( a I b ) <-> E. r e. ( Y L S ) r e. ( a I b ) )
25 24 anbi2i 
 |-  ( ( ( a e. ( P \ ( Y L S ) ) /\ b e. ( P \ ( Y L S ) ) ) /\ E. s e. ( Y L S ) s e. ( a I b ) ) <-> ( ( a e. ( P \ ( Y L S ) ) /\ b e. ( P \ ( Y L S ) ) ) /\ E. r e. ( Y L S ) r e. ( a I b ) ) )
26 25 opabbii 
 |-  { <. 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 ) ) } = { <. a , b >. | ( ( a e. ( P \ ( Y L S ) ) /\ b e. ( P \ ( Y L S ) ) ) /\ E. r e. ( Y L S ) r e. ( a I b ) ) }
27 5 26 eqtri 
 |-  O = { <. a , b >. | ( ( a e. ( P \ ( Y L S ) ) /\ b e. ( P \ ( Y L S ) ) ) /\ E. r e. ( Y L S ) r e. ( a I b ) ) }
28 7 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ s ( ( hlG ` G ) ` Y ) S ) -> G e. TarskiG )
29 8 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ s ( ( hlG ` G ) ` Y ) S ) -> S e. P )
30 9 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ s ( ( hlG ` G ) ` Y ) S ) -> T e. P )
31 10 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ s ( ( hlG ` G ) ` Y ) S ) -> U e. P )
32 11 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ s ( ( hlG ` G ) ` Y ) S ) -> V e. P )
33 12 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ s ( ( hlG ` G ) ` Y ) S ) -> W e. P )
34 13 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ s ( ( hlG ` G ) ` Y ) S ) -> X e. P )
35 14 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ s ( ( hlG ` G ) ` Y ) S ) -> Y e. P )
36 15 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ s ( ( hlG ` G ) ` Y ) S ) -> Z e. P )
37 16 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ s ( ( hlG ` G ) ` Y ) S ) -> Y =/= S )
38 17 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ s ( ( hlG ` G ) ` Y ) S ) -> V =/= T )
39 18 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ s ( ( hlG ` G ) ` Y ) S ) -> X O Z )
40 19 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ s ( ( hlG ` G ) ` Y ) S ) -> U Q W )
41 20 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ s ( ( hlG ` G ) ` Y ) S ) -> <" X Y S "> .~ <" U V T "> )
42 21 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ s ( ( hlG ` G ) ` Y ) S ) -> <" S Y Z "> .~ <" T V W "> )
43 22 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ s ( ( hlG ` G ) ` Y ) S ) -> -. Y e. ( X I Z ) )
44 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
45 simpllr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ s ( ( hlG ` G ) ` Y ) S ) -> s e. ( Y L S ) )
46 simplr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ s ( ( hlG ` G ) ` Y ) S ) -> s e. ( X I Z ) )
47 simpr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ s ( ( hlG ` G ) ` Y ) S ) -> s ( ( hlG ` G ) ` Y ) S )
48 1 2 3 4 27 6 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 tgaaddcpbllem1 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ s ( ( hlG ` G ) ` Y ) S ) -> <" X Y Z "> .~ <" U V W "> )
49 7 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ Y e. ( S I s ) ) -> G e. TarskiG )
50 8 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ Y e. ( S I s ) ) -> S e. P )
51 9 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ Y e. ( S I s ) ) -> T e. P )
52 10 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ Y e. ( S I s ) ) -> U e. P )
53 11 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ Y e. ( S I s ) ) -> V e. P )
54 12 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ Y e. ( S I s ) ) -> W e. P )
55 13 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ Y e. ( S I s ) ) -> X e. P )
56 14 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ Y e. ( S I s ) ) -> Y e. P )
57 15 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ Y e. ( S I s ) ) -> Z e. P )
58 16 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ Y e. ( S I s ) ) -> Y =/= S )
59 17 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ Y e. ( S I s ) ) -> V =/= T )
60 18 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ Y e. ( S I s ) ) -> X O Z )
61 19 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ Y e. ( S I s ) ) -> U Q W )
62 20 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ Y e. ( S I s ) ) -> <" X Y S "> .~ <" U V T "> )
63 21 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ Y e. ( S I s ) ) -> <" S Y Z "> .~ <" T V W "> )
64 22 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ Y e. ( S I s ) ) -> -. Y e. ( X I Z ) )
65 simpllr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ Y e. ( S I s ) ) -> s e. ( Y L S ) )
66 simplr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ Y e. ( S I s ) ) -> s e. ( X I Z ) )
67 simpr 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ Y e. ( S I s ) ) -> Y e. ( S I s ) )
68 eqid 
 |-  ( ( pInvG ` G ) ` V ) = ( ( pInvG ` G ) ` V )
69 1 2 3 4 27 6 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 44 tgaaddcpbllem2 
 |-  ( ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) /\ Y e. ( S I s ) ) -> <" X Y Z "> .~ <" U V W "> )
70 8 ad2antrr 
 |-  ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) -> S e. P )
71 14 ad2antrr 
 |-  ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) -> Y e. P )
72 7 ad2antrr 
 |-  ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) -> G e. TarskiG )
73 1 2 3 7 14 8 16 tgelrnln 
 |-  ( ph -> ( Y L S ) e. ran L )
74 73 ad2antrr 
 |-  ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) -> ( Y L S ) e. ran L )
75 simplr 
 |-  ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) -> s e. ( Y L S ) )
76 1 3 2 72 74 75 tglnpt 
 |-  ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) -> s e. P )
77 13 ad2antrr 
 |-  ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) -> X e. P )
78 16 necomd 
 |-  ( ph -> S =/= Y )
79 78 ad2antrr 
 |-  ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) -> S =/= Y )
80 1 2 3 72 70 71 76 79 75 lncom 
 |-  ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) -> s e. ( S L Y ) )
81 1 2 44 70 71 76 72 77 3 80 lnhl 
 |-  ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) -> ( s ( ( hlG ` G ) ` Y ) S \/ Y e. ( S I s ) ) )
82 48 69 81 mpjaodan 
 |-  ( ( ( ph /\ s e. ( Y L S ) ) /\ s e. ( X I Z ) ) -> <" X Y Z "> .~ <" U V W "> )
83 eqid 
 |-  ( dist ` G ) = ( dist ` G )
84 1 83 2 5 13 15 islnopp 
 |-  ( ph -> ( X O Z <-> ( ( -. X e. ( Y L S ) /\ -. Z e. ( Y L S ) ) /\ E. s e. ( Y L S ) s e. ( X I Z ) ) ) )
85 18 84 mpbid 
 |-  ( ph -> ( ( -. X e. ( Y L S ) /\ -. Z e. ( Y L S ) ) /\ E. s e. ( Y L S ) s e. ( X I Z ) ) )
86 85 simprd 
 |-  ( ph -> E. s e. ( Y L S ) s e. ( X I Z ) )
87 82 86 r19.29a 
 |-  ( ph -> <" X Y Z "> .~ <" U V W "> )