Metamath Proof Explorer

Theorem zerocgra

Description: Zero angles are congruent. Zero angles, that is, angles of degree zero, can be expressed by stating that points A and C are on the same ray starting at B , that is, A ( KB ) C . See also flatcgra . (Contributed by Thierry Arnoux, 23-Aug-2026)

Ref Expression
Hypotheses zerocgra.p 
|- P = ( Base ` G )
zerocgra.a 
|- .~ = ( cgrA ` G )
zerocgra.k 
|- K = ( hlG ` G )
zerocgra.g 
|- ( ph -> G e. TarskiG )
zerocgra.1 
|- ( ph -> A ( K ` B ) C )
zerocgra.2 
|- ( ph -> D ( K ` E ) F )
zerocgra.b 
|- ( ph -> B e. P )
zerocgra.e 
|- ( ph -> E e. P )
Assertion zerocgra 
|- ( ph -> <" A B C "> .~ <" D E F "> )

Proof

Step Hyp Ref Expression
1 zerocgra.p 
 |-  P = ( Base ` G )
2 zerocgra.a 
 |-  .~ = ( cgrA ` G )
3 zerocgra.k 
 |-  K = ( hlG ` G )
4 zerocgra.g 
 |-  ( ph -> G e. TarskiG )
5 zerocgra.1 
 |-  ( ph -> A ( K ` B ) C )
6 zerocgra.2 
 |-  ( ph -> D ( K ` E ) F )
7 zerocgra.b 
 |-  ( ph -> B e. P )
8 zerocgra.e 
 |-  ( ph -> E e. P )
9 2 eqcomi 
 |-  ( cgrA ` G ) = .~
10 9 a1i 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> ( cgrA ` G ) = .~ )
11 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
12 4 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> G e. TarskiG )
13 1 11 3 4 7 5 hlgrcl1 
 |-  ( ph -> A e. P )
14 13 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> A e. P )
15 7 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> B e. P )
16 1 11 3 4 7 5 hlgrcl2 
 |-  ( ph -> C e. P )
17 16 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> C e. P )
18 1 11 3 4 8 6 hlgrcl1 
 |-  ( ph -> D e. P )
19 18 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> D e. P )
20 8 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> E e. P )
21 1 11 3 4 8 6 hlgrcl2 
 |-  ( ph -> F e. P )
22 21 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> F e. P )
23 simp-6r 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> d e. P )
24 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> f e. P )
25 eqid 
 |-  ( dist ` G ) = ( dist ` G )
26 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
27 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) )
28 27 eqcomd 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> ( B ( dist ` G ) A ) = ( E ( dist ` G ) d ) )
29 1 25 11 12 15 14 20 23 28 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> ( A ( dist ` G ) B ) = ( d ( dist ` G ) E ) )
30 simpr 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) )
31 30 eqcomd 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> ( B ( dist ` G ) C ) = ( E ( dist ` G ) f ) )
32 5 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> A ( K ` B ) C )
33 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> d ( K ` E ) D )
34 simplr 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> f ( K ` E ) F )
35 6 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> D ( K ` E ) F )
36 1 11 3 19 22 20 12 35 hlcomd 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> F ( K ` E ) D )
37 1 11 3 24 22 19 12 20 34 36 hltr 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> f ( K ` E ) D )
38 1 11 3 24 19 20 12 37 hlcomd 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> D ( K ` E ) f )
39 1 11 3 23 19 24 12 20 33 38 hltr 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> d ( K ` E ) f )
40 1 25 3 12 15 20 32 39 31 28 tghlsub 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> ( C ( dist ` G ) A ) = ( f ( dist ` G ) d ) )
41 1 25 26 12 14 15 17 23 20 24 29 31 40 trgcgr 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> <" A B C "> ( cgrG ` G ) <" d E f "> )
42 1 11 3 12 14 15 17 19 20 22 23 24 41 33 34 iscgrad 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> <" A B C "> ( cgrA ` G ) <" D E F "> )
43 10 42 breqdi 
 |-  ( ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ f ( K ` E ) F ) /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) -> <" A B C "> .~ <" D E F "> )
44 43 anasss 
 |-  ( ( ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) /\ f e. P ) /\ ( f ( K ` E ) F /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) ) -> <" A B C "> .~ <" D E F "> )
45 1 11 3 18 21 8 4 6 hlne2 
 |-  ( ph -> F =/= E )
46 1 11 3 13 16 7 4 5 hlne2 
 |-  ( ph -> C =/= B )
47 46 necomd 
 |-  ( ph -> B =/= C )
48 1 11 3 8 7 16 4 21 25 45 47 hlcgrex 
 |-  ( ph -> E. f e. P ( f ( K ` E ) F /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) )
49 48 ad3antrrr 
 |-  ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) -> E. f e. P ( f ( K ` E ) F /\ ( E ( dist ` G ) f ) = ( B ( dist ` G ) C ) ) )
50 44 49 r19.29a 
 |-  ( ( ( ( ph /\ d e. P ) /\ d ( K ` E ) D ) /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) -> <" A B C "> .~ <" D E F "> )
51 50 anasss 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) ) -> <" A B C "> .~ <" D E F "> )
52 1 11 3 18 21 8 4 6 hlne1 
 |-  ( ph -> D =/= E )
53 1 11 3 13 16 7 4 5 hlne1 
 |-  ( ph -> A =/= B )
54 53 necomd 
 |-  ( ph -> B =/= A )
55 1 11 3 8 7 13 4 18 25 52 54 hlcgrex 
 |-  ( ph -> E. d e. P ( d ( K ` E ) D /\ ( E ( dist ` G ) d ) = ( B ( dist ` G ) A ) ) )
56 51 55 r19.29a 
 |-  ( ph -> <" A B C "> .~ <" D E F "> )