This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rngidpropd

Description: The ring unity 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 ‘ 𝐿 ) )