# Metamath Proof Explorer

## Theorem pm2mpghmlem2

Description: Lemma 2 for pm2mpghm . (Contributed by AV, 15-Oct-2019) (Revised by AV, 4-Dec-2019)

Ref Expression
Hypotheses pm2mpfo.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
pm2mpfo.c ${⊢}{C}={N}\mathrm{Mat}{P}$
pm2mpfo.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
pm2mpfo.m
pm2mpfo.e
pm2mpfo.x ${⊢}{X}={\mathrm{var}}_{1}\left({A}\right)$
pm2mpfo.a ${⊢}{A}={N}\mathrm{Mat}{R}$
pm2mpfo.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
Assertion pm2mpghmlem2

### Proof

Step Hyp Ref Expression
1 pm2mpfo.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 pm2mpfo.c ${⊢}{C}={N}\mathrm{Mat}{P}$
3 pm2mpfo.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
4 pm2mpfo.m
5 pm2mpfo.e
6 pm2mpfo.x ${⊢}{X}={\mathrm{var}}_{1}\left({A}\right)$
7 pm2mpfo.a ${⊢}{A}={N}\mathrm{Mat}{R}$
8 pm2mpfo.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
9 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
10 9 a1i ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {ℕ}_{0}\in \mathrm{V}$
11 7 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
12 11 3adant3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {A}\in \mathrm{Ring}$
13 8 ply1lmod ${⊢}{A}\in \mathrm{Ring}\to {Q}\in \mathrm{LMod}$
14 12 13 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {Q}\in \mathrm{LMod}$
15 8 ply1sca ${⊢}{A}\in \mathrm{Ring}\to {A}=\mathrm{Scalar}\left({Q}\right)$
16 12 15 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {A}=\mathrm{Scalar}\left({Q}\right)$
17 eqid ${⊢}{\mathrm{Base}}_{{Q}}={\mathrm{Base}}_{{Q}}$
18 simpl2 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {k}\in {ℕ}_{0}\right)\to {R}\in \mathrm{Ring}$
19 simpl3 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {k}\in {ℕ}_{0}\right)\to {M}\in {B}$
20 simpr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {k}\in {ℕ}_{0}\right)\to {k}\in {ℕ}_{0}$
21 eqid ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{{A}}$
22 1 2 3 7 21 decpmatcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {k}\in {ℕ}_{0}\right)\to {M}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
23 18 19 20 22 syl3anc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {k}\in {ℕ}_{0}\right)\to {M}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
24 eqid ${⊢}{\mathrm{mulGrp}}_{{Q}}={\mathrm{mulGrp}}_{{Q}}$
25 8 6 24 5 17 ply1moncl
26 12 25 sylan
27 eqid ${⊢}{0}_{{Q}}={0}_{{Q}}$
28 eqid ${⊢}{0}_{{A}}={0}_{{A}}$
29 1 2 3 7 28 decpmatfsupp ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {finSupp}_{{0}_{{A}}}\left(\left({k}\in {ℕ}_{0}⟼{M}\mathrm{decompPMat}{k}\right)\right)$
30 29 3adant1 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {finSupp}_{{0}_{{A}}}\left(\left({k}\in {ℕ}_{0}⟼{M}\mathrm{decompPMat}{k}\right)\right)$
31 10 14 16 17 23 26 27 28 4 30 mptscmfsupp0