Metamath Proof Explorer

Theorem cpmatelimp2

Description: Another implication of a set being a constant polynomial matrix. (Contributed by AV, 17-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 cpmatelimp2 ⊢ N ∈ Fin ∧ R ∈ Ring → M ∈ S → M ∈ B ∧ ∀ 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 cpmatpmat ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ S → M ∈ B
8 7 3expa ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ S → M ∈ B
9 1 2 3 4 5 6 cpmatel2 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → M ∈ S ↔ ∀ i ∈ N ∀ j ∈ N ∃ k ∈ K i M j = A ⁡ k
10 9 3expa ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → M ∈ S ↔ ∀ i ∈ N ∀ j ∈ N ∃ k ∈ K i M j = A ⁡ k
11 10 biimpd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → M ∈ S → ∀ i ∈ N ∀ j ∈ N ∃ k ∈ K i M j = A ⁡ k
12 11 impancom ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ S → M ∈ B → ∀ i ∈ N ∀ j ∈ N ∃ k ∈ K i M j = A ⁡ k
13 8 12 jcai ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ S → M ∈ B ∧ ∀ i ∈ N ∀ j ∈ N ∃ k ∈ K i M j = A ⁡ k
14 13 ex ⊢ N ∈ Fin ∧ R ∈ Ring → M ∈ S → M ∈ B ∧ ∀ i ∈ N ∀ j ∈ N ∃ k ∈ K i M j = A ⁡ k