Theorem pm2mpf1lem

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

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

Proof

Step	Hyp	Ref	Expression
1		pm2mpf1lem.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		pm2mpf1lem.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		pm2mpf1lem.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		pm2mpf1lem.m	⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
5		pm2mpf1lem.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
6		pm2mpf1lem.x	⊢ 𝑋 = ( var1 ‘ 𝐴 )
7		pm2mpf1lem.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
8		pm2mpf1lem.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
9		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
10	7	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
11	10	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → 𝐴 ∈ Ring )
12		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
13		eqid	⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
14		simpllr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑅 ∈ Ring )
15		simplrl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑈 ∈ 𝐵 )
16		simpr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
17	1 2 3 7 12	decpmatcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑈 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
18	14 15 16 17	syl3anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑈 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
19	18	ralrimiva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → ∀ 𝑘 ∈ ℕ0 ( 𝑈 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
20	1 2 3 7 13	decpmatfsupp	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝑈 decompPMat 𝑘 ) ) finSupp ( 0g ‘ 𝐴 ) )
21	20	ad2ant2lr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝑈 decompPMat 𝑘 ) ) finSupp ( 0g ‘ 𝐴 ) )
22		simprr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → 𝐾 ∈ ℕ0 )
23	8 9 6 5 11 12 4 13 19 21 22	gsummoncoe1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑈 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐾 ) = ⦋ 𝐾 / 𝑘 ⦌ ( 𝑈 decompPMat 𝑘 ) )
24		csbov2g	⊢ ( 𝐾 ∈ ℕ0 → ⦋ 𝐾 / 𝑘 ⦌ ( 𝑈 decompPMat 𝑘 ) = ( 𝑈 decompPMat ⦋ 𝐾 / 𝑘 ⦌ 𝑘 ) )
25	24	ad2antll	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → ⦋ 𝐾 / 𝑘 ⦌ ( 𝑈 decompPMat 𝑘 ) = ( 𝑈 decompPMat ⦋ 𝐾 / 𝑘 ⦌ 𝑘 ) )
26		csbvarg	⊢ ( 𝐾 ∈ ℕ0 → ⦋ 𝐾 / 𝑘 ⦌ 𝑘 = 𝐾 )
27	26	ad2antll	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → ⦋ 𝐾 / 𝑘 ⦌ 𝑘 = 𝐾 )
28	27	oveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → ( 𝑈 decompPMat ⦋ 𝐾 / 𝑘 ⦌ 𝑘 ) = ( 𝑈 decompPMat 𝐾 ) )
29	23 25 28	3eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑈 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐾 ) = ( 𝑈 decompPMat 𝐾 ) )