Theorem sraring

Description: Condition for a subring algebra to be a ring. (Contributed by Thierry Arnoux, 24-Jul-2023)

	Ref	Expression
Hypotheses	sraring.1	$$⊢A=\mathrm{subringAlg}\left(R\right)\left(V\right)$$
	sraring.2	$$⊢B={\mathrm{Base}}_R$$
Assertion	sraring	$$⊢\left(R\in \mathrm{Ring}\wedge V\subseteq B\right)\to A\in \mathrm{Ring}$$

Proof

Step	Hyp	Ref	Expression
1		sraring.1	$$⊢A=\mathrm{subringAlg}\left(R\right)\left(V\right)$$
2		sraring.2	$$⊢B={\mathrm{Base}}_R$$
3	2	a1i	$$⊢V\subseteq B\to B={\mathrm{Base}}_R$$
4	1	a1i	$$⊢V\subseteq B\to A=\mathrm{subringAlg}\left(R\right)\left(V\right)$$
5		id	$$⊢V\subseteq B\to V\subseteq B$$
6	5 2	sseqtrdi	$$⊢V\subseteq B\to V\subseteq {\mathrm{Base}}_R$$
7	4 6	srabase	$$⊢V\subseteq B\to {\mathrm{Base}}_R={\mathrm{Base}}_A$$
8	2 7	syl5eq	$$⊢V\subseteq B\to B={\mathrm{Base}}_A$$
9	4 6	sraaddg	$$⊢V\subseteq B\to {+}_R={+}_A$$
10	9	oveqdr	$$⊢\left(V\subseteq B\wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{R}y=x{+}_{A}y$$
11	4 6	sramulr	$$⊢V\subseteq B\to {\cdot }_R={\cdot }_A$$
12	11	oveqdr	$$⊢\left(V\subseteq B\wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{R}y=x{\cdot }_{A}y$$
13	3 8 10 12	ringpropd	$$⊢V\subseteq B\to \left(R\in \mathrm{Ring}\leftrightarrow A\in \mathrm{Ring}\right)$$
14	13	biimpac	$$⊢\left(R\in \mathrm{Ring}\wedge V\subseteq B\right)\to A\in \mathrm{Ring}$$