Metamath Proof Explorer

Theorem pmatcollpw

Description: Write a polynomial matrix (over a commutative ring) as a sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 26-Oct-2019) (Revised by AV, 4-Dec-2019)

Ref Expression
Hypotheses pmatcollpw.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
pmatcollpw.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
pmatcollpw.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
pmatcollpw.m ⊢ ∗ = ( ·𝑠 ‘ 𝐶 )
pmatcollpw.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
pmatcollpw.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
pmatcollpw.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
Assertion pmatcollpw ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pmatcollpw.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 pmatcollpw.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3 pmatcollpw.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
4 pmatcollpw.m ⊢ ∗ = ( ·𝑠 ‘ 𝐶 )
5 pmatcollpw.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
6 pmatcollpw.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
7 pmatcollpw.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
8 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
9 eqid ⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
10 1 2 3 9 5 6 pmatcollpw2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) ) ) ) )
11 8 10 syl3an2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) ) ) ) )
12 eqidd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) ) )
13 oveq12 ⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) = ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) )
14 13 oveq1d ⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) = ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) )
15 14 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) ) → ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) = ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) )
16 simprl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑎 ∈ 𝑁 )
17 simpr ⊢ ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑏 ∈ 𝑁 )
18 17 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑏 ∈ 𝑁 )
19 simp2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ CRing )
20 19 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑅 ∈ CRing )
21 20 8 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑅 ∈ Ring )
22 21 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
23 eqid ⊢ ( 𝑁 Mat 𝑅 ) = ( 𝑁 Mat 𝑅 )
24 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
25 eqid ⊢ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
26 simp3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ 𝐵 )
27 26 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑀 ∈ 𝐵 )
28 simpr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
29 1 2 3 23 25 decpmatcl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝑛 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
30 20 27 28 29 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝑛 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
31 30 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑀 decompPMat 𝑛 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
32 23 24 25 16 18 31 matecld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ∈ ( Base ‘ 𝑅 ) )
33 simplr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑛 ∈ ℕ0 )
34 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
35 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
36 24 1 6 9 34 5 35 ply1tmcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑃 ) )
37 22 32 33 36 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑃 ) )
38 12 15 16 18 37 ovmpod ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) ) 𝑏 ) = ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) )
39 1 2 3 4 5 6 7 pmatcollpwlem ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) = ( 𝑎 ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) 𝑏 ) )
40 39 3expb ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) = ( 𝑎 ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) 𝑏 ) )
41 38 40 eqtrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) ) 𝑏 ) = ( 𝑎 ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) 𝑏 ) )
42 41 ralrimivva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) ) 𝑏 ) = ( 𝑎 ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) 𝑏 ) )
43 simpl1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑁 ∈ Fin )
44 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
45 8 44 syl ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
46 45 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ Ring )
47 46 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑃 ∈ Ring )
48 21 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
49 simp2 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
50 simp3 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
51 30 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑀 decompPMat 𝑛 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
52 23 24 25 49 50 51 matecld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
53 28 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑛 ∈ ℕ0 )
54 24 1 6 9 34 5 35 ply1tmcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑃 ) )
55 48 52 53 54 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑃 ) )
56 2 35 3 43 47 55 matbas2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) ) ∈ 𝐵 )
57 8 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
58 1 6 34 5 35 ply1moncl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
59 57 58 sylan ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
60 57 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑅 ∈ Ring )
61 7 23 25 1 2 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑀 decompPMat 𝑛 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ) → ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ∈ ( Base ‘ 𝐶 ) )
62 43 60 30 61 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ∈ ( Base ‘ 𝐶 ) )
63 62 3 eleqtrrdi ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ∈ 𝐵 )
64 35 2 3 4 matvscl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) ∧ ( ( 𝑛 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ∈ 𝐵 ) ) → ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ∈ 𝐵 )
65 43 47 59 63 64 syl22anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ∈ 𝐵 )
66 2 3 eqmat ⊢ ( ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) ) ∈ 𝐵 ∧ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ∈ 𝐵 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) ) = ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ↔ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) ) 𝑏 ) = ( 𝑎 ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) 𝑏 ) ) )
67 56 65 66 syl2anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) ) = ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ↔ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) ) 𝑏 ) = ( 𝑎 ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) 𝑏 ) ) )
68 42 67 mpbird ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) ) = ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) )
69 68 mpteq2dva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) )
70 69 oveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) ) ) ) = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) )
71 11 70 eqtrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) )