Metamath Proof Explorer


Theorem subrgasclcl

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 subrgascl.p
|- P = ( I mPoly R )
subrgascl.a
|- A = ( algSc ` P )
subrgascl.h
|- H = ( R |`s T )
subrgascl.u
|- U = ( I mPoly H )
subrgascl.i
|- ( ph -> I e. W )
subrgascl.r
|- ( ph -> T e. ( SubRing ` R ) )
subrgasclcl.b
|- B = ( Base ` U )
subrgasclcl.k
|- K = ( Base ` R )
subrgasclcl.x
|- ( ph -> X e. K )
Assertion subrgasclcl
|- ( ph -> ( ( A ` X ) e. B <-> X e. T ) )

Proof

Step Hyp Ref Expression
1 subrgascl.p
 |-  P = ( I mPoly R )
2 subrgascl.a
 |-  A = ( algSc ` P )
3 subrgascl.h
 |-  H = ( R |`s T )
4 subrgascl.u
 |-  U = ( I mPoly H )
5 subrgascl.i
 |-  ( ph -> I e. W )
6 subrgascl.r
 |-  ( ph -> T e. ( SubRing ` R ) )
7 subrgasclcl.b
 |-  B = ( Base ` U )
8 subrgasclcl.k
 |-  K = ( Base ` R )
9 subrgasclcl.x
 |-  ( ph -> X e. K )
10 iftrue
 |-  ( x = ( I X. { 0 } ) -> if ( x = ( I X. { 0 } ) , X , ( 0g ` R ) ) = X )
11 10 eleq1d
 |-  ( x = ( I X. { 0 } ) -> ( if ( x = ( I X. { 0 } ) , X , ( 0g ` R ) ) e. ( Base ` H ) <-> X e. ( Base ` H ) ) )
12 eqid
 |-  ( I mPwSer H ) = ( I mPwSer H )
13 eqid
 |-  ( Base ` H ) = ( Base ` H )
14 eqid
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
15 eqid
 |-  ( Base ` ( I mPwSer H ) ) = ( Base ` ( I mPwSer H ) )
16 eqid
 |-  ( 0g ` R ) = ( 0g ` R )
17 subrgrcl
 |-  ( T e. ( SubRing ` R ) -> R e. Ring )
18 6 17 syl
 |-  ( ph -> R e. Ring )
19 1 14 16 8 2 5 18 9 mplascl
 |-  ( ph -> ( A ` X ) = ( x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( x = ( I X. { 0 } ) , X , ( 0g ` R ) ) ) )
20 19 adantr
 |-  ( ( ph /\ ( A ` X ) e. B ) -> ( A ` X ) = ( x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( x = ( I X. { 0 } ) , X , ( 0g ` R ) ) ) )
21 3 subrgring
 |-  ( T e. ( SubRing ` R ) -> H e. Ring )
22 6 21 syl
 |-  ( ph -> H e. Ring )
23 12 4 7 5 22 mplsubrg
 |-  ( ph -> B e. ( SubRing ` ( I mPwSer H ) ) )
24 15 subrgss
 |-  ( B e. ( SubRing ` ( I mPwSer H ) ) -> B C_ ( Base ` ( I mPwSer H ) ) )
25 23 24 syl
 |-  ( ph -> B C_ ( Base ` ( I mPwSer H ) ) )
26 25 sselda
 |-  ( ( ph /\ ( A ` X ) e. B ) -> ( A ` X ) e. ( Base ` ( I mPwSer H ) ) )
27 20 26 eqeltrrd
 |-  ( ( ph /\ ( A ` X ) e. B ) -> ( x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( x = ( I X. { 0 } ) , X , ( 0g ` R ) ) ) e. ( Base ` ( I mPwSer H ) ) )
28 12 13 14 15 27 psrelbas
 |-  ( ( ph /\ ( A ` X ) e. B ) -> ( x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( x = ( I X. { 0 } ) , X , ( 0g ` R ) ) ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` H ) )
29 eqid
 |-  ( x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( x = ( I X. { 0 } ) , X , ( 0g ` R ) ) ) = ( x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( x = ( I X. { 0 } ) , X , ( 0g ` R ) ) )
30 29 fmpt
 |-  ( A. x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } if ( x = ( I X. { 0 } ) , X , ( 0g ` R ) ) e. ( Base ` H ) <-> ( x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( x = ( I X. { 0 } ) , X , ( 0g ` R ) ) ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` H ) )
31 28 30 sylibr
 |-  ( ( ph /\ ( A ` X ) e. B ) -> A. x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } if ( x = ( I X. { 0 } ) , X , ( 0g ` R ) ) e. ( Base ` H ) )
32 5 adantr
 |-  ( ( ph /\ ( A ` X ) e. B ) -> I e. W )
33 14 psrbag0
 |-  ( I e. W -> ( I X. { 0 } ) e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } )
34 32 33 syl
 |-  ( ( ph /\ ( A ` X ) e. B ) -> ( I X. { 0 } ) e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } )
35 11 31 34 rspcdva
 |-  ( ( ph /\ ( A ` X ) e. B ) -> X e. ( Base ` H ) )
36 3 subrgbas
 |-  ( T e. ( SubRing ` R ) -> T = ( Base ` H ) )
37 6 36 syl
 |-  ( ph -> T = ( Base ` H ) )
38 37 adantr
 |-  ( ( ph /\ ( A ` X ) e. B ) -> T = ( Base ` H ) )
39 35 38 eleqtrrd
 |-  ( ( ph /\ ( A ` X ) e. B ) -> X e. T )
40 eqid
 |-  ( algSc ` U ) = ( algSc ` U )
41 1 2 3 4 5 6 40 subrgascl
 |-  ( ph -> ( algSc ` U ) = ( A |` T ) )
42 41 fveq1d
 |-  ( ph -> ( ( algSc ` U ) ` X ) = ( ( A |` T ) ` X ) )
43 fvres
 |-  ( X e. T -> ( ( A |` T ) ` X ) = ( A ` X ) )
44 42 43 sylan9eq
 |-  ( ( ph /\ X e. T ) -> ( ( algSc ` U ) ` X ) = ( A ` X ) )
45 eqid
 |-  ( Scalar ` U ) = ( Scalar ` U )
46 4 mplring
 |-  ( ( I e. W /\ H e. Ring ) -> U e. Ring )
47 4 mpllmod
 |-  ( ( I e. W /\ H e. Ring ) -> U e. LMod )
48 eqid
 |-  ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) )
49 40 45 46 47 48 7 asclf
 |-  ( ( I e. W /\ H e. Ring ) -> ( algSc ` U ) : ( Base ` ( Scalar ` U ) ) --> B )
50 5 22 49 syl2anc
 |-  ( ph -> ( algSc ` U ) : ( Base ` ( Scalar ` U ) ) --> B )
51 50 adantr
 |-  ( ( ph /\ X e. T ) -> ( algSc ` U ) : ( Base ` ( Scalar ` U ) ) --> B )
52 4 5 22 mplsca
 |-  ( ph -> H = ( Scalar ` U ) )
53 52 fveq2d
 |-  ( ph -> ( Base ` H ) = ( Base ` ( Scalar ` U ) ) )
54 37 53 eqtrd
 |-  ( ph -> T = ( Base ` ( Scalar ` U ) ) )
55 54 eleq2d
 |-  ( ph -> ( X e. T <-> X e. ( Base ` ( Scalar ` U ) ) ) )
56 55 biimpa
 |-  ( ( ph /\ X e. T ) -> X e. ( Base ` ( Scalar ` U ) ) )
57 51 56 ffvelrnd
 |-  ( ( ph /\ X e. T ) -> ( ( algSc ` U ) ` X ) e. B )
58 44 57 eqeltrrd
 |-  ( ( ph /\ X e. T ) -> ( A ` X ) e. B )
59 39 58 impbida
 |-  ( ph -> ( ( A ` X ) e. B <-> X e. T ) )