Metamath Proof Explorer

Theorem ragmir

Description: Right angle property is preserved by point inversion. Theorem 8.4 of Schwabhauser p. 58. (Contributed by Thierry Arnoux, 25-Aug-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)$
	Assertion	ragmir	$⊢ φ \to ⟨“ A B S (B) (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		eqid	$⊢ S (B) = S (B)$
12	1 2 3 4 5 6 8 11 9	mirmir	$⊢ φ \to S (B) (S (B) (C)) = C$
13	12	oveq2d	$⊢ φ \to A \underset{˙}{-} S (B) (S (B) (C)) = A \underset{˙}{-} C$
14	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))$
15	10 14	mpbid	$⊢ φ \to A \underset{˙}{-} C = A \underset{˙}{-} S (B) (C)$
16	13 15	eqtr2d	$⊢ φ \to A \underset{˙}{-} S (B) (C) = A \underset{˙}{-} S (B) (S (B) (C))$
17	1 2 3 4 5 6 8 11 9	mircl	$⊢ φ \to S (B) (C) \in P$
18	1 2 3 4 5 6 7 8 17	israg	$⊢ φ \to (⟨“ A B S (B) (C) ”⟩ \in ∟_{𝒢} (G) \leftrightarrow A \underset{˙}{-} S (B) (C) = A \underset{˙}{-} S (B) (S (B) (C)))$
19	16 18	mpbird	$⊢ φ \to ⟨“ A B S (B) (C) ”⟩ \in ∟_{𝒢} (G)$