idmot

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

Step	Hyp	Ref	Expression
1		ismot.p	$⊢ P = {Base}_{G}$
2		ismot.m	$⊢ \underset{˙}{-} = dist (G)$
3		motgrp.1	$⊢ φ \to G \in V$
4		f1oi	$⊢ ({I ↾}_{P}) : P \underset{1-1 onto}{⟶} P$
5	4	a1i	$⊢ φ \to ({I ↾}_{P}) : P \underset{1-1 onto}{⟶} P$
6		fvresi	$⊢ a \in P \to ({I ↾}_{P}) (a) = a$
7	6	ad2antrl	$⊢ (φ \land (a \in P \land b \in P)) \to ({I ↾}_{P}) (a) = a$
8		fvresi	$⊢ b \in P \to ({I ↾}_{P}) (b) = b$
9	8	ad2antll	$⊢ (φ \land (a \in P \land b \in P)) \to ({I ↾}_{P}) (b) = b$
10	7 9	oveq12d	$⊢ (φ \land (a \in P \land b \in P)) \to ({I ↾}_{P}) (a) \underset{˙}{-} ({I ↾}_{P}) (b) = a \underset{˙}{-} b$
11	10	ralrimivva	$⊢ φ \to \forall a \in P \forall b \in P ({I ↾}_{P}) (a) \underset{˙}{-} ({I ↾}_{P}) (b) = a \underset{˙}{-} b$
12	1 2	ismot	$⊢ G \in V \to ({I ↾}_{P} \in (G Ismt G) \leftrightarrow (({I ↾}_{P}) : P \underset{1-1 onto}{⟶} P \land \forall a \in P \forall b \in P ({I ↾}_{P}) (a) \underset{˙}{-} ({I ↾}_{P}) (b) = a \underset{˙}{-} b))$
13	12	biimpar	$⊢ (G \in V \land (({I ↾}_{P}) : P \underset{1-1 onto}{⟶} P \land \forall a \in P \forall b \in P ({I ↾}_{P}) (a) \underset{˙}{-} ({I ↾}_{P}) (b) = a \underset{˙}{-} b)) \to {I ↾}_{P} \in (G Ismt G)$
14	3 5 11 13	syl12anc	$⊢ φ \to {I ↾}_{P} \in (G Ismt G)$

Metamath Proof Explorer