# Metamath Proof Explorer

Description: Lemma B for cpmadugsum . (Contributed by AV, 2-Nov-2019)

Ref Expression
Hypotheses cpmadugsum.a ${⊢}{A}={N}\mathrm{Mat}{R}$
cpmadugsum.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
cpmadugsum.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
cpmadugsum.y ${⊢}{Y}={N}\mathrm{Mat}{P}$
cpmadugsum.t ${⊢}{T}={N}\mathrm{matToPolyMat}{R}$
cpmadugsum.x ${⊢}{X}={\mathrm{var}}_{1}\left({R}\right)$

### Proof

Step Hyp Ref Expression
1 cpmadugsum.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 cpmadugsum.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 cpmadugsum.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
4 cpmadugsum.y ${⊢}{Y}={N}\mathrm{Mat}{P}$
5 cpmadugsum.t ${⊢}{T}={N}\mathrm{matToPolyMat}{R}$
6 cpmadugsum.x ${⊢}{X}={\mathrm{var}}_{1}\left({R}\right)$
11 crngring ${⊢}{R}\in \mathrm{CRing}\to {R}\in \mathrm{Ring}$
12 3 ply1ring ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{Ring}$
13 11 12 syl ${⊢}{R}\in \mathrm{CRing}\to {P}\in \mathrm{Ring}$
14 13 3ad2ant2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {P}\in \mathrm{Ring}$
15 eqid ${⊢}{\mathrm{mulGrp}}_{{P}}={\mathrm{mulGrp}}_{{P}}$
16 15 ringmgp ${⊢}{P}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{P}}\in \mathrm{Mnd}$
17 14 16 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {\mathrm{mulGrp}}_{{P}}\in \mathrm{Mnd}$
18 17 ad2antrr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({s}\in {ℕ}_{0}\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\wedge {i}\in \left(0\dots {s}\right)\right)\to {\mathrm{mulGrp}}_{{P}}\in \mathrm{Mnd}$
19 elfznn0 ${⊢}{i}\in \left(0\dots {s}\right)\to {i}\in {ℕ}_{0}$
20 19 adantl ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({s}\in {ℕ}_{0}\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\wedge {i}\in \left(0\dots {s}\right)\right)\to {i}\in {ℕ}_{0}$
21 1nn0 ${⊢}1\in {ℕ}_{0}$
22 21 a1i ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({s}\in {ℕ}_{0}\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\wedge {i}\in \left(0\dots {s}\right)\right)\to 1\in {ℕ}_{0}$
23 11 3ad2ant2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {R}\in \mathrm{Ring}$
24 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
25 6 3 24 vr1cl ${⊢}{R}\in \mathrm{Ring}\to {X}\in {\mathrm{Base}}_{{P}}$
26 23 25 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {X}\in {\mathrm{Base}}_{{P}}$
27 26 ad2antrr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({s}\in {ℕ}_{0}\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\wedge {i}\in \left(0\dots {s}\right)\right)\to {X}\in {\mathrm{Base}}_{{P}}$
28 15 24 mgpbas ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{P}}}$
29 eqid ${⊢}{\cdot }_{{P}}={\cdot }_{{P}}$
30 15 29 mgpplusg ${⊢}{\cdot }_{{P}}={+}_{{\mathrm{mulGrp}}_{{P}}}$
31 28 7 30 mulgnn0dir
32 18 20 22 27 31 syl13anc
33 3 ply1crng ${⊢}{R}\in \mathrm{CRing}\to {P}\in \mathrm{CRing}$
34 33 anim2i ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to \left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{CRing}\right)$
35 34 3adant3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to \left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{CRing}\right)$
36 4 matsca2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{CRing}\right)\to {P}=\mathrm{Scalar}\left({Y}\right)$
37 35 36 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {P}=\mathrm{Scalar}\left({Y}\right)$
38 37 ad2antrr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({s}\in {ℕ}_{0}\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\wedge {i}\in \left(0\dots {s}\right)\right)\to {P}=\mathrm{Scalar}\left({Y}\right)$
39 38 fveq2d ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({s}\in {ℕ}_{0}\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\wedge {i}\in \left(0\dots {s}\right)\right)\to {\cdot }_{{P}}={\cdot }_{\mathrm{Scalar}\left({Y}\right)}$
40 eqidd
41 28 7 mulg1
42 26 41 syl
44 39 40 43 oveq123d
45 32 44 eqtrd
46 13 anim2i ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to \left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{Ring}\right)$
47 46 3adant3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to \left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{Ring}\right)$
48 4 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{Ring}\right)\to {Y}\in \mathrm{Ring}$
49 47 48 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {Y}\in \mathrm{Ring}$
50 49 ad2antrr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({s}\in {ℕ}_{0}\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\wedge {i}\in \left(0\dots {s}\right)\right)\to {Y}\in \mathrm{Ring}$
51 simpll1 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({s}\in {ℕ}_{0}\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\wedge {i}\in \left(0\dots {s}\right)\right)\to {N}\in \mathrm{Fin}$
52 23 ad2antrr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({s}\in {ℕ}_{0}\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\wedge {i}\in \left(0\dots {s}\right)\right)\to {R}\in \mathrm{Ring}$
53 simplrl ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({s}\in {ℕ}_{0}\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\wedge {i}\in \left(0\dots {s}\right)\right)\to {s}\in {ℕ}_{0}$
54 simprr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({s}\in {ℕ}_{0}\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\to {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)$
55 54 anim1i ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({s}\in {ℕ}_{0}\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\wedge {i}\in \left(0\dots {s}\right)\right)\to \left({b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\wedge {i}\in \left(0\dots {s}\right)\right)$
56 1 2 3 4 5 m2pmfzmap ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {s}\in {ℕ}_{0}\right)\wedge \left({b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\wedge {i}\in \left(0\dots {s}\right)\right)\right)\to {T}\left({b}\left({i}\right)\right)\in {\mathrm{Base}}_{{Y}}$
57 51 52 53 55 56 syl31anc ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({s}\in {ℕ}_{0}\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\wedge {i}\in \left(0\dots {s}\right)\right)\to {T}\left({b}\left({i}\right)\right)\in {\mathrm{Base}}_{{Y}}$
58 eqid ${⊢}{\mathrm{Base}}_{{Y}}={\mathrm{Base}}_{{Y}}$
59 58 9 10 ringlidm
60 50 57 59 syl2anc
61 60 eqcomd
62 45 61 oveq12d
63 4 matassa ${⊢}\left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{CRing}\right)\to {Y}\in \mathrm{AssAlg}$
64 34 63 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {Y}\in \mathrm{AssAlg}$
65 64 3adant3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {Y}\in \mathrm{AssAlg}$
66 65 ad2antrr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({s}\in {ℕ}_{0}\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\wedge {i}\in \left(0\dots {s}\right)\right)\to {Y}\in \mathrm{AssAlg}$
67 37 eqcomd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to \mathrm{Scalar}\left({Y}\right)={P}$
68 67 fveq2d ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({Y}\right)}={\mathrm{Base}}_{{P}}$
69 26 68 eleqtrrd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {X}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({Y}\right)}$
70 69 ad2antrr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({s}\in {ℕ}_{0}\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\wedge {i}\in \left(0\dots {s}\right)\right)\to {X}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({Y}\right)}$
71 28 7 mulgnn0cl
72 18 20 27 71 syl3anc
73 68 ad2antrr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({s}\in {ℕ}_{0}\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\wedge {i}\in \left(0\dots {s}\right)\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({Y}\right)}={\mathrm{Base}}_{{P}}$
74 72 73 eleqtrrd
75 46 48 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {Y}\in \mathrm{Ring}$
76 75 3adant3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {Y}\in \mathrm{Ring}$
77 58 10 ringidcl
78 76 77 syl
80 eqid ${⊢}\mathrm{Scalar}\left({Y}\right)=\mathrm{Scalar}\left({Y}\right)$
81 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({Y}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({Y}\right)}$
82 eqid ${⊢}{\cdot }_{\mathrm{Scalar}\left({Y}\right)}={\cdot }_{\mathrm{Scalar}\left({Y}\right)}$
83 58 80 81 82 8 9 assa2ass
84 66 70 74 79 57 83 syl122anc
85 84 eqcomd
86 62 85 eqtrd
87 86 mpteq2dva
88 87 oveq2d
89 eqid ${⊢}{0}_{{Y}}={0}_{{Y}}$
90 eqid ${⊢}{+}_{{Y}}={+}_{{Y}}$
91 76 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({s}\in {ℕ}_{0}\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\to {Y}\in \mathrm{Ring}$
92 ovexd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({s}\in {ℕ}_{0}\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\to \left(0\dots {s}\right)\in \mathrm{V}$
93 4 matlmod ${⊢}\left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{Ring}\right)\to {Y}\in \mathrm{LMod}$
94 46 93 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {Y}\in \mathrm{LMod}$
95 94 3adant3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {Y}\in \mathrm{LMod}$
96 11 adantl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {R}\in \mathrm{Ring}$
97 96 25 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {X}\in {\mathrm{Base}}_{{P}}$
98 34 36 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {P}=\mathrm{Scalar}\left({Y}\right)$
99 98 eqcomd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to \mathrm{Scalar}\left({Y}\right)={P}$
100 99 fveq2d ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({Y}\right)}={\mathrm{Base}}_{{P}}$
101 97 100 eleqtrrd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {X}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({Y}\right)}$
102 101 3adant3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {X}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({Y}\right)}$
103 49 77 syl
104 58 80 8 81 lmodvscl
105 95 102 103 104 syl3anc
107 95 ad2antrr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({s}\in {ℕ}_{0}\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\wedge {i}\in \left(0\dots {s}\right)\right)\to {Y}\in \mathrm{LMod}$
108 36 eqcomd ${⊢}\left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{CRing}\right)\to \mathrm{Scalar}\left({Y}\right)={P}$
109 108 fveq2d ${⊢}\left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{CRing}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({Y}\right)}={\mathrm{Base}}_{{P}}$
110 35 109 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({Y}\right)}={\mathrm{Base}}_{{P}}$
111 110 eleq2d
113 72 112 mpbird
114 58 80 8 81 lmodvscl
115 107 113 57 114 syl3anc
116 simpl1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({s}\in {ℕ}_{0}\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\to {N}\in \mathrm{Fin}$
117 23 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({s}\in {ℕ}_{0}\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\to {R}\in \mathrm{Ring}$
118 simprl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge \left({s}\in {ℕ}_{0}\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\to {s}\in {ℕ}_{0}$
119 eqid
120 fzfid ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {s}\in {ℕ}_{0}\right)\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\to \left(0\dots {s}\right)\in \mathrm{Fin}$
121 ovexd
122 fvexd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {s}\in {ℕ}_{0}\right)\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\to {0}_{{Y}}\in \mathrm{V}$
123 119 120 121 122 fsuppmptdm
124 116 117 118 54 123 syl31anc
125 58 89 90 9 91 92 106 115 124 gsummulc2
126 88 125 eqtr2d