Metamath Proof Explorer

Theorem flatcgra

Description: Flat angles are congruent. (Contributed by Thierry Arnoux, 13-Feb-2023)

Ref Expression
Hypotheses cgracol.p 
|- P = ( Base ` G )
cgracol.i 
|- I = ( Itv ` G )
cgracol.m 
|- .- = ( dist ` G )
cgracol.g 
|- ( ph -> G e. TarskiG )
cgracol.a 
|- ( ph -> A e. P )
cgracol.b 
|- ( ph -> B e. P )
cgracol.c 
|- ( ph -> C e. P )
cgracol.d 
|- ( ph -> D e. P )
cgracol.e 
|- ( ph -> E e. P )
cgracol.f 
|- ( ph -> F e. P )
flatcgra.1 
|- ( ph -> B e. ( A I C ) )
flatcgra.2 
|- ( ph -> E e. ( D I F ) )
flatcgra.3 
|- ( ph -> A =/= B )
flatcgra.4 
|- ( ph -> C =/= B )
flatcgra.5 
|- ( ph -> D =/= E )
flatcgra.6 
|- ( ph -> F =/= E )
Assertion flatcgra 
|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )

Proof

Step Hyp Ref Expression
1 cgracol.p 
 |-  P = ( Base ` G )
2 cgracol.i 
 |-  I = ( Itv ` G )
3 cgracol.m 
 |-  .- = ( dist ` G )
4 cgracol.g 
 |-  ( ph -> G e. TarskiG )
5 cgracol.a 
 |-  ( ph -> A e. P )
6 cgracol.b 
 |-  ( ph -> B e. P )
7 cgracol.c 
 |-  ( ph -> C e. P )
8 cgracol.d 
 |-  ( ph -> D e. P )
9 cgracol.e 
 |-  ( ph -> E e. P )
10 cgracol.f 
 |-  ( ph -> F e. P )
11 flatcgra.1 
 |-  ( ph -> B e. ( A I C ) )
12 flatcgra.2 
 |-  ( ph -> E e. ( D I F ) )
13 flatcgra.3 
 |-  ( ph -> A =/= B )
14 flatcgra.4 
 |-  ( ph -> C =/= B )
15 flatcgra.5 
 |-  ( ph -> D =/= E )
16 flatcgra.6 
 |-  ( ph -> F =/= E )
17 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
18 4 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> G e. TarskiG )
19 5 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> A e. P )
20 6 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> B e. P )
21 7 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> C e. P )
22 simpllr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> x e. P )
23 9 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> E e. P )
24 simplr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> y e. P )
25 simprlr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( E .- x ) = ( B .- A ) )
26 1 3 2 18 23 22 20 19 25 tgcgrcomlr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( x .- E ) = ( A .- B ) )
27 26 eqcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( A .- B ) = ( x .- E ) )
28 simprrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( E .- y ) = ( B .- C ) )
29 28 eqcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( B .- C ) = ( E .- y ) )
30 10 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> F e. P )
31 8 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> D e. P )
32 16 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> F =/= E )
33 15 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> D =/= E )
34 1 3 2 4 8 9 10 12 tgbtwncom 
 |-  ( ph -> E e. ( F I D ) )
35 34 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> E e. ( F I D ) )
36 simprll 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> E e. ( F I x ) )
37 simprrl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> E e. ( D I y ) )
38 1 2 18 30 23 31 22 24 32 33 35 36 37 tgbtwnconn22 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> E e. ( x I y ) )
39 11 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> B e. ( A I C ) )
40 1 3 2 18 22 23 24 19 20 21 38 39 26 28 tgcgrextend 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( x .- y ) = ( A .- C ) )
41 40 eqcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( A .- C ) = ( x .- y ) )
42 1 3 2 18 19 21 22 24 41 tgcgrcomlr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( C .- A ) = ( y .- x ) )
43 1 3 17 18 19 20 21 22 23 24 27 29 42 trgcgr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> <" A B C "> ( cgrG ` G ) <" x E y "> )
44 25 eqcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( B .- A ) = ( E .- x ) )
45 13 necomd 
 |-  ( ph -> B =/= A )
46 45 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> B =/= A )
47 1 3 2 18 20 19 23 22 44 46 tgcgrneq 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> E =/= x )
48 47 necomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> x =/= E )
49 1 2 18 30 23 22 31 32 36 35 tgbtwnconn2 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( x e. ( E I D ) \/ D e. ( E I x ) ) )
50 48 33 49 3jca 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( x =/= E /\ D =/= E /\ ( x e. ( E I D ) \/ D e. ( E I x ) ) ) )
51 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
52 1 2 51 22 31 23 18 ishlg 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( x ( ( hlG ` G ) ` E ) D <-> ( x =/= E /\ D =/= E /\ ( x e. ( E I D ) \/ D e. ( E I x ) ) ) ) )
53 50 52 mpbird 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> x ( ( hlG ` G ) ` E ) D )
54 14 necomd 
 |-  ( ph -> B =/= C )
55 54 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> B =/= C )
56 1 3 2 18 20 21 23 24 29 55 tgcgrneq 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> E =/= y )
57 56 necomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> y =/= E )
58 12 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> E e. ( D I F ) )
59 1 2 18 31 23 24 30 33 37 58 tgbtwnconn2 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( y e. ( E I F ) \/ F e. ( E I y ) ) )
60 57 32 59 3jca 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( y =/= E /\ F =/= E /\ ( y e. ( E I F ) \/ F e. ( E I y ) ) ) )
61 1 2 51 24 30 23 18 ishlg 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( y ( ( hlG ` G ) ` E ) F <-> ( y =/= E /\ F =/= E /\ ( y e. ( E I F ) \/ F e. ( E I y ) ) ) ) )
62 60 61 mpbird 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> y ( ( hlG ` G ) ` E ) F )
63 43 53 62 3jca 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) )
64 1 3 2 4 10 9 6 5 axtgsegcon 
 |-  ( ph -> E. x e. P ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) )
65 1 3 2 4 8 9 6 7 axtgsegcon 
 |-  ( ph -> E. y e. P ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) )
66 reeanv 
 |-  ( E. x e. P E. y e. P ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) <-> ( E. x e. P ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ E. y e. P ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) )
67 64 65 66 sylanbrc 
 |-  ( ph -> E. x e. P E. y e. P ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) )
68 63 67 reximddv2 
 |-  ( ph -> E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) )
69 1 2 51 4 5 6 7 8 9 10 iscgra 
 |-  ( ph -> ( <" A B C "> ( cgrA ` G ) <" D E F "> <-> E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) )
70 68 69 mpbird 
 |-  ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )