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

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 )