pm2mpf1lem

Description: Lemma for pm2mpf1 . (Contributed by AV, 14-Oct-2019) (Revised by AV, 4-Dec-2019)

	Ref	Expression
Hypotheses	pm2mpf1lem.p	$⊢ P = {Poly}_{1} (R)$
	pm2mpf1lem.c	$⊢ C = N Mat P$
	pm2mpf1lem.b	$⊢ B = {Base}_{C}$
	pm2mpf1lem.m	$⊢ \underset{˙}{*} = \cdot_{Q}$
	pm2mpf1lem.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Q}}$
	pm2mpf1lem.x	$⊢ X = {var}_{1} (A)$
	pm2mpf1lem.a	$⊢ A = N Mat R$
	pm2mpf1lem.q	$⊢ Q = {Poly}_{1} (A)$
Assertion	pm2mpf1lem	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land K \in ℕ_{0})) \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((U decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))) (K) = U decompPMat K$

Proof

Step	Hyp	Ref	Expression
1		pm2mpf1lem.p	$⊢ P = {Poly}_{1} (R)$
2		pm2mpf1lem.c	$⊢ C = N Mat P$
3		pm2mpf1lem.b	$⊢ B = {Base}_{C}$
4		pm2mpf1lem.m	$⊢ \underset{˙}{*} = \cdot_{Q}$
5		pm2mpf1lem.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Q}}$
6		pm2mpf1lem.x	$⊢ X = {var}_{1} (A)$
7		pm2mpf1lem.a	$⊢ A = N Mat R$
8		pm2mpf1lem.q	$⊢ Q = {Poly}_{1} (A)$
9		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
10	7	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
11	10	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land K \in ℕ_{0})) \to A \in Ring$
12		eqid	$⊢ {Base}_{A} = {Base}_{A}$
13		eqid	$⊢ 0_{A} = 0_{A}$
14		simpllr	$⊢ (((N \in Fin \land R \in Ring) \land (U \in B \land K \in ℕ_{0})) \land k \in ℕ_{0}) \to R \in Ring$
15		simplrl	$⊢ (((N \in Fin \land R \in Ring) \land (U \in B \land K \in ℕ_{0})) \land k \in ℕ_{0}) \to U \in B$
16		simpr	$⊢ (((N \in Fin \land R \in Ring) \land (U \in B \land K \in ℕ_{0})) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
17	1 2 3 7 12	decpmatcl	$⊢ (R \in Ring \land U \in B \land k \in ℕ_{0}) \to U decompPMat k \in {Base}_{A}$
18	14 15 16 17	syl3anc	$⊢ (((N \in Fin \land R \in Ring) \land (U \in B \land K \in ℕ_{0})) \land k \in ℕ_{0}) \to U decompPMat k \in {Base}_{A}$
19	18	ralrimiva	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land K \in ℕ_{0})) \to \forall k \in ℕ_{0} U decompPMat k \in {Base}_{A}$
20	1 2 3 7 13	decpmatfsupp	$⊢ (R \in Ring \land U \in B) \to {finSupp}_{0_{A}} ((k \in ℕ_{0} ⟼ U decompPMat k))$
21	20	ad2ant2lr	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land K \in ℕ_{0})) \to {finSupp}_{0_{A}} ((k \in ℕ_{0} ⟼ U decompPMat k))$
22		simprr	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land K \in ℕ_{0})) \to K \in ℕ_{0}$
23	8 9 6 5 11 12 4 13 19 21 22	gsummoncoe1	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land K \in ℕ_{0})) \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((U decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))) (K) = ⦋ K / k ⦌ (U decompPMat k)$
24		csbov2g	$⊢ K \in ℕ_{0} \to ⦋ K / k ⦌ (U decompPMat k) = U decompPMat ⦋ K / k ⦌ k$
25	24	ad2antll	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land K \in ℕ_{0})) \to ⦋ K / k ⦌ (U decompPMat k) = U decompPMat ⦋ K / k ⦌ k$
26		csbvarg	$⊢ K \in ℕ_{0} \to ⦋ K / k ⦌ k = K$
27	26	ad2antll	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land K \in ℕ_{0})) \to ⦋ K / k ⦌ k = K$
28	27	oveq2d	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land K \in ℕ_{0})) \to U decompPMat ⦋ K / k ⦌ k = U decompPMat K$
29	23 25 28	3eqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land K \in ℕ_{0})) \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((U decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))) (K) = U decompPMat K$

Metamath Proof Explorer

Theorem pm2mpf1lem

Proof