# Metamath Proof Explorer

## Theorem pm2mpf1lem

Description: Lemma for pm2mpf1 . (Contributed by AV, 14-Oct-2019) (Revised by AV, 4-Dec-2019)

Ref Expression
Hypotheses pm2mpf1lem.p $⊢ P = Poly 1 ⁡ R$
pm2mpf1lem.c $⊢ C = N Mat P$
pm2mpf1lem.b $⊢ B = Base C$
pm2mpf1lem.m
pm2mpf1lem.e
pm2mpf1lem.x $⊢ X = var 1 ⁡ A$
pm2mpf1lem.a $⊢ A = N Mat R$
pm2mpf1lem.q $⊢ Q = Poly 1 ⁡ A$
Assertion pm2mpf1lem

### Proof

Step Hyp Ref Expression
1 pm2mpf1lem.p $⊢ P = Poly 1 ⁡ R$
2 pm2mpf1lem.c $⊢ C = N Mat P$
3 pm2mpf1lem.b $⊢ B = Base C$
4 pm2mpf1lem.m
5 pm2mpf1lem.e
6 pm2mpf1lem.x $⊢ X = var 1 ⁡ A$
7 pm2mpf1lem.a $⊢ A = N Mat R$
8 pm2mpf1lem.q $⊢ Q = Poly 1 ⁡ A$
9 eqid $⊢ Base Q = Base Q$
10 7 matring $⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ Ring$
11 10 adantr $⊢ N ∈ Fin ∧ R ∈ Ring ∧ U ∈ B ∧ K ∈ ℕ 0 → A ∈ Ring$
12 eqid $⊢ Base A = Base A$
13 eqid $⊢ 0 A = 0 A$
14 simpllr $⊢ N ∈ Fin ∧ R ∈ Ring ∧ U ∈ B ∧ K ∈ ℕ 0 ∧ k ∈ ℕ 0 → R ∈ Ring$
15 simplrl $⊢ N ∈ Fin ∧ R ∈ Ring ∧ U ∈ B ∧ K ∈ ℕ 0 ∧ k ∈ ℕ 0 → U ∈ B$
16 simpr $⊢ N ∈ Fin ∧ R ∈ Ring ∧ U ∈ B ∧ K ∈ ℕ 0 ∧ k ∈ ℕ 0 → k ∈ ℕ 0$
17 1 2 3 7 12 decpmatcl $⊢ R ∈ Ring ∧ U ∈ B ∧ k ∈ ℕ 0 → U decompPMat k ∈ Base A$
18 14 15 16 17 syl3anc $⊢ N ∈ Fin ∧ R ∈ Ring ∧ U ∈ B ∧ K ∈ ℕ 0 ∧ k ∈ ℕ 0 → U decompPMat k ∈ Base A$
19 18 ralrimiva $⊢ N ∈ Fin ∧ R ∈ Ring ∧ U ∈ B ∧ K ∈ ℕ 0 → ∀ k ∈ ℕ 0 U decompPMat k ∈ Base A$
20 1 2 3 7 13 decpmatfsupp $⊢ R ∈ Ring ∧ U ∈ B → finSupp 0 A⁡ k ∈ ℕ 0 ⟼ U decompPMat k$
21 20 ad2ant2lr $⊢ N ∈ Fin ∧ R ∈ Ring ∧ U ∈ B ∧ K ∈ ℕ 0 → finSupp 0 A⁡ k ∈ ℕ 0 ⟼ U decompPMat k$
22 simprr $⊢ N ∈ Fin ∧ R ∈ Ring ∧ U ∈ B ∧ K ∈ ℕ 0 → K ∈ ℕ 0$
23 8 9 6 5 11 12 4 13 19 21 22 gsummoncoe1
24 csbov2g