Metamath Proof Explorer

Theorem ringidval

Description: The value of the unity element of a ring. (Contributed by NM, 27-Aug-2011) (Revised by Mario Carneiro, 27-Dec-2014)

Ref Expression
Hypotheses ringidval.g ⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
ringidval.u ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion ringidval 1 = ( 0g ‘ 𝐺 )

Proof

Step Hyp Ref Expression
1 ringidval.g ⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
2 ringidval.u ⊢ 1 = ( 1r ‘ 𝑅 )
3 df-ur ⊢ 1r = ( 0g ∘ mulGrp )
4 3 fveq1i ⊢ ( 1r ‘ 𝑅 ) = ( ( 0g ∘ mulGrp ) ‘ 𝑅 )
5 fnmgp ⊢ mulGrp Fn V
6 fvco2 ⊢ ( ( mulGrp Fn V ∧ 𝑅 ∈ V ) → ( ( 0g ∘ mulGrp ) ‘ 𝑅 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) )
7 5 6 mpan ⊢ ( 𝑅 ∈ V → ( ( 0g ∘ mulGrp ) ‘ 𝑅 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) )
8 4 7 syl5eq ⊢ ( 𝑅 ∈ V → ( 1r ‘ 𝑅 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) )
9 0g0 ⊢ ∅ = ( 0g ‘ ∅ )
10 fvprc ⊢ ( ¬ 𝑅 ∈ V → ( 1r ‘ 𝑅 ) = ∅ )
11 fvprc ⊢ ( ¬ 𝑅 ∈ V → ( mulGrp ‘ 𝑅 ) = ∅ )
12 11 fveq2d ⊢ ( ¬ 𝑅 ∈ V → ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) = ( 0g ‘ ∅ ) )
13 9 10 12 3eqtr4a ⊢ ( ¬ 𝑅 ∈ V → ( 1r ‘ 𝑅 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) )
14 8 13 pm2.61i ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
15 1 fveq2i ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
16 14 2 15 3eqtr4i ⊢ 1 = ( 0g ‘ 𝐺 )