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 = {hl}_{𝒢} (G)$
	cgrahlb.m	$⊢ \underset{˙}{-} = dist (G)$
	cgrahlb.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	cgrahlb.a	$⊢ φ \to A \in P$
	cgrahlb.b	$⊢ φ \to B \in P$
	cgrahlb.c	$⊢ φ \to C \in P$
	cgrahlb.d	$⊢ φ \to D \in P$
	cgrahlb.e	$⊢ φ \to E \in P$
	cgrahlb.f	$⊢ φ \to F \in P$
	cgrahlb.1	$⊢ φ \to A K (B) C$
	cgrahlb.2	$⊢ φ \to D K (E) F$
Assertion	cgrahlb	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (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 = {hl}_{𝒢} (G)$
4		cgrahlb.m	$⊢ \underset{˙}{-} = dist (G)$
5		cgrahlb.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		cgrahlb.a	$⊢ φ \to A \in P$
7		cgrahlb.b	$⊢ φ \to B \in P$
8		cgrahlb.c	$⊢ φ \to C \in P$
9		cgrahlb.d	$⊢ φ \to D \in P$
10		cgrahlb.e	$⊢ φ \to E \in P$
11		cgrahlb.f	$⊢ φ \to F \in P$
12		cgrahlb.1	$⊢ φ \to A K (B) C$
13		cgrahlb.2	$⊢ φ \to D K (E) F$
14		simplll	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to φ$
15	14 5	syl	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to G \in 𝒢_{Tarski}$
16	14 6	syl	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to A \in P$
17	14 7	syl	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to B \in P$
18	14 8	syl	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to C \in P$
19	14 9	syl	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to D \in P$
20	14 10	syl	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to E \in P$
21	14 11	syl	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to F \in P$
22		simpllr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to x \in P$
23		simplr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to y \in P$
24		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
25		simpr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))$
26	25	simpld	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to (x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A)$
27	26	simprd	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to E \underset{˙}{-} x = B \underset{˙}{-} A$
28	27	eqcomd	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to B \underset{˙}{-} A = E \underset{˙}{-} x$
29	1 4 2 15 17 16 20 22 28	tgcgrcomlr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to A \underset{˙}{-} B = x \underset{˙}{-} E$
30	25	simprd	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C)$
31	30	simprd	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to E \underset{˙}{-} y = B \underset{˙}{-} C$
32	31	eqcomd	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to B \underset{˙}{-} C = E \underset{˙}{-} y$
33		eqid	$⊢ \leq_{𝒢} (G) = \leq_{𝒢} (G)$
34	14 12	syl	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to A K (B) C$
35	1 2 3 16 18 17 15	ishlg	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to (A K (B) C \leftrightarrow (A \neq B \land C \neq B \land (A \in (B I C) \lor C \in (B I A))))$
36	34 35	mpbid	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to (A \neq B \land C \neq B \land (A \in (B I C) \lor C \in (B I A)))$
37	36	simp3d	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to (A \in (B I C) \lor C \in (B I A))$
38	26	simpld	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to x K (E) D$
39	14 13	syl	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to D K (E) F$
40	1 2 3 22 19 21 15 20 38 39	hltr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to x K (E) F$
41	30	simpld	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to y K (E) F$
42	1 2 3 23 21 20 15 41	hlcomd	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to F K (E) y$
43	1 2 3 22 21 23 15 20 40 42	hltr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to x K (E) y$
44	1 2 3 22 23 20 15	ishlg	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to (x K (E) y \leftrightarrow (x \neq E \land y \neq E \land (x \in (E I y) \lor y \in (E I x))))$
45	43 44	mpbid	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to (x \neq E \land y \neq E \land (x \in (E I y) \lor y \in (E I x)))$
46	45	simp3d	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to (x \in (E I y) \lor y \in (E I x))$
47	1 4 2 33 15 17 16 18 20 20 22 23 37 46 28 32	tgcgrsub2	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to A \underset{˙}{-} C = x \underset{˙}{-} y$
48	1 4 2 15 16 18 22 23 47	tgcgrcomlr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to C \underset{˙}{-} A = y \underset{˙}{-} x$
49	1 4 24 15 16 17 18 22 20 23 29 32 48	trgcgr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩$
50	1 2 3 15 16 17 18 19 20 21 22 23 49 38 41	iscgrad	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
51	1 2 3 9 11 10 5 13	hlne1	$⊢ φ \to D \neq E$
52	1 2 3 6 8 7 5 12	hlne1	$⊢ φ \to A \neq B$
53	52	necomd	$⊢ φ \to B \neq A$
54	1 2 3 10 7 6 5 9 4 51 53	hlcgrex	$⊢ φ \to \exists x \in P (x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A)$
55	1 2 3 9 11 10 5 13	hlne2	$⊢ φ \to F \neq E$
56	1 2 3 6 8 7 5 12	hlne2	$⊢ φ \to C \neq B$
57	56	necomd	$⊢ φ \to B \neq C$
58	1 2 3 10 7 8 5 11 4 55 57	hlcgrex	$⊢ φ \to \exists y \in P (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C)$
59	54 58	jca	$⊢ φ \to (\exists x \in P (x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land \exists y \in P (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))$
60		reeanv	$⊢ \exists x \in P \exists y \in P ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C)) \leftrightarrow (\exists x \in P (x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land \exists y \in P (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))$
61	59 60	sylibr	$⊢ φ \to \exists x \in P \exists y \in P ((x K (E) D \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (y K (E) F \land E \underset{˙}{-} y = B \underset{˙}{-} C))$
62	50 61	r19.29vva	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$

Metamath Proof Explorer

Theorem cgrahlb

Proof