Metamath Proof Explorer


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 𝑛 ) 𝑏 ) × ( 𝑛 𝑋 ) ) ) ) )