Metamath Proof Explorer

Theorem mat2pmatscmxcl

Description: A transformed matrix multiplied with a power of the variable of a polynomial is a polynomial matrix. (Contributed by AV, 6-Nov-2019) (Proof shortened by AV, 28-Nov-2019)

Ref Expression
Hypotheses mat2pmatscmxcl.a ⊢ A = N Mat R
mat2pmatscmxcl.k ⊢ K = Base A
mat2pmatscmxcl.t ⊢ T = N matToPolyMat R
mat2pmatscmxcl.p ⊢ P = Poly 1 ⁡ R
mat2pmatscmxcl.c ⊢ C = N Mat P
mat2pmatscmxcl.b ⊢ B = Base C
mat2pmatscmxcl.m ⊢ ∗ ˙ = ⋅ C
mat2pmatscmxcl.e ⊢ × ˙ = ⋅ mulGrp P
mat2pmatscmxcl.x ⊢ X = var 1 ⁡ R
Assertion mat2pmatscmxcl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ K ∧ L ∈ ℕ 0 → L × ˙ X ∗ ˙ T ⁡ M ∈ B

Proof

Step Hyp Ref Expression
1 mat2pmatscmxcl.a ⊢ A = N Mat R
2 mat2pmatscmxcl.k ⊢ K = Base A
3 mat2pmatscmxcl.t ⊢ T = N matToPolyMat R
4 mat2pmatscmxcl.p ⊢ P = Poly 1 ⁡ R
5 mat2pmatscmxcl.c ⊢ C = N Mat P
6 mat2pmatscmxcl.b ⊢ B = Base C
7 mat2pmatscmxcl.m ⊢ ∗ ˙ = ⋅ C
8 mat2pmatscmxcl.e ⊢ × ˙ = ⋅ mulGrp P
9 mat2pmatscmxcl.x ⊢ X = var 1 ⁡ R
10 simpll ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ K ∧ L ∈ ℕ 0 → N ∈ Fin
11 4 ply1ring ⊢ R ∈ Ring → P ∈ Ring
12 11 ad2antlr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ K ∧ L ∈ ℕ 0 → P ∈ Ring
13 eqid ⊢ mulGrp P = mulGrp P
14 eqid ⊢ Base P = Base P
15 4 9 13 8 14 ply1moncl ⊢ R ∈ Ring ∧ L ∈ ℕ 0 → L × ˙ X ∈ Base P
16 15 ad2ant2l ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ K ∧ L ∈ ℕ 0 → L × ˙ X ∈ Base P
17 simpl ⊢ M ∈ K ∧ L ∈ ℕ 0 → M ∈ K
18 17 anim2i ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ K ∧ L ∈ ℕ 0 → N ∈ Fin ∧ R ∈ Ring ∧ M ∈ K
19 df-3an ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ K ↔ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ K
20 18 19 sylibr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ K ∧ L ∈ ℕ 0 → N ∈ Fin ∧ R ∈ Ring ∧ M ∈ K
21 3 1 2 4 5 6 mat2pmatbas0 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ K → T ⁡ M ∈ B
22 20 21 syl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ K ∧ L ∈ ℕ 0 → T ⁡ M ∈ B
23 14 5 6 7 matvscl ⊢ N ∈ Fin ∧ P ∈ Ring ∧ L × ˙ X ∈ Base P ∧ T ⁡ M ∈ B → L × ˙ X ∗ ˙ T ⁡ M ∈ B
24 10 12 16 22 23 syl22anc ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ K ∧ L ∈ ℕ 0 → L × ˙ X ∗ ˙ T ⁡ M ∈ B