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	⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
	srasubrg.u	⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝑊 ) )
	srasubrg.s	⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
Assertion	srasubrg	⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		srasubrg.a	⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
2		srasubrg.u	⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝑊 ) )
3		srasubrg.s	⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
4		eqidd	⊢ ( 𝜑 → ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) )
5	1 3	srabase	⊢ ( 𝜑 → ( Base ‘ 𝑊 ) = ( Base ‘ 𝐴 ) )
6	1 3	sraaddg	⊢ ( 𝜑 → ( +g ‘ 𝑊 ) = ( +g ‘ 𝐴 ) )
7	6	oveqdr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) )
8	1 3	sramulr	⊢ ( 𝜑 → ( .r ‘ 𝑊 ) = ( .r ‘ 𝐴 ) )
9	8	oveqdr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) )
10	4 5 7 9	subrgpropd	⊢ ( 𝜑 → ( SubRing ‘ 𝑊 ) = ( SubRing ‘ 𝐴 ) )
11	2 10	eleqtrd	⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝐴 ) )