m2cpmfo

Description: The matrix transformation is a function from the matrices onto the constant polynomial matrices. (Contributed by AV, 19-Nov-2019) (Proof shortened by AV, 28-Nov-2019)

	Ref	Expression
Hypotheses	m2cpmfo.s	$⊢ S = N ConstPolyMat R$
	m2cpmfo.t	$⊢ T = N matToPolyMat R$
	m2cpmfo.a	$⊢ A = N Mat R$
	m2cpmfo.k	$⊢ K = {Base}_{A}$
Assertion	m2cpmfo	$⊢ (N \in Fin \land R \in Ring) \to T : K \underset{onto}{⟶} S$

Proof

Step	Hyp	Ref	Expression
1		m2cpmfo.s	$⊢ S = N ConstPolyMat R$
2		m2cpmfo.t	$⊢ T = N matToPolyMat R$
3		m2cpmfo.a	$⊢ A = N Mat R$
4		m2cpmfo.k	$⊢ K = {Base}_{A}$
5	1 2 3 4	m2cpmf	$⊢ (N \in Fin \land R \in Ring) \to T : K ⟶ S$
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7		simplll	$⊢ (((N \in Fin \land R \in Ring) \land x \in S) \land m \in S) \to N \in Fin$
8		simpllr	$⊢ (((N \in Fin \land R \in Ring) \land x \in S) \land m \in S) \to R \in Ring$
9		eqid	$⊢ N Mat {Poly}_{1} (R) = N Mat {Poly}_{1} (R)$
10		eqid	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{{Poly}_{1} (R)}$
11		eqid	$⊢ {Base}_{(N Mat {Poly}_{1} (R))} = {Base}_{(N Mat {Poly}_{1} (R))}$
12		simp2	$⊢ ((((N \in Fin \land R \in Ring) \land x \in S) \land m \in S) \land i \in N \land j \in N) \to i \in N$
13		simp3	$⊢ ((((N \in Fin \land R \in Ring) \land x \in S) \land m \in S) \land i \in N \land j \in N) \to j \in N$
14		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
15	1 14 9 11	cpmatpmat	$⊢ (N \in Fin \land R \in Ring \land m \in S) \to m \in {Base}_{(N Mat {Poly}_{1} (R))}$
16	15	ad4ant124	$⊢ (((N \in Fin \land R \in Ring) \land x \in S) \land m \in S) \to m \in {Base}_{(N Mat {Poly}_{1} (R))}$
17	16	3ad2ant1	$⊢ ((((N \in Fin \land R \in Ring) \land x \in S) \land m \in S) \land i \in N \land j \in N) \to m \in {Base}_{(N Mat {Poly}_{1} (R))}$
18	9 10 11 12 13 17	matecld	$⊢ ((((N \in Fin \land R \in Ring) \land x \in S) \land m \in S) \land i \in N \land j \in N) \to i m j \in {Base}_{{Poly}_{1} (R)}$
19		0nn0	$⊢ 0 \in ℕ_{0}$
20		eqid	$⊢ {coe}_{1} (i m j) = {coe}_{1} (i m j)$
21	20 10 14 6	coe1fvalcl	$⊢ (i m j \in {Base}_{{Poly}_{1} (R)} \land 0 \in ℕ_{0}) \to {coe}_{1} (i m j) (0) \in {Base}_{R}$
22	18 19 21	sylancl	$⊢ ((((N \in Fin \land R \in Ring) \land x \in S) \land m \in S) \land i \in N \land j \in N) \to {coe}_{1} (i m j) (0) \in {Base}_{R}$
23	3 6 4 7 8 22	matbas2d	$⊢ (((N \in Fin \land R \in Ring) \land x \in S) \land m \in S) \to (i \in N, j \in N ⟼ {coe}_{1} (i m j) (0)) \in K$
24	23	fmpttd	$⊢ ((N \in Fin \land R \in Ring) \land x \in S) \to (m \in S ⟼ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (0))) : S ⟶ K$
25		simpr	$⊢ ((N \in Fin \land R \in Ring) \land x \in S) \to x \in S$
26	24 25	ffvelcdmd	$⊢ ((N \in Fin \land R \in Ring) \land x \in S) \to (m \in S ⟼ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (0))) (x) \in K$
27		fveq2	$⊢ c = (m \in S ⟼ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (0))) (x) \to T (c) = T ((m \in S ⟼ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (0))) (x))$
28	27	eqeq2d	$⊢ c = (m \in S ⟼ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (0))) (x) \to (x = T (c) \leftrightarrow x = T ((m \in S ⟼ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (0))) (x)))$
29	28	adantl	$⊢ (((N \in Fin \land R \in Ring) \land x \in S) \land c = (m \in S ⟼ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (0))) (x)) \to (x = T (c) \leftrightarrow x = T ((m \in S ⟼ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (0))) (x)))$
30		eqid	$⊢ N cPolyMatToMat R = N cPolyMatToMat R$
31	30 1	cpm2mfval	$⊢ (N \in Fin \land R \in Ring) \to N cPolyMatToMat R = (m \in S ⟼ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (0)))$
32	31	fveq1d	$⊢ (N \in Fin \land R \in Ring) \to (N cPolyMatToMat R) (x) = (m \in S ⟼ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (0))) (x)$
33	32	3adant3	$⊢ (N \in Fin \land R \in Ring \land x \in S) \to (N cPolyMatToMat R) (x) = (m \in S ⟼ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (0))) (x)$
34	33	eqcomd	$⊢ (N \in Fin \land R \in Ring \land x \in S) \to (m \in S ⟼ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (0))) (x) = (N cPolyMatToMat R) (x)$
35	34	fveq2d	$⊢ (N \in Fin \land R \in Ring \land x \in S) \to T ((m \in S ⟼ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (0))) (x)) = T ((N cPolyMatToMat R) (x))$
36	1 30 2	m2cpminvid2	$⊢ (N \in Fin \land R \in Ring \land x \in S) \to T ((N cPolyMatToMat R) (x)) = x$
37	35 36	eqtrd	$⊢ (N \in Fin \land R \in Ring \land x \in S) \to T ((m \in S ⟼ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (0))) (x)) = x$
38	37	3expa	$⊢ ((N \in Fin \land R \in Ring) \land x \in S) \to T ((m \in S ⟼ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (0))) (x)) = x$
39	38	eqcomd	$⊢ ((N \in Fin \land R \in Ring) \land x \in S) \to x = T ((m \in S ⟼ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (0))) (x))$
40	26 29 39	rspcedvd	$⊢ ((N \in Fin \land R \in Ring) \land x \in S) \to \exists c \in K x = T (c)$
41	40	ralrimiva	$⊢ (N \in Fin \land R \in Ring) \to \forall x \in S \exists c \in K x = T (c)$
42		dffo3	$⊢ T : K \underset{onto}{⟶} S \leftrightarrow (T : K ⟶ S \land \forall x \in S \exists c \in K x = T (c))$
43	5 41 42	sylanbrc	$⊢ (N \in Fin \land R \in Ring) \to T : K \underset{onto}{⟶} S$

Metamath Proof Explorer

Theorem m2cpmfo

Proof