# Metamath Proof Explorer

## Theorem rngidpropd

Description: The ring identity depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014)

Ref Expression
Hypotheses rngidpropd.1 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{K}}$
rngidpropd.2 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{L}}$
rngidpropd.3 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{\cdot }_{{K}}{y}={x}{\cdot }_{{L}}{y}$
Assertion rngidpropd ${⊢}{\phi }\to {1}_{{K}}={1}_{{L}}$

### Proof

Step Hyp Ref Expression
1 rngidpropd.1 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{K}}$
2 rngidpropd.2 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{L}}$
3 rngidpropd.3 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{\cdot }_{{K}}{y}={x}{\cdot }_{{L}}{y}$
4 eqid ${⊢}{\mathrm{mulGrp}}_{{K}}={\mathrm{mulGrp}}_{{K}}$
5 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
6 4 5 mgpbas ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{K}}}$
7 1 6 syl6eq ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{K}}}$
8 eqid ${⊢}{\mathrm{mulGrp}}_{{L}}={\mathrm{mulGrp}}_{{L}}$
9 eqid ${⊢}{\mathrm{Base}}_{{L}}={\mathrm{Base}}_{{L}}$
10 8 9 mgpbas ${⊢}{\mathrm{Base}}_{{L}}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{L}}}$
11 2 10 syl6eq ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{L}}}$
12 eqid ${⊢}{\cdot }_{{K}}={\cdot }_{{K}}$
13 4 12 mgpplusg ${⊢}{\cdot }_{{K}}={+}_{{\mathrm{mulGrp}}_{{K}}}$
14 13 oveqi ${⊢}{x}{\cdot }_{{K}}{y}={x}{+}_{{\mathrm{mulGrp}}_{{K}}}{y}$
15 eqid ${⊢}{\cdot }_{{L}}={\cdot }_{{L}}$
16 8 15 mgpplusg ${⊢}{\cdot }_{{L}}={+}_{{\mathrm{mulGrp}}_{{L}}}$
17 16 oveqi ${⊢}{x}{\cdot }_{{L}}{y}={x}{+}_{{\mathrm{mulGrp}}_{{L}}}{y}$
18 3 14 17 3eqtr3g ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{+}_{{\mathrm{mulGrp}}_{{K}}}{y}={x}{+}_{{\mathrm{mulGrp}}_{{L}}}{y}$
19 7 11 18 grpidpropd ${⊢}{\phi }\to {0}_{{\mathrm{mulGrp}}_{{K}}}={0}_{{\mathrm{mulGrp}}_{{L}}}$
20 eqid ${⊢}{1}_{{K}}={1}_{{K}}$
21 4 20 ringidval ${⊢}{1}_{{K}}={0}_{{\mathrm{mulGrp}}_{{K}}}$
22 eqid ${⊢}{1}_{{L}}={1}_{{L}}$
23 8 22 ringidval ${⊢}{1}_{{L}}={0}_{{\mathrm{mulGrp}}_{{L}}}$
24 19 21 23 3eqtr4g ${⊢}{\phi }\to {1}_{{K}}={1}_{{L}}$