Metamath Proof Explorer


Theorem ringprop

Description: If two structures have the same ring components (properties), one is a ring iff the other one is. (Contributed by Mario Carneiro, 11-Oct-2013)

Ref Expression
Hypotheses ringprop.b ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 )
ringprop.p ( +g𝐾 ) = ( +g𝐿 )
ringprop.m ( .r𝐾 ) = ( .r𝐿 )
Assertion ringprop ( 𝐾 ∈ Ring ↔ 𝐿 ∈ Ring )

Proof

Step Hyp Ref Expression
1 ringprop.b ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 )
2 ringprop.p ( +g𝐾 ) = ( +g𝐿 )
3 ringprop.m ( .r𝐾 ) = ( .r𝐿 )
4 eqidd ( ⊤ → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) )
5 1 a1i ( ⊤ → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
6 2 oveqi ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 )
7 6 a1i ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
8 3 oveqi ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( .r𝐿 ) 𝑦 )
9 8 a1i ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( .r𝐿 ) 𝑦 ) )
10 4 5 7 9 ringpropd ( ⊤ → ( 𝐾 ∈ Ring ↔ 𝐿 ∈ Ring ) )
11 10 mptru ( 𝐾 ∈ Ring ↔ 𝐿 ∈ Ring )