Metamath Proof Explorer

Theorem tgaaddcpbllem2

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 ) )
tgaaddcpbllem2.1 
|- ( ph -> R e. ( Y L S ) )
tgaaddcpbllem2.2 
|- ( ph -> R e. ( X I Z ) )
tgaaddcpbllem2.3 
|- ( ph -> Y e. ( S I R ) )
tgaaddcpbllem2.m 
|- M = ( ( pInvG ` G ) ` V )
tgaaddcpbllem2.k 
|- K = ( hlG ` G )
Assertion tgaaddcpbllem2 
|- ( 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 tgaaddcpbllem2.1 
 |-  ( ph -> R e. ( Y L S ) )
24 tgaaddcpbllem2.2 
 |-  ( ph -> R e. ( X I Z ) )
25 tgaaddcpbllem2.3 
 |-  ( ph -> Y e. ( S I R ) )
26 tgaaddcpbllem2.m 
 |-  M = ( ( pInvG ` G ) ` V )
27 tgaaddcpbllem2.k 
 |-  K = ( hlG ` G )
28 eleq1w 
 |-  ( e = s -> ( e e. ( a I b ) <-> s e. ( a I b ) ) )
29 28 cbvrexvw 
 |-  ( E. e e. ( Y L R ) e e. ( a I b ) <-> E. s e. ( Y L R ) s e. ( a I b ) )
30 29 anbi2i 
 |-  ( ( ( a e. ( P \ ( Y L R ) ) /\ b e. ( P \ ( Y L R ) ) ) /\ E. e e. ( Y L R ) e e. ( a I b ) ) <-> ( ( a e. ( P \ ( Y L R ) ) /\ b e. ( P \ ( Y L R ) ) ) /\ E. s e. ( Y L R ) s e. ( a I b ) ) )
31 30 opabbii 
 |-  { <. a , b >. | ( ( a e. ( P \ ( Y L R ) ) /\ b e. ( P \ ( Y L R ) ) ) /\ E. e e. ( Y L R ) e e. ( a I b ) ) } = { <. a , b >. | ( ( a e. ( P \ ( Y L R ) ) /\ b e. ( P \ ( Y L R ) ) ) /\ E. s e. ( Y L R ) s e. ( a I b ) ) }
32 eleq1w 
 |-  ( a = c -> ( a e. ( P \ ( V L ( M ` T ) ) ) <-> c e. ( P \ ( V L ( M ` T ) ) ) ) )
33 eleq1w 
 |-  ( b = d -> ( b e. ( P \ ( V L ( M ` T ) ) ) <-> d e. ( P \ ( V L ( M ` T ) ) ) ) )
34 32 33 bi2anan9 
 |-  ( ( a = c /\ b = d ) -> ( ( a e. ( P \ ( V L ( M ` T ) ) ) /\ b e. ( P \ ( V L ( M ` T ) ) ) ) <-> ( c e. ( P \ ( V L ( M ` T ) ) ) /\ d e. ( P \ ( V L ( M ` T ) ) ) ) ) )
35 oveq12 
 |-  ( ( a = c /\ b = d ) -> ( a I b ) = ( c I d ) )
36 35 eleq2d 
 |-  ( ( a = c /\ b = d ) -> ( f e. ( a I b ) <-> f e. ( c I d ) ) )
37 36 rexbidv 
 |-  ( ( a = c /\ b = d ) -> ( E. f e. ( V L ( M ` T ) ) f e. ( a I b ) <-> E. f e. ( V L ( M ` T ) ) f e. ( c I d ) ) )
38 eleq1w 
 |-  ( f = t -> ( f e. ( c I d ) <-> t e. ( c I d ) ) )
39 38 cbvrexvw 
 |-  ( E. f e. ( V L ( M ` T ) ) f e. ( c I d ) <-> E. t e. ( V L ( M ` T ) ) t e. ( c I d ) )
40 37 39 bitrdi 
 |-  ( ( a = c /\ b = d ) -> ( E. f e. ( V L ( M ` T ) ) f e. ( a I b ) <-> E. t e. ( V L ( M ` T ) ) t e. ( c I d ) ) )
41 34 40 anbi12d 
 |-  ( ( a = c /\ b = d ) -> ( ( ( a e. ( P \ ( V L ( M ` T ) ) ) /\ b e. ( P \ ( V L ( M ` T ) ) ) ) /\ E. f e. ( V L ( M ` T ) ) f e. ( a I b ) ) <-> ( ( c e. ( P \ ( V L ( M ` T ) ) ) /\ d e. ( P \ ( V L ( M ` T ) ) ) ) /\ E. t e. ( V L ( M ` T ) ) t e. ( c I d ) ) ) )
42 41 cbvopabv 
 |-  { <. a , b >. | ( ( a e. ( P \ ( V L ( M ` T ) ) ) /\ b e. ( P \ ( V L ( M ` T ) ) ) ) /\ E. f e. ( V L ( M ` T ) ) f e. ( a I b ) ) } = { <. c , d >. | ( ( c e. ( P \ ( V L ( M ` T ) ) ) /\ d e. ( P \ ( V L ( M ` T ) ) ) ) /\ E. t e. ( V L ( M ` T ) ) t e. ( c I d ) ) }
43 1 2 3 7 14 8 16 tgelrnln 
 |-  ( ph -> ( Y L S ) e. ran L )
44 1 3 2 7 43 23 tglnpt 
 |-  ( ph -> R e. P )
45 eqid 
 |-  ( dist ` G ) = ( dist ` G )
46 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
47 1 45 2 3 46 7 11 26 9 mircl 
 |-  ( ph -> ( M ` T ) e. P )
48 24 22 elnelneq2d 
 |-  ( ph -> -. R = Y )
49 48 neqned 
 |-  ( ph -> R =/= Y )
50 49 necomd 
 |-  ( ph -> Y =/= R )
51 17 necomd 
 |-  ( ph -> T =/= V )
52 1 45 2 3 46 7 11 26 9 51 mirne 
 |-  ( ph -> ( M ` T ) =/= V )
53 52 necomd 
 |-  ( ph -> V =/= ( M ` T ) )
54 1 2 3 7 14 44 50 tglinerflx2 
 |-  ( ph -> R e. ( Y L R ) )
55 1 45 2 5 3 43 7 13 15 18 oppne1 
 |-  ( ph -> -. X e. ( Y L S ) )
56 1 2 3 7 14 8 16 44 49 23 tglineelsb2 
 |-  ( ph -> ( Y L S ) = ( Y L R ) )
57 55 56 neleqtrd 
 |-  ( ph -> -. X e. ( Y L R ) )
58 1 45 2 5 3 43 7 13 15 18 oppne2 
 |-  ( ph -> -. Z e. ( Y L S ) )
59 58 56 neleqtrd 
 |-  ( ph -> -. Z e. ( Y L R ) )
60 1 45 2 31 13 15 54 57 59 24 islnoppd 
 |-  ( ph -> X { <. a , b >. | ( ( a e. ( P \ ( Y L R ) ) /\ b e. ( P \ ( Y L R ) ) ) /\ E. e e. ( Y L R ) e e. ( a I b ) ) } Z )
61 1 45 2 3 46 7 11 26 9 mirbtwn 
 |-  ( ph -> V e. ( ( M ` T ) I T ) )
62 1 2 3 7 11 9 47 17 61 btwnlng2 
 |-  ( ph -> ( M ` T ) e. ( V L T ) )
63 1 2 3 7 11 9 17 47 52 62 tglineelsb2 
 |-  ( ph -> ( V L T ) = ( V L ( M ` T ) ) )
64 63 difeq2d 
 |-  ( ph -> ( P \ ( V L T ) ) = ( P \ ( V L ( M ` T ) ) ) )
65 64 eleq2d 
 |-  ( ph -> ( c e. ( P \ ( V L T ) ) <-> c e. ( P \ ( V L ( M ` T ) ) ) ) )
66 64 eleq2d 
 |-  ( ph -> ( d e. ( P \ ( V L T ) ) <-> d e. ( P \ ( V L ( M ` T ) ) ) ) )
67 65 66 anbi12d 
 |-  ( ph -> ( ( c e. ( P \ ( V L T ) ) /\ d e. ( P \ ( V L T ) ) ) <-> ( c e. ( P \ ( V L ( M ` T ) ) ) /\ d e. ( P \ ( V L ( M ` T ) ) ) ) ) )
68 63 rexeqdv 
 |-  ( ph -> ( E. t e. ( V L T ) t e. ( c I d ) <-> E. t e. ( V L ( M ` T ) ) t e. ( c I d ) ) )
69 67 68 anbi12d 
 |-  ( ph -> ( ( ( c e. ( P \ ( V L T ) ) /\ d e. ( P \ ( V L T ) ) ) /\ E. t e. ( V L T ) t e. ( c I d ) ) <-> ( ( c e. ( P \ ( V L ( M ` T ) ) ) /\ d e. ( P \ ( V L ( M ` T ) ) ) ) /\ E. t e. ( V L ( M ` T ) ) t e. ( c I d ) ) ) )
70 69 opabbidv 
 |-  ( ph -> { <. 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 ) ) } = { <. c , d >. | ( ( c e. ( P \ ( V L ( M ` T ) ) ) /\ d e. ( P \ ( V L ( M ` T ) ) ) ) /\ E. t e. ( V L ( M ` T ) ) t e. ( c I d ) ) } )
71 70 6 42 3eqtr4g 
 |-  ( ph -> Q = { <. a , b >. | ( ( a e. ( P \ ( V L ( M ` T ) ) ) /\ b e. ( P \ ( V L ( M ` T ) ) ) ) /\ E. f e. ( V L ( M ` T ) ) f e. ( a I b ) ) } )
72 71 19 breqdi 
 |-  ( ph -> U { <. a , b >. | ( ( a e. ( P \ ( V L ( M ` T ) ) ) /\ b e. ( P \ ( V L ( M ` T ) ) ) ) /\ E. f e. ( V L ( M ` T ) ) f e. ( a I b ) ) } W )
73 4 a1i 
 |-  ( ph -> .~ = ( cgrA ` G ) )
74 73 eqcomd 
 |-  ( ph -> ( cgrA ` G ) = .~ )
75 73 20 breqdi 
 |-  ( ph -> <" X Y S "> ( cgrA ` G ) <" U V T "> )
76 1 2 45 7 13 14 8 10 11 9 75 cgraswaplr 
 |-  ( ph -> <" S Y X "> ( cgrA ` G ) <" T V U "> )
77 1 45 2 7 47 11 9 61 tgbtwncom 
 |-  ( ph -> V e. ( T I ( M ` T ) ) )
78 1 2 45 7 8 14 13 9 11 10 44 47 76 25 77 50 53 sacgr 
 |-  ( ph -> <" R Y X "> ( cgrA ` G ) <" ( M ` T ) V U "> )
79 1 2 45 7 44 14 13 47 11 10 78 cgraswaplr 
 |-  ( ph -> <" X Y R "> ( cgrA ` G ) <" U V ( M ` T ) "> )
80 74 79 breqdi 
 |-  ( ph -> <" X Y R "> .~ <" U V ( M ` T ) "> )
81 73 21 breqdi 
 |-  ( ph -> <" S Y Z "> ( cgrA ` G ) <" T V W "> )
82 1 2 45 7 8 14 15 9 11 12 44 47 81 25 77 50 53 sacgr 
 |-  ( ph -> <" R Y Z "> ( cgrA ` G ) <" ( M ` T ) V W "> )
83 74 82 breqdi 
 |-  ( ph -> <" R Y Z "> .~ <" ( M ` T ) V W "> )
84 1 2 27 44 13 14 7 49 hlid 
 |-  ( ph -> R ( K ` Y ) R )
85 1 2 3 4 31 42 7 44 47 10 11 12 13 14 15 50 53 60 72 80 83 22 27 54 24 84 tgaaddcpbllem1 
 |-  ( ph -> <" X Y Z "> .~ <" U V W "> )