This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ran 𝐺
Assertion gidval ( 𝐺 ∈ 𝑉 → ( GId ‘ 𝐺 ) = ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 gidval.1 ⊢ 𝑋 = ran 𝐺
2 elex ⊢ ( 𝐺 ∈ 𝑉 → 𝐺 ∈ V )
3 rneq ⊢ ( 𝑔 = 𝐺 → ran 𝑔 = ran 𝐺 )
4 3 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ran 𝑔 = 𝑋 )
5 oveq ⊢ ( 𝑔 = 𝐺 → ( 𝑢 𝑔 𝑥 ) = ( 𝑢 𝐺 𝑥 ) )
6 5 eqeq1d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ↔ ( 𝑢 𝐺 𝑥 ) = 𝑥 ) )
7 oveq ⊢ ( 𝑔 = 𝐺 → ( 𝑥 𝑔 𝑢 ) = ( 𝑥 𝐺 𝑢 ) )
8 7 eqeq1d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑥 𝑔 𝑢 ) = 𝑥 ↔ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) )
9 6 8 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑔 𝑢 ) = 𝑥 ) ↔ ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
10 4 9 raleqbidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑥 ∈ ran 𝑔 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑔 𝑢 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
11 4 10 riotaeqbidv ⊢ ( 𝑔 = 𝐺 → ( ℩ 𝑢 ∈ ran 𝑔 ∀ 𝑥 ∈ ran 𝑔 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑔 𝑢 ) = 𝑥 ) ) = ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
12 df-gid ⊢ GId = ( 𝑔 ∈ V ↦ ( ℩ 𝑢 ∈ ran 𝑔 ∀ 𝑥 ∈ ran 𝑔 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑔 𝑢 ) = 𝑥 ) ) )
13 riotaex ⊢ ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ∈ V
14 11 12 13 fvmpt ⊢ ( 𝐺 ∈ V → ( GId ‘ 𝐺 ) = ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
15 2 14 syl ⊢ ( 𝐺 ∈ 𝑉 → ( GId ‘ 𝐺 ) = ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )