Metamath Proof Explorer

Theorem cpmadumatpoly

Description: The product of the characteristic matrix of a given matrix and its adjunct represented as a polynomial over matrices. (Contributed by AV, 20-Nov-2019) (Revised by AV, 7-Dec-2019)

Ref Expression
Hypotheses cpmadumatpoly.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
cpmadumatpoly.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
cpmadumatpoly.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
cpmadumatpoly.y ⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
cpmadumatpoly.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
cpmadumatpoly.r ⊢ × = ( .r ‘ 𝑌 )
cpmadumatpoly.m0 ⊢ − = ( -g ‘ 𝑌 )
cpmadumatpoly.0 ⊢ 0 = ( 0g ‘ 𝑌 )
cpmadumatpoly.g ⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
cpmadumatpoly.s ⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
cpmadumatpoly.m1 ⊢ · = ( ·𝑠 ‘ 𝑌 )
cpmadumatpoly.1 ⊢ 1 = ( 1r ‘ 𝑌 )
cpmadumatpoly.z ⊢ 𝑍 = ( var1 ‘ 𝑅 )
cpmadumatpoly.d ⊢ 𝐷 = ( ( 𝑍 · 1 ) − ( 𝑇 ‘ 𝑀 ) )
cpmadumatpoly.j ⊢ 𝐽 = ( 𝑁 maAdju 𝑃 )
cpmadumatpoly.w ⊢ 𝑊 = ( Base ‘ 𝑌 )
cpmadumatpoly.q ⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
cpmadumatpoly.x ⊢ 𝑋 = ( var1 ‘ 𝐴 )
cpmadumatpoly.m2 ⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
cpmadumatpoly.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
cpmadumatpoly.u ⊢ 𝑈 = ( 𝑁 cPolyMatToMat 𝑅 )
cpmadumatpoly.i ⊢ 𝐼 = ( 𝑁 pMatToMatPoly 𝑅 )
Assertion cpmadumatpoly ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐼 ‘ ( 𝐷 × ( 𝐽 ‘ 𝐷 ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cpmadumatpoly.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 cpmadumatpoly.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 cpmadumatpoly.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4 cpmadumatpoly.y ⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
5 cpmadumatpoly.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
6 cpmadumatpoly.r ⊢ × = ( .r ‘ 𝑌 )
7 cpmadumatpoly.m0 ⊢ − = ( -g ‘ 𝑌 )
8 cpmadumatpoly.0 ⊢ 0 = ( 0g ‘ 𝑌 )
9 cpmadumatpoly.g ⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
10 cpmadumatpoly.s ⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
11 cpmadumatpoly.m1 ⊢ · = ( ·𝑠 ‘ 𝑌 )
12 cpmadumatpoly.1 ⊢ 1 = ( 1r ‘ 𝑌 )
13 cpmadumatpoly.z ⊢ 𝑍 = ( var1 ‘ 𝑅 )
14 cpmadumatpoly.d ⊢ 𝐷 = ( ( 𝑍 · 1 ) − ( 𝑇 ‘ 𝑀 ) )
15 cpmadumatpoly.j ⊢ 𝐽 = ( 𝑁 maAdju 𝑃 )
16 cpmadumatpoly.w ⊢ 𝑊 = ( Base ‘ 𝑌 )
17 cpmadumatpoly.q ⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
18 cpmadumatpoly.x ⊢ 𝑋 = ( var1 ‘ 𝐴 )
19 cpmadumatpoly.m2 ⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
20 cpmadumatpoly.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
21 cpmadumatpoly.u ⊢ 𝑈 = ( 𝑁 cPolyMatToMat 𝑅 )
22 cpmadumatpoly.i ⊢ 𝐼 = ( 𝑁 pMatToMatPoly 𝑅 )
23 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
24 eqid ⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 )
25 eqeq1 ⊢ ( 𝑛 = 𝑧 → ( 𝑛 = 0 ↔ 𝑧 = 0 ) )
26 eqeq1 ⊢ ( 𝑛 = 𝑧 → ( 𝑛 = ( 𝑠 + 1 ) ↔ 𝑧 = ( 𝑠 + 1 ) ) )
27 breq2 ⊢ ( 𝑛 = 𝑧 → ( ( 𝑠 + 1 ) < 𝑛 ↔ ( 𝑠 + 1 ) < 𝑧 ) )
28 fvoveq1 ⊢ ( 𝑛 = 𝑧 → ( 𝑏 ‘ ( 𝑛 − 1 ) ) = ( 𝑏 ‘ ( 𝑧 − 1 ) ) )
29 28 fveq2d ⊢ ( 𝑛 = 𝑧 → ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) = ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑧 − 1 ) ) ) )
30 2fveq3 ⊢ ( 𝑛 = 𝑧 → ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) = ( 𝑇 ‘ ( 𝑏 ‘ 𝑧 ) ) )
31 30 oveq2d ⊢ ( 𝑛 = 𝑧 → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) = ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑧 ) ) ) )
32 29 31 oveq12d ⊢ ( 𝑛 = 𝑧 → ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) = ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑧 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑧 ) ) ) ) )
33 27 32 ifbieq2d ⊢ ( 𝑛 = 𝑧 → if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) = if ( ( 𝑠 + 1 ) < 𝑧 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑧 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑧 ) ) ) ) ) )
34 26 33 ifbieq2d ⊢ ( 𝑛 = 𝑧 → if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) = if ( 𝑧 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑧 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑧 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑧 ) ) ) ) ) ) )
35 25 34 ifbieq2d ⊢ ( 𝑛 = 𝑧 → if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) = if ( 𝑧 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑧 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑧 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑧 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑧 ) ) ) ) ) ) ) )
36 35 cbvmptv ⊢ ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) ) = ( 𝑧 ∈ ℕ0 ↦ if ( 𝑧 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑧 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑧 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑧 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑧 ) ) ) ) ) ) ) )
37 9 36 eqtri ⊢ 𝐺 = ( 𝑧 ∈ ℕ0 ↦ if ( 𝑧 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑧 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑧 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑧 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑧 ) ) ) ) ) ) ) )
38 1 2 3 4 5 13 23 11 6 12 24 7 14 15 8 37 cpmadugsum ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐷 × ( 𝐽 ‘ 𝐷 ) ) = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝐺 ‘ 𝑛 ) ) ) ) )
39 simp1 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑁 ∈ Fin )
40 39 ad3antrrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑁 ∈ Fin )
41 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
42 41 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
43 42 ad3antrrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑅 ∈ Ring )
44 1 2 3 4 6 7 8 5 9 10 chfacfisfcpmat ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝐺 : ℕ0 ⟶ 𝑆 )
45 41 44 syl3anl2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝐺 : ℕ0 ⟶ 𝑆 )
46 45 anassrs ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝐺 : ℕ0 ⟶ 𝑆 )
47 46 ffvelcdmda ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑛 ) ∈ 𝑆 )
48 10 21 5 m2cpminvid2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝐺 ‘ 𝑛 ) ∈ 𝑆 ) → ( 𝑇 ‘ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) = ( 𝐺 ‘ 𝑛 ) )
49 40 43 47 48 syl3anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑇 ‘ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) = ( 𝐺 ‘ 𝑛 ) )
50 49 eqcomd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑛 ) = ( 𝑇 ‘ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
51 50 oveq2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝐺 ‘ 𝑛 ) ) = ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝑇 ‘ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) )
52 51 mpteq2dva ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝐺 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝑇 ‘ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) )
53 52 oveq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝐺 ‘ 𝑛 ) ) ) ) = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝑇 ‘ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) ) )
54 53 eqeq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( ( 𝐷 × ( 𝐽 ‘ 𝐷 ) ) = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝐺 ‘ 𝑛 ) ) ) ) ↔ ( 𝐷 × ( 𝐽 ‘ 𝐷 ) ) = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝑇 ‘ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) ) ) )
55 fveq2 ⊢ ( ( 𝐷 × ( 𝐽 ‘ 𝐷 ) ) = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝑇 ‘ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) ) → ( 𝐼 ‘ ( 𝐷 × ( 𝐽 ‘ 𝐷 ) ) ) = ( 𝐼 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝑇 ‘ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) ) ) )
56 3simpa ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) )
57 56 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) )
58 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 cpmadumatpolylem1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑈 ∘ 𝐺 ) ∈ ( 𝐵 ↑m ℕ0 ) )
59 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 cpmadumatpolylem2 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑈 ∘ 𝐺 ) finSupp ( 0g ‘ 𝐴 ) )
60 3 4 16 19 20 18 1 2 17 22 23 13 11 5 pm2mp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( ( 𝑈 ∘ 𝐺 ) ∈ ( 𝐵 ↑m ℕ0 ) ∧ ( 𝑈 ∘ 𝐺 ) finSupp ( 0g ‘ 𝐴 ) ) ) → ( 𝐼 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝑇 ‘ ( ( 𝑈 ∘ 𝐺 ) ‘ 𝑛 ) ) ) ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑈 ∘ 𝐺 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) ) ) )
61 57 58 59 60 syl12anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝐼 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝑇 ‘ ( ( 𝑈 ∘ 𝐺 ) ‘ 𝑛 ) ) ) ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑈 ∘ 𝐺 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) ) ) )
62 fvco3 ⊢ ( ( 𝐺 : ℕ0 ⟶ 𝑆 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑈 ∘ 𝐺 ) ‘ 𝑛 ) = ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) )
63 62 eqcomd ⊢ ( ( 𝐺 : ℕ0 ⟶ 𝑆 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( 𝑈 ∘ 𝐺 ) ‘ 𝑛 ) )
64 46 63 sylan ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( 𝑈 ∘ 𝐺 ) ‘ 𝑛 ) )
65 64 fveq2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑇 ‘ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) = ( 𝑇 ‘ ( ( 𝑈 ∘ 𝐺 ) ‘ 𝑛 ) ) )
66 65 oveq2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝑇 ‘ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) = ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝑇 ‘ ( ( 𝑈 ∘ 𝐺 ) ‘ 𝑛 ) ) ) )
67 66 mpteq2dva ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝑇 ‘ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝑇 ‘ ( ( 𝑈 ∘ 𝐺 ) ‘ 𝑛 ) ) ) ) )
68 67 oveq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝑇 ‘ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝑇 ‘ ( ( 𝑈 ∘ 𝐺 ) ‘ 𝑛 ) ) ) ) ) )
69 68 fveq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝐼 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝑇 ‘ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) ) ) = ( 𝐼 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝑇 ‘ ( ( 𝑈 ∘ 𝐺 ) ‘ 𝑛 ) ) ) ) ) ) )
70 64 oveq1d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( ( ( 𝑈 ∘ 𝐺 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) )
71 70 mpteq2dva ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑈 ∘ 𝐺 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) ) )
72 71 oveq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑈 ∘ 𝐺 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) ) ) )
73 61 69 72 3eqtr4d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝐼 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝑇 ‘ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) ) ) )
74 55 73 sylan9eqr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ ( 𝐷 × ( 𝐽 ‘ 𝐷 ) ) = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝑇 ‘ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) ) ) → ( 𝐼 ‘ ( 𝐷 × ( 𝐽 ‘ 𝐷 ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) ) ) )
75 74 ex ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( ( 𝐷 × ( 𝐽 ‘ 𝐷 ) ) = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝑇 ‘ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) ) → ( 𝐼 ‘ ( 𝐷 × ( 𝐽 ‘ 𝐷 ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) ) ) ) )
76 54 75 sylbid ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( ( 𝐷 × ( 𝐽 ‘ 𝐷 ) ) = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝐺 ‘ 𝑛 ) ) ) ) → ( 𝐼 ‘ ( 𝐷 × ( 𝐽 ‘ 𝐷 ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) ) ) ) )
77 76 reximdva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) → ( ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐷 × ( 𝐽 ‘ 𝐷 ) ) = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝐺 ‘ 𝑛 ) ) ) ) → ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐼 ‘ ( 𝐷 × ( 𝐽 ‘ 𝐷 ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) ) ) ) )
78 77 reximdva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐷 × ( 𝐽 ‘ 𝐷 ) ) = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑍 ) · ( 𝐺 ‘ 𝑛 ) ) ) ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐼 ‘ ( 𝐷 × ( 𝐽 ‘ 𝐷 ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) ) ) ) )
79 38 78 mpd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐼 ‘ ( 𝐷 × ( 𝐽 ‘ 𝐷 ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) ) ) )