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	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_L$$
	ringprop.p	$$⊢{+}_K={+}_L$$
	ringprop.m	$$⊢{\cdot }_K={\cdot }_L$$
Assertion	ringprop	$$⊢K\in \mathrm{Ring}\leftrightarrow L\in \mathrm{Ring}$$

Proof

Step	Hyp	Ref	Expression
1		ringprop.b	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_L$$
2		ringprop.p	$$⊢{+}_K={+}_L$$
3		ringprop.m	$$⊢{\cdot }_K={\cdot }_L$$
4		eqidd	$$⊢\top \to {\mathrm{Base}}_K={\mathrm{Base}}_K$$
5	1	a1i	$$⊢\top \to {\mathrm{Base}}_K={\mathrm{Base}}_L$$
6	2	oveqi	$$⊢x{+}_{K}y=x{+}_{L}y$$
7	6	a1i	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_K\wedge y\in {\mathrm{Base}}_K\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
8	3	oveqi	$$⊢x{\cdot }_{K}y=x{\cdot }_{L}y$$
9	8	a1i	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_K\wedge y\in {\mathrm{Base}}_K\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
10	4 5 7 9	ringpropd	$$⊢\top \to \left(K\in \mathrm{Ring}\leftrightarrow L\in \mathrm{Ring}\right)$$
11	10	mptru	$$⊢K\in \mathrm{Ring}\leftrightarrow L\in \mathrm{Ring}$$