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	syl5eq	$⊢ (((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	ringmgp	$⊢ P \in Ring \to {mulGrp}_{P} \in Mnd$
51	17 50	syl	$⊢ R \in Ring \to {mulGrp}_{P} \in Mnd$
52		0nn0	$⊢ 0 \in ℕ_{0}$
53	52	a1i	$⊢ R \in Ring \to 0 \in ℕ_{0}$
54		eqid	$⊢ {var}_{1} (R) = {var}_{1} (R)$
55	54 1 12	vr1cl	$⊢ R \in Ring \to {var}_{1} (R) \in E$
56	49 12	mgpbas	$⊢ E = {Base}_{{mulGrp}_{P}}$
57		eqid	$⊢ \cdot_{{mulGrp}_{P}} = \cdot_{{mulGrp}_{P}}$
58	56 57	mulgnn0cl	$⊢ ({mulGrp}_{P} \in Mnd \land 0 \in ℕ_{0} \land {var}_{1} (R) \in E) \to 0 \cdot_{{mulGrp}_{P}} {var}_{1} (R) \in E$
59	51 53 55 58	syl3anc	$⊢ R \in Ring \to 0 \cdot_{{mulGrp}_{P}} {var}_{1} (R) \in E$
60	59	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$
61		eqid	$⊢ Scalar (P) = Scalar (P)$
62		eqid	$⊢ \cdot_{P} = \cdot_{P}$
63		eqid	$⊢ 0_{Scalar (P)} = 0_{Scalar (P)}$
64	12 61 62 63 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}$
65	48 60 64	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}$
66	1	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
67	66	adantl	$⊢ (N \in Fin \land R \in Ring) \to R = Scalar (P)$
68	67	fveq2d	$⊢ (N \in Fin \land R \in Ring) \to 0_{R} = 0_{Scalar (P)}$
69	68	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))$
70	69	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})$
71	70	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})$
72	65 71	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}$
73	46 72	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}$
74	73	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})$
75	74	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})$
76	35 75	syl5eq	$⊢ (((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})$
77		simpr	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to (L \in ℕ_{0} \land Q \in E)$
78	77	ancomd	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to (Q \in E \land L \in ℕ_{0})$
79		eqid	$⊢ {coe}_{1} (Q) = {coe}_{1} (Q)$
80	79 12 1 11	coe1fvalcl	$⊢ (Q \in E \land L \in ℕ_{0}) \to {coe}_{1} (Q) (L) \in K$
81	78 80	syl	$⊢ ((N \in Fin \land R \in Ring) \land (L \in ℕ_{0} \land Q \in E)) \to {coe}_{1} (Q) (L) \in K$
82	66	eqcomd	$⊢ R \in Ring \to Scalar (P) = R$
83	82	adantl	$⊢ (N \in Fin \land R \in Ring) \to Scalar (P) = R$
84	83	fveq2d	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{Scalar (P)} = {Base}_{R}$
85	84 11	eqtr4di	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{Scalar (P)} = K$
86	85	eleq2d	$⊢ (N \in Fin \land R \in Ring) \to ({coe}_{1} (Q) (L) \in {Base}_{Scalar (P)} \leftrightarrow {coe}_{1} (Q) (L) \in K)$
87	86	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)$
88	81 87	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)}$
89		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
90		eqid	$⊢ 1_{P} = 1_{P}$
91	10 61 89 62 90	asclval	$⊢ {coe}_{1} (Q) (L) \in {Base}_{Scalar (P)} \to U ({coe}_{1} (Q) (L)) = {coe}_{1} (Q) (L) \cdot_{P} 1_{P}$
92	88 91	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}$
93	1 54 49 57	ply1idvr1	$⊢ R \in Ring \to 0 \cdot_{{mulGrp}_{P}} {var}_{1} (R) = 1_{P}$
94	93	eqcomd	$⊢ R \in Ring \to 1_{P} = 0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)$
95	94	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)$
96	95	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))$
97	92 96	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))$
98	97	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})$
99	98	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})$
100	34 76 99	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