Theorem idmot

Description: The identity is a motion. (Contributed by Thierry Arnoux, 15-Dec-2019)

	Ref	Expression
Hypotheses	ismot.p	|- P = ( Base ` G )
	ismot.m	|- .- = ( dist ` G )
	motgrp.1	|- ( ph -> G e. V )
Assertion	idmot	|- ( ph -> ( _I |` P ) e. ( G Ismt G ) )

Proof

Step	Hyp	Ref	Expression
1		ismot.p	|- P = ( Base ` G )
2		ismot.m	|- .- = ( dist ` G )
3		motgrp.1	|- ( ph -> G e. V )
4		f1oi	|- ( _I |` P ) : P -1-1-onto-> P
5	4	a1i	|- ( ph -> ( _I |` P ) : P -1-1-onto-> P )
6		fvresi	|- ( a e. P -> ( ( _I |` P ) ` a ) = a )
7	6	ad2antrl	|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( _I |` P ) ` a ) = a )
8		fvresi	|- ( b e. P -> ( ( _I |` P ) ` b ) = b )
9	8	ad2antll	|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( _I |` P ) ` b ) = b )
10	7 9	oveq12d	|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( ( _I |` P ) ` a ) .- ( ( _I |` P ) ` b ) ) = ( a .- b ) )
11	10	ralrimivva	|- ( ph -> A. a e. P A. b e. P ( ( ( _I |` P ) ` a ) .- ( ( _I |` P ) ` b ) ) = ( a .- b ) )
12	1 2	ismot	|- ( G e. V -> ( ( _I |` P ) e. ( G Ismt G ) <-> ( ( _I |` P ) : P -1-1-onto-> P /\ A. a e. P A. b e. P ( ( ( _I |` P ) ` a ) .- ( ( _I |` P ) ` b ) ) = ( a .- b ) ) ) )
13	12	biimpar	|- ( ( G e. V /\ ( ( _I |` P ) : P -1-1-onto-> P /\ A. a e. P A. b e. P ( ( ( _I |` P ) ` a ) .- ( ( _I |` P ) ` b ) ) = ( a .- b ) ) ) -> ( _I |` P ) e. ( G Ismt G ) )
14	3 5 11 13	syl12anc	|- ( ph -> ( _I |` P ) e. ( G Ismt G ) )