Theorem cpmidpmatlem1

Description: Lemma 1 for cpmidpmat . (Contributed by AV, 13-Nov-2019)

	Ref	Expression
Hypotheses	cpmidgsum.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	cpmidgsum.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	cpmidgsum.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	cpmidgsum.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
	cpmidgsum.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	cpmidgsum.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	cpmidgsum.m	⊢ · = ( ·𝑠 ‘ 𝑌 )
	cpmidgsum.1	⊢ 1 = ( 1r ‘ 𝑌 )
	cpmidgsum.u	⊢ 𝑈 = ( algSc ‘ 𝑃 )
	cpmidgsum.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
	cpmidgsum.k	⊢ 𝐾 = ( 𝐶 ‘ 𝑀 )
	cpmidgsum.h	⊢ 𝐻 = ( 𝐾 · 1 )
	cpmidgsumm2pm.o	⊢ 𝑂 = ( 1r ‘ 𝐴 )
	cpmidgsumm2pm.m	⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
	cpmidgsumm2pm.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	cpmidpmat.g	⊢ 𝐺 = ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) )
Assertion	cpmidpmatlem1	⊢ ( 𝐿 ∈ ℕ0 → ( 𝐺 ‘ 𝐿 ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝐿 ) ∗ 𝑂 ) )

Proof

Step	Hyp	Ref	Expression
1		cpmidgsum.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		cpmidgsum.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		cpmidgsum.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4		cpmidgsum.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
5		cpmidgsum.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
6		cpmidgsum.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
7		cpmidgsum.m	⊢ · = ( ·𝑠 ‘ 𝑌 )
8		cpmidgsum.1	⊢ 1 = ( 1r ‘ 𝑌 )
9		cpmidgsum.u	⊢ 𝑈 = ( algSc ‘ 𝑃 )
10		cpmidgsum.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
11		cpmidgsum.k	⊢ 𝐾 = ( 𝐶 ‘ 𝑀 )
12		cpmidgsum.h	⊢ 𝐻 = ( 𝐾 · 1 )
13		cpmidgsumm2pm.o	⊢ 𝑂 = ( 1r ‘ 𝐴 )
14		cpmidgsumm2pm.m	⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
15		cpmidgsumm2pm.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
16		cpmidpmat.g	⊢ 𝐺 = ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) )
17		fveq2	⊢ ( 𝑘 = 𝐿 → ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) = ( ( coe1 ‘ 𝐾 ) ‘ 𝐿 ) )
18	17	oveq1d	⊢ ( 𝑘 = 𝐿 → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝐿 ) ∗ 𝑂 ) )
19		ovex	⊢ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝐿 ) ∗ 𝑂 ) ∈ V
20	18 16 19	fvmpt	⊢ ( 𝐿 ∈ ℕ0 → ( 𝐺 ‘ 𝐿 ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝐿 ) ∗ 𝑂 ) )