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 "> )