Metamath Proof Explorer

Theorem pm2mpfo

Description: The transformation of polynomial matrices into polynomials over matrices is a function mapping polynomial matrices onto polynomials over matrices. (Contributed by AV, 12-Oct-2019) (Revised by AV, 6-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
pm2mpfo.t ⊢ T = N pMatToMatPoly R
Assertion pm2mpfo ⊢ N ∈ Fin ∧ R ∈ Ring → T : B ⟶ onto 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 pm2mpfo.t ⊢ T = N pMatToMatPoly R
11 1 2 3 4 5 6 7 8 10 9 pm2mpf ⊢ N ∈ Fin ∧ R ∈ Ring → T : B ⟶ L
12 eqid ⊢ ⋅ P = ⋅ P
13 eqid ⊢ ⋅ mulGrp P = ⋅ mulGrp P
14 eqid ⊢ var 1 ⁡ R = var 1 ⁡ R
15 eqid ⊢ l ∈ L ⟼ i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ l ⁡ k j ⋅ P k ⋅ mulGrp P var 1 ⁡ R = l ∈ L ⟼ i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ l ⁡ k j ⋅ P k ⋅ mulGrp P var 1 ⁡ R
16 7 8 9 12 13 14 15 1 10 mp2pm2mp ⊢ N ∈ Fin ∧ R ∈ Ring ∧ p ∈ L → T ⁡ l ∈ L ⟼ i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ l ⁡ k j ⋅ P k ⋅ mulGrp P var 1 ⁡ R ⁡ p = p
17 16 3expa ⊢ N ∈ Fin ∧ R ∈ Ring ∧ p ∈ L → T ⁡ l ∈ L ⟼ i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ l ⁡ k j ⋅ P k ⋅ mulGrp P var 1 ⁡ R ⁡ p = p
18 7 8 9 1 12 13 14 15 2 3 mply1topmatcl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ p ∈ L → l ∈ L ⟼ i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ l ⁡ k j ⋅ P k ⋅ mulGrp P var 1 ⁡ R ⁡ p ∈ B
19 18 3expa ⊢ N ∈ Fin ∧ R ∈ Ring ∧ p ∈ L → l ∈ L ⟼ i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ l ⁡ k j ⋅ P k ⋅ mulGrp P var 1 ⁡ R ⁡ p ∈ B
20 simpr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ p ∈ L ∧ f = l ∈ L ⟼ i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ l ⁡ k j ⋅ P k ⋅ mulGrp P var 1 ⁡ R ⁡ p → f = l ∈ L ⟼ i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ l ⁡ k j ⋅ P k ⋅ mulGrp P var 1 ⁡ R ⁡ p
21 20 fveq2d ⊢ N ∈ Fin ∧ R ∈ Ring ∧ p ∈ L ∧ f = l ∈ L ⟼ i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ l ⁡ k j ⋅ P k ⋅ mulGrp P var 1 ⁡ R ⁡ p → T ⁡ f = T ⁡ l ∈ L ⟼ i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ l ⁡ k j ⋅ P k ⋅ mulGrp P var 1 ⁡ R ⁡ p
22 21 eqeq2d ⊢ N ∈ Fin ∧ R ∈ Ring ∧ p ∈ L ∧ f = l ∈ L ⟼ i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ l ⁡ k j ⋅ P k ⋅ mulGrp P var 1 ⁡ R ⁡ p → p = T ⁡ f ↔ p = T ⁡ l ∈ L ⟼ i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ l ⁡ k j ⋅ P k ⋅ mulGrp P var 1 ⁡ R ⁡ p
23 19 22 rspcedv ⊢ N ∈ Fin ∧ R ∈ Ring ∧ p ∈ L → p = T ⁡ l ∈ L ⟼ i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ l ⁡ k j ⋅ P k ⋅ mulGrp P var 1 ⁡ R ⁡ p → ∃ f ∈ B p = T ⁡ f
24 23 com12 ⊢ p = T ⁡ l ∈ L ⟼ i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ l ⁡ k j ⋅ P k ⋅ mulGrp P var 1 ⁡ R ⁡ p → N ∈ Fin ∧ R ∈ Ring ∧ p ∈ L → ∃ f ∈ B p = T ⁡ f
25 24 eqcoms ⊢ T ⁡ l ∈ L ⟼ i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ l ⁡ k j ⋅ P k ⋅ mulGrp P var 1 ⁡ R ⁡ p = p → N ∈ Fin ∧ R ∈ Ring ∧ p ∈ L → ∃ f ∈ B p = T ⁡ f
26 17 25 mpcom ⊢ N ∈ Fin ∧ R ∈ Ring ∧ p ∈ L → ∃ f ∈ B p = T ⁡ f
27 26 ralrimiva ⊢ N ∈ Fin ∧ R ∈ Ring → ∀ p ∈ L ∃ f ∈ B p = T ⁡ f
28 dffo3 ⊢ T : B ⟶ onto L ↔ T : B ⟶ L ∧ ∀ p ∈ L ∃ f ∈ B p = T ⁡ f
29 11 27 28 sylanbrc ⊢ N ∈ Fin ∧ R ∈ Ring → T : B ⟶ onto L