Metamath Proof Explorer

Theorem mp2pm2mplem1

Description: Lemma 1 for mp2pm2mp . (Contributed by AV, 9-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))))$
	Assertion	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)))$

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		fveq2	$⊢ p = O \to {coe}_{1} (p) = {coe}_{1} (O)$
9	8	fveq1d	$⊢ p = O \to {coe}_{1} (p) (k) = {coe}_{1} (O) (k)$
10	9	oveqd	$⊢ p = O \to i {coe}_{1} (p) (k) j = i {coe}_{1} (O) (k) j$
11	10	oveq1d	$⊢ p = O \to (i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y) = (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)$
12	11	mpteq2dv	$⊢ p = O \to (k \in ℕ_{0} ⟼ (i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y)) = (k \in ℕ_{0} ⟼ (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))$
13	12	oveq2d	$⊢ p = O \to \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y)) = \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))$
14	13	mpoeq3dv	$⊢ p = O \to (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{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)))$
15		simp3	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to O \in L$
16		simp1	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to N \in Fin$
17		mpoexga	$⊢ (N \in Fin \land N \in Fin) \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 V$
18	16 16 17	syl2anc	$⊢ (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 V$
19	7 14 15 18	fvmptd3	$⊢ (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)))$