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 - ˙ = dist G
israg.i I = Itv G
israg.l L = Line 𝒢 G
israg.s S = pInv 𝒢 G
israg.g φ G 𝒢 Tarski
israg.a φ A P
israg.b φ B P
israg.c φ C P
ragmir.1 φ ⟨“ ABC ”⟩ 𝒢 G
Assertion ragmir φ ⟨“ AB S B C ”⟩ 𝒢 G

Proof

Step Hyp Ref Expression
1 israg.p P = Base G
2 israg.d - ˙ = dist G
3 israg.i I = Itv G
4 israg.l L = Line 𝒢 G
5 israg.s S = pInv 𝒢 G
6 israg.g φ G 𝒢 Tarski
7 israg.a φ A P
8 israg.b φ B P
9 israg.c φ C P
10 ragmir.1 φ ⟨“ ABC ”⟩ 𝒢 G
11 eqid S B = S B
12 1 2 3 4 5 6 8 11 9 mirmir φ S B S B C = C
13 12 oveq2d φ A - ˙ S B S B C = A - ˙ C
14 1 2 3 4 5 6 7 8 9 israg φ ⟨“ ABC ”⟩ 𝒢 G A - ˙ C = A - ˙ S B C
15 10 14 mpbid φ A - ˙ C = A - ˙ S B C
16 13 15 eqtr2d φ A - ˙ S B C = A - ˙ S B S B C
17 1 2 3 4 5 6 8 11 9 mircl φ S B C P
18 1 2 3 4 5 6 7 8 17 israg φ ⟨“ AB S B C ”⟩ 𝒢 G A - ˙ S B C = A - ˙ S B S B C
19 16 18 mpbird φ ⟨“ AB S B C ”⟩ 𝒢 G