Metamath Proof Explorer

Theorem 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 ∈ V → GId ⁡ G = ι u ∈ X | ∀ x ∈ X u G x = x ∧ x G u = x

Proof

Step Hyp Ref Expression
1 gidval.1 ⊢ X = ran ⁡ G
2 elex ⊢ G ∈ V → G ∈ V
3 rneq ⊢ g = G → ran ⁡ g = ran ⁡ G
4 3 1 eqtr4di ⊢ g = G → ran ⁡ g = X
5 oveq ⊢ g = G → u g x = u G x
6 5 eqeq1d ⊢ g = G → u g x = x ↔ u G x = x
7 oveq ⊢ g = G → x g u = x G u
8 7 eqeq1d ⊢ g = G → x g u = x ↔ x G u = x
9 6 8 anbi12d ⊢ g = G → u g x = x ∧ x g u = x ↔ u G x = x ∧ x G u = x
10 4 9 raleqbidv ⊢ g = G → ∀ x ∈ ran ⁡ g u g x = x ∧ x g u = x ↔ ∀ x ∈ X u G x = x ∧ x G u = x
11 4 10 riotaeqbidv ⊢ g = G → ι u ∈ ran ⁡ g | ∀ x ∈ ran ⁡ g u g x = x ∧ x g u = x = ι u ∈ X | ∀ x ∈ X u G x = x ∧ x G u = x
12 df-gid ⊢ GId = g ∈ V ⟼ ι u ∈ ran ⁡ g | ∀ x ∈ ran ⁡ g u g x = x ∧ x g u = x
13 riotaex ⊢ ι u ∈ X | ∀ x ∈ X u G x = x ∧ x G u = x ∈ V
14 11 12 13 fvmpt ⊢ G ∈ V → GId ⁡ G = ι u ∈ X | ∀ x ∈ X u G x = x ∧ x G u = x
15 2 14 syl ⊢ G ∈ V → GId ⁡ G = ι u ∈ X | ∀ x ∈ X u G x = x ∧ x G u = x