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 𝑠 T
subrgascl.u U = I mPoly H
subrgascl.i φ I W
subrgascl.r φ T SubRing R
subrgasclcl.b B = Base U
subrgasclcl.k K = Base R
subrgasclcl.x φ X K
Assertion subrgasclcl φ A X B X T

Proof

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