gidval

Description: The value of the identity element of a group. (Contributed by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	gidval.1	$⊢ X = ran G$
	Assertion	gidval	$⊢ G \in V \to GId (G) = (ι u \in X \| \forall x \in X (u G x = x \land x G u = x))$

Step	Hyp	Ref	Expression
1		gidval.1	$⊢ X = ran G$
2		elex	$⊢ G \in V \to G \in V$
3		rneq	$⊢ g = G \to ran g = ran G$
4	3 1	eqtr4di	$⊢ g = G \to ran g = X$
5		oveq	$⊢ g = G \to u g x = u G x$
6	5	eqeq1d	$⊢ g = G \to (u g x = x \leftrightarrow u G x = x)$
7		oveq	$⊢ g = G \to x g u = x G u$
8	7	eqeq1d	$⊢ g = G \to (x g u = x \leftrightarrow x G u = x)$
9	6 8	anbi12d	$⊢ g = G \to ((u g x = x \land x g u = x) \leftrightarrow (u G x = x \land x G u = x))$
10	4 9	raleqbidv	$⊢ g = G \to (\forall x \in ran g (u g x = x \land x g u = x) \leftrightarrow \forall x \in X (u G x = x \land x G u = x))$
11	4 10	riotaeqbidv	$⊢ g = G \to (ι u \in ran g \| \forall x \in ran g (u g x = x \land x g u = x)) = (ι u \in X \| \forall x \in X (u G x = x \land x G u = x))$
12		df-gid	$⊢ GId = (g \in V ⟼ (ι u \in ran g \| \forall x \in ran g (u g x = x \land x g u = x)))$
13		riotaex	$⊢ (ι u \in X \| \forall x \in X (u G x = x \land x G u = x)) \in V$
14	11 12 13	fvmpt	$⊢ G \in V \to GId (G) = (ι u \in X \| \forall x \in X (u G x = x \land x G u = x))$
15	2 14	syl	$⊢ G \in V \to GId (G) = (ι u \in X \| \forall x \in X (u G x = x \land x G u = x))$

Metamath Proof Explorer