pmatcollpwscmatlem2

Description: Lemma 2 for pmatcollpwscmat . (Contributed by AV, 2-Nov-2019) (Revised by AV, 4-Dec-2019)

	Ref	Expression
Hypotheses	pmatcollpwscmat.p	$⊢ P = {Poly}_{1} (R)$
	pmatcollpwscmat.c	$⊢ C = N Mat P$
	pmatcollpwscmat.b	$⊢ B = {Base}_{C}$
	pmatcollpwscmat.m1	$⊢ \underset{˙}{*} = \cdot_{C}$
	pmatcollpwscmat.e1	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
	pmatcollpwscmat.x	$⊢ X = {var}_{1} (R)$
	pmatcollpwscmat.t	$⊢ T = N matToPolyMat R$
	pmatcollpwscmat.a	$⊢ A = N Mat R$
	pmatcollpwscmat.d	$⊢ D = {Base}_{A}$
	pmatcollpwscmat.u	$⊢ U = algSc (P)$
	pmatcollpwscmat.k	$⊢ K = {Base}_{R}$
	pmatcollpwscmat.e2	$⊢ E = {Base}_{P}$
	pmatcollpwscmat.s	$⊢ S = algSc (P)$
	pmatcollpwscmat.1	$⊢ \underset{˙}{1} = 1_{C}$
	pmatcollpwscmat.m2	$⊢ M = Q \underset{˙}{*} \underset{˙}{1}$
Assertion	pmatcollpwscmatlem2	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to T (M decompPMat L) = U ({coe}_{1} (Q) (L)) \underset{˙}{*} \underset{˙}{1}$

Proof

Step	Hyp	Ref	Expression
1		pmatcollpwscmat.p	$⊢ P = {Poly}_{1} (R)$
2		pmatcollpwscmat.c	$⊢ C = N Mat P$
3		pmatcollpwscmat.b	$⊢ B = {Base}_{C}$
4		pmatcollpwscmat.m1	$⊢ \underset{˙}{*} = \cdot_{C}$
5		pmatcollpwscmat.e1	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
6		pmatcollpwscmat.x	$⊢ X = {var}_{1} (R)$
7		pmatcollpwscmat.t	$⊢ T = N matToPolyMat R$
8		pmatcollpwscmat.a	$⊢ A = N Mat R$
9		pmatcollpwscmat.d	$⊢ D = {Base}_{A}$
10		pmatcollpwscmat.u	$⊢ U = algSc (P)$
11		pmatcollpwscmat.k	$⊢ K = {Base}_{R}$
12		pmatcollpwscmat.e2	$⊢ E = {Base}_{P}$
13		pmatcollpwscmat.s	$⊢ S = algSc (P)$
14		pmatcollpwscmat.1	$⊢ \underset{˙}{1} = 1_{C}$
15		pmatcollpwscmat.m2	$⊢ M = Q \underset{˙}{*} \underset{˙}{1}$
16		simpl	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to (N \in Fin \land R \in Ring)$
17		simpr	$⊢ (N \in Fin \land R \in Ring) \to R \in Ring$
18	17	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to R \in Ring$
19		simpr	$⊢ (L \in ℕ_{0} \land Q \in E) \to Q \in E$
20	19	anim2i	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to ((N \in Fin \land R \in Ring) \land Q \in E)$
21		df-3an	$⊢ (N \in Fin \land R \in Ring \land Q \in E) \leftrightarrow ((N \in Fin \land R \in Ring) \land Q \in E)$
22	20 21	sylibr	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to (N \in Fin \land R \in Ring \land Q \in E)$
23	1 2 3 12 4 14	1pmatscmul	$⊢ (N \in Fin \land R \in Ring \land Q \in E) \to Q \underset{˙}{*} \underset{˙}{1} \in B$
24	15 23	eqeltrid	$⊢ (N \in Fin \land R \in Ring \land Q \in E) \to M \in B$
25	22 24	syl	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to M \in B$
26		simprl	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to L \in ℕ_{0}$
27	1 2 3 8 9	decpmatcl	$⊢ (R \in Ring \land M \in B \land L \in ℕ_{0}) \to M decompPMat L \in D$
28	18 25 26 27	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to M decompPMat L \in D$
29		df-3an	$⊢ (N \in Fin \land R \in Ring \land M decompPMat L \in D) \leftrightarrow ((N \in Fin \land R \in Ring) \land M decompPMat L \in D)$
30	16 28 29	sylanbrc	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to (N \in Fin \land R \in Ring \land M decompPMat L \in D)$
31		eqid	$⊢ algSc (P) = algSc (P)$
32	7 8 9 1 31	mat2pmatval	$⊢ (N \in Fin \land R \in Ring \land M decompPMat L \in D) \to T (M decompPMat L) = (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat L) j))$
33	30 32	syl	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to T (M decompPMat L) = (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat L) j))$
34	18 25 26	3jca	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to (R \in Ring \land M \in B \land L \in ℕ_{0})$
35	34	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land i \in N \land j \in N) \to (R \in Ring \land M \in B \land L \in ℕ_{0})$
36		3simpc	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land i \in N \land j \in N) \to (i \in N \land j \in N)$
37	1 2 3	decpmate	$⊢ ((R \in Ring \land M \in B \land L \in ℕ_{0}) \land (i \in N \land j \in N)) \to i (M decompPMat L) j = {coe}_{1} (i M j) (L)$
38	35 36 37	syl2anc	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land i \in N \land j \in N) \to i (M decompPMat L) j = {coe}_{1} (i M j) (L)$
39	38	fveq2d	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land i \in N \land j \in N) \to algSc (P) (i (M decompPMat L) j) = algSc (P) ({coe}_{1} (i M j) (L))$
40	39	mpoeq3dva	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat L) j)) = (i \in N, j \in N ⟼ algSc (P) ({coe}_{1} (i M j) (L)))$
41		simp1lr	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land i \in N \land j \in N) \to R \in Ring$
42		simp2	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land i \in N \land j \in N) \to i \in N$
43		simp3	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land i \in N \land j \in N) \to j \in N$
44	25	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land i \in N \land j \in N) \to M \in B$
45	2 12 3 42 43 44	matecld	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land i \in N \land j \in N) \to i M j \in E$
46	26	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land i \in N \land j \in N) \to L \in ℕ_{0}$
47		eqid	$⊢ {coe}_{1} (i M j) = {coe}_{1} (i M j)$
48	47 12 1 11	coe1fvalcl	$⊢ (i M j \in E \land L \in ℕ_{0}) \to {coe}_{1} (i M j) (L) \in K$
49	45 46 48	syl2anc	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land i \in N \land j \in N) \to {coe}_{1} (i M j) (L) \in K$
50		eqid	$⊢ {var}_{1} (R) = {var}_{1} (R)$
51		eqid	$⊢ \cdot_{P} = \cdot_{P}$
52		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
53		eqid	$⊢ \cdot_{{mulGrp}_{P}} = \cdot_{{mulGrp}_{P}}$
54	11 1 50 51 52 53 31	ply1scltm	$⊢ (R \in Ring \land {coe}_{1} (i M j) (L) \in K) \to algSc (P) ({coe}_{1} (i M j) (L)) = {coe}_{1} (i M j) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))$
55	41 49 54	syl2anc	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land i \in N \land j \in N) \to algSc (P) ({coe}_{1} (i M j) (L)) = {coe}_{1} (i M j) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))$
56	55	mpoeq3dva	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to (i \in N, j \in N ⟼ algSc (P) ({coe}_{1} (i M j) (L))) = (i \in N, j \in N ⟼ {coe}_{1} (i M j) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)))$
57	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	pmatcollpwscmatlem1	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land (a \in N \land b \in N)) \to {coe}_{1} (a M b) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) = if (a = b, U ({coe}_{1} (Q) (L)), 0_{P})$
58		eqidd	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land (a \in N \land b \in N)) \to (i \in N, j \in N ⟼ {coe}_{1} (i M j) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))) = (i \in N, j \in N ⟼ {coe}_{1} (i M j) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)))$
59		oveq12	$⊢ (i = a \land j = b) \to i M j = a M b$
60	59	fveq2d	$⊢ (i = a \land j = b) \to {coe}_{1} (i M j) = {coe}_{1} (a M b)$
61	60	fveq1d	$⊢ (i = a \land j = b) \to {coe}_{1} (i M j) (L) = {coe}_{1} (a M b) (L)$
62	61	oveq1d	$⊢ (i = a \land j = b) \to {coe}_{1} (i M j) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) = {coe}_{1} (a M b) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))$
63	62	adantl	$⊢ ((((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land (a \in N \land b \in N)) \land (i = a \land j = b)) \to {coe}_{1} (i M j) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) = {coe}_{1} (a M b) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))$
64		simprl	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land (a \in N \land b \in N)) \to a \in N$
65		simprr	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land (a \in N \land b \in N)) \to b \in N$
66		ovexd	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land (a \in N \land b \in N)) \to {coe}_{1} (a M b) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \in V$
67	58 63 64 65 66	ovmpod	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land (a \in N \land b \in N)) \to a (i \in N, j \in N ⟼ {coe}_{1} (i M j) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))) b = {coe}_{1} (a M b) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))$
68		simpll	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to N \in Fin$
69	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
70	69	adantl	$⊢ (N \in Fin \land R \in Ring) \to P \in Ring$
71	70	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to P \in Ring$
72		pm3.22	$⊢ (L \in ℕ_{0} \land Q \in E) \to (Q \in E \land L \in ℕ_{0})$
73	72	adantl	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to (Q \in E \land L \in ℕ_{0})$
74		eqid	$⊢ {coe}_{1} (Q) = {coe}_{1} (Q)$
75	74 12 1 11	coe1fvalcl	$⊢ (Q \in E \land L \in ℕ_{0}) \to {coe}_{1} (Q) (L) \in K$
76	73 75	syl	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to {coe}_{1} (Q) (L) \in K$
77	1 10 11 12	ply1sclcl	$⊢ (R \in Ring \land {coe}_{1} (Q) (L) \in K) \to U ({coe}_{1} (Q) (L)) \in E$
78	18 76 77	syl2anc	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to U ({coe}_{1} (Q) (L)) \in E$
79	68 71 78	3jca	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to (N \in Fin \land P \in Ring \land U ({coe}_{1} (Q) (L)) \in E)$
80		eqid	$⊢ 0_{P} = 0_{P}$
81	2 12 80 14 4	scmatscmide	$⊢ ((N \in Fin \land P \in Ring \land U ({coe}_{1} (Q) (L)) \in E) \land (a \in N \land b \in N)) \to a (U ({coe}_{1} (Q) (L)) \underset{˙}{*} \underset{˙}{1}) b = if (a = b, U ({coe}_{1} (Q) (L)), 0_{P})$
82	79 81	sylan	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land (a \in N \land b \in N)) \to a (U ({coe}_{1} (Q) (L)) \underset{˙}{*} \underset{˙}{1}) b = if (a = b, U ({coe}_{1} (Q) (L)), 0_{P})$
83	57 67 82	3eqtr4d	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land (a \in N \land b \in N)) \to a (i \in N, j \in N ⟼ {coe}_{1} (i M j) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))) b = a (U ({coe}_{1} (Q) (L)) \underset{˙}{*} \underset{˙}{1}) b$
84	83	ralrimivva	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to \forall a \in N \forall b \in N a (i \in N, j \in N ⟼ {coe}_{1} (i M j) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))) b = a (U ({coe}_{1} (Q) (L)) \underset{˙}{*} \underset{˙}{1}) b$
85		0nn0	$⊢ 0 \in ℕ_{0}$
86	85	a1i	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land i \in N \land j \in N) \to 0 \in ℕ_{0}$
87	11 1 50 51 52 53 12	ply1tmcl	$⊢ (R \in Ring \land {coe}_{1} (i M j) (L) \in K \land 0 \in ℕ_{0}) \to {coe}_{1} (i M j) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \in E$
88	41 49 86 87	syl3anc	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land i \in N \land j \in N) \to {coe}_{1} (i M j) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \in E$
89	2 12 3 68 71 88	matbas2d	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to (i \in N, j \in N ⟼ {coe}_{1} (i M j) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))) \in B$
90	1 2 3 12 4 14	1pmatscmul	$⊢ (N \in Fin \land R \in Ring \land U ({coe}_{1} (Q) (L)) \in E) \to U ({coe}_{1} (Q) (L)) \underset{˙}{*} \underset{˙}{1} \in B$
91	68 18 78 90	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to U ({coe}_{1} (Q) (L)) \underset{˙}{*} \underset{˙}{1} \in B$
92	2 3	eqmat	$⊢ ((i \in N, j \in N ⟼ {coe}_{1} (i M j) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))) \in B \land U ({coe}_{1} (Q) (L)) \underset{˙}{} \underset{˙}{1} \in B) \to ((i \in N, j \in N ⟼ {coe}_{1} (i M j) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))) = U ({coe}_{1} (Q) (L)) \underset{˙}{} \underset{˙}{1} \leftrightarrow \forall a \in N \forall b \in N a (i \in N, j \in N ⟼ {coe}_{1} (i M j) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))) b = a (U ({coe}_{1} (Q) (L)) \underset{˙}{*} \underset{˙}{1}) b)$
93	89 91 92	syl2anc	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to ((i \in N, j \in N ⟼ {coe}_{1} (i M j) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))) = U ({coe}_{1} (Q) (L)) \underset{˙}{} \underset{˙}{1} \leftrightarrow \forall a \in N \forall b \in N a (i \in N, j \in N ⟼ {coe}_{1} (i M j) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))) b = a (U ({coe}_{1} (Q) (L)) \underset{˙}{} \underset{˙}{1}) b)$
94	84 93	mpbird	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to (i \in N, j \in N ⟼ {coe}_{1} (i M j) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))) = U ({coe}_{1} (Q) (L)) \underset{˙}{*} \underset{˙}{1}$
95	56 94	eqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to (i \in N, j \in N ⟼ algSc (P) ({coe}_{1} (i M j) (L))) = U ({coe}_{1} (Q) (L)) \underset{˙}{*} \underset{˙}{1}$
96	33 40 95	3eqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to T (M decompPMat L) = U ({coe}_{1} (Q) (L)) \underset{˙}{*} \underset{˙}{1}$

Metamath Proof Explorer

Theorem pmatcollpwscmatlem2

Proof