Metamath Proof Explorer

Theorem cayleyhamiltonALT

Description: Alternate proof of cayleyhamilton , the Cayley-Hamilton theorem. This proof does not use cayleyhamilton0 directly, but has the same structure as the proof of cayleyhamilton0 . In contrast to the proof of cayleyhamilton0 , only the definitions required to formulate the theorem itself are used, causing the definitions used in the lemmas being expanded, which makes the proof longer and more difficult to read. (Contributed by AV, 25-Nov-2019) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses cayleyhamilton.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
cayleyhamilton.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
cayleyhamilton.0 ⊢ 0 = ( 0g ‘ 𝐴 )
cayleyhamilton.c ⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
cayleyhamilton.k ⊢ 𝐾 = ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) )
cayleyhamilton.m ⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
cayleyhamilton.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝐴 ) )
Assertion cayleyhamiltonALT ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = 0 )

Proof

Step Hyp Ref Expression
1 cayleyhamilton.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 cayleyhamilton.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 cayleyhamilton.0 ⊢ 0 = ( 0g ‘ 𝐴 )
4 cayleyhamilton.c ⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
5 cayleyhamilton.k ⊢ 𝐾 = ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) )
6 cayleyhamilton.m ⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
7 cayleyhamilton.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝐴 ) )
8 eqid ⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
9 eqid ⊢ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) = ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) )
10 eqid ⊢ ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) = ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) )
11 eqid ⊢ ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) = ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) )
12 eqid ⊢ ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) = ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) )
13 eqid ⊢ ( 𝑁 matToPolyMat 𝑅 ) = ( 𝑁 matToPolyMat 𝑅 )
14 eqid ⊢ ( 𝐶 ‘ 𝑀 ) = ( 𝐶 ‘ 𝑀 )
15 eqeq1 ⊢ ( 𝑙 = 𝑛 → ( 𝑙 = 0 ↔ 𝑛 = 0 ) )
16 eqeq1 ⊢ ( 𝑙 = 𝑛 → ( 𝑙 = ( 𝑠 + 1 ) ↔ 𝑛 = ( 𝑠 + 1 ) ) )
17 breq2 ⊢ ( 𝑙 = 𝑛 → ( ( 𝑠 + 1 ) < 𝑙 ↔ ( 𝑠 + 1 ) < 𝑛 ) )
18 oveq1 ⊢ ( 𝑙 = 𝑛 → ( 𝑙 − 1 ) = ( 𝑛 − 1 ) )
19 18 fveq2d ⊢ ( 𝑙 = 𝑛 → ( 𝑏 ‘ ( 𝑙 − 1 ) ) = ( 𝑏 ‘ ( 𝑛 − 1 ) ) )
20 19 fveq2d ⊢ ( 𝑙 = 𝑛 → ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) = ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) )
21 fveq2 ⊢ ( 𝑙 = 𝑛 → ( 𝑏 ‘ 𝑙 ) = ( 𝑏 ‘ 𝑛 ) )
22 21 fveq2d ⊢ ( 𝑙 = 𝑛 → ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) = ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑛 ) ) )
23 22 oveq2d ⊢ ( 𝑙 = 𝑛 → ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) = ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑛 ) ) ) )
24 20 23 oveq12d ⊢ ( 𝑙 = 𝑛 → ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) = ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) )
25 17 24 ifbieq2d ⊢ ( 𝑙 = 𝑛 → if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) = if ( ( 𝑠 + 1 ) < 𝑛 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) )
26 16 25 ifbieq2d ⊢ ( 𝑙 = 𝑛 → if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) = if ( 𝑛 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) )
27 15 26 ifbieq2d ⊢ ( 𝑙 = 𝑛 → if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) = if ( 𝑛 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
28 27 cbvmptv ⊢ ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
29 eqid ⊢ ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) = ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) )
30 eqid ⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
31 eqid ⊢ ( 𝑁 cPolyMatToMat 𝑅 ) = ( 𝑁 cPolyMatToMat 𝑅 )
32 eqid ⊢ ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) = ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) )
33 1 2 8 9 10 11 12 13 4 14 28 29 30 6 31 7 32 cayhamlem4 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( ( 𝑁 cPolyMatToMat 𝑅 ) ‘ ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) ) )
34 eqid ⊢ ( 𝑁 ConstPolyMat 𝑅 ) = ( 𝑁 ConstPolyMat 𝑅 )
35 31 34 cpm2mfval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 cPolyMatToMat 𝑅 ) = ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) )
36 35 eqcomd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) = ( 𝑁 cPolyMatToMat 𝑅 ) )
37 36 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) = ( 𝑁 cPolyMatToMat 𝑅 ) )
38 37 fveq1d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ‘ ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) ) = ( ( 𝑁 cPolyMatToMat 𝑅 ) ‘ ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) ) )
39 38 eqeq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ‘ ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) ) ↔ ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( ( 𝑁 cPolyMatToMat 𝑅 ) ‘ ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) ) ) )
40 39 2rexbidv ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ‘ ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) ) ↔ ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( ( 𝑁 cPolyMatToMat 𝑅 ) ‘ ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) ) ) )
41 33 40 mpbird ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ‘ ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) ) )
42 5 eqcomi ⊢ ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) = 𝐾
43 42 a1i ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) = 𝐾 )
44 43 fveq1d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) = ( 𝐾 ‘ 𝑛 ) )
45 44 oveq1d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) = ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) )
46 45 mpteq2dva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) )
47 46 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) )
48 47 eqeq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ‘ ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) ) ↔ ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ‘ ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) ) ) )
49 48 biimpa ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ‘ ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) ) ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ‘ ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) ) )
50 oveq1 ⊢ ( 𝑛 = 𝑗 → ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) = ( 𝑗 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) )
51 fveq2 ⊢ ( 𝑛 = 𝑗 → ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) = ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑗 ) )
52 50 51 oveq12d ⊢ ( 𝑛 = 𝑗 → ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) = ( ( 𝑗 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑗 ) ) )
53 52 cbvmptv ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) = ( 𝑗 ∈ ℕ0 ↦ ( ( 𝑗 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑗 ) ) )
54 53 oveq2i ⊢ ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) = ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑗 ∈ ℕ0 ↦ ( ( 𝑗 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑗 ) ) ) )
55 54 a1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) = ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑗 ∈ ℕ0 ↦ ( ( 𝑗 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑗 ) ) ) ) )
56 1 2 8 9 10 11 12 13 28 32 cayhamlem1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑗 ∈ ℕ0 ↦ ( ( 𝑗 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑗 ) ) ) ) = ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) )
57 55 56 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) = ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) )
58 fveq2 ⊢ ( ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) = ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) → ( ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ‘ ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) ) = ( ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ‘ ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) )
59 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
60 59 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
61 60 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
62 31 34 cpm2mfval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑁 cPolyMatToMat 𝑅 ) = ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) )
63 62 eqcomd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) = ( 𝑁 cPolyMatToMat 𝑅 ) )
64 63 fveq1d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ‘ ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) = ( ( 𝑁 cPolyMatToMat 𝑅 ) ‘ ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) )
65 eqid ⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
66 1 31 8 9 65 12 m2cpminv0 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑁 cPolyMatToMat 𝑅 ) ‘ ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) = ( 0g ‘ 𝐴 ) )
67 64 66 eqtrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ‘ ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) = ( 0g ‘ 𝐴 ) )
68 61 67 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ‘ ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) = ( 0g ‘ 𝐴 ) )
69 68 3 eqtr4di ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ‘ ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) = 0 )
70 69 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ‘ ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) = 0 )
71 58 70 sylan9eqr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) = ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) → ( ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ‘ ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) ) = 0 )
72 57 71 mpdan ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ‘ ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) ) = 0 )
73 72 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ‘ ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) ) ) → ( ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ‘ ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) ) = 0 )
74 49 73 eqtrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ‘ ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) ) ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = 0 )
75 74 ex ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ‘ ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = 0 ) )
76 75 rexlimdvva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( ( 𝑚 ∈ ( 𝑁 ConstPolyMat 𝑅 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ‘ ( ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑠 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑏 ‘ 𝑙 ) ) ) ) ) ) ) ) ‘ 𝑛 ) ) ) ) ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = 0 ) )
77 41 76 mpd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = 0 )