Metamath Proof Explorer

Theorem mp2pm2mplem5

Description: Lemma 5 for mp2pm2mp . (Contributed by AV, 12-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)$
mp2pm2mplem5.m
mp2pm2mplem5.e
mp2pm2mplem5.x ${⊢}{X}={\mathrm{var}}_{1}\left({A}\right)$
Assertion mp2pm2mplem5

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 mp2pm2mplem5.m
10 mp2pm2mplem5.e
11 mp2pm2mplem5.x ${⊢}{X}={\mathrm{var}}_{1}\left({A}\right)$
12 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
13 12 a1i ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {ℕ}_{0}\in \mathrm{V}$
14 1 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
15 2 ply1lmod ${⊢}{A}\in \mathrm{Ring}\to {Q}\in \mathrm{LMod}$
16 14 15 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {Q}\in \mathrm{LMod}$
17 16 3adant3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {Q}\in \mathrm{LMod}$
18 14 3adant3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {A}\in \mathrm{Ring}$
19 2 ply1sca ${⊢}{A}\in \mathrm{Ring}\to {A}=\mathrm{Scalar}\left({Q}\right)$
20 18 19 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {A}=\mathrm{Scalar}\left({Q}\right)$
21 simpl2 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {k}\in {ℕ}_{0}\right)\to {R}\in \mathrm{Ring}$
22 eqid ${⊢}{N}\mathrm{Mat}{P}={N}\mathrm{Mat}{P}$
23 eqid ${⊢}{\mathrm{Base}}_{\left({N}\mathrm{Mat}{P}\right)}={\mathrm{Base}}_{\left({N}\mathrm{Mat}{P}\right)}$
24 1 2 3 8 4 5 6 7 22 23 mply1topmatcl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {I}\left({O}\right)\in {\mathrm{Base}}_{\left({N}\mathrm{Mat}{P}\right)}$
25 24 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {k}\in {ℕ}_{0}\right)\to {I}\left({O}\right)\in {\mathrm{Base}}_{\left({N}\mathrm{Mat}{P}\right)}$
26 simpr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {k}\in {ℕ}_{0}\right)\to {k}\in {ℕ}_{0}$
27 eqid ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{{A}}$
28 8 22 23 1 27 decpmatcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\left({O}\right)\in {\mathrm{Base}}_{\left({N}\mathrm{Mat}{P}\right)}\wedge {k}\in {ℕ}_{0}\right)\to {I}\left({O}\right)\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
29 21 25 26 28 syl3anc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {k}\in {ℕ}_{0}\right)\to {I}\left({O}\right)\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
30 eqid ${⊢}{\mathrm{mulGrp}}_{{Q}}={\mathrm{mulGrp}}_{{Q}}$
31 2 11 30 10 3 ply1moncl
32 18 31 sylan
33 eqid ${⊢}{0}_{{Q}}={0}_{{Q}}$
34 eqid ${⊢}{0}_{{A}}={0}_{{A}}$
35 fveq2 ${⊢}{k}={l}\to {\mathrm{coe}}_{1}\left({p}\right)\left({k}\right)={\mathrm{coe}}_{1}\left({p}\right)\left({l}\right)$
36 35 oveqd ${⊢}{k}={l}\to {i}{\mathrm{coe}}_{1}\left({p}\right)\left({k}\right){j}={i}{\mathrm{coe}}_{1}\left({p}\right)\left({l}\right){j}$
37 oveq1 ${⊢}{k}={l}\to {k}{E}{Y}={l}{E}{Y}$
38 36 37 oveq12d
39 38 cbvmptv
40 39 oveq2i
41 40 a1i
42 41 mpoeq3ia
43 42 mpteq2i
44 7 43 eqtri
45 1 2 3 4 5 6 44 8 mp2pm2mplem4 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {k}\in {ℕ}_{0}\right)\to {I}\left({O}\right)\mathrm{decompPMat}{k}={\mathrm{coe}}_{1}\left({O}\right)\left({k}\right)$
46 45 mpteq2dva ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to \left({k}\in {ℕ}_{0}⟼{I}\left({O}\right)\mathrm{decompPMat}{k}\right)=\left({k}\in {ℕ}_{0}⟼{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right)\right)$
47 2 3 34 mptcoe1fsupp ${⊢}\left({A}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {finSupp}_{{0}_{{A}}}\left(\left({k}\in {ℕ}_{0}⟼{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right)\right)\right)$
48 14 47 stoic3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {finSupp}_{{0}_{{A}}}\left(\left({k}\in {ℕ}_{0}⟼{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right)\right)\right)$
49 46 48 eqbrtrd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {finSupp}_{{0}_{{A}}}\left(\left({k}\in {ℕ}_{0}⟼{I}\left({O}\right)\mathrm{decompPMat}{k}\right)\right)$
50 13 17 20 3 29 32 33 34 9 49 mptscmfsupp0