This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )