# Metamath Proof Explorer

## Theorem mp2pm2mplem2

Description: Lemma 2 for mp2pm2mp . (Contributed by AV, 10-Oct-2019) (Revised by AV, 5-Dec-2019)

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

### Proof

Step Hyp Ref Expression
1 mp2pm2mp.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 mp2pm2mp.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
3 mp2pm2mp.l ${⊢}{L}={\mathrm{Base}}_{{Q}}$
4 mp2pm2mp.m
5 mp2pm2mp.e ${⊢}{E}={\cdot }_{{\mathrm{mulGrp}}_{{P}}}$
6 mp2pm2mp.y ${⊢}{Y}={\mathrm{var}}_{1}\left({R}\right)$
7 mp2pm2mp.i
8 mp2pm2mplem2.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
9 mp2pm2mplem2.c ${⊢}{C}={N}\mathrm{Mat}{P}$
10 mp2pm2mplem2.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
11 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
12 simp1 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {N}\in \mathrm{Fin}$
13 8 ply1ring ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{Ring}$
14 13 3ad2ant2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {P}\in \mathrm{Ring}$
15 eqid ${⊢}{0}_{{P}}={0}_{{P}}$
16 ringcmn ${⊢}{P}\in \mathrm{Ring}\to {P}\in \mathrm{CMnd}$
17 13 16 syl ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{CMnd}$
18 17 3ad2ant2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {P}\in \mathrm{CMnd}$
19 18 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{CMnd}$
20 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
21 20 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}$
22 simpl12 ${⊢}\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 {R}\in \mathrm{Ring}$
23 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
24 eqid ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{{A}}$
25 simpl2 ${⊢}\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}\in {N}$
26 simpl3 ${⊢}\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 {j}\in {N}$
27 simp13 ${⊢}\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 {O}\in {L}$
28 eqid ${⊢}{\mathrm{coe}}_{1}\left({O}\right)={\mathrm{coe}}_{1}\left({O}\right)$
29 28 3 2 24 coe1fvalcl ${⊢}\left({O}\in {L}\wedge {k}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({O}\right)\left({k}\right)\in {\mathrm{Base}}_{{A}}$
30 27 29 sylan ${⊢}\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{coe}}_{1}\left({O}\right)\left({k}\right)\in {\mathrm{Base}}_{{A}}$
31 1 23 24 25 26 30 matecld ${⊢}\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{Base}}_{{R}}$
32 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}$
33 eqid ${⊢}{\mathrm{mulGrp}}_{{P}}={\mathrm{mulGrp}}_{{P}}$
34 23 8 6 4 33 5 11 ply1tmcl
35 22 31 32 34 syl3anc
36 35 fmpttd
37 1 2 3 8 4 5 6 mply1topmatcllem
38 11 15 19 21 36 37 gsumcl
39 9 11 10 12 14 38 matbas2d