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	|- ( ph -> A = ( ( subringAlg ` W ) ` S ) )
	srasubrg.u	|- ( ph -> U e. ( SubRing ` W ) )
	srasubrg.s	|- ( ph -> S C_ ( Base ` W ) )
Assertion	srasubrg	|- ( ph -> U e. ( SubRing ` A ) )

Proof

Step	Hyp	Ref	Expression
1		srasubrg.a	|- ( ph -> A = ( ( subringAlg ` W ) ` S ) )
2		srasubrg.u	|- ( ph -> U e. ( SubRing ` W ) )
3		srasubrg.s	|- ( ph -> S C_ ( Base ` W ) )
4		eqidd	|- ( ph -> ( Base ` W ) = ( Base ` W ) )
5	1 3	srabase	|- ( ph -> ( Base ` W ) = ( Base ` A ) )
6	1 3	sraaddg	|- ( ph -> ( +g ` W ) = ( +g ` A ) )
7	6	oveqdr	|- ( ( ph /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( x ( +g ` W ) y ) = ( x ( +g ` A ) y ) )
8	1 3	sramulr	|- ( ph -> ( .r ` W ) = ( .r ` A ) )
9	8	oveqdr	|- ( ( ph /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( x ( .r ` W ) y ) = ( x ( .r ` A ) y ) )
10	4 5 7 9	subrgpropd	|- ( ph -> ( SubRing ` W ) = ( SubRing ` A ) )
11	2 10	eleqtrd	|- ( ph -> U e. ( SubRing ` A ) )