Metamath Proof Explorer

Theorem cgrahlb

Description: Two null angles are congruent: if A and C lie on one half-line from B , and D and F on one half-line from E , then angle <" A B C "> is congruent to <" D E F "> . This is GeoCoq l11__21__b ; set.mm has only the converse, cgrahl (GeoCoq l11__21__a ). Proved by copying both arms onto the target rays with hlcgrex and closing the third side by segment subtraction ( tgcgrsub2 ), so it needs no non-collinear frame. (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses cgrahlb.p 
|- P = ( Base ` G )
cgrahlb.i 
|- I = ( Itv ` G )
cgrahlb.k 
|- K = ( hlG ` G )
cgrahlb.m 
|- .- = ( dist ` G )
cgrahlb.g 
|- ( ph -> G e. TarskiG )
cgrahlb.a 
|- ( ph -> A e. P )
cgrahlb.b 
|- ( ph -> B e. P )
cgrahlb.c 
|- ( ph -> C e. P )
cgrahlb.d 
|- ( ph -> D e. P )
cgrahlb.e 
|- ( ph -> E e. P )
cgrahlb.f 
|- ( ph -> F e. P )
cgrahlb.1 
|- ( ph -> A ( K ` B ) C )
cgrahlb.2 
|- ( ph -> D ( K ` E ) F )
Assertion cgrahlb 
|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )

Proof

Step Hyp Ref Expression
1 cgrahlb.p 
 |-  P = ( Base ` G )
2 cgrahlb.i 
 |-  I = ( Itv ` G )
3 cgrahlb.k 
 |-  K = ( hlG ` G )
4 cgrahlb.m 
 |-  .- = ( dist ` G )
5 cgrahlb.g 
 |-  ( ph -> G e. TarskiG )
6 cgrahlb.a 
 |-  ( ph -> A e. P )
7 cgrahlb.b 
 |-  ( ph -> B e. P )
8 cgrahlb.c 
 |-  ( ph -> C e. P )
9 cgrahlb.d 
 |-  ( ph -> D e. P )
10 cgrahlb.e 
 |-  ( ph -> E e. P )
11 cgrahlb.f 
 |-  ( ph -> F e. P )
12 cgrahlb.1 
 |-  ( ph -> A ( K ` B ) C )
13 cgrahlb.2 
 |-  ( ph -> D ( K ` E ) F )
14 simplll 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> ph )
15 14 5 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> G e. TarskiG )
16 14 6 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> A e. P )
17 14 7 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> B e. P )
18 14 8 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> C e. P )
19 14 9 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> D e. P )
20 14 10 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> E e. P )
21 14 11 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> F e. P )
22 simpllr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> x e. P )
23 simplr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> y e. P )
24 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
25 simpr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) )
26 25 simpld 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) )
27 26 simprd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( E .- x ) = ( B .- A ) )
28 27 eqcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( B .- A ) = ( E .- x ) )
29 1 4 2 15 17 16 20 22 28 tgcgrcomlr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( A .- B ) = ( x .- E ) )
30 25 simprd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) )
31 30 simprd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( E .- y ) = ( B .- C ) )
32 31 eqcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( B .- C ) = ( E .- y ) )
33 eqid 
 |-  ( leG ` G ) = ( leG ` G )
34 14 12 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> A ( K ` B ) C )
35 1 2 3 16 18 17 15 ishlg 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( A ( K ` B ) C <-> ( A =/= B /\ C =/= B /\ ( A e. ( B I C ) \/ C e. ( B I A ) ) ) ) )
36 34 35 mpbid 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( A =/= B /\ C =/= B /\ ( A e. ( B I C ) \/ C e. ( B I A ) ) ) )
37 36 simp3d 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( A e. ( B I C ) \/ C e. ( B I A ) ) )
38 26 simpld 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> x ( K ` E ) D )
39 14 13 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> D ( K ` E ) F )
40 1 2 3 22 19 21 15 20 38 39 hltr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> x ( K ` E ) F )
41 30 simpld 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> y ( K ` E ) F )
42 1 2 3 23 21 20 15 41 hlcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> F ( K ` E ) y )
43 1 2 3 22 21 23 15 20 40 42 hltr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> x ( K ` E ) y )
44 1 2 3 22 23 20 15 ishlg 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( x ( K ` E ) y <-> ( x =/= E /\ y =/= E /\ ( x e. ( E I y ) \/ y e. ( E I x ) ) ) ) )
45 43 44 mpbid 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( x =/= E /\ y =/= E /\ ( x e. ( E I y ) \/ y e. ( E I x ) ) ) )
46 45 simp3d 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( x e. ( E I y ) \/ y e. ( E I x ) ) )
47 1 4 2 33 15 17 16 18 20 20 22 23 37 46 28 32 tgcgrsub2 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( A .- C ) = ( x .- y ) )
48 1 4 2 15 16 18 22 23 47 tgcgrcomlr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( C .- A ) = ( y .- x ) )
49 1 4 24 15 16 17 18 22 20 23 29 32 48 trgcgr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> <" A B C "> ( cgrG ` G ) <" x E y "> )
50 1 2 3 15 16 17 18 19 20 21 22 23 49 38 41 iscgrad 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) ) -> <" A B C "> ( cgrA ` G ) <" D E F "> )
51 1 2 3 9 11 10 5 13 hlne1 
 |-  ( ph -> D =/= E )
52 1 2 3 6 8 7 5 12 hlne1 
 |-  ( ph -> A =/= B )
53 52 necomd 
 |-  ( ph -> B =/= A )
54 1 2 3 10 7 6 5 9 4 51 53 hlcgrex 
 |-  ( ph -> E. x e. P ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) )
55 1 2 3 9 11 10 5 13 hlne2 
 |-  ( ph -> F =/= E )
56 1 2 3 6 8 7 5 12 hlne2 
 |-  ( ph -> C =/= B )
57 56 necomd 
 |-  ( ph -> B =/= C )
58 1 2 3 10 7 8 5 11 4 55 57 hlcgrex 
 |-  ( ph -> E. y e. P ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) )
59 54 58 jca 
 |-  ( ph -> ( E. x e. P ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ E. y e. P ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) )
60 reeanv 
 |-  ( E. x e. P E. y e. P ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) <-> ( E. x e. P ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ E. y e. P ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) )
61 59 60 sylibr 
 |-  ( ph -> E. x e. P E. y e. P ( ( x ( K ` E ) D /\ ( E .- x ) = ( B .- A ) ) /\ ( y ( K ` E ) F /\ ( E .- y ) = ( B .- C ) ) ) )
62 50 61 r19.29vva 
 |-  ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )