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 \in Fin \land R \in Ring) \to (M \in S \to (M \in B \land \forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i M j) (k) = 0_{R}))$

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 \in Fin \land R \in Ring \land M \in S) \to M \in B$
6	5	3expa	$⊢ ((N \in Fin \land R \in Ring) \land M \in S) \to M \in B$
7	1 2 3 4	cpmatel	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (M \in S \leftrightarrow \forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i M j) (k) = 0_{R})$
8	7	3expa	$⊢ ((N \in Fin \land R \in Ring) \land M \in B) \to (M \in S \leftrightarrow \forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i M j) (k) = 0_{R})$
9	8	biimpd	$⊢ ((N \in Fin \land R \in Ring) \land M \in B) \to (M \in S \to \forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i M j) (k) = 0_{R})$
10	9	impancom	$⊢ ((N \in Fin \land R \in Ring) \land M \in S) \to (M \in B \to \forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i M j) (k) = 0_{R})$
11	6 10	jcai	$⊢ ((N \in Fin \land R \in Ring) \land M \in S) \to (M \in B \land \forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i M j) (k) = 0_{R})$
12	11	ex	$⊢ (N \in Fin \land R \in Ring) \to (M \in S \to (M \in B \land \forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i M j) (k) = 0_{R}))$

Metamath Proof Explorer