Metamath Proof Explorer

Theorem cpmat

Description: Value of the constructor of the set of all constant polynomial matrices, i.e. the set of all N x N matrices of polynomials over a ring R . (Contributed by AV, 15-Nov-2019)

Ref Expression
Hypotheses cpmat.s ⊢ S = N ConstPolyMat R
cpmat.p ⊢ P = Poly 1 ⁡ R
cpmat.c ⊢ C = N Mat P
cpmat.b ⊢ B = Base C
Assertion cpmat ⊢ N ∈ Fin ∧ R ∈ V → S = m ∈ B | ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 R

Proof

Step Hyp Ref Expression
1 cpmat.s ⊢ S = N ConstPolyMat R
2 cpmat.p ⊢ P = Poly 1 ⁡ R
3 cpmat.c ⊢ C = N Mat P
4 cpmat.b ⊢ B = Base C
5 df-cpmat ⊢ ConstPolyMat = n ∈ Fin , r ∈ V ⟼ m ∈ Base n Mat Poly 1 ⁡ r | ∀ i ∈ n ∀ j ∈ n ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 r
6 5 a1i ⊢ N ∈ Fin ∧ R ∈ V → ConstPolyMat = n ∈ Fin , r ∈ V ⟼ m ∈ Base n Mat Poly 1 ⁡ r | ∀ i ∈ n ∀ j ∈ n ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 r
7 simpl ⊢ n = N ∧ r = R → n = N
8 fveq2 ⊢ r = R → Poly 1 ⁡ r = Poly 1 ⁡ R
9 8 adantl ⊢ n = N ∧ r = R → Poly 1 ⁡ r = Poly 1 ⁡ R
10 7 9 oveq12d ⊢ n = N ∧ r = R → n Mat Poly 1 ⁡ r = N Mat Poly 1 ⁡ R
11 10 fveq2d ⊢ n = N ∧ r = R → Base n Mat Poly 1 ⁡ r = Base N Mat Poly 1 ⁡ R
12 2 oveq2i ⊢ N Mat P = N Mat Poly 1 ⁡ R
13 3 12 eqtri ⊢ C = N Mat Poly 1 ⁡ R
14 13 fveq2i ⊢ Base C = Base N Mat Poly 1 ⁡ R
15 4 14 eqtri ⊢ B = Base N Mat Poly 1 ⁡ R
16 11 15 eqtr4di ⊢ n = N ∧ r = R → Base n Mat Poly 1 ⁡ r = B
17 fveq2 ⊢ r = R → 0 r = 0 R
18 17 adantl ⊢ n = N ∧ r = R → 0 r = 0 R
19 18 eqeq2d ⊢ n = N ∧ r = R → coe 1 ⁡ i m j ⁡ k = 0 r ↔ coe 1 ⁡ i m j ⁡ k = 0 R
20 19 ralbidv ⊢ n = N ∧ r = R → ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 r ↔ ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 R
21 7 20 raleqbidv ⊢ n = N ∧ r = R → ∀ j ∈ n ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 r ↔ ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 R
22 7 21 raleqbidv ⊢ n = N ∧ r = R → ∀ i ∈ n ∀ j ∈ n ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 r ↔ ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 R
23 16 22 rabeqbidv ⊢ n = N ∧ r = R → m ∈ Base n Mat Poly 1 ⁡ r | ∀ i ∈ n ∀ j ∈ n ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 r = m ∈ B | ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 R
24 23 adantl ⊢ N ∈ Fin ∧ R ∈ V ∧ n = N ∧ r = R → m ∈ Base n Mat Poly 1 ⁡ r | ∀ i ∈ n ∀ j ∈ n ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 r = m ∈ B | ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 R
25 simpl ⊢ N ∈ Fin ∧ R ∈ V → N ∈ Fin
26 elex ⊢ R ∈ V → R ∈ V
27 26 adantl ⊢ N ∈ Fin ∧ R ∈ V → R ∈ V
28 4 fvexi ⊢ B ∈ V
29 rabexg ⊢ B ∈ V → m ∈ B | ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 R ∈ V
30 28 29 mp1i ⊢ N ∈ Fin ∧ R ∈ V → m ∈ B | ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 R ∈ V
31 6 24 25 27 30 ovmpod ⊢ N ∈ Fin ∧ R ∈ V → N ConstPolyMat R = m ∈ B | ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 R
32 1 31 syl5eq ⊢ N ∈ Fin ∧ R ∈ V → S = m ∈ B | ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 R