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 )