# Metamath Proof Explorer

## Theorem mp2pm2mplem1

Description: Lemma 1 for mp2pm2mp . (Contributed by AV, 9-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
Assertion mp2pm2mplem1

### 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 fveq2 ${⊢}{p}={O}\to {\mathrm{coe}}_{1}\left({p}\right)={\mathrm{coe}}_{1}\left({O}\right)$
9 8 fveq1d ${⊢}{p}={O}\to {\mathrm{coe}}_{1}\left({p}\right)\left({k}\right)={\mathrm{coe}}_{1}\left({O}\right)\left({k}\right)$
10 9 oveqd ${⊢}{p}={O}\to {i}{\mathrm{coe}}_{1}\left({p}\right)\left({k}\right){j}={i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j}$
11 10 oveq1d
12 11 mpteq2dv
13 12 oveq2d
14 13 mpoeq3dv
15 simp3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {O}\in {L}$
16 simp1 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {N}\in \mathrm{Fin}$
17 mpoexga
18 16 16 17 syl2anc
19 7 14 15 18 fvmptd3