Theorem pm2mpghmlem2

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

	Ref	Expression
Hypotheses	pm2mpfo.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	pm2mpfo.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	pm2mpfo.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	pm2mpfo.m	⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
	pm2mpfo.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
	pm2mpfo.x	⊢ 𝑋 = ( var1 ‘ 𝐴 )
	pm2mpfo.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	pm2mpfo.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
Assertion	pm2mpghmlem2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑀 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		pm2mpfo.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		pm2mpfo.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		pm2mpfo.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		pm2mpfo.m	⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
5		pm2mpfo.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
6		pm2mpfo.x	⊢ 𝑋 = ( var1 ‘ 𝐴 )
7		pm2mpfo.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
8		pm2mpfo.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
9		nn0ex	⊢ ℕ0 ∈ V
10	9	a1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ℕ0 ∈ V )
11	7	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
12	11	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝐴 ∈ Ring )
13	8	ply1lmod	⊢ ( 𝐴 ∈ Ring → 𝑄 ∈ LMod )
14	12 13	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑄 ∈ LMod )
15	8	ply1sca	⊢ ( 𝐴 ∈ Ring → 𝐴 = ( Scalar ‘ 𝑄 ) )
16	12 15	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝐴 = ( Scalar ‘ 𝑄 ) )
17		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
18		simpl2	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑅 ∈ Ring )
19		simpl3	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ∈ 𝐵 )
20		simpr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
21		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
22	1 2 3 7 21	decpmatcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
23	18 19 20 22	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
24		eqid	⊢ ( mulGrp ‘ 𝑄 ) = ( mulGrp ‘ 𝑄 )
25	8 6 24 5 17	ply1moncl	⊢ ( ( 𝐴 ∈ Ring ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ ( Base ‘ 𝑄 ) )
26	12 25	sylan	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ ( Base ‘ 𝑄 ) )
27		eqid	⊢ ( 0g ‘ 𝑄 ) = ( 0g ‘ 𝑄 )
28		eqid	⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
29	1 2 3 7 28	decpmatfsupp	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝑀 decompPMat 𝑘 ) ) finSupp ( 0g ‘ 𝐴 ) )
30	29	3adant1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝑀 decompPMat 𝑘 ) ) finSupp ( 0g ‘ 𝐴 ) )
31	10 14 16 17 23 26 27 28 4 30	mptscmfsupp0	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑀 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑄 ) )