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 \in Fin \land R \in Ring) \to (M \in S \to (M \in B \land \forall i \in N \forall j \in N \exists k \in K i M j = A (k)))$

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 \in Fin \land R \in Ring \land M \in S) \to M \in B$
8	7	3expa	$⊢ ((N \in Fin \land R \in Ring) \land M \in S) \to M \in B$
9	1 2 3 4 5 6	cpmatel2	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (M \in S \leftrightarrow \forall i \in N \forall j \in N \exists k \in K i M j = A (k))$
10	9	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 \exists k \in K i M j = A (k))$
11	10	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 \exists k \in K i M j = A (k))$
12	11	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 \exists k \in K i M j = A (k))$
13	8 12	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 \exists k \in K i M j = A (k))$
14	13	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 \exists k \in K i M j = A (k)))$

Metamath Proof Explorer