Theorem subrg1asclcl

Description: The scalars in a polynomial algebra are in the subring algebra iff the scalar value is in the subring. (Contributed by Mario Carneiro, 4-Jul-2015)

	Ref	Expression
Hypotheses	subrg1ascl.p	|- P = ( Poly1 ` R )
	subrg1ascl.a	|- A = ( algSc ` P )
	subrg1ascl.h	|- H = ( R |`s T )
	subrg1ascl.u	|- U = ( Poly1 ` H )
	subrg1ascl.r	|- ( ph -> T e. ( SubRing ` R ) )
	subrg1asclcl.b	|- B = ( Base ` U )
	subrg1asclcl.k	|- K = ( Base ` R )
	subrg1asclcl.x	|- ( ph -> X e. K )
Assertion	subrg1asclcl	|- ( ph -> ( ( A ` X ) e. B <-> X e. T ) )

Proof

Step	Hyp	Ref	Expression
1		subrg1ascl.p	|- P = ( Poly1 ` R )
2		subrg1ascl.a	|- A = ( algSc ` P )
3		subrg1ascl.h	|- H = ( R |`s T )
4		subrg1ascl.u	|- U = ( Poly1 ` H )
5		subrg1ascl.r	|- ( ph -> T e. ( SubRing ` R ) )
6		subrg1asclcl.b	|- B = ( Base ` U )
7		subrg1asclcl.k	|- K = ( Base ` R )
8		subrg1asclcl.x	|- ( ph -> X e. K )
9		eqid	|- ( 1o mPoly R ) = ( 1o mPoly R )
10	1 2	ply1ascl	|- A = ( algSc ` ( 1o mPoly R ) )
11		eqid	|- ( 1o mPoly H ) = ( 1o mPoly H )
12		1on	|- 1o e. On
13	12	a1i	|- ( ph -> 1o e. On )
14		eqid	|- ( PwSer1 ` H ) = ( PwSer1 ` H )
15	4 14 6	ply1bas	|- B = ( Base ` ( 1o mPoly H ) )
16	9 10 3 11 13 5 15 7 8	subrgasclcl	|- ( ph -> ( ( A ` X ) e. B <-> X e. T ) )