Metamath Proof Explorer

Theorem cpmatel

Description: Property of a constant polynomial matrix. (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 cpmatel ⊢ N ∈ Fin ∧ R ∈ V ∧ M ∈ B → M ∈ S ↔ ∀ 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 1 2 3 4 cpmat ⊢ N ∈ Fin ∧ R ∈ V → S = m ∈ B | ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 R
6 5 3adant3 ⊢ N ∈ Fin ∧ R ∈ V ∧ M ∈ B → S = m ∈ B | ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 R
7 6 eleq2d ⊢ N ∈ Fin ∧ R ∈ V ∧ M ∈ B → M ∈ S ↔ M ∈ m ∈ B | ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 R
8 oveq ⊢ m = M → i m j = i M j
9 8 fveq2d ⊢ m = M → coe 1 ⁡ i m j = coe 1 ⁡ i M j
10 9 fveq1d ⊢ m = M → coe 1 ⁡ i m j ⁡ k = coe 1 ⁡ i M j ⁡ k
11 10 eqeq1d ⊢ m = M → coe 1 ⁡ i m j ⁡ k = 0 R ↔ coe 1 ⁡ i M j ⁡ k = 0 R
12 11 ralbidv ⊢ m = M → ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 R ↔ ∀ k ∈ ℕ coe 1 ⁡ i M j ⁡ k = 0 R
13 12 2ralbidv ⊢ m = M → ∀ 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
14 13 elrab ⊢ M ∈ m ∈ B | ∀ 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
15 7 14 bitrdi ⊢ N ∈ Fin ∧ R ∈ V ∧ M ∈ B → M ∈ S ↔ M ∈ B ∧ ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i M j ⁡ k = 0 R
16 15 3anibar ⊢ N ∈ Fin ∧ R ∈ V ∧ M ∈ B → M ∈ S ↔ ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i M j ⁡ k = 0 R