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 = ( LineG ` G )
	israg.s	|- S = ( pInvG ` G )
	israg.g	|- ( ph -> G e. TarskiG )
	israg.a	|- ( ph -> A e. P )
	israg.b	|- ( ph -> B e. P )
	israg.c	|- ( ph -> C e. P )
	motrag.f	|- ( ph -> F e. ( G Ismt G ) )
	motrag.1	|- ( ph -> <" A B C "> e. ( raG ` G ) )
Assertion	motrag	|- ( ph -> <" ( F ` A ) ( F ` B ) ( F ` C ) "> e. ( raG ` 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 = ( LineG ` G )
5		israg.s	|- S = ( pInvG ` G )
6		israg.g	|- ( ph -> G e. TarskiG )
7		israg.a	|- ( ph -> A e. P )
8		israg.b	|- ( ph -> B e. P )
9		israg.c	|- ( ph -> C e. P )
10		motrag.f	|- ( ph -> F e. ( G Ismt G ) )
11		motrag.1	|- ( ph -> <" A B C "> e. ( raG ` G ) )
12		eqid	|- ( cgrG ` G ) = ( cgrG ` G )
13	1 2 6 10 7	motcl	|- ( ph -> ( F ` A ) e. P )
14	1 2 6 10 8	motcl	|- ( ph -> ( F ` B ) e. P )
15	1 2 6 10 9	motcl	|- ( ph -> ( F ` C ) e. P )
16		eqidd	|- ( ph -> ( F ` A ) = ( F ` A ) )
17		eqidd	|- ( ph -> ( F ` B ) = ( F ` B ) )
18		eqidd	|- ( ph -> ( F ` C ) = ( F ` C ) )
19	1 2 12 6 7 8 9 16 17 18 10	motcgr3	|- ( ph -> <" A B C "> ( cgrG ` G ) <" ( F ` A ) ( F ` B ) ( F ` C ) "> )
20	1 2 3 4 5 6 7 8 9 12 13 14 15 11 19	ragcgr	|- ( ph -> <" ( F ` A ) ( F ` B ) ( F ` C ) "> e. ( raG ` G ) )