This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to A = subringAlg (W) (S)$
		srasubrg.u	$⊢ φ \to U \in SubRing (W)$
		srasubrg.s	$⊢ φ \to S \subseteq {Base}_{W}$
	Assertion	srasubrg	$⊢ φ \to U \in SubRing (A)$

Proof

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