mirrag

Description: Right angle is conserved by point inversion. (Contributed by Thierry Arnoux, 3-Nov-2019)

	Ref	Expression
Hypotheses	israg.p	$⊢ P = {Base}_{G}$
	israg.d	$⊢ \underset{˙}{-} = dist (G)$
	israg.i	$⊢ I = Itv (G)$
	israg.l	$⊢ L = {Line}_{𝒢} (G)$
	israg.s	$⊢ S = {pInv}_{𝒢} (G)$
	israg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	israg.a	$⊢ φ \to A \in P$
	israg.b	$⊢ φ \to B \in P$
	israg.c	$⊢ φ \to C \in P$
	ragmir.1	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
	mirrag.m	$⊢ M = S (D)$
	mirrag.d	$⊢ φ \to D \in P$
Assertion	mirrag	$⊢ φ \to ⟨“ M (A) M (B) M (C) ”⟩ \in ∟_{𝒢} (G)$

Proof

Step	Hyp	Ref	Expression
1		israg.p	$⊢ P = {Base}_{G}$
2		israg.d	$⊢ \underset{˙}{-} = dist (G)$
3		israg.i	$⊢ I = Itv (G)$
4		israg.l	$⊢ L = {Line}_{𝒢} (G)$
5		israg.s	$⊢ S = {pInv}_{𝒢} (G)$
6		israg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
7		israg.a	$⊢ φ \to A \in P$
8		israg.b	$⊢ φ \to B \in P$
9		israg.c	$⊢ φ \to C \in P$
10		ragmir.1	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
11		mirrag.m	$⊢ M = S (D)$
12		mirrag.d	$⊢ φ \to D \in P$
13		eqid	$⊢ S (B) = S (B)$
14	1 2 3 4 5 6 8 13 9	mircl	$⊢ φ \to S (B) (C) \in P$
15	1 2 3 4 5 6 7 8 9	israg	$⊢ φ \to (⟨“ A B C ”⟩ \in ∟_{𝒢} (G) \leftrightarrow A \underset{˙}{-} C = A \underset{˙}{-} S (B) (C))$
16	10 15	mpbid	$⊢ φ \to A \underset{˙}{-} C = A \underset{˙}{-} S (B) (C)$
17	1 2 3 4 5 6 12 11 7 9 7 14 16	mircgrs	$⊢ φ \to M (A) \underset{˙}{-} M (C) = M (A) \underset{˙}{-} M (S (B) (C))$
18	1 2 3 4 5 6 12 11 9 8	mirmir2	$⊢ φ \to M (S (B) (C)) = S (M (B)) (M (C))$
19	18	oveq2d	$⊢ φ \to M (A) \underset{˙}{-} M (S (B) (C)) = M (A) \underset{˙}{-} S (M (B)) (M (C))$
20	17 19	eqtrd	$⊢ φ \to M (A) \underset{˙}{-} M (C) = M (A) \underset{˙}{-} S (M (B)) (M (C))$
21	1 2 3 4 5 6 12 11 7	mircl	$⊢ φ \to M (A) \in P$
22	1 2 3 4 5 6 12 11 8	mircl	$⊢ φ \to M (B) \in P$
23	1 2 3 4 5 6 12 11 9	mircl	$⊢ φ \to M (C) \in P$
24	1 2 3 4 5 6 21 22 23	israg	$⊢ φ \to (⟨“ M (A) M (B) M (C) ”⟩ \in ∟_{𝒢} (G) \leftrightarrow M (A) \underset{˙}{-} M (C) = M (A) \underset{˙}{-} S (M (B)) (M (C)))$
25	20 24	mpbird	$⊢ φ \to ⟨“ M (A) M (B) M (C) ”⟩ \in ∟_{𝒢} (G)$

Metamath Proof Explorer

Theorem mirrag

Proof