mat2pmat1

Description: The transformation of the identity matrix results in the identity polynomial matrix. (Contributed by AV, 29-Oct-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	mat2pmat1	$⊢ (N \in Fin \land R \in Ring) \to T (1_{A}) = 1_{C}$

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		simpl	$⊢ (N \in Fin \land R \in Ring) \to N \in Fin$
8		simpr	$⊢ (N \in Fin \land R \in Ring) \to R \in Ring$
9	2	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
10		eqid	$⊢ 1_{A} = 1_{A}$
11	3 10	ringidcl	$⊢ A \in Ring \to 1_{A} \in B$
12	9 11	syl	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} \in B$
13	7 8 12	3jca	$⊢ (N \in Fin \land R \in Ring) \to (N \in Fin \land R \in Ring \land 1_{A} \in B)$
14		eqid	$⊢ algSc (P) = algSc (P)$
15	1 2 3 4 14	mat2pmatvalel	$⊢ ((N \in Fin \land R \in Ring \land 1_{A} \in B) \land (i \in N \land j \in N)) \to i T (1_{A}) j = algSc (P) (i 1_{A} j)$
16	13 15	sylan	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to i T (1_{A}) j = algSc (P) (i 1_{A} j)$
17		fvif	$⊢ algSc (P) (if (i = j, 1_{R}, 0_{R})) = if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R}))$
18		eqid	$⊢ 1_{R} = 1_{R}$
19		eqid	$⊢ 1_{P} = 1_{P}$
20	4 14 18 19	ply1scl1	$⊢ R \in Ring \to algSc (P) (1_{R}) = 1_{P}$
21	20	ad2antlr	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to algSc (P) (1_{R}) = 1_{P}$
22		eqid	$⊢ 0_{R} = 0_{R}$
23		eqid	$⊢ 0_{P} = 0_{P}$
24	4 14 22 23	ply1scl0	$⊢ R \in Ring \to algSc (P) (0_{R}) = 0_{P}$
25	24	ad2antlr	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to algSc (P) (0_{R}) = 0_{P}$
26	21 25	ifeq12d	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R})) = if (i = j, 1_{P}, 0_{P})$
27	17 26	eqtrid	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to algSc (P) (if (i = j, 1_{R}, 0_{R})) = if (i = j, 1_{P}, 0_{P})$
28	7	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to N \in Fin$
29	8	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to R \in Ring$
30		simpl	$⊢ (i \in N \land j \in N) \to i \in N$
31	30	adantl	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to i \in N$
32		simpr	$⊢ (i \in N \land j \in N) \to j \in N$
33	32	adantl	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to j \in N$
34	2 18 22 28 29 31 33 10	mat1ov	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to i 1_{A} j = if (i = j, 1_{R}, 0_{R})$
35	34	fveq2d	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to algSc (P) (i 1_{A} j) = algSc (P) (if (i = j, 1_{R}, 0_{R}))$
36	4	ply1ring	$⊢ R \in Ring \to P \in Ring$
37	36	ad2antlr	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to P \in Ring$
38		eqid	$⊢ 1_{C} = 1_{C}$
39	5 19 23 28 37 31 33 38	mat1ov	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to i 1_{C} j = if (i = j, 1_{P}, 0_{P})$
40	27 35 39	3eqtr4d	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to algSc (P) (i 1_{A} j) = i 1_{C} j$
41	16 40	eqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to i T (1_{A}) j = i 1_{C} j$
42	41	ralrimivva	$⊢ (N \in Fin \land R \in Ring) \to \forall i \in N \forall j \in N i T (1_{A}) j = i 1_{C} j$
43	1 2 3 4 5 6	mat2pmatbas0	$⊢ (N \in Fin \land R \in Ring \land 1_{A} \in B) \to T (1_{A}) \in H$
44	13 43	syl	$⊢ (N \in Fin \land R \in Ring) \to T (1_{A}) \in H$
45	4 5	pmatring	$⊢ (N \in Fin \land R \in Ring) \to C \in Ring$
46	6 38	ringidcl	$⊢ C \in Ring \to 1_{C} \in H$
47	45 46	syl	$⊢ (N \in Fin \land R \in Ring) \to 1_{C} \in H$
48	5 6	eqmat	$⊢ (T (1_{A}) \in H \land 1_{C} \in H) \to (T (1_{A}) = 1_{C} \leftrightarrow \forall i \in N \forall j \in N i T (1_{A}) j = i 1_{C} j)$
49	44 47 48	syl2anc	$⊢ (N \in Fin \land R \in Ring) \to (T (1_{A}) = 1_{C} \leftrightarrow \forall i \in N \forall j \in N i T (1_{A}) j = i 1_{C} j)$
50	42 49	mpbird	$⊢ (N \in Fin \land R \in Ring) \to T (1_{A}) = 1_{C}$

Metamath Proof Explorer

Theorem mat2pmat1

Proof