Metamath Proof Explorer

Theorem pmatcollpw1

Description: Write a polynomial matrix as a matrix of sums of scaled monomials. (Contributed by AV, 29-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 pmatcollpw1 ( ( 𝑁 ∈ 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 1 2 3 4 5 6 pmatcollpw1lem2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 𝑀 𝑏 ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) )
8 eqidd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ) )
9 oveq12 ⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) = ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) )
10 9 oveq1d ⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) = ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) × ( 𝑛 ↑ 𝑋 ) ) )
11 10 mpteq2dv ⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) × ( 𝑛 ↑ 𝑋 ) ) ) )
12 11 oveq2d ⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) )
13 12 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) ) → ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) )
14 simprl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑎 ∈ 𝑁 )
15 simprr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑏 ∈ 𝑁 )
16 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
17 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
18 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
19 ringcmn ⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ CMnd )
20 18 19 syl ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ CMnd )
21 20 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ CMnd )
22 21 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑃 ∈ CMnd )
23 nn0ex ⊢ ℕ0 ∈ V
24 23 a1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ℕ0 ∈ V )
25 simpl2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
26 25 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑅 ∈ Ring )
27 eqid ⊢ ( 𝑁 Mat 𝑅 ) = ( 𝑁 Mat 𝑅 )
28 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
29 eqid ⊢ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
30 simplrl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑎 ∈ 𝑁 )
31 15 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑏 ∈ 𝑁 )
32 simpl3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑀 ∈ 𝐵 )
33 32 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑀 ∈ 𝐵 )
34 simpr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
35 1 2 3 27 29 decpmatcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝑛 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
36 26 33 34 35 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝑛 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
37 27 28 29 30 31 36 matecld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ∈ ( Base ‘ 𝑅 ) )
38 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
39 28 1 6 4 38 5 16 ply1tmcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) × ( 𝑛 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑃 ) )
40 26 37 34 39 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) × ( 𝑛 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑃 ) )
41 40 fmpttd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) × ( 𝑛 ↑ 𝑋 ) ) ) : ℕ0 ⟶ ( Base ‘ 𝑃 ) )
42 1 2 3 4 5 6 pmatcollpw1lem1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) × ( 𝑛 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑃 ) )
43 42 3expb ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) × ( 𝑛 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑃 ) )
44 16 17 22 24 41 43 gsumcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ∈ ( Base ‘ 𝑃 ) )
45 8 13 14 15 44 ovmpod ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ) 𝑏 ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) )
46 7 45 eqtr4d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 𝑀 𝑏 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ) 𝑏 ) )
47 46 ralrimivva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( 𝑎 𝑀 𝑏 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ) 𝑏 ) )
48 simp3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ 𝐵 )
49 simp1 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑁 ∈ Fin )
50 18 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ Ring )
51 21 3ad2ant1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑃 ∈ CMnd )
52 23 a1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ℕ0 ∈ V )
53 simpl12 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑅 ∈ Ring )
54 simpl2 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑖 ∈ 𝑁 )
55 simpl3 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑗 ∈ 𝑁 )
56 48 3ad2ant1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑀 ∈ 𝐵 )
57 56 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑀 ∈ 𝐵 )
58 simpr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
59 53 57 58 35 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝑛 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
60 27 28 29 54 55 59 matecld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
61 28 1 6 4 38 5 16 ply1tmcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑃 ) )
62 53 60 58 61 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑃 ) )
63 62 fmpttd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) : ℕ0 ⟶ ( Base ‘ 𝑃 ) )
64 1 2 3 4 5 6 pmatcollpw1lem1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑃 ) )
65 16 17 51 52 63 64 gsumcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ∈ ( Base ‘ 𝑃 ) )
66 2 16 3 49 50 65 matbas2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ) ∈ 𝐵 )
67 2 3 eqmat ⊢ ( ( 𝑀 ∈ 𝐵 ∧ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ) ∈ 𝐵 ) → ( 𝑀 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ) ↔ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( 𝑎 𝑀 𝑏 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ) 𝑏 ) ) )
68 48 66 67 syl2anc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑀 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ) ↔ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( 𝑎 𝑀 𝑏 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ) 𝑏 ) ) )
69 47 68 mpbird ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑀 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ) )