Theorem idmot

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

	Ref	Expression
Hypotheses	ismot.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	ismot.m	⊢ − = ( dist ‘ 𝐺 )
	motgrp.1	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
Assertion	idmot	⊢ ( 𝜑 → ( I ↾ 𝑃 ) ∈ ( 𝐺 Ismt 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		ismot.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		ismot.m	⊢ − = ( dist ‘ 𝐺 )
3		motgrp.1	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
4		f1oi	⊢ ( I ↾ 𝑃 ) : 𝑃 –1-1-onto→ 𝑃
5	4	a1i	⊢ ( 𝜑 → ( I ↾ 𝑃 ) : 𝑃 –1-1-onto→ 𝑃 )
6		fvresi	⊢ ( 𝑎 ∈ 𝑃 → ( ( I ↾ 𝑃 ) ‘ 𝑎 ) = 𝑎 )
7	6	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ( I ↾ 𝑃 ) ‘ 𝑎 ) = 𝑎 )
8		fvresi	⊢ ( 𝑏 ∈ 𝑃 → ( ( I ↾ 𝑃 ) ‘ 𝑏 ) = 𝑏 )
9	8	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ( I ↾ 𝑃 ) ‘ 𝑏 ) = 𝑏 )
10	7 9	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ( ( I ↾ 𝑃 ) ‘ 𝑎 ) − ( ( I ↾ 𝑃 ) ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) )
11	10	ralrimivva	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( ( I ↾ 𝑃 ) ‘ 𝑎 ) − ( ( I ↾ 𝑃 ) ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) )
12	1 2	ismot	⊢ ( 𝐺 ∈ 𝑉 → ( ( I ↾ 𝑃 ) ∈ ( 𝐺 Ismt 𝐺 ) ↔ ( ( I ↾ 𝑃 ) : 𝑃 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( ( I ↾ 𝑃 ) ‘ 𝑎 ) − ( ( I ↾ 𝑃 ) ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) ) ) )
13	12	biimpar	⊢ ( ( 𝐺 ∈ 𝑉 ∧ ( ( I ↾ 𝑃 ) : 𝑃 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( ( I ↾ 𝑃 ) ‘ 𝑎 ) − ( ( I ↾ 𝑃 ) ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) ) ) → ( I ↾ 𝑃 ) ∈ ( 𝐺 Ismt 𝐺 ) )
14	3 5 11 13	syl12anc	⊢ ( 𝜑 → ( I ↾ 𝑃 ) ∈ ( 𝐺 Ismt 𝐺 ) )