Metamath Proof Explorer


Theorem motrag

Description: Right angles are preserved by motions. (Contributed by Thierry Arnoux, 16-Dec-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
motrag.f φ F G Ismt G
motrag.1 φ ⟨“ ABC ”⟩ 𝒢 G
Assertion motrag φ ⟨“ F A F B F 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 motrag.f φ F G Ismt G
11 motrag.1 φ ⟨“ ABC ”⟩ 𝒢 G
12 eqid 𝒢 G = 𝒢 G
13 1 2 6 10 7 motcl φ F A P
14 1 2 6 10 8 motcl φ F B P
15 1 2 6 10 9 motcl φ F C P
16 eqidd φ F A = F A
17 eqidd φ F B = F B
18 eqidd φ F C = F C
19 1 2 12 6 7 8 9 16 17 18 10 motcgr3 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ F A F B F C ”⟩
20 1 2 3 4 5 6 7 8 9 12 13 14 15 11 19 ragcgr φ ⟨“ F A F B F C ”⟩ 𝒢 G