Theorem motrag

Description: Right angles are preserved by motions. (Contributed by Thierry Arnoux, 16-Dec-2019)

	Ref	Expression
Hypotheses	israg.p	$$⊢P={\mathrm{Base}}_G$$
	israg.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	israg.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	israg.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	israg.s	$$⊢S={pInv}_{𝒢}\left(G\right)$$
	israg.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	israg.a	$$⊢\phi \to A\in P$$
	israg.b	$$⊢\phi \to B\in P$$
	israg.c	$$⊢\phi \to C\in P$$
	motrag.f	$$⊢\phi \to F\in \left(GIsmtG\right)$$
	motrag.1	$$⊢\phi \to ⟨“ABC”⟩\in {∟}_{𝒢}\left(G\right)$$
Assertion	motrag	$$⊢\phi \to ⟨“F\left(A\right)F\left(B\right)F\left(C\right)”⟩\in {∟}_{𝒢}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		israg.p	$$⊢P={\mathrm{Base}}_G$$
2		israg.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		israg.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		israg.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
5		israg.s	$$⊢S={pInv}_{𝒢}\left(G\right)$$
6		israg.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
7		israg.a	$$⊢\phi \to A\in P$$
8		israg.b	$$⊢\phi \to B\in P$$
9		israg.c	$$⊢\phi \to C\in P$$
10		motrag.f	$$⊢\phi \to F\in \left(GIsmtG\right)$$
11		motrag.1	$$⊢\phi \to ⟨“ABC”⟩\in {∟}_{𝒢}\left(G\right)$$
12		eqid	$$⊢{\sim }_{𝒢}\left(G\right)={\sim }_{𝒢}\left(G\right)$$
13	1 2 6 10 7	motcl	$$⊢\phi \to F\left(A\right)\in P$$
14	1 2 6 10 8	motcl	$$⊢\phi \to F\left(B\right)\in P$$
15	1 2 6 10 9	motcl	$$⊢\phi \to F\left(C\right)\in P$$
16		eqidd	$$⊢\phi \to F\left(A\right)=F\left(A\right)$$
17		eqidd	$$⊢\phi \to F\left(B\right)=F\left(B\right)$$
18		eqidd	$$⊢\phi \to F\left(C\right)=F\left(C\right)$$
19	1 2 12 6 7 8 9 16 17 18 10	motcgr3	$$⊢\phi \to ⟨“ABC”⟩{\sim }_{𝒢}\left(G\right)⟨“F\left(A\right)F\left(B\right)F\left(C\right)”⟩$$
20	1 2 3 4 5 6 7 8 9 12 13 14 15 11 19	ragcgr	$$⊢\phi \to ⟨“F\left(A\right)F\left(B\right)F\left(C\right)”⟩\in {∟}_{𝒢}\left(G\right)$$