mp2pm2mplem3

Description: Lemma 3 for mp2pm2mp . (Contributed by AV, 10-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)$
Assertion	mp2pm2mplem3	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to I (O) decompPMat K = (i \in N, j \in N ⟼ {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) (K))$

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	1 2 3 4 5 6 7	mp2pm2mplem1	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to I (O) = (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)))$
10	9	oveq1d	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to I (O) decompPMat K = (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) decompPMat K$
11	10	adantr	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to I (O) decompPMat K = (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) decompPMat K$
12		eqid	$⊢ N Mat P = N Mat P$
13		eqid	$⊢ {Base}_{(N Mat P)} = {Base}_{(N Mat P)}$
14	1 2 3 4 5 6 7 8 12 13	mp2pm2mplem2	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) \in {Base}_{(N Mat P)}$
15	12 13	decpmatval	$⊢ ((i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) \in {Base}_{(N Mat P)} \land K \in ℕ_{0}) \to (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) decompPMat K = (a \in N, b \in N ⟼ {coe}_{1} (a (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) b) (K))$
16	14 15	sylan	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) decompPMat K = (a \in N, b \in N ⟼ {coe}_{1} (a (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) b) (K))$
17		eqidd	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land a \in N \land b \in N) \to (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) = (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)))$
18		oveq12	$⊢ (i = a \land j = b) \to i {coe}_{1} (O) (k) j = a {coe}_{1} (O) (k) b$
19	18	oveq1d	$⊢ (i = a \land j = b) \to (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y) = (a {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y)$
20	19	mpteq2dv	$⊢ (i = a \land j = b) \to (k \in ℕ_{0} ⟼ (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)) = (k \in ℕ_{0} ⟼ (a {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y))$
21	20	oveq2d	$⊢ (i = a \land j = b) \to \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)) = \underset{k \in ℕ_{0}}{\sum_{P}} ((a {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y))$
22	21	adantl	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land a \in N \land b \in N) \land (i = a \land j = b)) \to \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)) = \underset{k \in ℕ_{0}}{\sum_{P}} ((a {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y))$
23		simp2	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land a \in N \land b \in N) \to a \in N$
24		simp3	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land a \in N \land b \in N) \to b \in N$
25		ovexd	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land a \in N \land b \in N) \to \underset{k \in ℕ_{0}}{\sum_{P}} ((a {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y)) \in V$
26	17 22 23 24 25	ovmpod	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land a \in N \land b \in N) \to a (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) b = \underset{k \in ℕ_{0}}{\sum_{P}} ((a {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y))$
27	26	fveq2d	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land a \in N \land b \in N) \to {coe}_{1} (a (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) b) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((a {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y)))$
28	27	fveq1d	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land a \in N \land b \in N) \to {coe}_{1} (a (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) b) (K) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((a {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y))) (K)$
29	28	mpoeq3dva	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to (a \in N, b \in N ⟼ {coe}_{1} (a (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) b) (K)) = (a \in N, b \in N ⟼ {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((a {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y))) (K))$
30		oveq1	$⊢ a = i \to a {coe}_{1} (O) (k) b = i {coe}_{1} (O) (k) b$
31	30	oveq1d	$⊢ a = i \to (a {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y) = (i {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y)$
32	31	mpteq2dv	$⊢ a = i \to (k \in ℕ_{0} ⟼ (a {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y)) = (k \in ℕ_{0} ⟼ (i {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y))$
33	32	oveq2d	$⊢ a = i \to \underset{k \in ℕ_{0}}{\sum_{P}} ((a {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y)) = \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y))$
34	33	fveq2d	$⊢ a = i \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((a {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y))) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y)))$
35	34	fveq1d	$⊢ a = i \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((a {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y))) (K) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y))) (K)$
36		simpl	$⊢ (b = j \land k \in ℕ_{0}) \to b = j$
37	36	oveq2d	$⊢ (b = j \land k \in ℕ_{0}) \to i {coe}_{1} (O) (k) b = i {coe}_{1} (O) (k) j$
38	37	oveq1d	$⊢ (b = j \land k \in ℕ_{0}) \to (i {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y) = (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)$
39	38	mpteq2dva	$⊢ b = j \to (k \in ℕ_{0} ⟼ (i {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y)) = (k \in ℕ_{0} ⟼ (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))$
40	39	oveq2d	$⊢ b = j \to \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y)) = \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))$
41	40	fveq2d	$⊢ b = j \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y))) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)))$
42	41	fveq1d	$⊢ b = j \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y))) (K) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) (K)$
43	35 42	cbvmpov	$⊢ (a \in N, b \in N ⟼ {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((a {coe}_{1} (O) (k) b) \underset{˙}{\cdot} (k E Y))) (K)) = (i \in N, j \in N ⟼ {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) (K))$
44	29 43	eqtrdi	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to (a \in N, b \in N ⟼ {coe}_{1} (a (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) b) (K)) = (i \in N, j \in N ⟼ {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) (K))$
45	11 16 44	3eqtrd	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to I (O) decompPMat K = (i \in N, j \in N ⟼ {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) (K))$

Metamath Proof Explorer

Theorem mp2pm2mplem3

Proof