pmatcollpwscmatlem1

Description: Lemma 1 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	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})$

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	15	oveqi	$⊢ a M b = a (Q \underset{˙}{*} \underset{˙}{1}) b$
17	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
18	17	anim2i	$⊢ (N \in Fin \land R \in Ring) \to (N \in Fin \land P \in Ring)$
19		simpr	$⊢ (L \in ℕ_{0} \land Q \in E) \to Q \in E$
20	18 19	anim12i	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to ((N \in Fin \land P \in Ring) \land Q \in E)$
21		df-3an	$⊢ (N \in Fin \land P \in Ring \land Q \in E) \leftrightarrow ((N \in Fin \land P \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 P \in Ring \land Q \in E)$
23		eqid	$⊢ 0_{P} = 0_{P}$
24	2 12 23 14 4	scmatscmide	$⊢ ((N \in Fin \land P \in Ring \land Q \in E) \land (a \in N \land b \in N)) \to a (Q \underset{˙}{*} \underset{˙}{1}) b = if (a = b, Q, 0_{P})$
25	22 24	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 (Q \underset{˙}{*} \underset{˙}{1}) b = if (a = b, Q, 0_{P})$
26	16 25	eqtrid	$⊢ (((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 M b = if (a = b, Q, 0_{P})$
27	26	fveq2d	$⊢ (((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) = {coe}_{1} (if (a = b, Q, 0_{P}))$
28	27	fveq1d	$⊢ (((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) = {coe}_{1} (if (a = b, Q, 0_{P})) (L)$
29		fvif	$⊢ {coe}_{1} (if (a = b, Q, 0_{P})) = if (a = b, {coe}_{1} (Q), {coe}_{1} (0_{P}))$
30	29	fveq1i	$⊢ {coe}_{1} (if (a = b, Q, 0_{P})) (L) = if (a = b, {coe}_{1} (Q), {coe}_{1} (0_{P})) (L)$
31		iffv	$⊢ if (a = b, {coe}_{1} (Q), {coe}_{1} (0_{P})) (L) = if (a = b, {coe}_{1} (Q) (L), {coe}_{1} (0_{P}) (L))$
32	30 31	eqtri	$⊢ {coe}_{1} (if (a = b, Q, 0_{P})) (L) = if (a = b, {coe}_{1} (Q) (L), {coe}_{1} (0_{P}) (L))$
33	28 32	eqtrdi	$⊢ (((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) = if (a = b, {coe}_{1} (Q) (L), {coe}_{1} (0_{P}) (L))$
34	33	oveq1d	$⊢ (((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, {coe}_{1} (Q) (L), {coe}_{1} (0_{P}) (L)) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))$
35		ovif	$⊢ if (a = b, {coe}_{1} (Q) (L), {coe}_{1} (0_{P}) (L)) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) = if (a = b, {coe}_{1} (Q) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)), {coe}_{1} (0_{P}) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)))$
36		eqid	$⊢ 0_{R} = 0_{R}$
37	1 23 36	coe1z	$⊢ R \in Ring \to {coe}_{1} (0_{P}) = ℕ_{0} \times \{0_{R}\}$
38	37	ad2antlr	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to {coe}_{1} (0_{P}) = ℕ_{0} \times \{0_{R}\}$
39	38	fveq1d	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to {coe}_{1} (0_{P}) (L) = (ℕ_{0} \times \{0_{R}\}) (L)$
40		fvexd	$⊢ (N \in Fin \land R \in Ring) \to 0_{R} \in V$
41		simpl	$⊢ (L \in ℕ_{0} \land Q \in E) \to L \in ℕ_{0}$
42	40 41	anim12i	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to (0_{R} \in V \land L \in ℕ_{0})$
43		fvconst2g	$⊢ (0_{R} \in V \land L \in ℕ_{0}) \to (ℕ_{0} \times \{0_{R}\}) (L) = 0_{R}$
44	42 43	syl	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to (ℕ_{0} \times \{0_{R}\}) (L) = 0_{R}$
45	39 44	eqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to {coe}_{1} (0_{P}) (L) = 0_{R}$
46	45	oveq1d	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to {coe}_{1} (0_{P}) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) = 0_{R} \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))$
47	1	ply1lmod	$⊢ R \in Ring \to P \in LMod$
48	47	ad2antlr	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to P \in LMod$
49		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
50	49 12	mgpbas	$⊢ E = {Base}_{{mulGrp}_{P}}$
51		eqid	$⊢ \cdot_{{mulGrp}_{P}} = \cdot_{{mulGrp}_{P}}$
52	49	ringmgp	$⊢ P \in Ring \to {mulGrp}_{P} \in Mnd$
53	17 52	syl	$⊢ R \in Ring \to {mulGrp}_{P} \in Mnd$
54		0nn0	$⊢ 0 \in ℕ_{0}$
55	54	a1i	$⊢ R \in Ring \to 0 \in ℕ_{0}$
56		eqid	$⊢ {var}_{1} (R) = {var}_{1} (R)$
57	56 1 12	vr1cl	$⊢ R \in Ring \to {var}_{1} (R) \in E$
58	50 51 53 55 57	mulgnn0cld	$⊢ R \in Ring \to 0 \cdot_{{mulGrp}_{P}} {var}_{1} (R) \in E$
59	58	ad2antlr	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to 0 \cdot_{{mulGrp}_{P}} {var}_{1} (R) \in E$
60		eqid	$⊢ Scalar (P) = Scalar (P)$
61		eqid	$⊢ \cdot_{P} = \cdot_{P}$
62		eqid	$⊢ 0_{Scalar (P)} = 0_{Scalar (P)}$
63	12 60 61 62 23	lmod0vs	$⊢ (P \in LMod \land 0 \cdot_{{mulGrp}_{P}} {var}_{1} (R) \in E) \to 0_{Scalar (P)} \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) = 0_{P}$
64	48 59 63	syl2anc	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to 0_{Scalar (P)} \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) = 0_{P}$
65	1	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
66	65	adantl	$⊢ (N \in Fin \land R \in Ring) \to R = Scalar (P)$
67	66	fveq2d	$⊢ (N \in Fin \land R \in Ring) \to 0_{R} = 0_{Scalar (P)}$
68	67	oveq1d	$⊢ (N \in Fin \land R \in Ring) \to 0_{R} \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) = 0_{Scalar (P)} \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))$
69	68	eqeq1d	$⊢ (N \in Fin \land R \in Ring) \to (0_{R} \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) = 0_{P} \leftrightarrow 0_{Scalar (P)} \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) = 0_{P})$
70	69	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to (0_{R} \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) = 0_{P} \leftrightarrow 0_{Scalar (P)} \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) = 0_{P})$
71	64 70	mpbird	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to 0_{R} \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) = 0_{P}$
72	46 71	eqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to {coe}_{1} (0_{P}) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) = 0_{P}$
73	72	ifeq2d	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to if (a = b, {coe}_{1} (Q) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)), {coe}_{1} (0_{P}) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))) = if (a = b, {coe}_{1} (Q) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)), 0_{P})$
74	73	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land (a \in N \land b \in N)) \to if (a = b, {coe}_{1} (Q) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)), {coe}_{1} (0_{P}) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))) = if (a = b, {coe}_{1} (Q) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)), 0_{P})$
75	35 74	eqtrid	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land (a \in N \land b \in N)) \to if (a = b, {coe}_{1} (Q) (L), {coe}_{1} (0_{P}) (L)) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) = if (a = b, {coe}_{1} (Q) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)), 0_{P})$
76		simpr	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to (L \in ℕ_{0} \land Q \in E)$
77	76	ancomd	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to (Q \in E \land L \in ℕ_{0})$
78		eqid	$⊢ {coe}_{1} (Q) = {coe}_{1} (Q)$
79	78 12 1 11	coe1fvalcl	$⊢ (Q \in E \land L \in ℕ_{0}) \to {coe}_{1} (Q) (L) \in K$
80	77 79	syl	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to {coe}_{1} (Q) (L) \in K$
81	65	eqcomd	$⊢ R \in Ring \to Scalar (P) = R$
82	81	adantl	$⊢ (N \in Fin \land R \in Ring) \to Scalar (P) = R$
83	82	fveq2d	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{Scalar (P)} = {Base}_{R}$
84	83 11	eqtr4di	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{Scalar (P)} = K$
85	84	eleq2d	$⊢ (N \in Fin \land R \in Ring) \to ({coe}_{1} (Q) (L) \in {Base}_{Scalar (P)} \leftrightarrow {coe}_{1} (Q) (L) \in K)$
86	85	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to ({coe}_{1} (Q) (L) \in {Base}_{Scalar (P)} \leftrightarrow {coe}_{1} (Q) (L) \in K)$
87	80 86	mpbird	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to {coe}_{1} (Q) (L) \in {Base}_{Scalar (P)}$
88		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
89		eqid	$⊢ 1_{P} = 1_{P}$
90	10 60 88 61 89	asclval	$⊢ {coe}_{1} (Q) (L) \in {Base}_{Scalar (P)} \to U ({coe}_{1} (Q) (L)) = {coe}_{1} (Q) (L) \cdot_{P} 1_{P}$
91	87 90	syl	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to U ({coe}_{1} (Q) (L)) = {coe}_{1} (Q) (L) \cdot_{P} 1_{P}$
92	1 56 49 51	ply1idvr1	$⊢ R \in Ring \to 0 \cdot_{{mulGrp}_{P}} {var}_{1} (R) = 1_{P}$
93	92	eqcomd	$⊢ R \in Ring \to 1_{P} = 0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)$
94	93	ad2antlr	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to 1_{P} = 0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)$
95	94	oveq2d	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to {coe}_{1} (Q) (L) \cdot_{P} 1_{P} = {coe}_{1} (Q) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))$
96	91 95	eqtr2d	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to {coe}_{1} (Q) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) = U ({coe}_{1} (Q) (L))$
97	96	ifeq1d	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to if (a = b, {coe}_{1} (Q) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)), 0_{P}) = if (a = b, U ({coe}_{1} (Q) (L)), 0_{P})$
98	97	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \land (a \in N \land b \in N)) \to if (a = b, {coe}_{1} (Q) (L) \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)), 0_{P}) = if (a = b, U ({coe}_{1} (Q) (L)), 0_{P})$
99	34 75 98	3eqtrd	$⊢ (((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})$

Metamath Proof Explorer

Theorem pmatcollpwscmatlem1

Proof