Theorem subrgmvrf

Description: The variables in a polynomial algebra are contained in every subring algebra. (Contributed by Mario Carneiro, 4-Jul-2015)

	Ref	Expression
Hypotheses	subrgmvr.v	|- V = ( I mVar R )
	subrgmvr.i	|- ( ph -> I e. W )
	subrgmvr.r	|- ( ph -> T e. ( SubRing ` R ) )
	subrgmvr.h	|- H = ( R |`s T )
	subrgmvrf.u	|- U = ( I mPoly H )
	subrgmvrf.b	|- B = ( Base ` U )
Assertion	subrgmvrf	|- ( ph -> V : I --> B )

Proof

Step	Hyp	Ref	Expression
1		subrgmvr.v	|- V = ( I mVar R )
2		subrgmvr.i	|- ( ph -> I e. W )
3		subrgmvr.r	|- ( ph -> T e. ( SubRing ` R ) )
4		subrgmvr.h	|- H = ( R |`s T )
5		subrgmvrf.u	|- U = ( I mPoly H )
6		subrgmvrf.b	|- B = ( Base ` U )
7		eqid	|- ( I mPwSer R ) = ( I mPwSer R )
8		eqid	|- ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
9		subrgrcl	|- ( T e. ( SubRing ` R ) -> R e. Ring )
10	3 9	syl	|- ( ph -> R e. Ring )
11	7 1 8 2 10	mvrf	|- ( ph -> V : I --> ( Base ` ( I mPwSer R ) ) )
12	11	ffnd	|- ( ph -> V Fn I )
13	1 2 3 4	subrgmvr	|- ( ph -> V = ( I mVar H ) )
14	13	fveq1d	|- ( ph -> ( V ` x ) = ( ( I mVar H ) ` x ) )
15	14	adantr	|- ( ( ph /\ x e. I ) -> ( V ` x ) = ( ( I mVar H ) ` x ) )
16		eqid	|- ( I mVar H ) = ( I mVar H )
17	2	adantr	|- ( ( ph /\ x e. I ) -> I e. W )
18	4	subrgring	|- ( T e. ( SubRing ` R ) -> H e. Ring )
19	3 18	syl	|- ( ph -> H e. Ring )
20	19	adantr	|- ( ( ph /\ x e. I ) -> H e. Ring )
21		simpr	|- ( ( ph /\ x e. I ) -> x e. I )
22	5 16 6 17 20 21	mvrcl	|- ( ( ph /\ x e. I ) -> ( ( I mVar H ) ` x ) e. B )
23	15 22	eqeltrd	|- ( ( ph /\ x e. I ) -> ( V ` x ) e. B )
24	23	ralrimiva	|- ( ph -> A. x e. I ( V ` x ) e. B )
25		ffnfv	|- ( V : I --> B <-> ( V Fn I /\ A. x e. I ( V ` x ) e. B ) )
26	12 24 25	sylanbrc	|- ( ph -> V : I --> B )