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 ` K ) = ( Base ` L )
	ringprop.p	|- ( +g ` K ) = ( +g ` L )
	ringprop.m	|- ( .r ` K ) = ( .r ` L )
Assertion	ringprop	|- ( K e. Ring <-> L e. Ring )

Proof

Step	Hyp	Ref	Expression
1		ringprop.b	|- ( Base ` K ) = ( Base ` L )
2		ringprop.p	|- ( +g ` K ) = ( +g ` L )
3		ringprop.m	|- ( .r ` K ) = ( .r ` L )
4		eqidd	|- ( T. -> ( Base ` K ) = ( Base ` K ) )
5	1	a1i	|- ( T. -> ( Base ` K ) = ( Base ` L ) )
6	2	oveqi	|- ( x ( +g ` K ) y ) = ( x ( +g ` L ) y )
7	6	a1i	|- ( ( T. /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
8	3	oveqi	|- ( x ( .r ` K ) y ) = ( x ( .r ` L ) y )
9	8	a1i	|- ( ( T. /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
10	4 5 7 9	ringpropd	|- ( T. -> ( K e. Ring <-> L e. Ring ) )
11	10	mptru	|- ( K e. Ring <-> L e. Ring )