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 φ B = Base K
rngidpropd.2 φ B = Base L
rngidpropd.3 φ x B y B x K y = x L y
Assertion rngidpropd φ 1 K = 1 L

Proof

Step Hyp Ref Expression
1 rngidpropd.1 φ B = Base K
2 rngidpropd.2 φ B = Base L
3 rngidpropd.3 φ x B y B x K y = x L y
4 eqid mulGrp K = mulGrp K
5 eqid Base K = Base K
6 4 5 mgpbas Base K = Base mulGrp K
7 1 6 eqtrdi φ B = Base mulGrp K
8 eqid mulGrp L = mulGrp L
9 eqid Base L = Base L
10 8 9 mgpbas Base L = Base mulGrp L
11 2 10 eqtrdi φ B = Base mulGrp L
12 eqid K = K
13 4 12 mgpplusg K = + mulGrp K
14 13 oveqi x K y = x + mulGrp K y
15 eqid L = L
16 8 15 mgpplusg L = + mulGrp L
17 16 oveqi x L y = x + mulGrp L y
18 3 14 17 3eqtr3g φ x B y B x + mulGrp K y = x + mulGrp L y
19 7 11 18 grpidpropd φ 0 mulGrp K = 0 mulGrp L
20 eqid 1 K = 1 K
21 4 20 ringidval 1 K = 0 mulGrp K
22 eqid 1 L = 1 L
23 8 22 ringidval 1 L = 0 mulGrp L
24 19 21 23 3eqtr4g φ 1 K = 1 L