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