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

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

Dummy variable 𝑛 is distinct from all other variables.
StepHypRef Expression
1 oveq2 7163 . . 3 ((𝐽𝐼) = (𝑌 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 𝑋) · (𝑇‘(𝑏𝑛))))) → (𝐼 × (𝐽𝐼)) = (𝐼 × (𝑌 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 𝑋) · (𝑇‘(𝑏𝑛)))))))
2 cpmadugsum.i . . . . . 6 𝐼 = ((𝑋 · 1 ) (𝑇𝑀))
32a1i 11 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → 𝐼 = ((𝑋 · 1 ) (𝑇𝑀)))
43oveq1d 7170 . . . 4 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝐼 × (𝑌 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 𝑋) · (𝑇‘(𝑏𝑛)))))) = (((𝑋 · 1 ) (𝑇𝑀)) × (𝑌 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 𝑋) · (𝑇‘(𝑏𝑛)))))))
5 eqid 2821 . . . . 5 (Base‘𝑌) = (Base‘𝑌)
6 cpmadugsum.r . . . . 5 × = (.r𝑌)
7 cpmadugsum.s . . . . 5 = (-g𝑌)
8 crngring 19307 . . . . . . . . 9 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
98anim2i 618 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
1093adant3 1128 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
1110ad2antrr 724 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
12 cpmadugsum.p . . . . . . 7 𝑃 = (Poly1𝑅)
13 cpmadugsum.y . . . . . . 7 𝑌 = (𝑁 Mat 𝑃)
1412, 13pmatring 21300 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring)
1511, 14syl 17 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → 𝑌 ∈ Ring)
1612, 13pmatlmod 21301 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ LMod)
178, 16sylan2 594 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ LMod)
188adantl 484 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 ∈ Ring)
19 cpmadugsum.x . . . . . . . . . . 11 𝑋 = (var1𝑅)
20 eqid 2821 . . . . . . . . . . 11 (Base‘𝑃) = (Base‘𝑃)
2119, 12, 20vr1cl 20384 . . . . . . . . . 10 (𝑅 ∈ Ring → 𝑋 ∈ (Base‘𝑃))
2218, 21syl 17 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑋 ∈ (Base‘𝑃))
2312ply1crng 20365 . . . . . . . . . . 11 (𝑅 ∈ CRing → 𝑃 ∈ CRing)
2413matsca2 21028 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑃 ∈ CRing) → 𝑃 = (Scalar‘𝑌))
2523, 24sylan2 594 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 = (Scalar‘𝑌))
2625fveq2d 6673 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (Base‘𝑃) = (Base‘(Scalar‘𝑌)))
2722, 26eleqtrd 2915 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑋 ∈ (Base‘(Scalar‘𝑌)))
288, 14sylan2 594 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ Ring)
29 cpmadugsum.1 . . . . . . . . . 10 1 = (1r𝑌)
305, 29ringidcl 19317 . . . . . . . . 9 (𝑌 ∈ Ring → 1 ∈ (Base‘𝑌))
3128, 30syl 17 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 1 ∈ (Base‘𝑌))
32 eqid 2821 . . . . . . . . 9 (Scalar‘𝑌) = (Scalar‘𝑌)
33 cpmadugsum.m . . . . . . . . 9 · = ( ·𝑠𝑌)
34 eqid 2821 . . . . . . . . 9 (Base‘(Scalar‘𝑌)) = (Base‘(Scalar‘𝑌))
355, 32, 33, 34lmodvscl 19650 . . . . . . . 8 ((𝑌 ∈ LMod ∧ 𝑋 ∈ (Base‘(Scalar‘𝑌)) ∧ 1 ∈ (Base‘𝑌)) → (𝑋 · 1 ) ∈ (Base‘𝑌))
3617, 27, 31, 35syl3anc 1367 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑋 · 1 ) ∈ (Base‘𝑌))
37363adant3 1128 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑋 · 1 ) ∈ (Base‘𝑌))
3837ad2antrr 724 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝑋 · 1 ) ∈ (Base‘𝑌))
39 cpmadugsum.t . . . . . . . 8 𝑇 = (𝑁 matToPolyMat 𝑅)
40 cpmadugsum.a . . . . . . . 8 𝐴 = (𝑁 Mat 𝑅)
41 cpmadugsum.b . . . . . . . 8 𝐵 = (Base‘𝐴)
4239, 40, 41, 12, 13mat2pmatbas 21333 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) → (𝑇𝑀) ∈ (Base‘𝑌))
438, 42syl3an2 1160 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑇𝑀) ∈ (Base‘𝑌))
4443ad2antrr 724 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝑇𝑀) ∈ (Base‘𝑌))
45 ringcmn 19330 . . . . . . . . 9 (𝑌 ∈ Ring → 𝑌 ∈ CMnd)
4628, 45syl 17 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ CMnd)
47463adant3 1128 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ CMnd)
4847ad2antrr 724 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → 𝑌 ∈ CMnd)
49 fzfid 13340 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (0...𝑠) ∈ Fin)
5010ad3antrrr 728 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ (0...𝑠)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
51 elmapi 8427 . . . . . . . . . . 11 (𝑏 ∈ (𝐵m (0...𝑠)) → 𝑏:(0...𝑠)⟶𝐵)
52 ffvelrn 6848 . . . . . . . . . . . 12 ((𝑏:(0...𝑠)⟶𝐵𝑛 ∈ (0...𝑠)) → (𝑏𝑛) ∈ 𝐵)
5352ex 415 . . . . . . . . . . 11 (𝑏:(0...𝑠)⟶𝐵 → (𝑛 ∈ (0...𝑠) → (𝑏𝑛) ∈ 𝐵))
5451, 53syl 17 . . . . . . . . . 10 (𝑏 ∈ (𝐵m (0...𝑠)) → (𝑛 ∈ (0...𝑠) → (𝑏𝑛) ∈ 𝐵))
5554adantl 484 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝑛 ∈ (0...𝑠) → (𝑏𝑛) ∈ 𝐵))
5655imp 409 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ (0...𝑠)) → (𝑏𝑛) ∈ 𝐵)
57 elfznn0 12999 . . . . . . . . 9 (𝑛 ∈ (0...𝑠) → 𝑛 ∈ ℕ0)
5857adantl 484 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ (0...𝑠)) → 𝑛 ∈ ℕ0)
59 cpmadugsum.e . . . . . . . . 9 = (.g‘(mulGrp‘𝑃))
6040, 41, 39, 12, 13, 5, 33, 59, 19mat2pmatscmxcl 21347 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝑏𝑛) ∈ 𝐵𝑛 ∈ ℕ0)) → ((𝑛 𝑋) · (𝑇‘(𝑏𝑛))) ∈ (Base‘𝑌))
6150, 56, 58, 60syl12anc 834 . . . . . . 7 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ (0...𝑠)) → ((𝑛 𝑋) · (𝑇‘(𝑏𝑛))) ∈ (Base‘𝑌))
6261ralrimiva 3182 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → ∀𝑛 ∈ (0...𝑠)((𝑛 𝑋) · (𝑇‘(𝑏𝑛))) ∈ (Base‘𝑌))
635, 48, 49, 62gsummptcl 19086 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝑌 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 𝑋) · (𝑇‘(𝑏𝑛))))) ∈ (Base‘𝑌))
645, 6, 7, 15, 38, 44, 63rngsubdir 19349 . . . 4 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (((𝑋 · 1 ) (𝑇𝑀)) × (𝑌 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 𝑋) · (𝑇‘(𝑏𝑛)))))) = (((𝑋 · 1 ) × (𝑌 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 𝑋) · (𝑇‘(𝑏𝑛)))))) ((𝑇𝑀) × (𝑌 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 𝑋) · (𝑇‘(𝑏𝑛))))))))
65 oveq1 7162 . . . . . . . . . 10 (𝑛 = 𝑖 → (𝑛 𝑋) = (𝑖 𝑋))
66 2fveq3 6674 . . . . . . . . . 10 (𝑛 = 𝑖 → (𝑇‘(𝑏𝑛)) = (𝑇‘(𝑏𝑖)))
6765, 66oveq12d 7173 . . . . . . . . 9 (𝑛 = 𝑖 → ((𝑛 𝑋) · (𝑇‘(𝑏𝑛))) = ((𝑖 𝑋) · (𝑇‘(𝑏𝑖))))
6867cbvmptv 5168 . . . . . . . 8 (𝑛 ∈ (0...𝑠) ↦ ((𝑛 𝑋) · (𝑇‘(𝑏𝑛)))) = (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖))))
6968oveq2i 7166 . . . . . . 7 (𝑌 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 𝑋) · (𝑇‘(𝑏𝑛))))) = (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖)))))
7069oveq2i 7166 . . . . . 6 ((𝑋 · 1 ) × (𝑌 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 𝑋) · (𝑇‘(𝑏𝑛)))))) = ((𝑋 · 1 ) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖))))))
7169oveq2i 7166 . . . . . 6 ((𝑇𝑀) × (𝑌 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 𝑋) · (𝑇‘(𝑏𝑛)))))) = ((𝑇𝑀) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖))))))
7270, 71oveq12i 7167 . . . . 5 (((𝑋 · 1 ) × (𝑌 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 𝑋) · (𝑇‘(𝑏𝑛)))))) ((𝑇𝑀) × (𝑌 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 𝑋) · (𝑇‘(𝑏𝑛))))))) = (((𝑋 · 1 ) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖)))))) ((𝑇𝑀) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖)))))))
73 cpmadugsum.g . . . . . . 7 + = (+g𝑌)
7440, 41, 12, 13, 39, 19, 59, 33, 6, 29, 73, 7cpmadugsumlemF 21483 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → (((𝑋 · 1 ) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖)))))) ((𝑇𝑀) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖))))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
7574anassrs 470 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (((𝑋 · 1 ) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖)))))) ((𝑇𝑀) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 𝑋) · (𝑇‘(𝑏𝑖))))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
7672, 75syl5eq 2868 . . . 4 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (((𝑋 · 1 ) × (𝑌 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 𝑋) · (𝑇‘(𝑏𝑛)))))) ((𝑇𝑀) × (𝑌 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 𝑋) · (𝑇‘(𝑏𝑛))))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
774, 64, 763eqtrd 2860 . . 3 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝐼 × (𝑌 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 𝑋) · (𝑇‘(𝑏𝑛)))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
781, 77sylan9eqr 2878 . 2 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ (𝐽𝐼) = (𝑌 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 𝑋) · (𝑇‘(𝑏𝑛)))))) → (𝐼 × (𝐽𝐼)) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))
79 cpmadugsum.j . . . . . . 7 𝐽 = (𝑁 maAdju 𝑃)
8013, 79, 5maduf 21249 . . . . . 6 (𝑃 ∈ CRing → 𝐽:(Base‘𝑌)⟶(Base‘𝑌))
8123, 80syl 17 . . . . 5 (𝑅 ∈ CRing → 𝐽:(Base‘𝑌)⟶(Base‘𝑌))
82813ad2ant2 1130 . . . 4 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝐽:(Base‘𝑌)⟶(Base‘𝑌))
8340, 41, 12, 13, 19, 39, 7, 33, 29, 2chmatcl 21435 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) → 𝐼 ∈ (Base‘𝑌))
848, 83syl3an2 1160 . . . 4 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝐼 ∈ (Base‘𝑌))
8582, 84ffvelrnd 6851 . . 3 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝐽𝐼) ∈ (Base‘𝑌))
8612, 13, 5, 33, 59, 19, 39, 40, 41pmatcollpw3fi1 21395 . . 3 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ (𝐽𝐼) ∈ (Base‘𝑌)) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵m (0...𝑠))(𝐽𝐼) = (𝑌 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 𝑋) · (𝑇‘(𝑏𝑛))))))
8785, 86syld3an3 1405 . 2 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵m (0...𝑠))(𝐽𝐼) = (𝑌 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 𝑋) · (𝑇‘(𝑏𝑛))))))
8878, 87reximddv2 3278 1 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵m (0...𝑠))(𝐼 × (𝐽𝐼)) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑖))))))) + ((((𝑠 + 1) 𝑋) · (𝑇‘(𝑏𝑠))) ((𝑇𝑀) × (𝑇‘(𝑏‘0))))))