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	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
	zerocgra.k	$⊢ K = {hl}_{𝒢} (G)$
	zerocgra.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	zerocgra.1	$⊢ φ \to A K (B) C$
	zerocgra.2	$⊢ φ \to D K (E) F$
	zerocgra.b	$⊢ φ \to B \in P$
	zerocgra.e	$⊢ φ \to E \in P$
Assertion	zerocgra	$⊢ φ \to ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D E F ”⟩$

Proof

Step	Hyp	Ref	Expression
1		zerocgra.p	$⊢ P = {Base}_{G}$
2		zerocgra.a	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
3		zerocgra.k	$⊢ K = {hl}_{𝒢} (G)$
4		zerocgra.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		zerocgra.1	$⊢ φ \to A K (B) C$
6		zerocgra.2	$⊢ φ \to D K (E) F$
7		zerocgra.b	$⊢ φ \to B \in P$
8		zerocgra.e	$⊢ φ \to E \in P$
9	2	eqcomi	$⊢ \sim_{𝒢}^{∠} (G) = \underset{˙}{\sim}$
10	9	a1i	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to \sim_{𝒢}^{∠} (G) = \underset{˙}{\sim}$
11		eqid	$⊢ Itv (G) = Itv (G)$
12	4	ad6antr	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to G \in 𝒢_{Tarski}$
13	1 11 3 4 7 5	hlgrcl1	$⊢ φ \to A \in P$
14	13	ad6antr	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to A \in P$
15	7	ad6antr	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to B \in P$
16	1 11 3 4 7 5	hlgrcl2	$⊢ φ \to C \in P$
17	16	ad6antr	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to C \in P$
18	1 11 3 4 8 6	hlgrcl1	$⊢ φ \to D \in P$
19	18	ad6antr	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to D \in P$
20	8	ad6antr	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to E \in P$
21	1 11 3 4 8 6	hlgrcl2	$⊢ φ \to F \in P$
22	21	ad6antr	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to F \in P$
23		simp-6r	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to d \in P$
24		simpllr	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to f \in P$
25		eqid	$⊢ dist (G) = dist (G)$
26		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
27		simp-4r	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to E dist (G) d = B dist (G) A$
28	27	eqcomd	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to B dist (G) A = E dist (G) d$
29	1 25 11 12 15 14 20 23 28	tgcgrcomlr	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to A dist (G) B = d dist (G) E$
30		simpr	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to E dist (G) f = B dist (G) C$
31	30	eqcomd	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to B dist (G) C = E dist (G) f$
32	5	ad6antr	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to A K (B) C$
33		simp-5r	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to d K (E) D$
34		simplr	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to f K (E) F$
35	6	ad6antr	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to D K (E) F$
36	1 11 3 19 22 20 12 35	hlcomd	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to F K (E) D$
37	1 11 3 24 22 19 12 20 34 36	hltr	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to f K (E) D$
38	1 11 3 24 19 20 12 37	hlcomd	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to D K (E) f$
39	1 11 3 23 19 24 12 20 33 38	hltr	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to d K (E) f$
40	1 25 3 12 15 20 32 39 31 28	tghlsub	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to C dist (G) A = f dist (G) d$
41	1 25 26 12 14 15 17 23 20 24 29 31 40	trgcgr	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E f ”⟩$
42	1 11 3 12 14 15 17 19 20 22 23 24 41 33 34	iscgrad	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
43	10 42	breqdi	$⊢ ((((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land f K (E) F) \land E dist (G) f = B dist (G) C) \to ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D E F ”⟩$
44	43	anasss	$⊢ (((((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \land f \in P) \land (f K (E) F \land E dist (G) f = B dist (G) C)) \to ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D E F ”⟩$
45	1 11 3 18 21 8 4 6	hlne2	$⊢ φ \to F \neq E$
46	1 11 3 13 16 7 4 5	hlne2	$⊢ φ \to C \neq B$
47	46	necomd	$⊢ φ \to B \neq C$
48	1 11 3 8 7 16 4 21 25 45 47	hlcgrex	$⊢ φ \to \exists f \in P (f K (E) F \land E dist (G) f = B dist (G) C)$
49	48	ad3antrrr	$⊢ (((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \to \exists f \in P (f K (E) F \land E dist (G) f = B dist (G) C)$
50	44 49	r19.29a	$⊢ (((φ \land d \in P) \land d K (E) D) \land E dist (G) d = B dist (G) A) \to ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D E F ”⟩$
51	50	anasss	$⊢ ((φ \land d \in P) \land (d K (E) D \land E dist (G) d = B dist (G) A)) \to ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D E F ”⟩$
52	1 11 3 18 21 8 4 6	hlne1	$⊢ φ \to D \neq E$
53	1 11 3 13 16 7 4 5	hlne1	$⊢ φ \to A \neq B$
54	53	necomd	$⊢ φ \to B \neq A$
55	1 11 3 8 7 13 4 18 25 52 54	hlcgrex	$⊢ φ \to \exists d \in P (d K (E) D \land E dist (G) d = B dist (G) A)$
56	51 55	r19.29a	$⊢ φ \to ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D E F ”⟩$

Metamath Proof Explorer

Theorem zerocgra

Proof