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

Theorem decpmatmul 20855
Description: The matrix consisting of the coefficients in the polynomial entries of the product of two polynomial matrices is a sum of products of the matrices consisting of the coefficients in the polynomial entries of the polynomial matrices for the same power. (Contributed by AV, 21-Oct-2019.) (Revised by AV, 3-Dec-2019.)
Hypotheses
Ref Expression
decpmatmul.p 𝑃 = (Poly1𝑅)
decpmatmul.c 𝐶 = (𝑁 Mat 𝑃)
decpmatmul.b 𝐵 = (Base‘𝐶)
decpmatmul.a 𝐴 = (𝑁 Mat 𝑅)
Assertion
Ref Expression
decpmatmul ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) → ((𝑈(.r𝐶)𝑊) decompPMat 𝐾) = (𝐴 Σg (𝑘 ∈ (0...𝐾) ↦ ((𝑈 decompPMat 𝑘)(.r𝐴)(𝑊 decompPMat (𝐾𝑘))))))
Distinct variable groups:   𝐵,𝑘   𝑘,𝐾   𝑘,𝑁   𝑃,𝑘   𝑅,𝑘   𝑈,𝑘   𝑘,𝑊   𝐴,𝑘
Allowed substitution hint:   𝐶(𝑘)

Proof of Theorem decpmatmul
Dummy variables 𝑡 𝑖 𝑗 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqidd 2765 . . . . 5 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → (𝑥𝑁, 𝑦𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝐾) ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦))))))) = (𝑥𝑁, 𝑦𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝐾) ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦))))))))
2 oveq1 6848 . . . . . . . . . . 11 (𝑥 = 𝑖 → (𝑥(𝑈 decompPMat 𝑘)𝑡) = (𝑖(𝑈 decompPMat 𝑘)𝑡))
3 oveq2 6849 . . . . . . . . . . 11 (𝑦 = 𝑗 → (𝑡(𝑊 decompPMat (𝐾𝑘))𝑦) = (𝑡(𝑊 decompPMat (𝐾𝑘))𝑗))
42, 3oveqan12d 6860 . . . . . . . . . 10 ((𝑥 = 𝑖𝑦 = 𝑗) → ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦)) = ((𝑖(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑗)))
54mpteq2dv 4903 . . . . . . . . 9 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦))) = (𝑡𝑁 ↦ ((𝑖(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑗))))
65oveq2d 6857 . . . . . . . 8 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑅 Σg (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦)))) = (𝑅 Σg (𝑡𝑁 ↦ ((𝑖(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑗)))))
76mpteq2dv 4903 . . . . . . 7 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑘 ∈ (0...𝐾) ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦))))) = (𝑘 ∈ (0...𝐾) ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑖(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑗))))))
87oveq2d 6857 . . . . . 6 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑅 Σg (𝑘 ∈ (0...𝐾) ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦)))))) = (𝑅 Σg (𝑘 ∈ (0...𝐾) ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑖(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑗)))))))
98adantl 473 . . . . 5 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ (𝑥 = 𝑖𝑦 = 𝑗)) → (𝑅 Σg (𝑘 ∈ (0...𝐾) ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦)))))) = (𝑅 Σg (𝑘 ∈ (0...𝐾) ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑖(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑗)))))))
10 simprl 787 . . . . 5 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → 𝑖𝑁)
11 simprr 789 . . . . 5 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → 𝑗𝑁)
12 ovexd 6875 . . . . 5 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → (𝑅 Σg (𝑘 ∈ (0...𝐾) ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑖(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑗)))))) ∈ V)
131, 9, 10, 11, 12ovmpt2d 6985 . . . 4 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → (𝑖(𝑥𝑁, 𝑦𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝐾) ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦)))))))𝑗) = (𝑅 Σg (𝑘 ∈ (0...𝐾) ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑖(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑗)))))))
14 decpmatmul.c . . . . . . . . . . . . . . . . . . . 20 𝐶 = (𝑁 Mat 𝑃)
15 decpmatmul.b . . . . . . . . . . . . . . . . . . . 20 𝐵 = (Base‘𝐶)
1614, 15matrcl 20493 . . . . . . . . . . . . . . . . . . 19 (𝑈𝐵 → (𝑁 ∈ Fin ∧ 𝑃 ∈ V))
1716simpld 488 . . . . . . . . . . . . . . . . . 18 (𝑈𝐵𝑁 ∈ Fin)
1817adantr 472 . . . . . . . . . . . . . . . . 17 ((𝑈𝐵𝑊𝐵) → 𝑁 ∈ Fin)
1918anim2i 610 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵)) → (𝑅 ∈ Ring ∧ 𝑁 ∈ Fin))
2019ancomd 453 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
21203adant3 1162 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
22 decpmatmul.a . . . . . . . . . . . . . . 15 𝐴 = (𝑁 Mat 𝑅)
23 eqid 2764 . . . . . . . . . . . . . . 15 (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)
2422, 23matmulr 20519 . . . . . . . . . . . . . 14 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (.r𝐴))
2521, 24syl 17 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (.r𝐴))
2625adantr 472 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (.r𝐴))
2726adantr 472 . . . . . . . . . . 11 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (.r𝐴))
2827eqcomd 2770 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → (.r𝐴) = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩))
2928oveqd 6858 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → ((𝑈 decompPMat 𝑘)(.r𝐴)(𝑊 decompPMat (𝐾𝑘))) = ((𝑈 decompPMat 𝑘)(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)(𝑊 decompPMat (𝐾𝑘))))
30 eqid 2764 . . . . . . . . . 10 (Base‘𝑅) = (Base‘𝑅)
31 eqid 2764 . . . . . . . . . 10 (.r𝑅) = (.r𝑅)
32 simp1 1166 . . . . . . . . . . . 12 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) → 𝑅 ∈ Ring)
3332adantr 472 . . . . . . . . . . 11 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → 𝑅 ∈ Ring)
3433adantr 472 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → 𝑅 ∈ Ring)
3521simpld 488 . . . . . . . . . . . 12 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) → 𝑁 ∈ Fin)
3635adantr 472 . . . . . . . . . . 11 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → 𝑁 ∈ Fin)
3736adantr 472 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → 𝑁 ∈ Fin)
38 simpl2l 1297 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → 𝑈𝐵)
3938adantr 472 . . . . . . . . . . . . 13 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → 𝑈𝐵)
40 elfznn0 12639 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐾) → 𝑘 ∈ ℕ0)
4140adantl 473 . . . . . . . . . . . . 13 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → 𝑘 ∈ ℕ0)
4234, 39, 413jca 1158 . . . . . . . . . . . 12 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → (𝑅 ∈ Ring ∧ 𝑈𝐵𝑘 ∈ ℕ0))
43 decpmatmul.p . . . . . . . . . . . . 13 𝑃 = (Poly1𝑅)
44 eqid 2764 . . . . . . . . . . . . 13 (Base‘𝐴) = (Base‘𝐴)
4543, 14, 15, 22, 44decpmatcl 20850 . . . . . . . . . . . 12 ((𝑅 ∈ Ring ∧ 𝑈𝐵𝑘 ∈ ℕ0) → (𝑈 decompPMat 𝑘) ∈ (Base‘𝐴))
4642, 45syl 17 . . . . . . . . . . 11 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → (𝑈 decompPMat 𝑘) ∈ (Base‘𝐴))
4722, 30, 44matbas2i 20503 . . . . . . . . . . 11 ((𝑈 decompPMat 𝑘) ∈ (Base‘𝐴) → (𝑈 decompPMat 𝑘) ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
4846, 47syl 17 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → (𝑈 decompPMat 𝑘) ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
49 simpl2r 1299 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → 𝑊𝐵)
5049adantr 472 . . . . . . . . . . . . 13 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → 𝑊𝐵)
51 fznn0sub 12579 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐾) → (𝐾𝑘) ∈ ℕ0)
5251adantl 473 . . . . . . . . . . . . 13 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → (𝐾𝑘) ∈ ℕ0)
5334, 50, 523jca 1158 . . . . . . . . . . . 12 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → (𝑅 ∈ Ring ∧ 𝑊𝐵 ∧ (𝐾𝑘) ∈ ℕ0))
5443, 14, 15, 22, 44decpmatcl 20850 . . . . . . . . . . . 12 ((𝑅 ∈ Ring ∧ 𝑊𝐵 ∧ (𝐾𝑘) ∈ ℕ0) → (𝑊 decompPMat (𝐾𝑘)) ∈ (Base‘𝐴))
5553, 54syl 17 . . . . . . . . . . 11 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → (𝑊 decompPMat (𝐾𝑘)) ∈ (Base‘𝐴))
5622, 30, 44matbas2i 20503 . . . . . . . . . . 11 ((𝑊 decompPMat (𝐾𝑘)) ∈ (Base‘𝐴) → (𝑊 decompPMat (𝐾𝑘)) ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
5755, 56syl 17 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → (𝑊 decompPMat (𝐾𝑘)) ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
5823, 30, 31, 34, 37, 37, 37, 48, 57mamuval 20467 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → ((𝑈 decompPMat 𝑘)(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)(𝑊 decompPMat (𝐾𝑘))) = (𝑥𝑁, 𝑦𝑁 ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦))))))
5929, 58eqtrd 2798 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → ((𝑈 decompPMat 𝑘)(.r𝐴)(𝑊 decompPMat (𝐾𝑘))) = (𝑥𝑁, 𝑦𝑁 ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦))))))
6059mpteq2dva 4902 . . . . . . 7 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → (𝑘 ∈ (0...𝐾) ↦ ((𝑈 decompPMat 𝑘)(.r𝐴)(𝑊 decompPMat (𝐾𝑘)))) = (𝑘 ∈ (0...𝐾) ↦ (𝑥𝑁, 𝑦𝑁 ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦)))))))
6160oveq2d 6857 . . . . . 6 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → (𝐴 Σg (𝑘 ∈ (0...𝐾) ↦ ((𝑈 decompPMat 𝑘)(.r𝐴)(𝑊 decompPMat (𝐾𝑘))))) = (𝐴 Σg (𝑘 ∈ (0...𝐾) ↦ (𝑥𝑁, 𝑦𝑁 ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦))))))))
62 eqid 2764 . . . . . . 7 (0g𝐴) = (0g𝐴)
63 ovexd 6875 . . . . . . 7 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → (0...𝐾) ∈ V)
64 ringcmn 18847 . . . . . . . . . . . . 13 (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
6532, 64syl 17 . . . . . . . . . . . 12 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) → 𝑅 ∈ CMnd)
6665adantr 472 . . . . . . . . . . 11 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → 𝑅 ∈ CMnd)
6766adantr 472 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → 𝑅 ∈ CMnd)
68673ad2ant1 1163 . . . . . . . . 9 (((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑥𝑁𝑦𝑁) → 𝑅 ∈ CMnd)
69373ad2ant1 1163 . . . . . . . . 9 (((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑥𝑁𝑦𝑁) → 𝑁 ∈ Fin)
70343ad2ant1 1163 . . . . . . . . . . . 12 (((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑥𝑁𝑦𝑁) → 𝑅 ∈ Ring)
7170adantr 472 . . . . . . . . . . 11 ((((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑥𝑁𝑦𝑁) ∧ 𝑡𝑁) → 𝑅 ∈ Ring)
72 simpl2 1244 . . . . . . . . . . . 12 ((((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑥𝑁𝑦𝑁) ∧ 𝑡𝑁) → 𝑥𝑁)
73 simpr 477 . . . . . . . . . . . 12 ((((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑥𝑁𝑦𝑁) ∧ 𝑡𝑁) → 𝑡𝑁)
74423ad2ant1 1163 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑥𝑁𝑦𝑁) → (𝑅 ∈ Ring ∧ 𝑈𝐵𝑘 ∈ ℕ0))
7574adantr 472 . . . . . . . . . . . . 13 ((((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑥𝑁𝑦𝑁) ∧ 𝑡𝑁) → (𝑅 ∈ Ring ∧ 𝑈𝐵𝑘 ∈ ℕ0))
7675, 45syl 17 . . . . . . . . . . . 12 ((((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑥𝑁𝑦𝑁) ∧ 𝑡𝑁) → (𝑈 decompPMat 𝑘) ∈ (Base‘𝐴))
7722, 30, 44, 72, 73, 76matecld 20507 . . . . . . . . . . 11 ((((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑥𝑁𝑦𝑁) ∧ 𝑡𝑁) → (𝑥(𝑈 decompPMat 𝑘)𝑡) ∈ (Base‘𝑅))
78 simpl3 1246 . . . . . . . . . . . 12 ((((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑥𝑁𝑦𝑁) ∧ 𝑡𝑁) → 𝑦𝑁)
79553ad2ant1 1163 . . . . . . . . . . . . 13 (((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑥𝑁𝑦𝑁) → (𝑊 decompPMat (𝐾𝑘)) ∈ (Base‘𝐴))
8079adantr 472 . . . . . . . . . . . 12 ((((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑥𝑁𝑦𝑁) ∧ 𝑡𝑁) → (𝑊 decompPMat (𝐾𝑘)) ∈ (Base‘𝐴))
8122, 30, 44, 73, 78, 80matecld 20507 . . . . . . . . . . 11 ((((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑥𝑁𝑦𝑁) ∧ 𝑡𝑁) → (𝑡(𝑊 decompPMat (𝐾𝑘))𝑦) ∈ (Base‘𝑅))
8230, 31ringcl 18827 . . . . . . . . . . 11 ((𝑅 ∈ Ring ∧ (𝑥(𝑈 decompPMat 𝑘)𝑡) ∈ (Base‘𝑅) ∧ (𝑡(𝑊 decompPMat (𝐾𝑘))𝑦) ∈ (Base‘𝑅)) → ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦)) ∈ (Base‘𝑅))
8371, 77, 81, 82syl3anc 1490 . . . . . . . . . 10 ((((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑥𝑁𝑦𝑁) ∧ 𝑡𝑁) → ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦)) ∈ (Base‘𝑅))
8483ralrimiva 3112 . . . . . . . . 9 (((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑥𝑁𝑦𝑁) → ∀𝑡𝑁 ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦)) ∈ (Base‘𝑅))
8530, 68, 69, 84gsummptcl 18631 . . . . . . . 8 (((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑥𝑁𝑦𝑁) → (𝑅 Σg (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦)))) ∈ (Base‘𝑅))
8622, 30, 44, 37, 34, 85matbas2d 20504 . . . . . . 7 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → (𝑥𝑁, 𝑦𝑁 ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦))))) ∈ (Base‘𝐴))
87 eqid 2764 . . . . . . . 8 (𝑘 ∈ (0...𝐾) ↦ (𝑥𝑁, 𝑦𝑁 ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦)))))) = (𝑘 ∈ (0...𝐾) ↦ (𝑥𝑁, 𝑦𝑁 ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦))))))
88 fzfid 12979 . . . . . . . 8 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → (0...𝐾) ∈ Fin)
89 simpl 474 . . . . . . . . . . . . . . 15 ((𝑁 ∈ Fin ∧ 𝑃 ∈ V) → 𝑁 ∈ Fin)
9089, 89jca 507 . . . . . . . . . . . . . 14 ((𝑁 ∈ Fin ∧ 𝑃 ∈ V) → (𝑁 ∈ Fin ∧ 𝑁 ∈ Fin))
9116, 90syl 17 . . . . . . . . . . . . 13 (𝑈𝐵 → (𝑁 ∈ Fin ∧ 𝑁 ∈ Fin))
9291adantr 472 . . . . . . . . . . . 12 ((𝑈𝐵𝑊𝐵) → (𝑁 ∈ Fin ∧ 𝑁 ∈ Fin))
93923ad2ant2 1164 . . . . . . . . . . 11 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) → (𝑁 ∈ Fin ∧ 𝑁 ∈ Fin))
9493adantr 472 . . . . . . . . . 10 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → (𝑁 ∈ Fin ∧ 𝑁 ∈ Fin))
9594adantr 472 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → (𝑁 ∈ Fin ∧ 𝑁 ∈ Fin))
96 mpt2exga 7446 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑁 ∈ Fin) → (𝑥𝑁, 𝑦𝑁 ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦))))) ∈ V)
9795, 96syl 17 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → (𝑥𝑁, 𝑦𝑁 ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦))))) ∈ V)
98 fvexd 6389 . . . . . . . 8 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → (0g𝐴) ∈ V)
9987, 88, 97, 98fsuppmptdm 8492 . . . . . . 7 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → (𝑘 ∈ (0...𝐾) ↦ (𝑥𝑁, 𝑦𝑁 ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦)))))) finSupp (0g𝐴))
10022, 44, 62, 36, 63, 33, 86, 99matgsum 20518 . . . . . 6 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → (𝐴 Σg (𝑘 ∈ (0...𝐾) ↦ (𝑥𝑁, 𝑦𝑁 ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦))))))) = (𝑥𝑁, 𝑦𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝐾) ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦))))))))
10161, 100eqtrd 2798 . . . . 5 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → (𝐴 Σg (𝑘 ∈ (0...𝐾) ↦ ((𝑈 decompPMat 𝑘)(.r𝐴)(𝑊 decompPMat (𝐾𝑘))))) = (𝑥𝑁, 𝑦𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝐾) ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦))))))))
102101oveqd 6858 . . . 4 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → (𝑖(𝐴 Σg (𝑘 ∈ (0...𝐾) ↦ ((𝑈 decompPMat 𝑘)(.r𝐴)(𝑊 decompPMat (𝐾𝑘)))))𝑗) = (𝑖(𝑥𝑁, 𝑦𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝐾) ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑥(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑦)))))))𝑗))
103 simpl2 1244 . . . . . 6 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → (𝑈𝐵𝑊𝐵))
104 simpl3 1246 . . . . . 6 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → 𝐾 ∈ ℕ0)
10543, 14, 15decpmatmullem 20854 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑈𝐵𝑊𝐵) ∧ (𝑖𝑁𝑗𝑁𝐾 ∈ ℕ0)) → (𝑖((𝑈(.r𝐶)𝑊) decompPMat 𝐾)𝑗) = (𝑅 Σg (𝑡𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝐾) ↦ (((coe1‘(𝑖𝑈𝑡))‘𝑘)(.r𝑅)((coe1‘(𝑡𝑊𝑗))‘(𝐾𝑘))))))))
10636, 33, 103, 10, 11, 104, 105syl213anc 1508 . . . . 5 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → (𝑖((𝑈(.r𝐶)𝑊) decompPMat 𝐾)𝑗) = (𝑅 Σg (𝑡𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝐾) ↦ (((coe1‘(𝑖𝑈𝑡))‘𝑘)(.r𝑅)((coe1‘(𝑡𝑊𝑗))‘(𝐾𝑘))))))))
107 simpll1 1269 . . . . . . 7 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ (𝑡𝑁𝑘 ∈ (0...𝐾))) → 𝑅 ∈ Ring)
108 simplrl 795 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ (𝑡𝑁𝑘 ∈ (0...𝐾))) → 𝑖𝑁)
109 simprl 787 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ (𝑡𝑁𝑘 ∈ (0...𝐾))) → 𝑡𝑁)
11015eleq2i 2835 . . . . . . . . . . . . . 14 (𝑈𝐵𝑈 ∈ (Base‘𝐶))
111110biimpi 207 . . . . . . . . . . . . 13 (𝑈𝐵𝑈 ∈ (Base‘𝐶))
112111adantr 472 . . . . . . . . . . . 12 ((𝑈𝐵𝑊𝐵) → 𝑈 ∈ (Base‘𝐶))
1131123ad2ant2 1164 . . . . . . . . . . 11 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) → 𝑈 ∈ (Base‘𝐶))
114113adantr 472 . . . . . . . . . 10 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → 𝑈 ∈ (Base‘𝐶))
115114adantr 472 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ (𝑡𝑁𝑘 ∈ (0...𝐾))) → 𝑈 ∈ (Base‘𝐶))
116 eqid 2764 . . . . . . . . . 10 (Base‘𝑃) = (Base‘𝑃)
11714, 116matecl 20506 . . . . . . . . 9 ((𝑖𝑁𝑡𝑁𝑈 ∈ (Base‘𝐶)) → (𝑖𝑈𝑡) ∈ (Base‘𝑃))
118108, 109, 115, 117syl3anc 1490 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ (𝑡𝑁𝑘 ∈ (0...𝐾))) → (𝑖𝑈𝑡) ∈ (Base‘𝑃))
11940ad2antll 720 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ (𝑡𝑁𝑘 ∈ (0...𝐾))) → 𝑘 ∈ ℕ0)
120 eqid 2764 . . . . . . . . 9 (coe1‘(𝑖𝑈𝑡)) = (coe1‘(𝑖𝑈𝑡))
121120, 116, 43, 30coe1fvalcl 19854 . . . . . . . 8 (((𝑖𝑈𝑡) ∈ (Base‘𝑃) ∧ 𝑘 ∈ ℕ0) → ((coe1‘(𝑖𝑈𝑡))‘𝑘) ∈ (Base‘𝑅))
122118, 119, 121syl2anc 579 . . . . . . 7 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ (𝑡𝑁𝑘 ∈ (0...𝐾))) → ((coe1‘(𝑖𝑈𝑡))‘𝑘) ∈ (Base‘𝑅))
123 simplrr 796 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ (𝑡𝑁𝑘 ∈ (0...𝐾))) → 𝑗𝑁)
12449adantr 472 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ (𝑡𝑁𝑘 ∈ (0...𝐾))) → 𝑊𝐵)
12514, 116, 15, 109, 123, 124matecld 20507 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ (𝑡𝑁𝑘 ∈ (0...𝐾))) → (𝑡𝑊𝑗) ∈ (Base‘𝑃))
12651ad2antll 720 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ (𝑡𝑁𝑘 ∈ (0...𝐾))) → (𝐾𝑘) ∈ ℕ0)
127 eqid 2764 . . . . . . . . 9 (coe1‘(𝑡𝑊𝑗)) = (coe1‘(𝑡𝑊𝑗))
128127, 116, 43, 30coe1fvalcl 19854 . . . . . . . 8 (((𝑡𝑊𝑗) ∈ (Base‘𝑃) ∧ (𝐾𝑘) ∈ ℕ0) → ((coe1‘(𝑡𝑊𝑗))‘(𝐾𝑘)) ∈ (Base‘𝑅))
129125, 126, 128syl2anc 579 . . . . . . 7 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ (𝑡𝑁𝑘 ∈ (0...𝐾))) → ((coe1‘(𝑡𝑊𝑗))‘(𝐾𝑘)) ∈ (Base‘𝑅))
13030, 31ringcl 18827 . . . . . . 7 ((𝑅 ∈ Ring ∧ ((coe1‘(𝑖𝑈𝑡))‘𝑘) ∈ (Base‘𝑅) ∧ ((coe1‘(𝑡𝑊𝑗))‘(𝐾𝑘)) ∈ (Base‘𝑅)) → (((coe1‘(𝑖𝑈𝑡))‘𝑘)(.r𝑅)((coe1‘(𝑡𝑊𝑗))‘(𝐾𝑘))) ∈ (Base‘𝑅))
131107, 122, 129, 130syl3anc 1490 . . . . . 6 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ (𝑡𝑁𝑘 ∈ (0...𝐾))) → (((coe1‘(𝑖𝑈𝑡))‘𝑘)(.r𝑅)((coe1‘(𝑡𝑊𝑗))‘(𝐾𝑘))) ∈ (Base‘𝑅))
13230, 66, 36, 88, 131gsumcom3fi 20481 . . . . 5 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → (𝑅 Σg (𝑡𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝐾) ↦ (((coe1‘(𝑖𝑈𝑡))‘𝑘)(.r𝑅)((coe1‘(𝑡𝑊𝑗))‘(𝐾𝑘))))))) = (𝑅 Σg (𝑘 ∈ (0...𝐾) ↦ (𝑅 Σg (𝑡𝑁 ↦ (((coe1‘(𝑖𝑈𝑡))‘𝑘)(.r𝑅)((coe1‘(𝑡𝑊𝑗))‘(𝐾𝑘))))))))
13342adantr 472 . . . . . . . . . . . 12 (((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑡𝑁) → (𝑅 ∈ Ring ∧ 𝑈𝐵𝑘 ∈ ℕ0))
13410adantr 472 . . . . . . . . . . . . 13 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → 𝑖𝑁)
135134anim1i 608 . . . . . . . . . . . 12 (((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑡𝑁) → (𝑖𝑁𝑡𝑁))
13643, 14, 15decpmate 20849 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝑈𝐵𝑘 ∈ ℕ0) ∧ (𝑖𝑁𝑡𝑁)) → (𝑖(𝑈 decompPMat 𝑘)𝑡) = ((coe1‘(𝑖𝑈𝑡))‘𝑘))
137133, 135, 136syl2anc 579 . . . . . . . . . . 11 (((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑡𝑁) → (𝑖(𝑈 decompPMat 𝑘)𝑡) = ((coe1‘(𝑖𝑈𝑡))‘𝑘))
13853adantr 472 . . . . . . . . . . . 12 (((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑡𝑁) → (𝑅 ∈ Ring ∧ 𝑊𝐵 ∧ (𝐾𝑘) ∈ ℕ0))
139 simplrr 796 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → 𝑗𝑁)
140139anim1i 608 . . . . . . . . . . . . 13 (((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑡𝑁) → (𝑗𝑁𝑡𝑁))
141140ancomd 453 . . . . . . . . . . . 12 (((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑡𝑁) → (𝑡𝑁𝑗𝑁))
14243, 14, 15decpmate 20849 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝑊𝐵 ∧ (𝐾𝑘) ∈ ℕ0) ∧ (𝑡𝑁𝑗𝑁)) → (𝑡(𝑊 decompPMat (𝐾𝑘))𝑗) = ((coe1‘(𝑡𝑊𝑗))‘(𝐾𝑘)))
143138, 141, 142syl2anc 579 . . . . . . . . . . 11 (((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑡𝑁) → (𝑡(𝑊 decompPMat (𝐾𝑘))𝑗) = ((coe1‘(𝑡𝑊𝑗))‘(𝐾𝑘)))
144137, 143oveq12d 6859 . . . . . . . . . 10 (((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑡𝑁) → ((𝑖(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑗)) = (((coe1‘(𝑖𝑈𝑡))‘𝑘)(.r𝑅)((coe1‘(𝑡𝑊𝑗))‘(𝐾𝑘))))
145144eqcomd 2770 . . . . . . . . 9 (((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) ∧ 𝑡𝑁) → (((coe1‘(𝑖𝑈𝑡))‘𝑘)(.r𝑅)((coe1‘(𝑡𝑊𝑗))‘(𝐾𝑘))) = ((𝑖(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑗)))
146145mpteq2dva 4902 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → (𝑡𝑁 ↦ (((coe1‘(𝑖𝑈𝑡))‘𝑘)(.r𝑅)((coe1‘(𝑡𝑊𝑗))‘(𝐾𝑘)))) = (𝑡𝑁 ↦ ((𝑖(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑗))))
147146oveq2d 6857 . . . . . . 7 ((((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑘 ∈ (0...𝐾)) → (𝑅 Σg (𝑡𝑁 ↦ (((coe1‘(𝑖𝑈𝑡))‘𝑘)(.r𝑅)((coe1‘(𝑡𝑊𝑗))‘(𝐾𝑘))))) = (𝑅 Σg (𝑡𝑁 ↦ ((𝑖(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑗)))))
148147mpteq2dva 4902 . . . . . 6 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → (𝑘 ∈ (0...𝐾) ↦ (𝑅 Σg (𝑡𝑁 ↦ (((coe1‘(𝑖𝑈𝑡))‘𝑘)(.r𝑅)((coe1‘(𝑡𝑊𝑗))‘(𝐾𝑘)))))) = (𝑘 ∈ (0...𝐾) ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑖(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑗))))))
149148oveq2d 6857 . . . . 5 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → (𝑅 Σg (𝑘 ∈ (0...𝐾) ↦ (𝑅 Σg (𝑡𝑁 ↦ (((coe1‘(𝑖𝑈𝑡))‘𝑘)(.r𝑅)((coe1‘(𝑡𝑊𝑗))‘(𝐾𝑘))))))) = (𝑅 Σg (𝑘 ∈ (0...𝐾) ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑖(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑗)))))))
150106, 132, 1493eqtrd 2802 . . . 4 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → (𝑖((𝑈(.r𝐶)𝑊) decompPMat 𝐾)𝑗) = (𝑅 Σg (𝑘 ∈ (0...𝐾) ↦ (𝑅 Σg (𝑡𝑁 ↦ ((𝑖(𝑈 decompPMat 𝑘)𝑡)(.r𝑅)(𝑡(𝑊 decompPMat (𝐾𝑘))𝑗)))))))
15113, 102, 1503eqtr4rd 2809 . . 3 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ (𝑖𝑁𝑗𝑁)) → (𝑖((𝑈(.r𝐶)𝑊) decompPMat 𝐾)𝑗) = (𝑖(𝐴 Σg (𝑘 ∈ (0...𝐾) ↦ ((𝑈 decompPMat 𝑘)(.r𝐴)(𝑊 decompPMat (𝐾𝑘)))))𝑗))
152151ralrimivva 3117 . 2 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) → ∀𝑖𝑁𝑗𝑁 (𝑖((𝑈(.r𝐶)𝑊) decompPMat 𝐾)𝑗) = (𝑖(𝐴 Σg (𝑘 ∈ (0...𝐾) ↦ ((𝑈 decompPMat 𝑘)(.r𝐴)(𝑊 decompPMat (𝐾𝑘)))))𝑗))
15343, 14pmatring 20776 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring)
15420, 153syl 17 . . . . . 6 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵)) → 𝐶 ∈ Ring)
155 simprl 787 . . . . . 6 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵)) → 𝑈𝐵)
156 simprr 789 . . . . . 6 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵)) → 𝑊𝐵)
157 eqid 2764 . . . . . . 7 (.r𝐶) = (.r𝐶)
15815, 157ringcl 18827 . . . . . 6 ((𝐶 ∈ Ring ∧ 𝑈𝐵𝑊𝐵) → (𝑈(.r𝐶)𝑊) ∈ 𝐵)
159154, 155, 156, 158syl3anc 1490 . . . . 5 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵)) → (𝑈(.r𝐶)𝑊) ∈ 𝐵)
1601593adant3 1162 . . . 4 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) → (𝑈(.r𝐶)𝑊) ∈ 𝐵)
16143, 14, 15, 22, 44decpmatcl 20850 . . . 4 ((𝑅 ∈ Ring ∧ (𝑈(.r𝐶)𝑊) ∈ 𝐵𝐾 ∈ ℕ0) → ((𝑈(.r𝐶)𝑊) decompPMat 𝐾) ∈ (Base‘𝐴))
162160, 161syld3an2 1531 . . 3 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) → ((𝑈(.r𝐶)𝑊) decompPMat 𝐾) ∈ (Base‘𝐴))
16322matring 20524 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring)
16421, 163syl 17 . . . . 5 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) → 𝐴 ∈ Ring)
165 ringcmn 18847 . . . . 5 (𝐴 ∈ Ring → 𝐴 ∈ CMnd)
166164, 165syl 17 . . . 4 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) → 𝐴 ∈ CMnd)
167 fzfid 12979 . . . 4 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) → (0...𝐾) ∈ Fin)
168164adantr 472 . . . . . 6 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝐾)) → 𝐴 ∈ Ring)
16932adantr 472 . . . . . . . 8 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝐾)) → 𝑅 ∈ Ring)
170 simpl2l 1297 . . . . . . . 8 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝐾)) → 𝑈𝐵)
17140adantl 473 . . . . . . . 8 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝐾)) → 𝑘 ∈ ℕ0)
172169, 170, 1713jca 1158 . . . . . . 7 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝐾)) → (𝑅 ∈ Ring ∧ 𝑈𝐵𝑘 ∈ ℕ0))
173172, 45syl 17 . . . . . 6 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝐾)) → (𝑈 decompPMat 𝑘) ∈ (Base‘𝐴))
174 simpl2r 1299 . . . . . . . 8 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝐾)) → 𝑊𝐵)
17551adantl 473 . . . . . . . 8 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝐾)) → (𝐾𝑘) ∈ ℕ0)
176169, 174, 1753jca 1158 . . . . . . 7 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝐾)) → (𝑅 ∈ Ring ∧ 𝑊𝐵 ∧ (𝐾𝑘) ∈ ℕ0))
177176, 54syl 17 . . . . . 6 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝐾)) → (𝑊 decompPMat (𝐾𝑘)) ∈ (Base‘𝐴))
178 eqid 2764 . . . . . . 7 (.r𝐴) = (.r𝐴)
17944, 178ringcl 18827 . . . . . 6 ((𝐴 ∈ Ring ∧ (𝑈 decompPMat 𝑘) ∈ (Base‘𝐴) ∧ (𝑊 decompPMat (𝐾𝑘)) ∈ (Base‘𝐴)) → ((𝑈 decompPMat 𝑘)(.r𝐴)(𝑊 decompPMat (𝐾𝑘))) ∈ (Base‘𝐴))
180168, 173, 177, 179syl3anc 1490 . . . . 5 (((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝐾)) → ((𝑈 decompPMat 𝑘)(.r𝐴)(𝑊 decompPMat (𝐾𝑘))) ∈ (Base‘𝐴))
181180ralrimiva 3112 . . . 4 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) → ∀𝑘 ∈ (0...𝐾)((𝑈 decompPMat 𝑘)(.r𝐴)(𝑊 decompPMat (𝐾𝑘))) ∈ (Base‘𝐴))
18244, 166, 167, 181gsummptcl 18631 . . 3 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) → (𝐴 Σg (𝑘 ∈ (0...𝐾) ↦ ((𝑈 decompPMat 𝑘)(.r𝐴)(𝑊 decompPMat (𝐾𝑘))))) ∈ (Base‘𝐴))
18322, 44eqmat 20505 . . 3 ((((𝑈(.r𝐶)𝑊) decompPMat 𝐾) ∈ (Base‘𝐴) ∧ (𝐴 Σg (𝑘 ∈ (0...𝐾) ↦ ((𝑈 decompPMat 𝑘)(.r𝐴)(𝑊 decompPMat (𝐾𝑘))))) ∈ (Base‘𝐴)) → (((𝑈(.r𝐶)𝑊) decompPMat 𝐾) = (𝐴 Σg (𝑘 ∈ (0...𝐾) ↦ ((𝑈 decompPMat 𝑘)(.r𝐴)(𝑊 decompPMat (𝐾𝑘))))) ↔ ∀𝑖𝑁𝑗𝑁 (𝑖((𝑈(.r𝐶)𝑊) decompPMat 𝐾)𝑗) = (𝑖(𝐴 Σg (𝑘 ∈ (0...𝐾) ↦ ((𝑈 decompPMat 𝑘)(.r𝐴)(𝑊 decompPMat (𝐾𝑘)))))𝑗)))
184162, 182, 183syl2anc 579 . 2 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) → (((𝑈(.r𝐶)𝑊) decompPMat 𝐾) = (𝐴 Σg (𝑘 ∈ (0...𝐾) ↦ ((𝑈 decompPMat 𝑘)(.r𝐴)(𝑊 decompPMat (𝐾𝑘))))) ↔ ∀𝑖𝑁𝑗𝑁 (𝑖((𝑈(.r𝐶)𝑊) decompPMat 𝐾)𝑗) = (𝑖(𝐴 Σg (𝑘 ∈ (0...𝐾) ↦ ((𝑈 decompPMat 𝑘)(.r𝐴)(𝑊 decompPMat (𝐾𝑘)))))𝑗)))
185152, 184mpbird 248 1 ((𝑅 ∈ Ring ∧ (𝑈𝐵𝑊𝐵) ∧ 𝐾 ∈ ℕ0) → ((𝑈(.r𝐶)𝑊) decompPMat 𝐾) = (𝐴 Σg (𝑘 ∈ (0...𝐾) ↦ ((𝑈 decompPMat 𝑘)(.r𝐴)(𝑊 decompPMat (𝐾𝑘))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wral 3054  Vcvv 3349  cotp 4341  cmpt 4887   × cxp 5274  cfv 6067  (class class class)co 6841  cmpt2 6843  𝑚 cmap 8059  Fincfn 8159  0cc0 10188  cmin 10519  0cn0 11537  ...cfz 12532  Basecbs 16131  .rcmulr 16216  0gc0g 16367   Σg cgsu 16368  CMndccmn 18458  Ringcrg 18813  Poly1cpl1 19819  coe1cco1 19820   maMul cmmul 20464   Mat cmat 20488   decompPMat cdecpmat 20845
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-inf2 8752  ax-cnex 10244  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-ot 4342  df-uni 4594  df-int 4633  df-iun 4677  df-iin 4678  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-se 5236  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-isom 6076  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-of 7094  df-ofr 7095  df-om 7263  df-1st 7365  df-2nd 7366  df-supp 7497  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-1o 7763  df-2o 7764  df-oadd 7767  df-er 7946  df-map 8061  df-pm 8062  df-ixp 8113  df-en 8160  df-dom 8161  df-sdom 8162  df-fin 8163  df-fsupp 8482  df-sup 8554  df-oi 8621  df-card 9015  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-nn 11274  df-2 11334  df-3 11335  df-4 11336  df-5 11337  df-6 11338  df-7 11339  df-8 11340  df-9 11341  df-n0 11538  df-z 11624  df-dec 11740  df-uz 11886  df-fz 12533  df-fzo 12673  df-seq 13008  df-hash 13321  df-struct 16133  df-ndx 16134  df-slot 16135  df-base 16137  df-sets 16138  df-ress 16139  df-plusg 16228  df-mulr 16229  df-sca 16231  df-vsca 16232  df-ip 16233  df-tset 16234  df-ple 16235  df-ds 16237  df-hom 16239  df-cco 16240  df-0g 16369  df-gsum 16370  df-prds 16375  df-pws 16377  df-mre 16513  df-mrc 16514  df-acs 16516  df-mgm 17509  df-sgrp 17551  df-mnd 17562  df-mhm 17602  df-submnd 17603  df-grp 17693  df-minusg 17694  df-sbg 17695  df-mulg 17809  df-subg 17856  df-ghm 17923  df-cntz 18014  df-cmn 18460  df-abl 18461  df-mgp 18756  df-ur 18768  df-ring 18815  df-subrg 19046  df-lmod 19133  df-lss 19201  df-sra 19445  df-rgmod 19446  df-psr 19629  df-mpl 19631  df-opsr 19633  df-psr1 19822  df-ply1 19824  df-coe1 19825  df-dsmm 20351  df-frlm 20366  df-mamu 20465  df-mat 20489  df-decpmat 20846
This theorem is referenced by:  decpmatmulsumfsupp  20856  pm2mpmhmlem1  20901  pm2mpmhmlem2  20902
  Copyright terms: Public domain W3C validator