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 = Poly 1 ⁡ R
pm2mpfo.c ⊢ C = N Mat P
pm2mpfo.b ⊢ B = Base C
pm2mpfo.m ⊢ ∗ ˙ = ⋅ Q
pm2mpfo.e ⊢ × ˙ = ⋅ mulGrp Q
pm2mpfo.x ⊢ X = var 1 ⁡ A
pm2mpfo.a ⊢ A = N Mat R
pm2mpfo.q ⊢ Q = Poly 1 ⁡ A
Assertion pm2mpghmlem2 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → finSupp 0 Q⁡ k ∈ ℕ 0 ⟼ M decompPMat k ∗ ˙ k × ˙ X

Proof

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