decpmatid

Description: The matrix consisting of the coefficients in the polynomial entries of the identity matrix is an identity or a zero matrix. (Contributed by AV, 28-Sep-2019) (Revised by AV, 2-Dec-2019)

	Ref	Expression
Hypotheses	decpmatid.p	$⊢ P = {Poly}_{1} (R)$
	decpmatid.c	$⊢ C = N Mat P$
	decpmatid.i	$⊢ I = 1_{C}$
	decpmatid.a	$⊢ A = N Mat R$
	decpmatid.0	$⊢ \underset{˙}{0} = 0_{A}$
	decpmatid.1	$⊢ \underset{˙}{1} = 1_{A}$
Assertion	decpmatid	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to I decompPMat K = if (K = 0, \underset{˙}{1}, \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		decpmatid.p	$⊢ P = {Poly}_{1} (R)$
2		decpmatid.c	$⊢ C = N Mat P$
3		decpmatid.i	$⊢ I = 1_{C}$
4		decpmatid.a	$⊢ A = N Mat R$
5		decpmatid.0	$⊢ \underset{˙}{0} = 0_{A}$
6		decpmatid.1	$⊢ \underset{˙}{1} = 1_{A}$
7	1 2	pmatring	$⊢ (N \in Fin \land R \in Ring) \to C \in Ring$
8	7	3adant3	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to C \in Ring$
9		eqid	$⊢ {Base}_{C} = {Base}_{C}$
10	9 3	ringidcl	$⊢ C \in Ring \to I \in {Base}_{C}$
11	8 10	syl	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to I \in {Base}_{C}$
12		simp3	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to K \in ℕ_{0}$
13	2 9	decpmatval	$⊢ (I \in {Base}_{C} \land K \in ℕ_{0}) \to I decompPMat K = (i \in N, j \in N ⟼ {coe}_{1} (i I j) (K))$
14	11 12 13	syl2anc	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to I decompPMat K = (i \in N, j \in N ⟼ {coe}_{1} (i I j) (K))$
15		eqid	$⊢ 0_{P} = 0_{P}$
16		eqid	$⊢ 1_{P} = 1_{P}$
17		simp11	$⊢ ((N \in Fin \land R \in Ring \land K \in ℕ_{0}) \land i \in N \land j \in N) \to N \in Fin$
18		simp12	$⊢ ((N \in Fin \land R \in Ring \land K \in ℕ_{0}) \land i \in N \land j \in N) \to R \in Ring$
19		simp2	$⊢ ((N \in Fin \land R \in Ring \land K \in ℕ_{0}) \land i \in N \land j \in N) \to i \in N$
20		simp3	$⊢ ((N \in Fin \land R \in Ring \land K \in ℕ_{0}) \land i \in N \land j \in N) \to j \in N$
21	1 2 15 16 17 18 19 20 3	pmat1ovd	$⊢ ((N \in Fin \land R \in Ring \land K \in ℕ_{0}) \land i \in N \land j \in N) \to i I j = if (i = j, 1_{P}, 0_{P})$
22	21	fveq2d	$⊢ ((N \in Fin \land R \in Ring \land K \in ℕ_{0}) \land i \in N \land j \in N) \to {coe}_{1} (i I j) = {coe}_{1} (if (i = j, 1_{P}, 0_{P}))$
23	22	fveq1d	$⊢ ((N \in Fin \land R \in Ring \land K \in ℕ_{0}) \land i \in N \land j \in N) \to {coe}_{1} (i I j) (K) = {coe}_{1} (if (i = j, 1_{P}, 0_{P})) (K)$
24		fvif	$⊢ {coe}_{1} (if (i = j, 1_{P}, 0_{P})) = if (i = j, {coe}_{1} (1_{P}), {coe}_{1} (0_{P}))$
25	24	fveq1i	$⊢ {coe}_{1} (if (i = j, 1_{P}, 0_{P})) (K) = if (i = j, {coe}_{1} (1_{P}), {coe}_{1} (0_{P})) (K)$
26		iffv	$⊢ if (i = j, {coe}_{1} (1_{P}), {coe}_{1} (0_{P})) (K) = if (i = j, {coe}_{1} (1_{P}) (K), {coe}_{1} (0_{P}) (K))$
27	25 26	eqtri	$⊢ {coe}_{1} (if (i = j, 1_{P}, 0_{P})) (K) = if (i = j, {coe}_{1} (1_{P}) (K), {coe}_{1} (0_{P}) (K))$
28		eqid	$⊢ {var}_{1} (R) = {var}_{1} (R)$
29		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
30		eqid	$⊢ \cdot_{{mulGrp}_{P}} = \cdot_{{mulGrp}_{P}}$
31	1 28 29 30	ply1idvr1	$⊢ R \in Ring \to 0 \cdot_{{mulGrp}_{P}} {var}_{1} (R) = 1_{P}$
32	31	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to 0 \cdot_{{mulGrp}_{P}} {var}_{1} (R) = 1_{P}$
33	32	eqcomd	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to 1_{P} = 0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)$
34	33	fveq2d	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to {coe}_{1} (1_{P}) = {coe}_{1} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))$
35	34	fveq1d	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to {coe}_{1} (1_{P}) (K) = {coe}_{1} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) (K)$
36	1	ply1lmod	$⊢ R \in Ring \to P \in LMod$
37	36	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to P \in LMod$
38		0nn0	$⊢ 0 \in ℕ_{0}$
39		eqid	$⊢ {Base}_{P} = {Base}_{P}$
40	1 28 29 30 39	ply1moncl	$⊢ (R \in Ring \land 0 \in ℕ_{0}) \to 0 \cdot_{{mulGrp}_{P}} {var}_{1} (R) \in {Base}_{P}$
41	38 40	mpan2	$⊢ R \in Ring \to 0 \cdot_{{mulGrp}_{P}} {var}_{1} (R) \in {Base}_{P}$
42	41	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to 0 \cdot_{{mulGrp}_{P}} {var}_{1} (R) \in {Base}_{P}$
43		eqid	$⊢ Scalar (P) = Scalar (P)$
44		eqid	$⊢ \cdot_{P} = \cdot_{P}$
45		eqid	$⊢ 1_{Scalar (P)} = 1_{Scalar (P)}$
46	39 43 44 45	lmodvs1	$⊢ (P \in LMod \land 0 \cdot_{{mulGrp}_{P}} {var}_{1} (R) \in {Base}_{P}) \to 1_{Scalar (P)} \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) = 0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)$
47	37 42 46	syl2anc	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to 1_{Scalar (P)} \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) = 0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)$
48	47	eqcomd	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to 0 \cdot_{{mulGrp}_{P}} {var}_{1} (R) = 1_{Scalar (P)} \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))$
49	48	fveq2d	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to {coe}_{1} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) = {coe}_{1} (1_{Scalar (P)} \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)))$
50	49	fveq1d	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to {coe}_{1} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) (K) = {coe}_{1} (1_{Scalar (P)} \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))) (K)$
51		simp2	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to R \in Ring$
52	1	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
53	52	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to R = Scalar (P)$
54	53	eqcomd	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to Scalar (P) = R$
55	54	fveq2d	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to 1_{Scalar (P)} = 1_{R}$
56		eqid	$⊢ {Base}_{R} = {Base}_{R}$
57		eqid	$⊢ 1_{R} = 1_{R}$
58	56 57	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
59	58	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to 1_{R} \in {Base}_{R}$
60	55 59	eqeltrd	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to 1_{Scalar (P)} \in {Base}_{R}$
61	38	a1i	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to 0 \in ℕ_{0}$
62		eqid	$⊢ 0_{R} = 0_{R}$
63	62 56 1 28 44 29 30	coe1tm	$⊢ (R \in Ring \land 1_{Scalar (P)} \in {Base}_{R} \land 0 \in ℕ_{0}) \to {coe}_{1} (1_{Scalar (P)} \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))) = (k \in ℕ_{0} ⟼ if (k = 0, 1_{Scalar (P)}, 0_{R}))$
64	51 60 61 63	syl3anc	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to {coe}_{1} (1_{Scalar (P)} \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))) = (k \in ℕ_{0} ⟼ if (k = 0, 1_{Scalar (P)}, 0_{R}))$
65		eqeq1	$⊢ k = K \to (k = 0 \leftrightarrow K = 0)$
66	65	ifbid	$⊢ k = K \to if (k = 0, 1_{Scalar (P)}, 0_{R}) = if (K = 0, 1_{Scalar (P)}, 0_{R})$
67	66	adantl	$⊢ ((N \in Fin \land R \in Ring \land K \in ℕ_{0}) \land k = K) \to if (k = 0, 1_{Scalar (P)}, 0_{R}) = if (K = 0, 1_{Scalar (P)}, 0_{R})$
68		fvex	$⊢ 1_{Scalar (P)} \in V$
69		fvex	$⊢ 0_{R} \in V$
70	68 69	ifex	$⊢ if (K = 0, 1_{Scalar (P)}, 0_{R}) \in V$
71	70	a1i	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to if (K = 0, 1_{Scalar (P)}, 0_{R}) \in V$
72	64 67 12 71	fvmptd	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to {coe}_{1} (1_{Scalar (P)} \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))) (K) = if (K = 0, 1_{Scalar (P)}, 0_{R})$
73	35 50 72	3eqtrd	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to {coe}_{1} (1_{P}) (K) = if (K = 0, 1_{Scalar (P)}, 0_{R})$
74	1 15 62	coe1z	$⊢ R \in Ring \to {coe}_{1} (0_{P}) = ℕ_{0} \times \{0_{R}\}$
75	74	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to {coe}_{1} (0_{P}) = ℕ_{0} \times \{0_{R}\}$
76	75	fveq1d	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to {coe}_{1} (0_{P}) (K) = (ℕ_{0} \times \{0_{R}\}) (K)$
77	69	a1i	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to 0_{R} \in V$
78		fvconst2g	$⊢ (0_{R} \in V \land K \in ℕ_{0}) \to (ℕ_{0} \times \{0_{R}\}) (K) = 0_{R}$
79	77 12 78	syl2anc	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to (ℕ_{0} \times \{0_{R}\}) (K) = 0_{R}$
80	76 79	eqtrd	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to {coe}_{1} (0_{P}) (K) = 0_{R}$
81	73 80	ifeq12d	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to if (i = j, {coe}_{1} (1_{P}) (K), {coe}_{1} (0_{P}) (K)) = if (i = j, if (K = 0, 1_{Scalar (P)}, 0_{R}), 0_{R})$
82	81	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring \land K \in ℕ_{0}) \land i \in N \land j \in N) \to if (i = j, {coe}_{1} (1_{P}) (K), {coe}_{1} (0_{P}) (K)) = if (i = j, if (K = 0, 1_{Scalar (P)}, 0_{R}), 0_{R})$
83	27 82	syl5eq	$⊢ ((N \in Fin \land R \in Ring \land K \in ℕ_{0}) \land i \in N \land j \in N) \to {coe}_{1} (if (i = j, 1_{P}, 0_{P})) (K) = if (i = j, if (K = 0, 1_{Scalar (P)}, 0_{R}), 0_{R})$
84	23 83	eqtrd	$⊢ ((N \in Fin \land R \in Ring \land K \in ℕ_{0}) \land i \in N \land j \in N) \to {coe}_{1} (i I j) (K) = if (i = j, if (K = 0, 1_{Scalar (P)}, 0_{R}), 0_{R})$
85	84	mpoeq3dva	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to (i \in N, j \in N ⟼ {coe}_{1} (i I j) (K)) = (i \in N, j \in N ⟼ if (i = j, if (K = 0, 1_{Scalar (P)}, 0_{R}), 0_{R}))$
86	53	adantl	$⊢ (K = 0 \land (N \in Fin \land R \in Ring \land K \in ℕ_{0})) \to R = Scalar (P)$
87	86	eqcomd	$⊢ (K = 0 \land (N \in Fin \land R \in Ring \land K \in ℕ_{0})) \to Scalar (P) = R$
88	87	fveq2d	$⊢ (K = 0 \land (N \in Fin \land R \in Ring \land K \in ℕ_{0})) \to 1_{Scalar (P)} = 1_{R}$
89	88	ifeq1d	$⊢ (K = 0 \land (N \in Fin \land R \in Ring \land K \in ℕ_{0})) \to if (i = j, 1_{Scalar (P)}, 0_{R}) = if (i = j, 1_{R}, 0_{R})$
90	89	mpoeq3dv	$⊢ (K = 0 \land (N \in Fin \land R \in Ring \land K \in ℕ_{0})) \to (i \in N, j \in N ⟼ if (i = j, 1_{Scalar (P)}, 0_{R})) = (i \in N, j \in N ⟼ if (i = j, 1_{R}, 0_{R}))$
91		iftrue	$⊢ K = 0 \to if (K = 0, 1_{Scalar (P)}, 0_{R}) = 1_{Scalar (P)}$
92	91	ifeq1d	$⊢ K = 0 \to if (i = j, if (K = 0, 1_{Scalar (P)}, 0_{R}), 0_{R}) = if (i = j, 1_{Scalar (P)}, 0_{R})$
93	92	adantr	$⊢ (K = 0 \land (N \in Fin \land R \in Ring \land K \in ℕ_{0})) \to if (i = j, if (K = 0, 1_{Scalar (P)}, 0_{R}), 0_{R}) = if (i = j, 1_{Scalar (P)}, 0_{R})$
94	93	mpoeq3dv	$⊢ (K = 0 \land (N \in Fin \land R \in Ring \land K \in ℕ_{0})) \to (i \in N, j \in N ⟼ if (i = j, if (K = 0, 1_{Scalar (P)}, 0_{R}), 0_{R})) = (i \in N, j \in N ⟼ if (i = j, 1_{Scalar (P)}, 0_{R}))$
95	4 57 62	mat1	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} = (i \in N, j \in N ⟼ if (i = j, 1_{R}, 0_{R}))$
96	6 95	syl5eq	$⊢ (N \in Fin \land R \in Ring) \to \underset{˙}{1} = (i \in N, j \in N ⟼ if (i = j, 1_{R}, 0_{R}))$
97	96	3adant3	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to \underset{˙}{1} = (i \in N, j \in N ⟼ if (i = j, 1_{R}, 0_{R}))$
98	97	adantl	$⊢ (K = 0 \land (N \in Fin \land R \in Ring \land K \in ℕ_{0})) \to \underset{˙}{1} = (i \in N, j \in N ⟼ if (i = j, 1_{R}, 0_{R}))$
99	90 94 98	3eqtr4d	$⊢ (K = 0 \land (N \in Fin \land R \in Ring \land K \in ℕ_{0})) \to (i \in N, j \in N ⟼ if (i = j, if (K = 0, 1_{Scalar (P)}, 0_{R}), 0_{R})) = \underset{˙}{1}$
100		iftrue	$⊢ K = 0 \to if (K = 0, \underset{˙}{1}, \underset{˙}{0}) = \underset{˙}{1}$
101	100	eqcomd	$⊢ K = 0 \to \underset{˙}{1} = if (K = 0, \underset{˙}{1}, \underset{˙}{0})$
102	101	adantr	$⊢ (K = 0 \land (N \in Fin \land R \in Ring \land K \in ℕ_{0})) \to \underset{˙}{1} = if (K = 0, \underset{˙}{1}, \underset{˙}{0})$
103	99 102	eqtrd	$⊢ (K = 0 \land (N \in Fin \land R \in Ring \land K \in ℕ_{0})) \to (i \in N, j \in N ⟼ if (i = j, if (K = 0, 1_{Scalar (P)}, 0_{R}), 0_{R})) = if (K = 0, \underset{˙}{1}, \underset{˙}{0})$
104		ifid	$⊢ if (i = j, 0_{R}, 0_{R}) = 0_{R}$
105	104	a1i	$⊢ (\neg K = 0 \land (N \in Fin \land R \in Ring \land K \in ℕ_{0})) \to if (i = j, 0_{R}, 0_{R}) = 0_{R}$
106	105	mpoeq3dv	$⊢ (\neg K = 0 \land (N \in Fin \land R \in Ring \land K \in ℕ_{0})) \to (i \in N, j \in N ⟼ if (i = j, 0_{R}, 0_{R})) = (i \in N, j \in N ⟼ 0_{R})$
107		iffalse	$⊢ \neg K = 0 \to if (K = 0, 1_{Scalar (P)}, 0_{R}) = 0_{R}$
108	107	adantr	$⊢ (\neg K = 0 \land (N \in Fin \land R \in Ring \land K \in ℕ_{0})) \to if (K = 0, 1_{Scalar (P)}, 0_{R}) = 0_{R}$
109	108	ifeq1d	$⊢ (\neg K = 0 \land (N \in Fin \land R \in Ring \land K \in ℕ_{0})) \to if (i = j, if (K = 0, 1_{Scalar (P)}, 0_{R}), 0_{R}) = if (i = j, 0_{R}, 0_{R})$
110	109	mpoeq3dv	$⊢ (\neg K = 0 \land (N \in Fin \land R \in Ring \land K \in ℕ_{0})) \to (i \in N, j \in N ⟼ if (i = j, if (K = 0, 1_{Scalar (P)}, 0_{R}), 0_{R})) = (i \in N, j \in N ⟼ if (i = j, 0_{R}, 0_{R}))$
111		3simpa	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to (N \in Fin \land R \in Ring)$
112	111	adantl	$⊢ (\neg K = 0 \land (N \in Fin \land R \in Ring \land K \in ℕ_{0})) \to (N \in Fin \land R \in Ring)$
113	4 62	mat0op	$⊢ (N \in Fin \land R \in Ring) \to 0_{A} = (i \in N, j \in N ⟼ 0_{R})$
114	5 113	syl5eq	$⊢ (N \in Fin \land R \in Ring) \to \underset{˙}{0} = (i \in N, j \in N ⟼ 0_{R})$
115	112 114	syl	$⊢ (\neg K = 0 \land (N \in Fin \land R \in Ring \land K \in ℕ_{0})) \to \underset{˙}{0} = (i \in N, j \in N ⟼ 0_{R})$
116	106 110 115	3eqtr4d	$⊢ (\neg K = 0 \land (N \in Fin \land R \in Ring \land K \in ℕ_{0})) \to (i \in N, j \in N ⟼ if (i = j, if (K = 0, 1_{Scalar (P)}, 0_{R}), 0_{R})) = \underset{˙}{0}$
117		iffalse	$⊢ \neg K = 0 \to if (K = 0, \underset{˙}{1}, \underset{˙}{0}) = \underset{˙}{0}$
118	117	eqcomd	$⊢ \neg K = 0 \to \underset{˙}{0} = if (K = 0, \underset{˙}{1}, \underset{˙}{0})$
119	118	adantr	$⊢ (\neg K = 0 \land (N \in Fin \land R \in Ring \land K \in ℕ_{0})) \to \underset{˙}{0} = if (K = 0, \underset{˙}{1}, \underset{˙}{0})$
120	116 119	eqtrd	$⊢ (\neg K = 0 \land (N \in Fin \land R \in Ring \land K \in ℕ_{0})) \to (i \in N, j \in N ⟼ if (i = j, if (K = 0, 1_{Scalar (P)}, 0_{R}), 0_{R})) = if (K = 0, \underset{˙}{1}, \underset{˙}{0})$
121	103 120	pm2.61ian	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to (i \in N, j \in N ⟼ if (i = j, if (K = 0, 1_{Scalar (P)}, 0_{R}), 0_{R})) = if (K = 0, \underset{˙}{1}, \underset{˙}{0})$
122	14 85 121	3eqtrd	$⊢ (N \in Fin \land R \in Ring \land K \in ℕ_{0}) \to I decompPMat K = if (K = 0, \underset{˙}{1}, \underset{˙}{0})$

Metamath Proof Explorer

Theorem decpmatid

Proof