Metamath Proof Explorer

Theorem pm2mpghmlem1

Description: Lemma 1 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
pm2mpfo.l ⊢ L = Base Q
Assertion pm2mpghmlem1 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B ∧ K ∈ ℕ 0 → M decompPMat K ∗ ˙ K × ˙ X ∈ L

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 pm2mpfo.l ⊢ L = Base Q
10 7 matring ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ Ring
11 10 3adant3 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → A ∈ Ring
12 11 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B ∧ K ∈ ℕ 0 → A ∈ Ring
13 simpl2 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B ∧ K ∈ ℕ 0 → R ∈ Ring
14 simpl3 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B ∧ K ∈ ℕ 0 → M ∈ B
15 simpr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B ∧ K ∈ ℕ 0 → K ∈ ℕ 0
16 eqid ⊢ Base A = Base A
17 1 2 3 7 16 decpmatcl ⊢ R ∈ Ring ∧ M ∈ B ∧ K ∈ ℕ 0 → M decompPMat K ∈ Base A
18 13 14 15 17 syl3anc ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B ∧ K ∈ ℕ 0 → M decompPMat K ∈ Base A
19 eqid ⊢ mulGrp Q = mulGrp Q
20 16 8 6 4 19 5 9 ply1tmcl ⊢ A ∈ Ring ∧ M decompPMat K ∈ Base A ∧ K ∈ ℕ 0 → M decompPMat K ∗ ˙ K × ˙ X ∈ L
21 12 18 15 20 syl3anc ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B ∧ K ∈ ℕ 0 → M decompPMat K ∗ ˙ K × ˙ X ∈ L