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	\|- ( 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 ) )