m2cpm

Description: The result of a matrix transformation is a constant polynomial matrix. (Contributed by AV, 18-Nov-2019) (Proof shortened by AV, 28-Nov-2019)

	Ref	Expression
Hypotheses	m2cpm.s	$⊢ S = N ConstPolyMat R$
	m2cpm.t	$⊢ T = N matToPolyMat R$
	m2cpm.a	$⊢ A = N Mat R$
	m2cpm.b	$⊢ B = {Base}_{A}$
Assertion	m2cpm	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in S$

Proof

Step	Hyp	Ref	Expression
1		m2cpm.s	$⊢ S = N ConstPolyMat R$
2		m2cpm.t	$⊢ T = N matToPolyMat R$
3		m2cpm.a	$⊢ A = N Mat R$
4		m2cpm.b	$⊢ B = {Base}_{A}$
5		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
6		eqid	$⊢ algSc ({Poly}_{1} (R)) = algSc ({Poly}_{1} (R))$
7	2 3 4 5 6	mat2pmatvalel	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \to i T (M) j = algSc ({Poly}_{1} (R)) (i M j)$
8	7	adantr	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \land n \in ℕ) \to i T (M) j = algSc ({Poly}_{1} (R)) (i M j)$
9	8	fveq2d	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \land n \in ℕ) \to {coe}_{1} (i T (M) j) = {coe}_{1} (algSc ({Poly}_{1} (R)) (i M j))$
10	9	fveq1d	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \land n \in ℕ) \to {coe}_{1} (i T (M) j) (n) = {coe}_{1} (algSc ({Poly}_{1} (R)) (i M j)) (n)$
11		simpl2	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \to R \in Ring$
12		eqid	$⊢ {Base}_{R} = {Base}_{R}$
13		simprl	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \to i \in N$
14		simprr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \to j \in N$
15		simpl3	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \to M \in B$
16	3 12 4 13 14 15	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}_{R}$
17	11 16	jca	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \to (R \in Ring \land i M j \in {Base}_{R})$
18	17	adantr	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \land n \in ℕ) \to (R \in Ring \land i M j \in {Base}_{R})$
19		eqid	$⊢ 0_{R} = 0_{R}$
20	5 6 12 19	coe1scl	$⊢ (R \in Ring \land i M j \in {Base}_{R}) \to {coe}_{1} (algSc ({Poly}_{1} (R)) (i M j)) = (k \in ℕ_{0} ⟼ if (k = 0, i M j, 0_{R}))$
21	18 20	syl	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \land n \in ℕ) \to {coe}_{1} (algSc ({Poly}_{1} (R)) (i M j)) = (k \in ℕ_{0} ⟼ if (k = 0, i M j, 0_{R}))$
22		eqeq1	$⊢ k = n \to (k = 0 \leftrightarrow n = 0)$
23	22	ifbid	$⊢ k = n \to if (k = 0, i M j, 0_{R}) = if (n = 0, i M j, 0_{R})$
24	23	adantl	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \land n \in ℕ) \land k = n) \to if (k = 0, i M j, 0_{R}) = if (n = 0, i M j, 0_{R})$
25		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
26	25	adantl	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \land n \in ℕ) \to n \in ℕ_{0}$
27		ovex	$⊢ i M j \in V$
28		fvex	$⊢ 0_{R} \in V$
29	27 28	ifex	$⊢ if (n = 0, i M j, 0_{R}) \in V$
30	29	a1i	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \land n \in ℕ) \to if (n = 0, i M j, 0_{R}) \in V$
31	21 24 26 30	fvmptd	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \land n \in ℕ) \to {coe}_{1} (algSc ({Poly}_{1} (R)) (i M j)) (n) = if (n = 0, i M j, 0_{R})$
32		nnne0	$⊢ n \in ℕ \to n \neq 0$
33	32	neneqd	$⊢ n \in ℕ \to \neg n = 0$
34	33	adantl	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \land n \in ℕ) \to \neg n = 0$
35	34	iffalsed	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \land n \in ℕ) \to if (n = 0, i M j, 0_{R}) = 0_{R}$
36	10 31 35	3eqtrd	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \land n \in ℕ) \to {coe}_{1} (i T (M) j) (n) = 0_{R}$
37	36	ralrimiva	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \to \forall n \in ℕ {coe}_{1} (i T (M) j) (n) = 0_{R}$
38	37	ralrimivva	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \forall i \in N \forall j \in N \forall n \in ℕ {coe}_{1} (i T (M) j) (n) = 0_{R}$
39		eqid	$⊢ N Mat {Poly}_{1} (R) = N Mat {Poly}_{1} (R)$
40	2 3 4 5 39	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in {Base}_{(N Mat {Poly}_{1} (R))}$
41		eqid	$⊢ {Base}_{(N Mat {Poly}_{1} (R))} = {Base}_{(N Mat {Poly}_{1} (R))}$
42	1 5 39 41	cpmatel	$⊢ (N \in Fin \land R \in Ring \land T (M) \in {Base}_{(N Mat {Poly}_{1} (R))}) \to (T (M) \in S \leftrightarrow \forall i \in N \forall j \in N \forall n \in ℕ {coe}_{1} (i T (M) j) (n) = 0_{R})$
43	40 42	syld3an3	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (T (M) \in S \leftrightarrow \forall i \in N \forall j \in N \forall n \in ℕ {coe}_{1} (i T (M) j) (n) = 0_{R})$
44	38 43	mpbird	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in S$

Metamath Proof Explorer

Theorem m2cpm

Proof