cpmatpmat

Description: A constant polynomial matrix is a polynomial matrix. (Contributed by AV, 16-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	cpmatpmat	$⊢ (N \in Fin \land R \in V \land M \in S) \to M \in B$

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 \in Fin \land R \in V) \to S = \{m \in B \| \forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i m j) (k) = 0_{R}\}$
6	5	eleq2d	$⊢ (N \in Fin \land R \in V) \to (M \in S \leftrightarrow M \in \{m \in B \| \forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i m j) (k) = 0_{R}\})$
7		elrabi	$⊢ M \in \{m \in B \| \forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i m j) (k) = 0_{R}\} \to M \in B$
8	6 7	syl6bi	$⊢ (N \in Fin \land R \in V) \to (M \in S \to M \in B)$
9	8	3impia	$⊢ (N \in Fin \land R \in V \land M \in S) \to M \in B$

Metamath Proof Explorer