Theorem pmatcollpw1lem2

Description: Lemma 2 for pmatcollpw1 : An entry of a polynomial matrix is the sum of the entries of the matrix consisting of the coefficients in the entries of the polynomial matrix multiplied with the corresponding power of the variable. (Contributed by AV, 25-Sep-2019) (Revised by AV, 3-Dec-2019)

	Ref	Expression
Hypotheses	pmatcollpw1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	pmatcollpw1.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	pmatcollpw1.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	pmatcollpw1.m	⊢ × = ( ·𝑠 ‘ 𝑃 )
	pmatcollpw1.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	pmatcollpw1.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
Assertion	pmatcollpw1lem2	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 𝑀 𝑏 ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pmatcollpw1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		pmatcollpw1.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		pmatcollpw1.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		pmatcollpw1.m	⊢ × = ( ·𝑠 ‘ 𝑃 )
5		pmatcollpw1.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
6		pmatcollpw1.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
7		simpl2	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
8		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
9		simprl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑎 ∈ 𝑁 )
10		simprr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑏 ∈ 𝑁 )
11		simpl3	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑀 ∈ 𝐵 )
12	2 8 3 9 10 11	matecld	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 𝑀 𝑏 ) ∈ ( Base ‘ 𝑃 ) )
13		eqid	⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
14		eqid	⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
15		eqid	⊢ ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) ) = ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) )
16	1 6 8 4 13 14 15	ply1coe	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑎 𝑀 𝑏 ) ∈ ( Base ‘ 𝑃 ) ) → ( 𝑎 𝑀 𝑏 ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) ) ‘ 𝑛 ) × ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) ) ) )
17	7 12 16	syl2anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 𝑀 𝑏 ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) ) ‘ 𝑛 ) × ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) ) ) )
18	7	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑅 ∈ Ring )
19	11	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑀 ∈ 𝐵 )
20		simpr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
21		simpr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) )
22	21	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) )
23	1 2 3	decpmate	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) = ( ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) ) ‘ 𝑛 ) )
24	18 19 20 22 23	syl31anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) = ( ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) ) ‘ 𝑛 ) )
25	24	eqcomd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) ) ‘ 𝑛 ) = ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) )
26	5	eqcomi	⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ↑
27	26	oveqi	⊢ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) = ( 𝑛 ↑ 𝑋 )
28	27	a1i	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) = ( 𝑛 ↑ 𝑋 ) )
29	25 28	oveq12d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) ) ‘ 𝑛 ) × ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) = ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) × ( 𝑛 ↑ 𝑋 ) ) )
30	29	mpteq2dva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) ) ‘ 𝑛 ) × ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) × ( 𝑛 ↑ 𝑋 ) ) ) )
31	30	oveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) ) ‘ 𝑛 ) × ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) ) ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) )
32	17 31	eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 𝑀 𝑏 ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) )