mp2pm2mplem5

Description: Lemma 5 for mp2pm2mp . (Contributed by AV, 12-Oct-2019) (Revised by AV, 5-Dec-2019)

	Ref	Expression
Hypotheses	mp2pm2mp.a	$⊢ A = N Mat R$
	mp2pm2mp.q	$⊢ Q = {Poly}_{1} (A)$
	mp2pm2mp.l	$⊢ L = {Base}_{Q}$
	mp2pm2mp.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	mp2pm2mp.e	$⊢ E = \cdot_{{mulGrp}_{P}}$
	mp2pm2mp.y	$⊢ Y = {var}_{1} (R)$
	mp2pm2mp.i	$⊢ I = (p \in L ⟼ (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y))))$
	mp2pm2mplem2.p	$⊢ P = {Poly}_{1} (R)$
	mp2pm2mplem5.m	$⊢ \underset{˙}{*} = \cdot_{Q}$
	mp2pm2mplem5.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Q}}$
	mp2pm2mplem5.x	$⊢ X = {var}_{1} (A)$
Assertion	mp2pm2mplem5	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to {finSupp}_{0_{Q}} ((k \in ℕ_{0} ⟼ (I (O) decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X)))$

Proof

Step	Hyp	Ref	Expression
1		mp2pm2mp.a	$⊢ A = N Mat R$
2		mp2pm2mp.q	$⊢ Q = {Poly}_{1} (A)$
3		mp2pm2mp.l	$⊢ L = {Base}_{Q}$
4		mp2pm2mp.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
5		mp2pm2mp.e	$⊢ E = \cdot_{{mulGrp}_{P}}$
6		mp2pm2mp.y	$⊢ Y = {var}_{1} (R)$
7		mp2pm2mp.i	$⊢ I = (p \in L ⟼ (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y))))$
8		mp2pm2mplem2.p	$⊢ P = {Poly}_{1} (R)$
9		mp2pm2mplem5.m	$⊢ \underset{˙}{*} = \cdot_{Q}$
10		mp2pm2mplem5.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Q}}$
11		mp2pm2mplem5.x	$⊢ X = {var}_{1} (A)$
12		nn0ex	$⊢ ℕ_{0} \in V$
13	12	a1i	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to ℕ_{0} \in V$
14	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
15	2	ply1lmod	$⊢ A \in Ring \to Q \in LMod$
16	14 15	syl	$⊢ (N \in Fin \land R \in Ring) \to Q \in LMod$
17	16	3adant3	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to Q \in LMod$
18	14	3adant3	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to A \in Ring$
19	2	ply1sca	$⊢ A \in Ring \to A = Scalar (Q)$
20	18 19	syl	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to A = Scalar (Q)$
21		simpl2	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land k \in ℕ_{0}) \to R \in Ring$
22		eqid	$⊢ N Mat P = N Mat P$
23		eqid	$⊢ {Base}_{(N Mat P)} = {Base}_{(N Mat P)}$
24	1 2 3 8 4 5 6 7 22 23	mply1topmatcl	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to I (O) \in {Base}_{(N Mat P)}$
25	24	adantr	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land k \in ℕ_{0}) \to I (O) \in {Base}_{(N Mat P)}$
26		simpr	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
27		eqid	$⊢ {Base}_{A} = {Base}_{A}$
28	8 22 23 1 27	decpmatcl	$⊢ (R \in Ring \land I (O) \in {Base}_{(N Mat P)} \land k \in ℕ_{0}) \to I (O) decompPMat k \in {Base}_{A}$
29	21 25 26 28	syl3anc	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land k \in ℕ_{0}) \to I (O) decompPMat k \in {Base}_{A}$
30		eqid	$⊢ {mulGrp}_{Q} = {mulGrp}_{Q}$
31	2 11 30 10 3	ply1moncl	$⊢ (A \in Ring \land k \in ℕ_{0}) \to k \underset{˙}{\times} X \in L$
32	18 31	sylan	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land k \in ℕ_{0}) \to k \underset{˙}{\times} X \in L$
33		eqid	$⊢ 0_{Q} = 0_{Q}$
34		eqid	$⊢ 0_{A} = 0_{A}$
35		fveq2	$⊢ k = l \to {coe}_{1} (p) (k) = {coe}_{1} (p) (l)$
36	35	oveqd	$⊢ k = l \to i {coe}_{1} (p) (k) j = i {coe}_{1} (p) (l) j$
37		oveq1	$⊢ k = l \to k E Y = l E Y$
38	36 37	oveq12d	$⊢ k = l \to (i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y) = (i {coe}_{1} (p) (l) j) \underset{˙}{\cdot} (l E Y)$
39	38	cbvmptv	$⊢ (k \in ℕ_{0} ⟼ (i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y)) = (l \in ℕ_{0} ⟼ (i {coe}_{1} (p) (l) j) \underset{˙}{\cdot} (l E Y))$
40	39	oveq2i	$⊢ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y)) = \underset{l \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (l) j) \underset{˙}{\cdot} (l E Y))$
41	40	a1i	$⊢ (i \in N \land j \in N) \to \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y)) = \underset{l \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (l) j) \underset{˙}{\cdot} (l E Y))$
42	41	mpoeq3ia	$⊢ (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y))) = (i \in N, j \in N ⟼ \underset{l \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (l) j) \underset{˙}{\cdot} (l E Y)))$
43	42	mpteq2i	$⊢ (p \in L ⟼ (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y)))) = (p \in L ⟼ (i \in N, j \in N ⟼ \underset{l \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (l) j) \underset{˙}{\cdot} (l E Y))))$
44	7 43	eqtri	$⊢ I = (p \in L ⟼ (i \in N, j \in N ⟼ \underset{l \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (l) j) \underset{˙}{\cdot} (l E Y))))$
45	1 2 3 4 5 6 44 8	mp2pm2mplem4	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land k \in ℕ_{0}) \to I (O) decompPMat k = {coe}_{1} (O) (k)$
46	45	mpteq2dva	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to (k \in ℕ_{0} ⟼ I (O) decompPMat k) = (k \in ℕ_{0} ⟼ {coe}_{1} (O) (k))$
47	2 3 34	mptcoe1fsupp	$⊢ (A \in Ring \land O \in L) \to {finSupp}_{0_{A}} ((k \in ℕ_{0} ⟼ {coe}_{1} (O) (k)))$
48	14 47	stoic3	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to {finSupp}_{0_{A}} ((k \in ℕ_{0} ⟼ {coe}_{1} (O) (k)))$
49	46 48	eqbrtrd	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to {finSupp}_{0_{A}} ((k \in ℕ_{0} ⟼ I (O) decompPMat k))$
50	13 17 20 3 29 32 33 34 9 49	mptscmfsupp0	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to {finSupp}_{0_{Q}} ((k \in ℕ_{0} ⟼ (I (O) decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X)))$

Metamath Proof Explorer

Theorem mp2pm2mplem5

Proof