Metamath Proof Explorer

Theorem cpmatelimp

Description: Implication of a set being a constant polynomial matrix. (Contributed by AV, 18-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 cpmatelimp ⊢ N ∈ Fin ∧ R ∈ Ring → M ∈ 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 1 2 3 4 cpmatpmat ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ S → M ∈ B
6 5 3expa ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ S → M ∈ B
7 1 2 3 4 cpmatel ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → M ∈ S ↔ ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i M j ⁡ k = 0 R
8 7 3expa ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → M ∈ S ↔ ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i M j ⁡ k = 0 R
9 8 biimpd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → M ∈ S → ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i M j ⁡ k = 0 R
10 9 impancom ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ S → M ∈ B → ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i M j ⁡ k = 0 R
11 6 10 jcai ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ S → M ∈ B ∧ ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i M j ⁡ k = 0 R
12 11 ex ⊢ N ∈ Fin ∧ R ∈ Ring → M ∈ S → M ∈ B ∧ ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i M j ⁡ k = 0 R