Metamath Proof Explorer

Theorem tgextalt2

Description: tgexta 's SECOND conjunct, strict, at a supplied second extension point E . This is NOT a permutation of the first conjunct: E is a new point, C between A and E , and tgextale / tgextancgra are applied a second time at the reconfigured triangle (the roles of A and B exchanged, exterior angle <" B C E "> ). tgextaoa then identifies <" B C E "> with <" A C D "> as vertical angles, and the two halves are transported across that congruence -- leacgra for leA , and cgratr under mtand for the negation, which leacgra cannot move. E is existentially constructed by tgexta , not here. (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses tgextalt2.p 
|- P = ( Base ` G )
tgextalt2.m 
|- .- = ( dist ` G )
tgextalt2.i 
|- I = ( Itv ` G )
tgextalt2.l 
|- L = ( LineG ` G )
tgextalt2.k 
|- K = ( hlG ` G )
tgextalt2.s 
|- .<_ = ( leA ` G )
tgextalt2.g 
|- ( ph -> G e. TarskiG )
tgextalt2.a 
|- ( ph -> A e. P )
tgextalt2.b 
|- ( ph -> B e. P )
tgextalt2.c 
|- ( ph -> C e. P )
tgextalt2.d 
|- ( ph -> D e. P )
tgextalt2.e 
|- ( ph -> E e. P )
tgextalt2.ext 
|- ( ph -> C e. ( B I D ) )
tgextalt2.ext2 
|- ( ph -> C e. ( A I E ) )
tgextalt2.ncol 
|- ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
tgextalt2.ne 
|- ( ph -> C =/= D )
tgextalt2.ne2 
|- ( ph -> C =/= E )
Assertion tgextalt2 
|- ( ph -> ( <" A B C "> .<_ <" A C D "> /\ -. <" A B C "> ( cgrA ` G ) <" A C D "> ) )

Proof

Step Hyp Ref Expression
1 tgextalt2.p 
 |-  P = ( Base ` G )
2 tgextalt2.m 
 |-  .- = ( dist ` G )
3 tgextalt2.i 
 |-  I = ( Itv ` G )
4 tgextalt2.l 
 |-  L = ( LineG ` G )
5 tgextalt2.k 
 |-  K = ( hlG ` G )
6 tgextalt2.s 
 |-  .<_ = ( leA ` G )
7 tgextalt2.g 
 |-  ( ph -> G e. TarskiG )
8 tgextalt2.a 
 |-  ( ph -> A e. P )
9 tgextalt2.b 
 |-  ( ph -> B e. P )
10 tgextalt2.c 
 |-  ( ph -> C e. P )
11 tgextalt2.d 
 |-  ( ph -> D e. P )
12 tgextalt2.e 
 |-  ( ph -> E e. P )
13 tgextalt2.ext 
 |-  ( ph -> C e. ( B I D ) )
14 tgextalt2.ext2 
 |-  ( ph -> C e. ( A I E ) )
15 tgextalt2.ncol 
 |-  ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
16 tgextalt2.ne 
 |-  ( ph -> C =/= D )
17 tgextalt2.ne2 
 |-  ( ph -> C =/= E )
18 1 4 3 7 9 10 8 15 ncolrot2 
 |-  ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
19 1 4 3 7 8 9 10 18 ncolcom 
 |-  ( ph -> -. ( C e. ( B L A ) \/ B = A ) )
20 1 4 3 7 9 8 10 19 ncolrot1 
 |-  ( ph -> -. ( B e. ( A L C ) \/ A = C ) )
21 1 2 3 4 5 7 9 8 10 12 14 20 17 tgextale 
 |-  ( ph -> <" C B A "> ( leA ` G ) <" B C E "> )
22 6 breqi 
 |-  ( <" C B A "> .<_ <" B C E "> <-> <" C B A "> ( leA ` G ) <" B C E "> )
23 21 22 sylibr 
 |-  ( ph -> <" C B A "> .<_ <" B C E "> )
24 1 4 3 7 9 10 8 15 ncolrot1 
 |-  ( ph -> -. ( B e. ( C L A ) \/ C = A ) )
25 1 3 4 7 9 10 8 24 ncolne1 
 |-  ( ph -> B =/= C )
26 25 necomd 
 |-  ( ph -> C =/= B )
27 1 3 4 7 8 9 10 15 ncolne1 
 |-  ( ph -> A =/= B )
28 27 necomd 
 |-  ( ph -> B =/= A )
29 1 3 7 5 10 9 8 26 28 cgraswap 
 |-  ( ph -> <" C B A "> ( cgrA ` G ) <" A B C "> )
30 1 3 4 7 8 9 10 15 ncolne2 
 |-  ( ph -> A =/= C )
31 30 necomd 
 |-  ( ph -> C =/= A )
32 16 necomd 
 |-  ( ph -> D =/= C )
33 1 2 3 5 7 8 9 10 11 12 13 14 26 31 32 17 tgextaoa 
 |-  ( ph -> <" B C E "> ( cgrA ` G ) <" A C D "> )
34 1 3 5 6 7 10 9 8 9 10 12 8 9 10 8 10 11 23 29 33 leacgra 
 |-  ( ph -> <" A B C "> .<_ <" A C D "> )
35 1 2 3 4 5 7 9 8 10 12 14 20 17 tgextancgra 
 |-  ( ph -> -. <" C B A "> ( cgrA ` G ) <" B C E "> )
36 7 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" A C D "> ) -> G e. TarskiG )
37 10 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" A C D "> ) -> C e. P )
38 9 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" A C D "> ) -> B e. P )
39 8 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" A C D "> ) -> A e. P )
40 11 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" A C D "> ) -> D e. P )
41 29 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" A C D "> ) -> <" C B A "> ( cgrA ` G ) <" A B C "> )
42 simpr 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" A C D "> ) -> <" A B C "> ( cgrA ` G ) <" A C D "> )
43 1 3 36 5 37 38 39 39 38 37 41 39 37 40 42 cgratr 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" A C D "> ) -> <" C B A "> ( cgrA ` G ) <" A C D "> )
44 12 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" A C D "> ) -> E e. P )
45 1 3 7 5 9 10 12 8 10 11 33 cgracom 
 |-  ( ph -> <" A C D "> ( cgrA ` G ) <" B C E "> )
46 45 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" A C D "> ) -> <" A C D "> ( cgrA ` G ) <" B C E "> )
47 1 3 36 5 37 38 39 39 37 40 43 38 37 44 46 cgratr 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" A C D "> ) -> <" C B A "> ( cgrA ` G ) <" B C E "> )
48 35 47 mtand 
 |-  ( ph -> -. <" A B C "> ( cgrA ` G ) <" A C D "> )
49 34 48 jca 
 |-  ( ph -> ( <" A B C "> .<_ <" A C D "> /\ -. <" A B C "> ( cgrA ` G ) <" A C D "> ) )