Metamath Proof Explorer

Theorem cpmatel2

Description: Another property of a constant polynomial matrix. (Contributed by AV, 16-Nov-2019) (Proof shortened by AV, 27-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
cpmatel2.k ⊢ K = Base R
cpmatel2.a ⊢ A = algSc ⁡ P
Assertion cpmatel2 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → M ∈ S ↔ ∀ i ∈ N ∀ j ∈ N ∃ k ∈ K i M j = A ⁡ k

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 cpmatel2.k ⊢ K = Base R
6 cpmatel2.a ⊢ A = algSc ⁡ P
7 1 2 3 4 cpmatel ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → M ∈ S ↔ ∀ i ∈ N ∀ j ∈ N ∀ l ∈ ℕ coe 1 ⁡ i M j ⁡ l = 0 R
8 simpl2 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B ∧ i ∈ N ∧ j ∈ N → R ∈ Ring
9 eqid ⊢ Base P = Base P
10 simprl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B ∧ i ∈ N ∧ j ∈ N → i ∈ N
11 simprr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B ∧ i ∈ N ∧ j ∈ N → j ∈ N
12 simpl3 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B ∧ i ∈ N ∧ j ∈ N → M ∈ B
13 3 9 4 10 11 12 matecld ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B ∧ i ∈ N ∧ j ∈ N → i M j ∈ Base P
14 eqid ⊢ 0 R = 0 R
15 5 14 2 9 6 cply1coe0bi ⊢ R ∈ Ring ∧ i M j ∈ Base P → ∃ k ∈ K i M j = A ⁡ k ↔ ∀ l ∈ ℕ coe 1 ⁡ i M j ⁡ l = 0 R
16 8 13 15 syl2anc ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B ∧ i ∈ N ∧ j ∈ N → ∃ k ∈ K i M j = A ⁡ k ↔ ∀ l ∈ ℕ coe 1 ⁡ i M j ⁡ l = 0 R
17 16 bicomd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B ∧ i ∈ N ∧ j ∈ N → ∀ l ∈ ℕ coe 1 ⁡ i M j ⁡ l = 0 R ↔ ∃ k ∈ K i M j = A ⁡ k
18 17 2ralbidva ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → ∀ i ∈ N ∀ j ∈ N ∀ l ∈ ℕ coe 1 ⁡ i M j ⁡ l = 0 R ↔ ∀ i ∈ N ∀ j ∈ N ∃ k ∈ K i M j = A ⁡ k
19 7 18 bitrd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → M ∈ S ↔ ∀ i ∈ N ∀ j ∈ N ∃ k ∈ K i M j = A ⁡ k