mat2pmatf1

Description: The matrix transformation is a 1-1 function from the matrices to the polynomial matrices. (Contributed by AV, 28-Oct-2019) (Proof shortened by AV, 27-Nov-2019)

	Ref	Expression
Hypotheses	mat2pmatbas.t	$⊢ T = N matToPolyMat R$
	mat2pmatbas.a	$⊢ A = N Mat R$
	mat2pmatbas.b	$⊢ B = {Base}_{A}$
	mat2pmatbas.p	$⊢ P = {Poly}_{1} (R)$
	mat2pmatbas.c	$⊢ C = N Mat P$
	mat2pmatbas0.h	$⊢ H = {Base}_{C}$
Assertion	mat2pmatf1	$⊢ (N \in Fin \land R \in Ring) \to T : B \underset{1-1}{⟶} H$

Proof

Step	Hyp	Ref	Expression
1		mat2pmatbas.t	$⊢ T = N matToPolyMat R$
2		mat2pmatbas.a	$⊢ A = N Mat R$
3		mat2pmatbas.b	$⊢ B = {Base}_{A}$
4		mat2pmatbas.p	$⊢ P = {Poly}_{1} (R)$
5		mat2pmatbas.c	$⊢ C = N Mat P$
6		mat2pmatbas0.h	$⊢ H = {Base}_{C}$
7	1 2 3 4 5 6	mat2pmatf	$⊢ (N \in Fin \land R \in Ring) \to T : B ⟶ H$
8		simpl	$⊢ (x \in B \land y \in B) \to x \in B$
9	8	anim2i	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to ((N \in Fin \land R \in Ring) \land x \in B)$
10		df-3an	$⊢ (N \in Fin \land R \in Ring \land x \in B) \leftrightarrow ((N \in Fin \land R \in Ring) \land x \in B)$
11	9 10	sylibr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (N \in Fin \land R \in Ring \land x \in B)$
12		eqid	$⊢ algSc (P) = algSc (P)$
13	1 2 3 4 12	mat2pmatvalel	$⊢ ((N \in Fin \land R \in Ring \land x \in B) \land (i \in N \land j \in N)) \to i T (x) j = algSc (P) (i x j)$
14	11 13	sylan	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land (i \in N \land j \in N)) \to i T (x) j = algSc (P) (i x j)$
15		simpr	$⊢ (x \in B \land y \in B) \to y \in B$
16	15	anim2i	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to ((N \in Fin \land R \in Ring) \land y \in B)$
17		df-3an	$⊢ (N \in Fin \land R \in Ring \land y \in B) \leftrightarrow ((N \in Fin \land R \in Ring) \land y \in B)$
18	16 17	sylibr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (N \in Fin \land R \in Ring \land y \in B)$
19	1 2 3 4 12	mat2pmatvalel	$⊢ ((N \in Fin \land R \in Ring \land y \in B) \land (i \in N \land j \in N)) \to i T (y) j = algSc (P) (i y j)$
20	18 19	sylan	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land (i \in N \land j \in N)) \to i T (y) j = algSc (P) (i y j)$
21	14 20	eqeq12d	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land (i \in N \land j \in N)) \to (i T (x) j = i T (y) j \leftrightarrow algSc (P) (i x j) = algSc (P) (i y j))$
22		eqid	$⊢ {Base}_{R} = {Base}_{R}$
23		eqid	$⊢ {Base}_{P} = {Base}_{P}$
24	4 12 22 23	ply1sclf1	$⊢ R \in Ring \to algSc (P) : {Base}_{R} \underset{1-1}{⟶} {Base}_{P}$
25	24	ad3antlr	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land (i \in N \land j \in N)) \to algSc (P) : {Base}_{R} \underset{1-1}{⟶} {Base}_{P}$
26		simprl	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land (i \in N \land j \in N)) \to i \in N$
27		simprr	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land (i \in N \land j \in N)) \to j \in N$
28		simplrl	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land (i \in N \land j \in N)) \to x \in B$
29	2 22 3 26 27 28	matecld	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land (i \in N \land j \in N)) \to i x j \in {Base}_{R}$
30		simplrr	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land (i \in N \land j \in N)) \to y \in B$
31	2 22 3 26 27 30	matecld	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land (i \in N \land j \in N)) \to i y j \in {Base}_{R}$
32		f1veqaeq	$⊢ (algSc (P) : {Base}_{R} \underset{1-1}{⟶} {Base}_{P} \land (i x j \in {Base}_{R} \land i y j \in {Base}_{R})) \to (algSc (P) (i x j) = algSc (P) (i y j) \to i x j = i y j)$
33	25 29 31 32	syl12anc	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land (i \in N \land j \in N)) \to (algSc (P) (i x j) = algSc (P) (i y j) \to i x j = i y j)$
34	21 33	sylbid	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land (i \in N \land j \in N)) \to (i T (x) j = i T (y) j \to i x j = i y j)$
35	34	ralimdvva	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (\forall i \in N \forall j \in N i T (x) j = i T (y) j \to \forall i \in N \forall j \in N i x j = i y j)$
36	1 2 3 4 5 6	mat2pmatbas0	$⊢ (N \in Fin \land R \in Ring \land x \in B) \to T (x) \in H$
37	11 36	syl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to T (x) \in H$
38	1 2 3 4 5 6	mat2pmatbas0	$⊢ (N \in Fin \land R \in Ring \land y \in B) \to T (y) \in H$
39	18 38	syl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to T (y) \in H$
40	5 6	eqmat	$⊢ (T (x) \in H \land T (y) \in H) \to (T (x) = T (y) \leftrightarrow \forall i \in N \forall j \in N i T (x) j = i T (y) j)$
41	37 39 40	syl2anc	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (T (x) = T (y) \leftrightarrow \forall i \in N \forall j \in N i T (x) j = i T (y) j)$
42	2 3	eqmat	$⊢ (x \in B \land y \in B) \to (x = y \leftrightarrow \forall i \in N \forall j \in N i x j = i y j)$
43	42	adantl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (x = y \leftrightarrow \forall i \in N \forall j \in N i x j = i y j)$
44	35 41 43	3imtr4d	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (T (x) = T (y) \to x = y)$
45	44	ralrimivva	$⊢ (N \in Fin \land R \in Ring) \to \forall x \in B \forall y \in B (T (x) = T (y) \to x = y)$
46		dff13	$⊢ T : B \underset{1-1}{⟶} H \leftrightarrow (T : B ⟶ H \land \forall x \in B \forall y \in B (T (x) = T (y) \to x = y))$
47	7 45 46	sylanbrc	$⊢ (N \in Fin \land R \in Ring) \to T : B \underset{1-1}{⟶} H$

Metamath Proof Explorer

Theorem mat2pmatf1

Proof