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 \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))$

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 \in Fin \land R \in Ring \land M \in B) \to (M \in S \leftrightarrow \forall i \in N \forall j \in N \forall l \in ℕ {coe}_{1} (i M j) (l) = 0_{R})$
8		simpl2	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \to R \in Ring$
9		eqid	$⊢ {Base}_{P} = {Base}_{P}$
10		simprl	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \to i \in N$
11		simprr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \to j \in N$
12		simpl3	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \to M \in B$
13	3 9 4 10 11 12	matecld	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \to i M j \in {Base}_{P}$
14		eqid	$⊢ 0_{R} = 0_{R}$
15	5 14 2 9 6	cply1coe0bi	$⊢ (R \in Ring \land i M j \in {Base}_{P}) \to (\exists k \in K i M j = A (k) \leftrightarrow \forall l \in ℕ {coe}_{1} (i M j) (l) = 0_{R})$
16	8 13 15	syl2anc	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \to (\exists k \in K i M j = A (k) \leftrightarrow \forall l \in ℕ {coe}_{1} (i M j) (l) = 0_{R})$
17	16	bicomd	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \to (\forall l \in ℕ {coe}_{1} (i M j) (l) = 0_{R} \leftrightarrow \exists k \in K i M j = A (k))$
18	17	2ralbidva	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (\forall i \in N \forall j \in N \forall l \in ℕ {coe}_{1} (i M j) (l) = 0_{R} \leftrightarrow \forall i \in N \forall j \in N \exists k \in K i M j = A (k))$
19	7 18	bitrd	$⊢ (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))$