pm2mpghmlem2

Description: Lemma 2 for pm2mpghm . (Contributed by AV, 15-Oct-2019) (Revised by AV, 4-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		pm2mpfo.p	$⊢ P = {Poly}_{1} (R)$
2		pm2mpfo.c	$⊢ C = N Mat P$
3		pm2mpfo.b	$⊢ B = {Base}_{C}$
4		pm2mpfo.m	$⊢ \underset{˙}{*} = \cdot_{Q}$
5		pm2mpfo.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Q}}$
6		pm2mpfo.x	$⊢ X = {var}_{1} (A)$
7		pm2mpfo.a	$⊢ A = N Mat R$
8		pm2mpfo.q	$⊢ Q = {Poly}_{1} (A)$
9		nn0ex	$⊢ ℕ_{0} \in V$
10	9	a1i	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to ℕ_{0} \in V$
11	7	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
12	11	3adant3	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to A \in Ring$
13	8	ply1lmod	$⊢ A \in Ring \to Q \in LMod$
14	12 13	syl	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to Q \in LMod$
15	8	ply1sca	$⊢ A \in Ring \to A = Scalar (Q)$
16	12 15	syl	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to A = Scalar (Q)$
17		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
18		simpl2	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land k \in ℕ_{0}) \to R \in Ring$
19		simpl3	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land k \in ℕ_{0}) \to M \in B$
20		simpr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
21		eqid	$⊢ {Base}_{A} = {Base}_{A}$
22	1 2 3 7 21	decpmatcl	$⊢ (R \in Ring \land M \in B \land k \in ℕ_{0}) \to M decompPMat k \in {Base}_{A}$
23	18 19 20 22	syl3anc	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land k \in ℕ_{0}) \to M decompPMat k \in {Base}_{A}$
24		eqid	$⊢ {mulGrp}_{Q} = {mulGrp}_{Q}$
25	8 6 24 5 17	ply1moncl	$⊢ (A \in Ring \land k \in ℕ_{0}) \to k \underset{˙}{\times} X \in {Base}_{Q}$
26	12 25	sylan	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land k \in ℕ_{0}) \to k \underset{˙}{\times} X \in {Base}_{Q}$
27		eqid	$⊢ 0_{Q} = 0_{Q}$
28		eqid	$⊢ 0_{A} = 0_{A}$
29	1 2 3 7 28	decpmatfsupp	$⊢ (R \in Ring \land M \in B) \to {finSupp}_{0_{A}} ((k \in ℕ_{0} ⟼ M decompPMat k))$
30	29	3adant1	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to {finSupp}_{0_{A}} ((k \in ℕ_{0} ⟼ M decompPMat k))$
31	10 14 16 17 23 26 27 28 4 30	mptscmfsupp0	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to {finSupp}_{0_{Q}} ((k \in ℕ_{0} ⟼ (M decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X)))$

Metamath Proof Explorer

Theorem pm2mpghmlem2

Proof