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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tgmircgrg.m	⊢ − = ( dist ‘ 𝐺 )
	tgmircgrg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tgmircgrg.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tgmircgrg.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tgmircgrg.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	tgmircgrg.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	tgmircgrg.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	tgmircgrg.ncol	⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
Assertion	tgmircgra	⊢ ( 𝜑 → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ”⟩ )

Proof

Step	Hyp	Ref	Expression
1		tgmircgrg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tgmircgrg.m	⊢ − = ( dist ‘ 𝐺 )
3		tgmircgrg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		tgmircgrg.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		tgmircgrg.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6		tgmircgrg.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7		tgmircgrg.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8		tgmircgrg.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9		tgmircgrg.ncol	⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
10		eqid	⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
11		eqid	⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
12	1 4 3 5 7 8 6 9	ncoltgdim2	⊢ ( 𝜑 → 𝐺 Dim_TarskiG≥ 2 )
13	1 2 3 5 12 6 8	midcl	⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ 𝑃 )
14		eqid	⊢ ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) = ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) )
15	1 2 3 4 11 5 13 14 7	mircl	⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ 𝑃 )
16	1 3 4 5 7 8 6 9	tgbcne	⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
17	1 3 4 5 7 8 6 9	tgacne	⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
18	17	necomd	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
19	1 2 3 4 5 6 7 8 9	tgmircgrg	⊢ ( 𝜑 → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐶 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ”⟩ )
20	1 3 5 10 8 6 7 6 8 15 16 18 19	cgrcgra	⊢ ( 𝜑 → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ”⟩ )

Metamath Proof Explorer

Theorem tgmircgra

Proof