mirmid

Description: Point inversion preserves midpoints. (Contributed by Thierry Arnoux, 12-Dec-2019)

	Ref	Expression
Hypotheses	ismid.p	$⊢ P = {Base}_{G}$
	ismid.d	$⊢ \underset{˙}{-} = dist (G)$
	ismid.i	$⊢ I = Itv (G)$
	ismid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	ismid.1	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
	midcl.1	$⊢ φ \to A \in P$
	midcl.2	$⊢ φ \to B \in P$
	mirmid.s	$⊢ S = {pInv}_{𝒢} (G) (M)$
	mirmid.x	$⊢ φ \to M \in P$
Assertion	mirmid	$⊢ φ \to S (A) {mid}_{𝒢} (G) S (B) = S (A {mid}_{𝒢} (G) B)$

Proof

Step	Hyp	Ref	Expression
1		ismid.p	$⊢ P = {Base}_{G}$
2		ismid.d	$⊢ \underset{˙}{-} = dist (G)$
3		ismid.i	$⊢ I = Itv (G)$
4		ismid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		ismid.1	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
6		midcl.1	$⊢ φ \to A \in P$
7		midcl.2	$⊢ φ \to B \in P$
8		mirmid.s	$⊢ S = {pInv}_{𝒢} (G) (M)$
9		mirmid.x	$⊢ φ \to M \in P$
10		eqidd	$⊢ φ \to A {mid}_{𝒢} (G) B = A {mid}_{𝒢} (G) B$
11		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
12	1 2 3 4 5 6 7	midcl	$⊢ φ \to A {mid}_{𝒢} (G) B \in P$
13	1 2 3 4 5 6 7 11 12	ismidb	$⊢ φ \to (B = {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) B) (A) \leftrightarrow A {mid}_{𝒢} (G) B = A {mid}_{𝒢} (G) B)$
14	10 13	mpbird	$⊢ φ \to B = {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) B) (A)$
15	14	fveq2d	$⊢ φ \to S (B) = S ({pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) B) (A))$
16		eqid	$⊢ {Line}_{𝒢} (G) = {Line}_{𝒢} (G)$
17	1 2 3 16 11 4 9 8 6 12	mirmir2	$⊢ φ \to S ({pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) B) (A)) = {pInv}_{𝒢} (G) (S (A {mid}_{𝒢} (G) B)) (S (A))$
18	15 17	eqtrd	$⊢ φ \to S (B) = {pInv}_{𝒢} (G) (S (A {mid}_{𝒢} (G) B)) (S (A))$
19	1 2 3 16 11 4 9 8 6	mircl	$⊢ φ \to S (A) \in P$
20	1 2 3 16 11 4 9 8 7	mircl	$⊢ φ \to S (B) \in P$
21	1 2 3 16 11 4 9 8 12	mircl	$⊢ φ \to S (A {mid}_{𝒢} (G) B) \in P$
22	1 2 3 4 5 19 20 11 21	ismidb	$⊢ φ \to (S (B) = {pInv}_{𝒢} (G) (S (A {mid}_{𝒢} (G) B)) (S (A)) \leftrightarrow S (A) {mid}_{𝒢} (G) S (B) = S (A {mid}_{𝒢} (G) B))$
23	18 22	mpbid	$⊢ φ \to S (A) {mid}_{𝒢} (G) S (B) = S (A {mid}_{𝒢} (G) B)$

Metamath Proof Explorer

Theorem mirmid

Proof