idpm2idmp

Description: The transformation of the identity polynomial matrix into polynomials over matrices results in the identity of the polynomials over matrices. (Contributed by AV, 18-Oct-2019) (Revised by AV, 5-Dec-2019)

	Ref	Expression
Hypotheses	pm2mpval.p	$⊢ P = {Poly}_{1} (R)$
	pm2mpval.c	$⊢ C = N Mat P$
	pm2mpval.b	$⊢ B = {Base}_{C}$
	pm2mpval.m	$⊢ \underset{˙}{*} = \cdot_{Q}$
	pm2mpval.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Q}}$
	pm2mpval.x	$⊢ X = {var}_{1} (A)$
	pm2mpval.a	$⊢ A = N Mat R$
	pm2mpval.q	$⊢ Q = {Poly}_{1} (A)$
	pm2mpval.t	$⊢ T = N pMatToMatPoly R$
Assertion	idpm2idmp	$⊢ (N \in Fin \land R \in Ring) \to T (1_{C}) = 1_{Q}$

Proof

Step	Hyp	Ref	Expression
1		pm2mpval.p	$⊢ P = {Poly}_{1} (R)$
2		pm2mpval.c	$⊢ C = N Mat P$
3		pm2mpval.b	$⊢ B = {Base}_{C}$
4		pm2mpval.m	$⊢ \underset{˙}{*} = \cdot_{Q}$
5		pm2mpval.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Q}}$
6		pm2mpval.x	$⊢ X = {var}_{1} (A)$
7		pm2mpval.a	$⊢ A = N Mat R$
8		pm2mpval.q	$⊢ Q = {Poly}_{1} (A)$
9		pm2mpval.t	$⊢ T = N pMatToMatPoly R$
10	1 2	pmatring	$⊢ (N \in Fin \land R \in Ring) \to C \in Ring$
11		eqid	$⊢ 1_{C} = 1_{C}$
12	3 11	ringidcl	$⊢ C \in Ring \to 1_{C} \in B$
13	10 12	syl	$⊢ (N \in Fin \land R \in Ring) \to 1_{C} \in B$
14	1 2 3 4 5 6 7 8 9	pm2mpfval	$⊢ (N \in Fin \land R \in Ring \land 1_{C} \in B) \to T (1_{C}) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((1_{C} decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
15	13 14	mpd3an3	$⊢ (N \in Fin \land R \in Ring) \to T (1_{C}) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((1_{C} decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
16		eqid	$⊢ 0_{A} = 0_{A}$
17		eqid	$⊢ 1_{A} = 1_{A}$
18	1 2 11 7 16 17	decpmatid	$⊢ (N \in Fin \land R \in Ring \land k \in ℕ_{0}) \to 1_{C} decompPMat k = if (k = 0, 1_{A}, 0_{A})$
19	18	3expa	$⊢ ((N \in Fin \land R \in Ring) \land k \in ℕ_{0}) \to 1_{C} decompPMat k = if (k = 0, 1_{A}, 0_{A})$
20	19	oveq1d	$⊢ ((N \in Fin \land R \in Ring) \land k \in ℕ_{0}) \to (1_{C} decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X) = if (k = 0, 1_{A}, 0_{A}) \underset{˙}{} (k \underset{˙}{\times} X)$
21	20	mpteq2dva	$⊢ (N \in Fin \land R \in Ring) \to (k \in ℕ_{0} ⟼ (1_{C} decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X)) = (k \in ℕ_{0} ⟼ if (k = 0, 1_{A}, 0_{A}) \underset{˙}{} (k \underset{˙}{\times} X))$
22	21	oveq2d	$⊢ (N \in Fin \land R \in Ring) \to \underset{k \in ℕ_{0}}{\sum_{Q}} ((1_{C} decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X)) = \underset{k \in ℕ_{0}}{\sum_{Q}} (if (k = 0, 1_{A}, 0_{A}) \underset{˙}{} (k \underset{˙}{\times} X))$
23		ovif	$⊢ if (k = 0, 1_{A}, 0_{A}) \underset{˙}{} (k \underset{˙}{\times} X) = if (k = 0, 1_{A} \underset{˙}{} (k \underset{˙}{\times} X), 0_{A} \underset{˙}{*} (k \underset{˙}{\times} X))$
24	7	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
25	8	ply1sca	$⊢ A \in Ring \to A = Scalar (Q)$
26	24 25	syl	$⊢ (N \in Fin \land R \in Ring) \to A = Scalar (Q)$
27	26	adantr	$⊢ ((N \in Fin \land R \in Ring) \land k \in ℕ_{0}) \to A = Scalar (Q)$
28	27	fveq2d	$⊢ ((N \in Fin \land R \in Ring) \land k \in ℕ_{0}) \to 1_{A} = 1_{Scalar (Q)}$
29	28	oveq1d	$⊢ ((N \in Fin \land R \in Ring) \land k \in ℕ_{0}) \to 1_{A} \underset{˙}{} (k \underset{˙}{\times} X) = 1_{Scalar (Q)} \underset{˙}{} (k \underset{˙}{\times} X)$
30	8	ply1lmod	$⊢ A \in Ring \to Q \in LMod$
31	24 30	syl	$⊢ (N \in Fin \land R \in Ring) \to Q \in LMod$
32		eqid	$⊢ {mulGrp}_{Q} = {mulGrp}_{Q}$
33		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
34	8 6 32 5 33	ply1moncl	$⊢ (A \in Ring \land k \in ℕ_{0}) \to k \underset{˙}{\times} X \in {Base}_{Q}$
35	24 34	sylan	$⊢ ((N \in Fin \land R \in Ring) \land k \in ℕ_{0}) \to k \underset{˙}{\times} X \in {Base}_{Q}$
36		eqid	$⊢ Scalar (Q) = Scalar (Q)$
37		eqid	$⊢ 1_{Scalar (Q)} = 1_{Scalar (Q)}$
38	33 36 4 37	lmodvs1	$⊢ (Q \in LMod \land k \underset{˙}{\times} X \in {Base}_{Q}) \to 1_{Scalar (Q)} \underset{˙}{*} (k \underset{˙}{\times} X) = k \underset{˙}{\times} X$
39	31 35 38	syl2an2r	$⊢ ((N \in Fin \land R \in Ring) \land k \in ℕ_{0}) \to 1_{Scalar (Q)} \underset{˙}{*} (k \underset{˙}{\times} X) = k \underset{˙}{\times} X$
40	29 39	eqtrd	$⊢ ((N \in Fin \land R \in Ring) \land k \in ℕ_{0}) \to 1_{A} \underset{˙}{*} (k \underset{˙}{\times} X) = k \underset{˙}{\times} X$
41	27	fveq2d	$⊢ ((N \in Fin \land R \in Ring) \land k \in ℕ_{0}) \to 0_{A} = 0_{Scalar (Q)}$
42	41	oveq1d	$⊢ ((N \in Fin \land R \in Ring) \land k \in ℕ_{0}) \to 0_{A} \underset{˙}{} (k \underset{˙}{\times} X) = 0_{Scalar (Q)} \underset{˙}{} (k \underset{˙}{\times} X)$
43		eqid	$⊢ 0_{Scalar (Q)} = 0_{Scalar (Q)}$
44		eqid	$⊢ 0_{Q} = 0_{Q}$
45	33 36 4 43 44	lmod0vs	$⊢ (Q \in LMod \land k \underset{˙}{\times} X \in {Base}_{Q}) \to 0_{Scalar (Q)} \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{Q}$
46	31 35 45	syl2an2r	$⊢ ((N \in Fin \land R \in Ring) \land k \in ℕ_{0}) \to 0_{Scalar (Q)} \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{Q}$
47	42 46	eqtrd	$⊢ ((N \in Fin \land R \in Ring) \land k \in ℕ_{0}) \to 0_{A} \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{Q}$
48	40 47	ifeq12d	$⊢ ((N \in Fin \land R \in Ring) \land k \in ℕ_{0}) \to if (k = 0, 1_{A} \underset{˙}{} (k \underset{˙}{\times} X), 0_{A} \underset{˙}{} (k \underset{˙}{\times} X)) = if (k = 0, k \underset{˙}{\times} X, 0_{Q})$
49	23 48	syl5eq	$⊢ ((N \in Fin \land R \in Ring) \land k \in ℕ_{0}) \to if (k = 0, 1_{A}, 0_{A}) \underset{˙}{*} (k \underset{˙}{\times} X) = if (k = 0, k \underset{˙}{\times} X, 0_{Q})$
50	49	mpteq2dva	$⊢ (N \in Fin \land R \in Ring) \to (k \in ℕ_{0} ⟼ if (k = 0, 1_{A}, 0_{A}) \underset{˙}{*} (k \underset{˙}{\times} X)) = (k \in ℕ_{0} ⟼ if (k = 0, k \underset{˙}{\times} X, 0_{Q}))$
51	50	oveq2d	$⊢ (N \in Fin \land R \in Ring) \to \underset{k \in ℕ_{0}}{\sum_{Q}} (if (k = 0, 1_{A}, 0_{A}) \underset{˙}{*} (k \underset{˙}{\times} X)) = \underset{k \in ℕ_{0}}{\sum_{Q}} if (k = 0, k \underset{˙}{\times} X, 0_{Q})$
52	8	ply1ring	$⊢ A \in Ring \to Q \in Ring$
53		ringmnd	$⊢ Q \in Ring \to Q \in Mnd$
54	24 52 53	3syl	$⊢ (N \in Fin \land R \in Ring) \to Q \in Mnd$
55		nn0ex	$⊢ ℕ_{0} \in V$
56	55	a1i	$⊢ (N \in Fin \land R \in Ring) \to ℕ_{0} \in V$
57		0nn0	$⊢ 0 \in ℕ_{0}$
58	57	a1i	$⊢ (N \in Fin \land R \in Ring) \to 0 \in ℕ_{0}$
59		eqid	$⊢ (k \in ℕ_{0} ⟼ if (k = 0, k \underset{˙}{\times} X, 0_{Q})) = (k \in ℕ_{0} ⟼ if (k = 0, k \underset{˙}{\times} X, 0_{Q}))$
60	35	ralrimiva	$⊢ (N \in Fin \land R \in Ring) \to \forall k \in ℕ_{0} k \underset{˙}{\times} X \in {Base}_{Q}$
61	44 54 56 58 59 60	gsummpt1n0	$⊢ (N \in Fin \land R \in Ring) \to \underset{k \in ℕ_{0}}{\sum_{Q}} if (k = 0, k \underset{˙}{\times} X, 0_{Q}) = ⦋ 0 / k ⦌ (k \underset{˙}{\times} X)$
62		c0ex	$⊢ 0 \in V$
63		csbov1g	$⊢ 0 \in V \to ⦋ 0 / k ⦌ (k \underset{˙}{\times} X) = ⦋ 0 / k ⦌ k \underset{˙}{\times} X$
64	62 63	mp1i	$⊢ (N \in Fin \land R \in Ring) \to ⦋ 0 / k ⦌ (k \underset{˙}{\times} X) = ⦋ 0 / k ⦌ k \underset{˙}{\times} X$
65		csbvarg	$⊢ 0 \in V \to ⦋ 0 / k ⦌ k = 0$
66	62 65	mp1i	$⊢ (N \in Fin \land R \in Ring) \to ⦋ 0 / k ⦌ k = 0$
67	66	oveq1d	$⊢ (N \in Fin \land R \in Ring) \to ⦋ 0 / k ⦌ k \underset{˙}{\times} X = 0 \underset{˙}{\times} X$
68	8 6 32 5	ply1idvr1	$⊢ A \in Ring \to 0 \underset{˙}{\times} X = 1_{Q}$
69	24 68	syl	$⊢ (N \in Fin \land R \in Ring) \to 0 \underset{˙}{\times} X = 1_{Q}$
70	64 67 69	3eqtrd	$⊢ (N \in Fin \land R \in Ring) \to ⦋ 0 / k ⦌ (k \underset{˙}{\times} X) = 1_{Q}$
71	51 61 70	3eqtrd	$⊢ (N \in Fin \land R \in Ring) \to \underset{k \in ℕ_{0}}{\sum_{Q}} (if (k = 0, 1_{A}, 0_{A}) \underset{˙}{*} (k \underset{˙}{\times} X)) = 1_{Q}$
72	15 22 71	3eqtrd	$⊢ (N \in Fin \land R \in Ring) \to T (1_{C}) = 1_{Q}$

Metamath Proof Explorer

Theorem idpm2idmp

Proof