tgmircgrg

Description: Reflecting B through the midpoint of A and C carries triangle C A B onto A C P , where P is the reflected point. The dimension condition the mid* family carries is discharged from the non-collinearity through ncoltgdim2 , not taken as a hypothesis. (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	tgmircgrg	⊢ ( 𝜑 → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐶 ( ( ( 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	⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
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		eqidd	⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = ( 𝐴 − 𝐶 ) )
17	1 2 3 5 6 8 6 8 16	tgcgrcoml	⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝐴 − 𝐶 ) )
18		eqidd	⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) )
19	1 2 3 5 12 6 8 11 13	ismidb	⊢ ( 𝜑 → ( 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐴 ) ↔ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) )
20	18 19	mpbird	⊢ ( 𝜑 → 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐴 ) )
21	20	oveq1d	⊢ ( 𝜑 → ( 𝐶 − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) = ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐴 ) − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) )
22	1 2 3 4 11 5 13 14 6 7	miriso	⊢ ( 𝜑 → ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐴 ) − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) = ( 𝐴 − 𝐵 ) )
23	21 22	eqtrd	⊢ ( 𝜑 → ( 𝐶 − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) = ( 𝐴 − 𝐵 ) )
24	23	eqcomd	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐶 − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) )
25	1 2 3 4 11 5 13 14 7 8	miriso	⊢ ( 𝜑 → ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐶 ) ) = ( 𝐵 − 𝐶 ) )
26	20	fveq2d	⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐴 ) ) )
27	1 2 3 4 11 5 13 14 6	mirmir	⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐴 ) ) = 𝐴 )
28	26 27	eqtrd	⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐶 ) = 𝐴 )
29	28	oveq2d	⊢ ( 𝜑 → ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐶 ) ) = ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) − 𝐴 ) )
30	25 29	eqtr3d	⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) − 𝐴 ) )
31	1 2 10 5 8 6 7 6 8 15 17 24 30	trgcgr	⊢ ( 𝜑 → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐶 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ”⟩ )

Metamath Proof Explorer

Theorem tgmircgrg

Proof