# Metamath Proof Explorer

## Theorem mp2pm2mplem3

Description: Lemma 3 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)$
Assertion mp2pm2mplem3

### 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 1 2 3 4 5 6 7 mp2pm2mplem1
10 9 oveq1d
12 eqid ${⊢}{N}\mathrm{Mat}{P}={N}\mathrm{Mat}{P}$
13 eqid ${⊢}{\mathrm{Base}}_{\left({N}\mathrm{Mat}{P}\right)}={\mathrm{Base}}_{\left({N}\mathrm{Mat}{P}\right)}$
14 1 2 3 4 5 6 7 8 12 13 mp2pm2mplem2
15 12 13 decpmatval
16 14 15 sylan
17 eqidd
18 oveq12 ${⊢}\left({i}={a}\wedge {j}={b}\right)\to {i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j}={a}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){b}$
19 18 oveq1d
20 19 mpteq2dv
21 20 oveq2d
23 simp2 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\to {a}\in {N}$
24 simp3 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {a}\in {N}\wedge {b}\in {N}\right)\to {b}\in {N}$
25 ovexd
26 17 22 23 24 25 ovmpod
27 26 fveq2d
28 27 fveq1d
29 28 mpoeq3dva
30 oveq1 ${⊢}{a}={i}\to {a}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){b}={i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){b}$
31 30 oveq1d
32 31 mpteq2dv
33 32 oveq2d
34 33 fveq2d
35 34 fveq1d
36 simpl ${⊢}\left({b}={j}\wedge {k}\in {ℕ}_{0}\right)\to {b}={j}$
37 36 oveq2d ${⊢}\left({b}={j}\wedge {k}\in {ℕ}_{0}\right)\to {i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){b}={i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j}$
38 37 oveq1d
39 38 mpteq2dva
40 39 oveq2d
41 40 fveq2d
42 41 fveq1d
43 35 42 cbvmpov
44 29 43 syl6eq
45 11 16 44 3eqtrd