cgrcgra

Description: Triangle congruence implies angle congruence. This is a portion of CPCTC, focusing on a specific angle. (Contributed by Arnoux, 2-Aug-2020)

	Ref	Expression
Hypotheses	cgraid.p	$⊢ P = {Base}_{G}$
	cgraid.i	$⊢ I = Itv (G)$
	cgraid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	cgraid.k	$⊢ K = {hl}_{𝒢} (G)$
	cgraid.a	$⊢ φ \to A \in P$
	cgraid.b	$⊢ φ \to B \in P$
	cgraid.c	$⊢ φ \to C \in P$
	cgracom.d	$⊢ φ \to D \in P$
	cgracom.e	$⊢ φ \to E \in P$
	cgracom.f	$⊢ φ \to F \in P$
	cgrcgra.1	$⊢ φ \to A \neq B$
	cgrcgra.2	$⊢ φ \to B \neq C$
	cgrcgra.3	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E F ”⟩$
Assertion	cgrcgra	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$

Proof

Step	Hyp	Ref	Expression
1		cgraid.p	$⊢ P = {Base}_{G}$
2		cgraid.i	$⊢ I = Itv (G)$
3		cgraid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
4		cgraid.k	$⊢ K = {hl}_{𝒢} (G)$
5		cgraid.a	$⊢ φ \to A \in P$
6		cgraid.b	$⊢ φ \to B \in P$
7		cgraid.c	$⊢ φ \to C \in P$
8		cgracom.d	$⊢ φ \to D \in P$
9		cgracom.e	$⊢ φ \to E \in P$
10		cgracom.f	$⊢ φ \to F \in P$
11		cgrcgra.1	$⊢ φ \to A \neq B$
12		cgrcgra.2	$⊢ φ \to B \neq C$
13		cgrcgra.3	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E F ”⟩$
14		eqid	$⊢ dist (G) = dist (G)$
15		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
16	1 14 2 15 3 5 6 7 8 9 10 13	cgr3simp1	$⊢ φ \to A dist (G) B = D dist (G) E$
17	1 14 2 3 5 6 8 9 16 11	tgcgrneq	$⊢ φ \to D \neq E$
18	1 2 4 8 5 9 3 17	hlid	$⊢ φ \to D K (E) D$
19	1 14 2 15 3 5 6 7 8 9 10 13	cgr3simp2	$⊢ φ \to B dist (G) C = E dist (G) F$
20	1 14 2 3 6 7 9 10 19	tgcgrcomlr	$⊢ φ \to C dist (G) B = F dist (G) E$
21	12	necomd	$⊢ φ \to C \neq B$
22	1 14 2 3 7 6 10 9 20 21	tgcgrneq	$⊢ φ \to F \neq E$
23	1 2 4 10 5 9 3 22	hlid	$⊢ φ \to F K (E) F$
24	1 2 4 3 5 6 7 8 9 10 8 10 13 18 23	iscgrad	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$

Metamath Proof Explorer

Theorem cgrcgra

Proof