# 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 ${⊢}{G}={\mathrm{mulGrp}}_{{R}}$
ringidval.u
Assertion ringidval

### Proof

Step Hyp Ref Expression
1 ringidval.g ${⊢}{G}={\mathrm{mulGrp}}_{{R}}$
2 ringidval.u
3 df-ur ${⊢}{1}_{r}={0}_{𝑔}\circ \mathrm{mulGrp}$
4 3 fveq1i ${⊢}{1}_{{R}}=\left({0}_{𝑔}\circ \mathrm{mulGrp}\right)\left({R}\right)$
5 fnmgp ${⊢}\mathrm{mulGrp}Fn\mathrm{V}$
6 fvco2 ${⊢}\left(\mathrm{mulGrp}Fn\mathrm{V}\wedge {R}\in \mathrm{V}\right)\to \left({0}_{𝑔}\circ \mathrm{mulGrp}\right)\left({R}\right)={0}_{{\mathrm{mulGrp}}_{{R}}}$
7 5 6 mpan ${⊢}{R}\in \mathrm{V}\to \left({0}_{𝑔}\circ \mathrm{mulGrp}\right)\left({R}\right)={0}_{{\mathrm{mulGrp}}_{{R}}}$
8 4 7 syl5eq ${⊢}{R}\in \mathrm{V}\to {1}_{{R}}={0}_{{\mathrm{mulGrp}}_{{R}}}$
9 0g0 ${⊢}\varnothing ={0}_{\varnothing }$
10 fvprc ${⊢}¬{R}\in \mathrm{V}\to {1}_{{R}}=\varnothing$
11 fvprc ${⊢}¬{R}\in \mathrm{V}\to {\mathrm{mulGrp}}_{{R}}=\varnothing$
12 11 fveq2d ${⊢}¬{R}\in \mathrm{V}\to {0}_{{\mathrm{mulGrp}}_{{R}}}={0}_{\varnothing }$
13 9 10 12 3eqtr4a ${⊢}¬{R}\in \mathrm{V}\to {1}_{{R}}={0}_{{\mathrm{mulGrp}}_{{R}}}$
14 8 13 pm2.61i ${⊢}{1}_{{R}}={0}_{{\mathrm{mulGrp}}_{{R}}}$
15 1 fveq2i ${⊢}{0}_{{G}}={0}_{{\mathrm{mulGrp}}_{{R}}}$
16 14 2 15 3eqtr4i