Theorem motcgr3

Description: Property of a motion: distances are preserved, special case of triangles. (Contributed by Thierry Arnoux, 15-Dec-2019)

	Ref	Expression
Hypotheses	motcgr3.p	$$⊢P={\mathrm{Base}}_G$$
	motcgr3.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	motcgr3.r	$$⊢\underset{\dot{}}{\sim }={\sim }_{𝒢}\left(G\right)$$
	motcgr3.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	motcgr3.a	$$⊢\phi \to A\in P$$
	motcgr3.b	$$⊢\phi \to B\in P$$
	motcgr3.c	$$⊢\phi \to C\in P$$
	motcgr3.d	$$⊢\phi \to D=H\left(A\right)$$
	motcgr3.e	$$⊢\phi \to E=H\left(B\right)$$
	motcgr3.f	$$⊢\phi \to F=H\left(C\right)$$
	motcgr3.h	$$⊢\phi \to H\in \left(GIsmtG\right)$$
Assertion	motcgr3	$$⊢\phi \to ⟨“ABC”⟩\underset{\dot{}}{\sim }⟨“DEF”⟩$$

Proof

Step	Hyp	Ref	Expression
1		motcgr3.p	$$⊢P={\mathrm{Base}}_G$$
2		motcgr3.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		motcgr3.r	$$⊢\underset{\dot{}}{\sim }={\sim }_{𝒢}\left(G\right)$$
4		motcgr3.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		motcgr3.a	$$⊢\phi \to A\in P$$
6		motcgr3.b	$$⊢\phi \to B\in P$$
7		motcgr3.c	$$⊢\phi \to C\in P$$
8		motcgr3.d	$$⊢\phi \to D=H\left(A\right)$$
9		motcgr3.e	$$⊢\phi \to E=H\left(B\right)$$
10		motcgr3.f	$$⊢\phi \to F=H\left(C\right)$$
11		motcgr3.h	$$⊢\phi \to H\in \left(GIsmtG\right)$$
12	1 2 4 11 5	motcl	$$⊢\phi \to H\left(A\right)\in P$$
13	8 12	eqeltrd	$$⊢\phi \to D\in P$$
14	1 2 4 11 6	motcl	$$⊢\phi \to H\left(B\right)\in P$$
15	9 14	eqeltrd	$$⊢\phi \to E\in P$$
16	1 2 4 11 7	motcl	$$⊢\phi \to H\left(C\right)\in P$$
17	10 16	eqeltrd	$$⊢\phi \to F\in P$$
18	8 9	oveq12d	$$⊢\phi \to D\underset{\dot{}}{-}E=H\left(A\right)\underset{\dot{}}{-}H\left(B\right)$$
19	1 2 4 5 6 11	motcgr	$$⊢\phi \to H\left(A\right)\underset{\dot{}}{-}H\left(B\right)=A\underset{\dot{}}{-}B$$
20	18 19	eqtr2d	$$⊢\phi \to A\underset{\dot{}}{-}B=D\underset{\dot{}}{-}E$$
21	9 10	oveq12d	$$⊢\phi \to E\underset{\dot{}}{-}F=H\left(B\right)\underset{\dot{}}{-}H\left(C\right)$$
22	1 2 4 6 7 11	motcgr	$$⊢\phi \to H\left(B\right)\underset{\dot{}}{-}H\left(C\right)=B\underset{\dot{}}{-}C$$
23	21 22	eqtr2d	$$⊢\phi \to B\underset{\dot{}}{-}C=E\underset{\dot{}}{-}F$$
24	10 8	oveq12d	$$⊢\phi \to F\underset{\dot{}}{-}D=H\left(C\right)\underset{\dot{}}{-}H\left(A\right)$$
25	1 2 4 7 5 11	motcgr	$$⊢\phi \to H\left(C\right)\underset{\dot{}}{-}H\left(A\right)=C\underset{\dot{}}{-}A$$
26	24 25	eqtr2d	$$⊢\phi \to C\underset{\dot{}}{-}A=F\underset{\dot{}}{-}D$$
27	1 2 3 4 5 6 7 13 15 17 20 23 26	trgcgr	$$⊢\phi \to ⟨“ABC”⟩\underset{\dot{}}{\sim }⟨“DEF”⟩$$