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 ( 𝜑𝐵 = ( Base ‘ 𝐾 ) )
rngidpropd.2 ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
rngidpropd.3 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( .r𝐿 ) 𝑦 ) )
Assertion rngidpropd ( 𝜑 → ( 1r𝐾 ) = ( 1r𝐿 ) )

Proof

Step Hyp Ref Expression
1 rngidpropd.1 ( 𝜑𝐵 = ( Base ‘ 𝐾 ) )
2 rngidpropd.2 ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
3 rngidpropd.3 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( .r𝐿 ) 𝑦 ) )
4 eqid ( mulGrp ‘ 𝐾 ) = ( mulGrp ‘ 𝐾 )
5 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6 4 5 mgpbas ( Base ‘ 𝐾 ) = ( Base ‘ ( mulGrp ‘ 𝐾 ) )
7 1 6 eqtrdi ( 𝜑𝐵 = ( Base ‘ ( mulGrp ‘ 𝐾 ) ) )
8 eqid ( mulGrp ‘ 𝐿 ) = ( mulGrp ‘ 𝐿 )
9 eqid ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
10 8 9 mgpbas ( Base ‘ 𝐿 ) = ( Base ‘ ( mulGrp ‘ 𝐿 ) )
11 2 10 eqtrdi ( 𝜑𝐵 = ( Base ‘ ( mulGrp ‘ 𝐿 ) ) )
12 eqid ( .r𝐾 ) = ( .r𝐾 )
13 4 12 mgpplusg ( .r𝐾 ) = ( +g ‘ ( mulGrp ‘ 𝐾 ) )
14 13 oveqi ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 )
15 eqid ( .r𝐿 ) = ( .r𝐿 )
16 8 15 mgpplusg ( .r𝐿 ) = ( +g ‘ ( mulGrp ‘ 𝐿 ) )
17 16 oveqi ( 𝑥 ( .r𝐿 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝐿 ) ) 𝑦 )
18 3 14 17 3eqtr3g ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝐿 ) ) 𝑦 ) )
19 7 11 18 grpidpropd ( 𝜑 → ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) = ( 0g ‘ ( mulGrp ‘ 𝐿 ) ) )
20 eqid ( 1r𝐾 ) = ( 1r𝐾 )
21 4 20 ringidval ( 1r𝐾 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) )
22 eqid ( 1r𝐿 ) = ( 1r𝐿 )
23 8 22 ringidval ( 1r𝐿 ) = ( 0g ‘ ( mulGrp ‘ 𝐿 ) )
24 19 21 23 3eqtr4g ( 𝜑 → ( 1r𝐾 ) = ( 1r𝐿 ) )