Theorem srasubrg

Description: A subring of the original structure is also a subring of the constructed subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023)

	Ref	Expression
Hypotheses	srasubrg.a	$$⊢\phi \to A=\mathrm{subringAlg}\left(W\right)\left(S\right)$$
	srasubrg.u	$$⊢\phi \to U\in \mathrm{SubRing}\left(W\right)$$
	srasubrg.s	$$⊢\phi \to S\subseteq {\mathrm{Base}}_W$$
Assertion	srasubrg	$$⊢\phi \to U\in \mathrm{SubRing}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		srasubrg.a	$$⊢\phi \to A=\mathrm{subringAlg}\left(W\right)\left(S\right)$$
2		srasubrg.u	$$⊢\phi \to U\in \mathrm{SubRing}\left(W\right)$$
3		srasubrg.s	$$⊢\phi \to S\subseteq {\mathrm{Base}}_W$$
4		eqidd	$$⊢\phi \to {\mathrm{Base}}_W={\mathrm{Base}}_W$$
5	1 3	srabase	$$⊢\phi \to {\mathrm{Base}}_W={\mathrm{Base}}_A$$
6	1 3	sraaddg	$$⊢\phi \to {+}_W={+}_A$$
7	6	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_W\wedge y\in {\mathrm{Base}}_W\right)\right)\to x{+}_{W}y=x{+}_{A}y$$
8	1 3	sramulr	$$⊢\phi \to {\cdot }_W={\cdot }_A$$
9	8	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_W\wedge y\in {\mathrm{Base}}_W\right)\right)\to x{\cdot }_{W}y=x{\cdot }_{A}y$$
10	4 5 7 9	subrgpropd	$$⊢\phi \to \mathrm{SubRing}\left(W\right)=\mathrm{SubRing}\left(A\right)$$
11	2 10	eleqtrd	$$⊢\phi \to U\in \mathrm{SubRing}\left(A\right)$$