Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cpmadugsum Structured version   Visualization version   GIF version

 Description: The product of the characteristic matrix of a given matrix and its adjunct represented as an infinite sum. (Contributed by AV, 10-Nov-2019.)
Hypotheses
Ref Expression
cpmadugsum.a 𝐴 = (𝑁 Mat 𝑅)
cpmadugsum.y 𝑌 = (𝑁 Mat 𝑃)
cpmadugsum.t 𝑇 = (𝑁 matToPolyMat 𝑅)
cpmadugsum.i 𝐼 = ((𝑋 · 1 ) (𝑇𝑀))
cpmadugsum.g2 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛))))))))
Assertion
Ref Expression
cpmadugsum ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵𝑚 (0...𝑠))(𝐼 × (𝐽𝐼)) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖)))))
Distinct variable groups:   𝐵,𝑖   𝑖,𝑀   𝑖,𝑁   𝑅,𝑖   𝑖,𝑋   𝑖,𝑌   × ,𝑖   · ,𝑖   1 ,𝑖   𝑖,𝑏,𝑠,𝑇   ,𝑖   ,𝑖   𝐴,𝑏,𝑛,𝑠   𝐵,𝑏,𝑛,𝑠   𝐼,𝑏,𝑖,𝑛,𝑠   𝐽,𝑏,𝑖,𝑛,𝑠   𝑀,𝑏,𝑛,𝑠   𝑁,𝑏,𝑛,𝑠   𝑃,𝑖,𝑛   𝑅,𝑏,𝑛,𝑠   𝑇,𝑏,𝑛,𝑠   𝑋,𝑏,𝑛,𝑠   𝑌,𝑏,𝑛,𝑠   ,𝑛,𝑠,𝑏   · ,𝑏,𝑛,𝑠   𝑖,𝐺   × ,𝑛   0 ,𝑛   ,𝑛
Allowed substitution hints:   𝐴(𝑖)   𝑃(𝑠,𝑏)   + (𝑖,𝑛,𝑠,𝑏)   × (𝑠,𝑏)   1 (𝑛,𝑠,𝑏)   𝐺(𝑛,𝑠,𝑏)   (𝑠,𝑏)   0 (𝑖,𝑠,𝑏)

StepHypRef Expression
1 cpmadugsum.a . . 3 𝐴 = (𝑁 Mat 𝑅)
2 cpmadugsum.b . . 3 𝐵 = (Base‘𝐴)
3 cpmadugsum.p . . 3 𝑃 = (Poly1𝑅)
4 cpmadugsum.y . . 3 𝑌 = (𝑁 Mat 𝑃)
5 cpmadugsum.t . . 3 𝑇 = (𝑁 matToPolyMat 𝑅)
6 cpmadugsum.x . . 3 𝑋 = (var1𝑅)
7 cpmadugsum.e . . 3 = (.g‘(mulGrp‘𝑃))
8 cpmadugsum.m . . 3 · = ( ·𝑠𝑌)
9 cpmadugsum.r . . 3 × = (.r𝑌)
10 cpmadugsum.1 . . 3 1 = (1r𝑌)
11 cpmadugsum.g . . 3 + = (+g𝑌)
12 cpmadugsum.s . . 3 = (-g𝑌)
13 cpmadugsum.i . . 3 𝐼 = ((𝑋 · 1 ) (𝑇𝑀))
151, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14cpmadugsumfi 20501 . 2 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵𝑚 (0...𝑠))(𝐼 × (𝐽𝐼)) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
16 simpr 476 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ (𝐼 × (𝐽𝐼)) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))) → (𝐼 × (𝐽𝐼)) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
17 cpmadugsum.0 . . . . . . . . . 10 0 = (0g𝑌)
18 cpmadugsum.g2 . . . . . . . . . 10 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛))))))))
191, 2, 3, 4, 9, 12, 17, 5, 18, 6, 8, 7, 11chfacfscmulgsum 20484 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
2019eqcomd 2616 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖)))))
2120adantr 480 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ (𝐼 × (𝐽𝐼)) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))) → ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖)))))
2216, 21eqtrd 2644 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) ∧ (𝐼 × (𝐽𝐼)) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0)))))) → (𝐼 × (𝐽𝐼)) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖)))))
2322ex 449 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → ((𝐼 × (𝐽𝐼)) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))) → (𝐼 × (𝐽𝐼)) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖))))))
2423anassrs 678 . . . 4 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → ((𝐼 × (𝐽𝐼)) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))) → (𝐼 × (𝐽𝐼)) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖))))))
2524reximdva 3000 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) → (∃𝑏 ∈ (𝐵𝑚 (0...𝑠))(𝐼 × (𝐽𝐼)) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))) → ∃𝑏 ∈ (𝐵𝑚 (0...𝑠))(𝐼 × (𝐽𝐼)) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖))))))
2625reximdva 3000 . 2 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵𝑚 (0...𝑠))(𝐼 × (𝐽𝐼)) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵𝑚 (0...𝑠))(𝐼 × (𝐽𝐼)) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖))))))
2715, 26mpd 15 1 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵𝑚 (0...𝑠))(𝐼 × (𝐽𝐼)) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 𝑋) · (𝐺𝑖)))))