tgmircgra

Description: The angle congruence the exterior-angle theorem opens with: the interior angle at A in triangle C A B is congruent to the angle at C in the midpoint-reflected triangle. This is cgrcgra over tgmircgrg ; the vertex distinctnesses come from the non-collinearity via tgbcne and tgacne . (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	tgmircgrg.p	$⊢ P = {Base}_{G}$
	tgmircgrg.m	$⊢ \underset{˙}{-} = dist (G)$
	tgmircgrg.i	$⊢ I = Itv (G)$
	tgmircgrg.l	$⊢ L = {Line}_{𝒢} (G)$
	tgmircgrg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgmircgrg.a	$⊢ φ \to A \in P$
	tgmircgrg.b	$⊢ φ \to B \in P$
	tgmircgrg.c	$⊢ φ \to C \in P$
	tgmircgrg.ncol	$⊢ φ \to \neg (A \in (B L C) \lor B = C)$
Assertion	tgmircgra	$⊢ φ \to ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) C) (B) ”⟩$

Proof

Step	Hyp	Ref	Expression
1		tgmircgrg.p	$⊢ P = {Base}_{G}$
2		tgmircgrg.m	$⊢ \underset{˙}{-} = dist (G)$
3		tgmircgrg.i	$⊢ I = Itv (G)$
4		tgmircgrg.l	$⊢ L = {Line}_{𝒢} (G)$
5		tgmircgrg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		tgmircgrg.a	$⊢ φ \to A \in P$
7		tgmircgrg.b	$⊢ φ \to B \in P$
8		tgmircgrg.c	$⊢ φ \to C \in P$
9		tgmircgrg.ncol	$⊢ φ \to \neg (A \in (B L C) \lor B = C)$
10		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
11		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
12	1 4 3 5 7 8 6 9	ncoltgdim2	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
13	1 2 3 5 12 6 8	midcl	$⊢ φ \to A {mid}_{𝒢} (G) C \in P$
14		eqid	$⊢ {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) C) = {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) C)$
15	1 2 3 4 11 5 13 14 7	mircl	$⊢ φ \to {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) C) (B) \in P$
16	1 3 4 5 7 8 6 9	tgbcne	$⊢ φ \to C \neq A$
17	1 3 4 5 7 8 6 9	tgacne	$⊢ φ \to B \neq A$
18	17	necomd	$⊢ φ \to A \neq B$
19	1 2 3 4 5 6 7 8 9	tgmircgrg	$⊢ φ \to ⟨“ C A B ”⟩ \sim_{𝒢} (G) ⟨“ A C {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) C) (B) ”⟩$
20	1 3 5 10 8 6 7 6 8 15 16 18 19	cgrcgra	$⊢ φ \to ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) C) (B) ”⟩$

Metamath Proof Explorer

Theorem tgmircgra

Proof