# Metamath Proof Explorer

## Theorem mply1topmatcllem

Description: Lemma for mply1topmatcl . (Contributed by AV, 6-Oct-2019)

Ref Expression
Hypotheses mply1topmat.a ${⊢}{A}={N}\mathrm{Mat}{R}$
mply1topmat.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
mply1topmat.l ${⊢}{L}={\mathrm{Base}}_{{Q}}$
mply1topmat.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
mply1topmat.m
mply1topmat.e ${⊢}{E}={\cdot }_{{\mathrm{mulGrp}}_{{P}}}$
mply1topmat.y ${⊢}{Y}={\mathrm{var}}_{1}\left({R}\right)$
Assertion mply1topmatcllem

### Proof

Step Hyp Ref Expression
1 mply1topmat.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 mply1topmat.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
3 mply1topmat.l ${⊢}{L}={\mathrm{Base}}_{{Q}}$
4 mply1topmat.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
5 mply1topmat.m
6 mply1topmat.e ${⊢}{E}={\cdot }_{{\mathrm{mulGrp}}_{{P}}}$
7 mply1topmat.y ${⊢}{Y}={\mathrm{var}}_{1}\left({R}\right)$
8 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
9 8 a1i ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\to {ℕ}_{0}\in \mathrm{V}$
10 4 ply1lmod ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{LMod}$
11 10 3ad2ant2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {P}\in \mathrm{LMod}$
12 11 3ad2ant1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\to {P}\in \mathrm{LMod}$
13 simp12 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\to {R}\in \mathrm{Ring}$
14 4 ply1sca ${⊢}{R}\in \mathrm{Ring}\to {R}=\mathrm{Scalar}\left({P}\right)$
15 13 14 syl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\to {R}=\mathrm{Scalar}\left({P}\right)$
16 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
17 ovexd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {I}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){J}\in \mathrm{V}$
18 4 ply1ring ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{Ring}$
19 eqid ${⊢}{\mathrm{mulGrp}}_{{P}}={\mathrm{mulGrp}}_{{P}}$
20 19 ringmgp ${⊢}{P}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{P}}\in \mathrm{Mnd}$
21 18 20 syl ${⊢}{R}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{P}}\in \mathrm{Mnd}$
22 21 3ad2ant2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {\mathrm{mulGrp}}_{{P}}\in \mathrm{Mnd}$
23 22 3ad2ant1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\to {\mathrm{mulGrp}}_{{P}}\in \mathrm{Mnd}$
24 23 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {\mathrm{mulGrp}}_{{P}}\in \mathrm{Mnd}$
25 simpr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {k}\in {ℕ}_{0}$
26 7 4 16 vr1cl ${⊢}{R}\in \mathrm{Ring}\to {Y}\in {\mathrm{Base}}_{{P}}$
27 26 3ad2ant2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {Y}\in {\mathrm{Base}}_{{P}}$
28 27 3ad2ant1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\to {Y}\in {\mathrm{Base}}_{{P}}$
29 28 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {Y}\in {\mathrm{Base}}_{{P}}$
30 19 16 mgpbas ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{P}}}$
31 30 6 mulgnn0cl ${⊢}\left({\mathrm{mulGrp}}_{{P}}\in \mathrm{Mnd}\wedge {k}\in {ℕ}_{0}\wedge {Y}\in {\mathrm{Base}}_{{P}}\right)\to {k}{E}{Y}\in {\mathrm{Base}}_{{P}}$
32 24 25 29 31 syl3anc ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {k}{E}{Y}\in {\mathrm{Base}}_{{P}}$
33 eqid ${⊢}{0}_{{P}}={0}_{{P}}$
34 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
35 1 2 3 mptcoe1matfsupp ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\to {finSupp}_{{0}_{{R}}}\left(\left({k}\in {ℕ}_{0}⟼{I}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){J}\right)\right)$
36 9 12 15 16 17 32 33 34 5 35 mptscmfsupp0