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