pm2mpghmlem1

Description: Lemma 1 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)$
	pm2mpfo.l	$⊢ L = {Base}_{Q}$
Assertion	pm2mpghmlem1	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in ℕ_{0}) \to (M decompPMat K) \underset{˙}{*} (K \underset{˙}{\times} X) \in L$

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		pm2mpfo.l	$⊢ L = {Base}_{Q}$
10	7	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
11	10	3adant3	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to A \in Ring$
12	11	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in ℕ_{0}) \to A \in Ring$
13		simpl2	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in ℕ_{0}) \to R \in Ring$
14		simpl3	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in ℕ_{0}) \to M \in B$
15		simpr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in ℕ_{0}) \to K \in ℕ_{0}$
16		eqid	$⊢ {Base}_{A} = {Base}_{A}$
17	1 2 3 7 16	decpmatcl	$⊢ (R \in Ring \land M \in B \land K \in ℕ_{0}) \to M decompPMat K \in {Base}_{A}$
18	13 14 15 17	syl3anc	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in ℕ_{0}) \to M decompPMat K \in {Base}_{A}$
19		eqid	$⊢ {mulGrp}_{Q} = {mulGrp}_{Q}$
20	16 8 6 4 19 5 9	ply1tmcl	$⊢ (A \in Ring \land M decompPMat K \in {Base}_{A} \land K \in ℕ_{0}) \to (M decompPMat K) \underset{˙}{*} (K \underset{˙}{\times} X) \in L$
21	12 18 15 20	syl3anc	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in ℕ_{0}) \to (M decompPMat K) \underset{˙}{*} (K \underset{˙}{\times} X) \in L$

Metamath Proof Explorer