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

Theorem decpmatmul 22629
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 2727 . . . . 5 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑅 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦))))))) = (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑅 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦))))))))
2 oveq1 7412 . . . . . . . . . . 11 (π‘₯ = 𝑖 β†’ (π‘₯(π‘ˆ decompPMat π‘˜)𝑑) = (𝑖(π‘ˆ decompPMat π‘˜)𝑑))
3 oveq2 7413 . . . . . . . . . . 11 (𝑦 = 𝑗 β†’ (𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦) = (𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑗))
42, 3oveqan12d 7424 . . . . . . . . . 10 ((π‘₯ = 𝑖 ∧ 𝑦 = 𝑗) β†’ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦)) = ((𝑖(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑗)))
54mpteq2dv 5243 . . . . . . . . 9 ((π‘₯ = 𝑖 ∧ 𝑦 = 𝑗) β†’ (𝑑 ∈ 𝑁 ↦ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦))) = (𝑑 ∈ 𝑁 ↦ ((𝑖(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑗))))
65oveq2d 7421 . . . . . . . 8 ((π‘₯ = 𝑖 ∧ 𝑦 = 𝑗) β†’ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦)))) = (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((𝑖(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑗)))))
76mpteq2dv 5243 . . . . . . 7 ((π‘₯ = 𝑖 ∧ 𝑦 = 𝑗) β†’ (π‘˜ ∈ (0...𝐾) ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦))))) = (π‘˜ ∈ (0...𝐾) ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((𝑖(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑗))))))
87oveq2d 7421 . . . . . 6 ((π‘₯ = 𝑖 ∧ 𝑦 = 𝑗) β†’ (𝑅 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦)))))) = (𝑅 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((𝑖(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑗)))))))
98adantl 481 . . . . 5 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (π‘₯ = 𝑖 ∧ 𝑦 = 𝑗)) β†’ (𝑅 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦)))))) = (𝑅 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((𝑖(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑗)))))))
10 simprl 768 . . . . 5 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ 𝑖 ∈ 𝑁)
11 simprr 770 . . . . 5 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ 𝑗 ∈ 𝑁)
12 ovexd 7440 . . . . 5 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ (𝑅 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((𝑖(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑗)))))) ∈ V)
131, 9, 10, 11, 12ovmpod 7556 . . . 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 22267 . . . . . . . . . . . . . . . . . . 19 (π‘ˆ ∈ 𝐡 β†’ (𝑁 ∈ Fin ∧ 𝑃 ∈ V))
1716simpld 494 . . . . . . . . . . . . . . . . . 18 (π‘ˆ ∈ 𝐡 β†’ 𝑁 ∈ Fin)
1817adantr 480 . . . . . . . . . . . . . . . . 17 ((π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) β†’ 𝑁 ∈ Fin)
1918anim2i 616 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡)) β†’ (𝑅 ∈ Ring ∧ 𝑁 ∈ Fin))
2019ancomd 461 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡)) β†’ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
21203adant3 1129 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) β†’ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
22 decpmatmul.a . . . . . . . . . . . . . . 15 𝐴 = (𝑁 Mat 𝑅)
23 eqid 2726 . . . . . . . . . . . . . . 15 (𝑅 maMul βŸ¨π‘, 𝑁, π‘βŸ©) = (𝑅 maMul βŸ¨π‘, 𝑁, π‘βŸ©)
2422, 23matmulr 22295 . . . . . . . . . . . . . 14 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) β†’ (𝑅 maMul βŸ¨π‘, 𝑁, π‘βŸ©) = (.rβ€˜π΄))
2521, 24syl 17 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) β†’ (𝑅 maMul βŸ¨π‘, 𝑁, π‘βŸ©) = (.rβ€˜π΄))
2625adantr 480 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ (𝑅 maMul βŸ¨π‘, 𝑁, π‘βŸ©) = (.rβ€˜π΄))
2726adantr 480 . . . . . . . . . . 11 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ (𝑅 maMul βŸ¨π‘, 𝑁, π‘βŸ©) = (.rβ€˜π΄))
2827eqcomd 2732 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ (.rβ€˜π΄) = (𝑅 maMul βŸ¨π‘, 𝑁, π‘βŸ©))
2928oveqd 7422 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ ((π‘ˆ decompPMat π‘˜)(.rβ€˜π΄)(π‘Š decompPMat (𝐾 βˆ’ π‘˜))) = ((π‘ˆ decompPMat π‘˜)(𝑅 maMul βŸ¨π‘, 𝑁, π‘βŸ©)(π‘Š decompPMat (𝐾 βˆ’ π‘˜))))
30 eqid 2726 . . . . . . . . . 10 (Baseβ€˜π‘…) = (Baseβ€˜π‘…)
31 eqid 2726 . . . . . . . . . 10 (.rβ€˜π‘…) = (.rβ€˜π‘…)
32 simp1 1133 . . . . . . . . . . . 12 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) β†’ 𝑅 ∈ Ring)
3332adantr 480 . . . . . . . . . . 11 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ 𝑅 ∈ Ring)
3433adantr 480 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ 𝑅 ∈ Ring)
3521simpld 494 . . . . . . . . . . . 12 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) β†’ 𝑁 ∈ Fin)
3635adantr 480 . . . . . . . . . . 11 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ 𝑁 ∈ Fin)
3736adantr 480 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ 𝑁 ∈ Fin)
38 simpl2l 1223 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ π‘ˆ ∈ 𝐡)
3938adantr 480 . . . . . . . . . . . . 13 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ π‘ˆ ∈ 𝐡)
40 elfznn0 13600 . . . . . . . . . . . . . 14 (π‘˜ ∈ (0...𝐾) β†’ π‘˜ ∈ β„•0)
4140adantl 481 . . . . . . . . . . . . 13 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ π‘˜ ∈ β„•0)
4234, 39, 413jca 1125 . . . . . . . . . . . 12 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ (𝑅 ∈ Ring ∧ π‘ˆ ∈ 𝐡 ∧ π‘˜ ∈ β„•0))
43 decpmatmul.p . . . . . . . . . . . . 13 𝑃 = (Poly1β€˜π‘…)
44 eqid 2726 . . . . . . . . . . . . 13 (Baseβ€˜π΄) = (Baseβ€˜π΄)
4543, 14, 15, 22, 44decpmatcl 22624 . . . . . . . . . . . 12 ((𝑅 ∈ Ring ∧ π‘ˆ ∈ 𝐡 ∧ π‘˜ ∈ β„•0) β†’ (π‘ˆ decompPMat π‘˜) ∈ (Baseβ€˜π΄))
4642, 45syl 17 . . . . . . . . . . 11 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ (π‘ˆ decompPMat π‘˜) ∈ (Baseβ€˜π΄))
4722, 30, 44matbas2i 22279 . . . . . . . . . . 11 ((π‘ˆ decompPMat π‘˜) ∈ (Baseβ€˜π΄) β†’ (π‘ˆ decompPMat π‘˜) ∈ ((Baseβ€˜π‘…) ↑m (𝑁 Γ— 𝑁)))
4846, 47syl 17 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ (π‘ˆ decompPMat π‘˜) ∈ ((Baseβ€˜π‘…) ↑m (𝑁 Γ— 𝑁)))
49 simpl2r 1224 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ π‘Š ∈ 𝐡)
5049adantr 480 . . . . . . . . . . . . 13 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ π‘Š ∈ 𝐡)
51 fznn0sub 13539 . . . . . . . . . . . . . 14 (π‘˜ ∈ (0...𝐾) β†’ (𝐾 βˆ’ π‘˜) ∈ β„•0)
5251adantl 481 . . . . . . . . . . . . 13 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ (𝐾 βˆ’ π‘˜) ∈ β„•0)
5334, 50, 523jca 1125 . . . . . . . . . . . 12 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ (𝑅 ∈ Ring ∧ π‘Š ∈ 𝐡 ∧ (𝐾 βˆ’ π‘˜) ∈ β„•0))
5443, 14, 15, 22, 44decpmatcl 22624 . . . . . . . . . . . 12 ((𝑅 ∈ Ring ∧ π‘Š ∈ 𝐡 ∧ (𝐾 βˆ’ π‘˜) ∈ β„•0) β†’ (π‘Š decompPMat (𝐾 βˆ’ π‘˜)) ∈ (Baseβ€˜π΄))
5553, 54syl 17 . . . . . . . . . . 11 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ (π‘Š decompPMat (𝐾 βˆ’ π‘˜)) ∈ (Baseβ€˜π΄))
5622, 30, 44matbas2i 22279 . . . . . . . . . . 11 ((π‘Š decompPMat (𝐾 βˆ’ π‘˜)) ∈ (Baseβ€˜π΄) β†’ (π‘Š decompPMat (𝐾 βˆ’ π‘˜)) ∈ ((Baseβ€˜π‘…) ↑m (𝑁 Γ— 𝑁)))
5755, 56syl 17 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ (π‘Š decompPMat (𝐾 βˆ’ π‘˜)) ∈ ((Baseβ€˜π‘…) ↑m (𝑁 Γ— 𝑁)))
5823, 30, 31, 34, 37, 37, 37, 48, 57mamuval 22243 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ ((π‘ˆ decompPMat π‘˜)(𝑅 maMul βŸ¨π‘, 𝑁, π‘βŸ©)(π‘Š decompPMat (𝐾 βˆ’ π‘˜))) = (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦))))))
5929, 58eqtrd 2766 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ ((π‘ˆ decompPMat π‘˜)(.rβ€˜π΄)(π‘Š decompPMat (𝐾 βˆ’ π‘˜))) = (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦))))))
6059mpteq2dva 5241 . . . . . . 7 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ (π‘˜ ∈ (0...𝐾) ↦ ((π‘ˆ decompPMat π‘˜)(.rβ€˜π΄)(π‘Š decompPMat (𝐾 βˆ’ π‘˜)))) = (π‘˜ ∈ (0...𝐾) ↦ (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦)))))))
6160oveq2d 7421 . . . . . 6 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ (𝐴 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ ((π‘ˆ decompPMat π‘˜)(.rβ€˜π΄)(π‘Š decompPMat (𝐾 βˆ’ π‘˜))))) = (𝐴 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦))))))))
62 eqid 2726 . . . . . . 7 (0gβ€˜π΄) = (0gβ€˜π΄)
63 ovexd 7440 . . . . . . 7 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ (0...𝐾) ∈ V)
64 ringcmn 20181 . . . . . . . . . . . . 13 (𝑅 ∈ Ring β†’ 𝑅 ∈ CMnd)
6532, 64syl 17 . . . . . . . . . . . 12 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) β†’ 𝑅 ∈ CMnd)
6665adantr 480 . . . . . . . . . . 11 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ 𝑅 ∈ CMnd)
6766adantr 480 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ 𝑅 ∈ CMnd)
68673ad2ant1 1130 . . . . . . . . 9 (((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ π‘₯ ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) β†’ 𝑅 ∈ CMnd)
69373ad2ant1 1130 . . . . . . . . 9 (((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ π‘₯ ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) β†’ 𝑁 ∈ Fin)
70343ad2ant1 1130 . . . . . . . . . . . 12 (((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ π‘₯ ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) β†’ 𝑅 ∈ Ring)
7170adantr 480 . . . . . . . . . . 11 ((((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ π‘₯ ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) ∧ 𝑑 ∈ 𝑁) β†’ 𝑅 ∈ Ring)
72 simpl2 1189 . . . . . . . . . . . 12 ((((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ π‘₯ ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) ∧ 𝑑 ∈ 𝑁) β†’ π‘₯ ∈ 𝑁)
73 simpr 484 . . . . . . . . . . . 12 ((((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ π‘₯ ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) ∧ 𝑑 ∈ 𝑁) β†’ 𝑑 ∈ 𝑁)
74423ad2ant1 1130 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ π‘₯ ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) β†’ (𝑅 ∈ Ring ∧ π‘ˆ ∈ 𝐡 ∧ π‘˜ ∈ β„•0))
7574adantr 480 . . . . . . . . . . . . 13 ((((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ π‘₯ ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) ∧ 𝑑 ∈ 𝑁) β†’ (𝑅 ∈ Ring ∧ π‘ˆ ∈ 𝐡 ∧ π‘˜ ∈ β„•0))
7675, 45syl 17 . . . . . . . . . . . 12 ((((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ π‘₯ ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) ∧ 𝑑 ∈ 𝑁) β†’ (π‘ˆ decompPMat π‘˜) ∈ (Baseβ€˜π΄))
7722, 30, 44, 72, 73, 76matecld 22283 . . . . . . . . . . 11 ((((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ π‘₯ ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) ∧ 𝑑 ∈ 𝑁) β†’ (π‘₯(π‘ˆ decompPMat π‘˜)𝑑) ∈ (Baseβ€˜π‘…))
78 simpl3 1190 . . . . . . . . . . . 12 ((((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ π‘₯ ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) ∧ 𝑑 ∈ 𝑁) β†’ 𝑦 ∈ 𝑁)
79553ad2ant1 1130 . . . . . . . . . . . . 13 (((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ π‘₯ ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) β†’ (π‘Š decompPMat (𝐾 βˆ’ π‘˜)) ∈ (Baseβ€˜π΄))
8079adantr 480 . . . . . . . . . . . 12 ((((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ π‘₯ ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) ∧ 𝑑 ∈ 𝑁) β†’ (π‘Š decompPMat (𝐾 βˆ’ π‘˜)) ∈ (Baseβ€˜π΄))
8122, 30, 44, 73, 78, 80matecld 22283 . . . . . . . . . . 11 ((((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ π‘₯ ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) ∧ 𝑑 ∈ 𝑁) β†’ (𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦) ∈ (Baseβ€˜π‘…))
8230, 31ringcl 20155 . . . . . . . . . . 11 ((𝑅 ∈ Ring ∧ (π‘₯(π‘ˆ decompPMat π‘˜)𝑑) ∈ (Baseβ€˜π‘…) ∧ (𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦) ∈ (Baseβ€˜π‘…)) β†’ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦)) ∈ (Baseβ€˜π‘…))
8371, 77, 81, 82syl3anc 1368 . . . . . . . . . 10 ((((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ π‘₯ ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) ∧ 𝑑 ∈ 𝑁) β†’ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦)) ∈ (Baseβ€˜π‘…))
8483ralrimiva 3140 . . . . . . . . 9 (((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ π‘₯ ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) β†’ βˆ€π‘‘ ∈ 𝑁 ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦)) ∈ (Baseβ€˜π‘…))
8530, 68, 69, 84gsummptcl 19887 . . . . . . . 8 (((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ π‘₯ ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) β†’ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦)))) ∈ (Baseβ€˜π‘…))
8622, 30, 44, 37, 34, 85matbas2d 22280 . . . . . . 7 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦))))) ∈ (Baseβ€˜π΄))
87 eqid 2726 . . . . . . . 8 (π‘˜ ∈ (0...𝐾) ↦ (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦)))))) = (π‘˜ ∈ (0...𝐾) ↦ (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦))))))
88 fzfid 13944 . . . . . . . 8 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ (0...𝐾) ∈ Fin)
89 simpl 482 . . . . . . . . . . . . . . 15 ((𝑁 ∈ Fin ∧ 𝑃 ∈ V) β†’ 𝑁 ∈ Fin)
9089, 89jca 511 . . . . . . . . . . . . . 14 ((𝑁 ∈ Fin ∧ 𝑃 ∈ V) β†’ (𝑁 ∈ Fin ∧ 𝑁 ∈ Fin))
9116, 90syl 17 . . . . . . . . . . . . 13 (π‘ˆ ∈ 𝐡 β†’ (𝑁 ∈ Fin ∧ 𝑁 ∈ Fin))
9291adantr 480 . . . . . . . . . . . 12 ((π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) β†’ (𝑁 ∈ Fin ∧ 𝑁 ∈ Fin))
93923ad2ant2 1131 . . . . . . . . . . 11 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) β†’ (𝑁 ∈ Fin ∧ 𝑁 ∈ Fin))
9493adantr 480 . . . . . . . . . 10 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ (𝑁 ∈ Fin ∧ 𝑁 ∈ Fin))
9594adantr 480 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ (𝑁 ∈ Fin ∧ 𝑁 ∈ Fin))
96 mpoexga 8063 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑁 ∈ Fin) β†’ (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦))))) ∈ V)
9795, 96syl 17 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦))))) ∈ V)
98 fvexd 6900 . . . . . . . 8 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ (0gβ€˜π΄) ∈ V)
9987, 88, 97, 98fsuppmptdm 9376 . . . . . . 7 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ (π‘˜ ∈ (0...𝐾) ↦ (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦)))))) finSupp (0gβ€˜π΄))
10022, 44, 62, 36, 63, 33, 86, 99matgsum 22294 . . . . . 6 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ (𝐴 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦))))))) = (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑅 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦))))))))
10161, 100eqtrd 2766 . . . . 5 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ (𝐴 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ ((π‘ˆ decompPMat π‘˜)(.rβ€˜π΄)(π‘Š decompPMat (𝐾 βˆ’ π‘˜))))) = (π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑅 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦))))))))
102101oveqd 7422 . . . 4 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ (𝑖(𝐴 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ ((π‘ˆ decompPMat π‘˜)(.rβ€˜π΄)(π‘Š decompPMat (𝐾 βˆ’ π‘˜)))))𝑗) = (𝑖(π‘₯ ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑅 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((π‘₯(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑦)))))))𝑗))
103 simpl2 1189 . . . . . 6 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡))
104 simpl3 1190 . . . . . 6 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ 𝐾 ∈ β„•0)
10543, 14, 15decpmatmullem 22628 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ∧ 𝐾 ∈ β„•0)) β†’ (𝑖((π‘ˆ(.rβ€˜πΆ)π‘Š) decompPMat 𝐾)𝑗) = (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ (𝑅 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ (((coe1β€˜(π‘–π‘ˆπ‘‘))β€˜π‘˜)(.rβ€˜π‘…)((coe1β€˜(π‘‘π‘Šπ‘—))β€˜(𝐾 βˆ’ π‘˜))))))))
10636, 33, 103, 10, 11, 104, 105syl213anc 1386 . . . . 5 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ (𝑖((π‘ˆ(.rβ€˜πΆ)π‘Š) decompPMat 𝐾)𝑗) = (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ (𝑅 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ (((coe1β€˜(π‘–π‘ˆπ‘‘))β€˜π‘˜)(.rβ€˜π‘…)((coe1β€˜(π‘‘π‘Šπ‘—))β€˜(𝐾 βˆ’ π‘˜))))))))
107 simpll1 1209 . . . . . . 7 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑑 ∈ 𝑁 ∧ π‘˜ ∈ (0...𝐾))) β†’ 𝑅 ∈ Ring)
108 simplrl 774 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑑 ∈ 𝑁 ∧ π‘˜ ∈ (0...𝐾))) β†’ 𝑖 ∈ 𝑁)
109 simprl 768 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑑 ∈ 𝑁 ∧ π‘˜ ∈ (0...𝐾))) β†’ 𝑑 ∈ 𝑁)
11015eleq2i 2819 . . . . . . . . . . . . . 14 (π‘ˆ ∈ 𝐡 ↔ π‘ˆ ∈ (Baseβ€˜πΆ))
111110biimpi 215 . . . . . . . . . . . . 13 (π‘ˆ ∈ 𝐡 β†’ π‘ˆ ∈ (Baseβ€˜πΆ))
112111adantr 480 . . . . . . . . . . . 12 ((π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) β†’ π‘ˆ ∈ (Baseβ€˜πΆ))
1131123ad2ant2 1131 . . . . . . . . . . 11 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) β†’ π‘ˆ ∈ (Baseβ€˜πΆ))
114113adantr 480 . . . . . . . . . 10 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ π‘ˆ ∈ (Baseβ€˜πΆ))
115114adantr 480 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑑 ∈ 𝑁 ∧ π‘˜ ∈ (0...𝐾))) β†’ π‘ˆ ∈ (Baseβ€˜πΆ))
116 eqid 2726 . . . . . . . . . 10 (Baseβ€˜π‘ƒ) = (Baseβ€˜π‘ƒ)
11714, 116matecl 22282 . . . . . . . . 9 ((𝑖 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ∧ π‘ˆ ∈ (Baseβ€˜πΆ)) β†’ (π‘–π‘ˆπ‘‘) ∈ (Baseβ€˜π‘ƒ))
118108, 109, 115, 117syl3anc 1368 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑑 ∈ 𝑁 ∧ π‘˜ ∈ (0...𝐾))) β†’ (π‘–π‘ˆπ‘‘) ∈ (Baseβ€˜π‘ƒ))
11940ad2antll 726 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑑 ∈ 𝑁 ∧ π‘˜ ∈ (0...𝐾))) β†’ π‘˜ ∈ β„•0)
120 eqid 2726 . . . . . . . . 9 (coe1β€˜(π‘–π‘ˆπ‘‘)) = (coe1β€˜(π‘–π‘ˆπ‘‘))
121120, 116, 43, 30coe1fvalcl 22086 . . . . . . . 8 (((π‘–π‘ˆπ‘‘) ∈ (Baseβ€˜π‘ƒ) ∧ π‘˜ ∈ β„•0) β†’ ((coe1β€˜(π‘–π‘ˆπ‘‘))β€˜π‘˜) ∈ (Baseβ€˜π‘…))
122118, 119, 121syl2anc 583 . . . . . . 7 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑑 ∈ 𝑁 ∧ π‘˜ ∈ (0...𝐾))) β†’ ((coe1β€˜(π‘–π‘ˆπ‘‘))β€˜π‘˜) ∈ (Baseβ€˜π‘…))
123 simplrr 775 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑑 ∈ 𝑁 ∧ π‘˜ ∈ (0...𝐾))) β†’ 𝑗 ∈ 𝑁)
12449adantr 480 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑑 ∈ 𝑁 ∧ π‘˜ ∈ (0...𝐾))) β†’ π‘Š ∈ 𝐡)
12514, 116, 15, 109, 123, 124matecld 22283 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑑 ∈ 𝑁 ∧ π‘˜ ∈ (0...𝐾))) β†’ (π‘‘π‘Šπ‘—) ∈ (Baseβ€˜π‘ƒ))
12651ad2antll 726 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑑 ∈ 𝑁 ∧ π‘˜ ∈ (0...𝐾))) β†’ (𝐾 βˆ’ π‘˜) ∈ β„•0)
127 eqid 2726 . . . . . . . . 9 (coe1β€˜(π‘‘π‘Šπ‘—)) = (coe1β€˜(π‘‘π‘Šπ‘—))
128127, 116, 43, 30coe1fvalcl 22086 . . . . . . . 8 (((π‘‘π‘Šπ‘—) ∈ (Baseβ€˜π‘ƒ) ∧ (𝐾 βˆ’ π‘˜) ∈ β„•0) β†’ ((coe1β€˜(π‘‘π‘Šπ‘—))β€˜(𝐾 βˆ’ π‘˜)) ∈ (Baseβ€˜π‘…))
129125, 126, 128syl2anc 583 . . . . . . 7 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑑 ∈ 𝑁 ∧ π‘˜ ∈ (0...𝐾))) β†’ ((coe1β€˜(π‘‘π‘Šπ‘—))β€˜(𝐾 βˆ’ π‘˜)) ∈ (Baseβ€˜π‘…))
13030, 31ringcl 20155 . . . . . . 7 ((𝑅 ∈ Ring ∧ ((coe1β€˜(π‘–π‘ˆπ‘‘))β€˜π‘˜) ∈ (Baseβ€˜π‘…) ∧ ((coe1β€˜(π‘‘π‘Šπ‘—))β€˜(𝐾 βˆ’ π‘˜)) ∈ (Baseβ€˜π‘…)) β†’ (((coe1β€˜(π‘–π‘ˆπ‘‘))β€˜π‘˜)(.rβ€˜π‘…)((coe1β€˜(π‘‘π‘Šπ‘—))β€˜(𝐾 βˆ’ π‘˜))) ∈ (Baseβ€˜π‘…))
131107, 122, 129, 130syl3anc 1368 . . . . . 6 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑑 ∈ 𝑁 ∧ π‘˜ ∈ (0...𝐾))) β†’ (((coe1β€˜(π‘–π‘ˆπ‘‘))β€˜π‘˜)(.rβ€˜π‘…)((coe1β€˜(π‘‘π‘Šπ‘—))β€˜(𝐾 βˆ’ π‘˜))) ∈ (Baseβ€˜π‘…))
13230, 66, 36, 88, 131gsumcom3fi 19899 . . . . 5 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ (𝑅 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ (((coe1β€˜(π‘–π‘ˆπ‘‘))β€˜π‘˜)(.rβ€˜π‘…)((coe1β€˜(π‘‘π‘Šπ‘—))β€˜(𝐾 βˆ’ π‘˜))))))) = (𝑅 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ (((coe1β€˜(π‘–π‘ˆπ‘‘))β€˜π‘˜)(.rβ€˜π‘…)((coe1β€˜(π‘‘π‘Šπ‘—))β€˜(𝐾 βˆ’ π‘˜))))))))
13310adantr 480 . . . . . . . . . . . . 13 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ 𝑖 ∈ 𝑁)
134133anim1i 614 . . . . . . . . . . . 12 (((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ 𝑑 ∈ 𝑁) β†’ (𝑖 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁))
13543, 14, 15decpmate 22623 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ π‘ˆ ∈ 𝐡 ∧ π‘˜ ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) β†’ (𝑖(π‘ˆ decompPMat π‘˜)𝑑) = ((coe1β€˜(π‘–π‘ˆπ‘‘))β€˜π‘˜))
13642, 134, 135syl2an2r 682 . . . . . . . . . . 11 (((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ 𝑑 ∈ 𝑁) β†’ (𝑖(π‘ˆ decompPMat π‘˜)𝑑) = ((coe1β€˜(π‘–π‘ˆπ‘‘))β€˜π‘˜))
137 simplrr 775 . . . . . . . . . . . . 13 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ 𝑗 ∈ 𝑁)
138137anim1ci 615 . . . . . . . . . . . 12 (((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ 𝑑 ∈ 𝑁) β†’ (𝑑 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁))
13943, 14, 15decpmate 22623 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ π‘Š ∈ 𝐡 ∧ (𝐾 βˆ’ π‘˜) ∈ β„•0) ∧ (𝑑 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ (𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑗) = ((coe1β€˜(π‘‘π‘Šπ‘—))β€˜(𝐾 βˆ’ π‘˜)))
14053, 138, 139syl2an2r 682 . . . . . . . . . . 11 (((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ 𝑑 ∈ 𝑁) β†’ (𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑗) = ((coe1β€˜(π‘‘π‘Šπ‘—))β€˜(𝐾 βˆ’ π‘˜)))
141136, 140oveq12d 7423 . . . . . . . . . 10 (((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ 𝑑 ∈ 𝑁) β†’ ((𝑖(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑗)) = (((coe1β€˜(π‘–π‘ˆπ‘‘))β€˜π‘˜)(.rβ€˜π‘…)((coe1β€˜(π‘‘π‘Šπ‘—))β€˜(𝐾 βˆ’ π‘˜))))
142141eqcomd 2732 . . . . . . . . 9 (((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) ∧ 𝑑 ∈ 𝑁) β†’ (((coe1β€˜(π‘–π‘ˆπ‘‘))β€˜π‘˜)(.rβ€˜π‘…)((coe1β€˜(π‘‘π‘Šπ‘—))β€˜(𝐾 βˆ’ π‘˜))) = ((𝑖(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑗)))
143142mpteq2dva 5241 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ (𝑑 ∈ 𝑁 ↦ (((coe1β€˜(π‘–π‘ˆπ‘‘))β€˜π‘˜)(.rβ€˜π‘…)((coe1β€˜(π‘‘π‘Šπ‘—))β€˜(𝐾 βˆ’ π‘˜)))) = (𝑑 ∈ 𝑁 ↦ ((𝑖(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑗))))
144143oveq2d 7421 . . . . . . 7 ((((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ π‘˜ ∈ (0...𝐾)) β†’ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ (((coe1β€˜(π‘–π‘ˆπ‘‘))β€˜π‘˜)(.rβ€˜π‘…)((coe1β€˜(π‘‘π‘Šπ‘—))β€˜(𝐾 βˆ’ π‘˜))))) = (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((𝑖(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑗)))))
145144mpteq2dva 5241 . . . . . 6 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ (π‘˜ ∈ (0...𝐾) ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ (((coe1β€˜(π‘–π‘ˆπ‘‘))β€˜π‘˜)(.rβ€˜π‘…)((coe1β€˜(π‘‘π‘Šπ‘—))β€˜(𝐾 βˆ’ π‘˜)))))) = (π‘˜ ∈ (0...𝐾) ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((𝑖(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑗))))))
146145oveq2d 7421 . . . . 5 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ (𝑅 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ (((coe1β€˜(π‘–π‘ˆπ‘‘))β€˜π‘˜)(.rβ€˜π‘…)((coe1β€˜(π‘‘π‘Šπ‘—))β€˜(𝐾 βˆ’ π‘˜))))))) = (𝑅 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((𝑖(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑗)))))))
147106, 132, 1463eqtrd 2770 . . . 4 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ (𝑖((π‘ˆ(.rβ€˜πΆ)π‘Š) decompPMat 𝐾)𝑗) = (𝑅 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ (𝑅 Ξ£g (𝑑 ∈ 𝑁 ↦ ((𝑖(π‘ˆ decompPMat π‘˜)𝑑)(.rβ€˜π‘…)(𝑑(π‘Š decompPMat (𝐾 βˆ’ π‘˜))𝑗)))))))
14813, 102, 1473eqtr4rd 2777 . . 3 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) β†’ (𝑖((π‘ˆ(.rβ€˜πΆ)π‘Š) decompPMat 𝐾)𝑗) = (𝑖(𝐴 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ ((π‘ˆ decompPMat π‘˜)(.rβ€˜π΄)(π‘Š decompPMat (𝐾 βˆ’ π‘˜)))))𝑗))
149148ralrimivva 3194 . 2 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) β†’ βˆ€π‘– ∈ 𝑁 βˆ€π‘— ∈ 𝑁 (𝑖((π‘ˆ(.rβ€˜πΆ)π‘Š) decompPMat 𝐾)𝑗) = (𝑖(𝐴 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ ((π‘ˆ decompPMat π‘˜)(.rβ€˜π΄)(π‘Š decompPMat (𝐾 βˆ’ π‘˜)))))𝑗))
15043, 14pmatring 22549 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) β†’ 𝐢 ∈ Ring)
15120, 150syl 17 . . . . . 6 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡)) β†’ 𝐢 ∈ Ring)
152 simprl 768 . . . . . 6 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡)) β†’ π‘ˆ ∈ 𝐡)
153 simprr 770 . . . . . 6 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡)) β†’ π‘Š ∈ 𝐡)
154 eqid 2726 . . . . . . 7 (.rβ€˜πΆ) = (.rβ€˜πΆ)
15515, 154ringcl 20155 . . . . . 6 ((𝐢 ∈ Ring ∧ π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) β†’ (π‘ˆ(.rβ€˜πΆ)π‘Š) ∈ 𝐡)
156151, 152, 153, 155syl3anc 1368 . . . . 5 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡)) β†’ (π‘ˆ(.rβ€˜πΆ)π‘Š) ∈ 𝐡)
1571563adant3 1129 . . . 4 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) β†’ (π‘ˆ(.rβ€˜πΆ)π‘Š) ∈ 𝐡)
15843, 14, 15, 22, 44decpmatcl 22624 . . . 4 ((𝑅 ∈ Ring ∧ (π‘ˆ(.rβ€˜πΆ)π‘Š) ∈ 𝐡 ∧ 𝐾 ∈ β„•0) β†’ ((π‘ˆ(.rβ€˜πΆ)π‘Š) decompPMat 𝐾) ∈ (Baseβ€˜π΄))
159157, 158syld3an2 1408 . . 3 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) β†’ ((π‘ˆ(.rβ€˜πΆ)π‘Š) decompPMat 𝐾) ∈ (Baseβ€˜π΄))
16022matring 22300 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) β†’ 𝐴 ∈ Ring)
16121, 160syl 17 . . . . 5 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) β†’ 𝐴 ∈ Ring)
162 ringcmn 20181 . . . . 5 (𝐴 ∈ Ring β†’ 𝐴 ∈ CMnd)
163161, 162syl 17 . . . 4 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) β†’ 𝐴 ∈ CMnd)
164 fzfid 13944 . . . 4 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) β†’ (0...𝐾) ∈ Fin)
165161adantr 480 . . . . . 6 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ π‘˜ ∈ (0...𝐾)) β†’ 𝐴 ∈ Ring)
16632adantr 480 . . . . . . . 8 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ π‘˜ ∈ (0...𝐾)) β†’ 𝑅 ∈ Ring)
167 simpl2l 1223 . . . . . . . 8 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ π‘˜ ∈ (0...𝐾)) β†’ π‘ˆ ∈ 𝐡)
16840adantl 481 . . . . . . . 8 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ π‘˜ ∈ (0...𝐾)) β†’ π‘˜ ∈ β„•0)
169166, 167, 1683jca 1125 . . . . . . 7 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ π‘˜ ∈ (0...𝐾)) β†’ (𝑅 ∈ Ring ∧ π‘ˆ ∈ 𝐡 ∧ π‘˜ ∈ β„•0))
170169, 45syl 17 . . . . . 6 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ π‘˜ ∈ (0...𝐾)) β†’ (π‘ˆ decompPMat π‘˜) ∈ (Baseβ€˜π΄))
171 simpl2r 1224 . . . . . . . 8 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ π‘˜ ∈ (0...𝐾)) β†’ π‘Š ∈ 𝐡)
17251adantl 481 . . . . . . . 8 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ π‘˜ ∈ (0...𝐾)) β†’ (𝐾 βˆ’ π‘˜) ∈ β„•0)
173166, 171, 1723jca 1125 . . . . . . 7 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ π‘˜ ∈ (0...𝐾)) β†’ (𝑅 ∈ Ring ∧ π‘Š ∈ 𝐡 ∧ (𝐾 βˆ’ π‘˜) ∈ β„•0))
174173, 54syl 17 . . . . . 6 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ π‘˜ ∈ (0...𝐾)) β†’ (π‘Š decompPMat (𝐾 βˆ’ π‘˜)) ∈ (Baseβ€˜π΄))
175 eqid 2726 . . . . . . 7 (.rβ€˜π΄) = (.rβ€˜π΄)
17644, 175ringcl 20155 . . . . . 6 ((𝐴 ∈ Ring ∧ (π‘ˆ decompPMat π‘˜) ∈ (Baseβ€˜π΄) ∧ (π‘Š decompPMat (𝐾 βˆ’ π‘˜)) ∈ (Baseβ€˜π΄)) β†’ ((π‘ˆ decompPMat π‘˜)(.rβ€˜π΄)(π‘Š decompPMat (𝐾 βˆ’ π‘˜))) ∈ (Baseβ€˜π΄))
177165, 170, 174, 176syl3anc 1368 . . . . 5 (((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) ∧ π‘˜ ∈ (0...𝐾)) β†’ ((π‘ˆ decompPMat π‘˜)(.rβ€˜π΄)(π‘Š decompPMat (𝐾 βˆ’ π‘˜))) ∈ (Baseβ€˜π΄))
178177ralrimiva 3140 . . . 4 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) β†’ βˆ€π‘˜ ∈ (0...𝐾)((π‘ˆ decompPMat π‘˜)(.rβ€˜π΄)(π‘Š decompPMat (𝐾 βˆ’ π‘˜))) ∈ (Baseβ€˜π΄))
17944, 163, 164, 178gsummptcl 19887 . . 3 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) β†’ (𝐴 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ ((π‘ˆ decompPMat π‘˜)(.rβ€˜π΄)(π‘Š decompPMat (𝐾 βˆ’ π‘˜))))) ∈ (Baseβ€˜π΄))
18022, 44eqmat 22281 . . 3 ((((π‘ˆ(.rβ€˜πΆ)π‘Š) decompPMat 𝐾) ∈ (Baseβ€˜π΄) ∧ (𝐴 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ ((π‘ˆ decompPMat π‘˜)(.rβ€˜π΄)(π‘Š decompPMat (𝐾 βˆ’ π‘˜))))) ∈ (Baseβ€˜π΄)) β†’ (((π‘ˆ(.rβ€˜πΆ)π‘Š) decompPMat 𝐾) = (𝐴 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ ((π‘ˆ decompPMat π‘˜)(.rβ€˜π΄)(π‘Š decompPMat (𝐾 βˆ’ π‘˜))))) ↔ βˆ€π‘– ∈ 𝑁 βˆ€π‘— ∈ 𝑁 (𝑖((π‘ˆ(.rβ€˜πΆ)π‘Š) decompPMat 𝐾)𝑗) = (𝑖(𝐴 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ ((π‘ˆ decompPMat π‘˜)(.rβ€˜π΄)(π‘Š decompPMat (𝐾 βˆ’ π‘˜)))))𝑗)))
181159, 179, 180syl2anc 583 . 2 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) β†’ (((π‘ˆ(.rβ€˜πΆ)π‘Š) decompPMat 𝐾) = (𝐴 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ ((π‘ˆ decompPMat π‘˜)(.rβ€˜π΄)(π‘Š decompPMat (𝐾 βˆ’ π‘˜))))) ↔ βˆ€π‘– ∈ 𝑁 βˆ€π‘— ∈ 𝑁 (𝑖((π‘ˆ(.rβ€˜πΆ)π‘Š) decompPMat 𝐾)𝑗) = (𝑖(𝐴 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ ((π‘ˆ decompPMat π‘˜)(.rβ€˜π΄)(π‘Š decompPMat (𝐾 βˆ’ π‘˜)))))𝑗)))
182149, 181mpbird 257 1 ((𝑅 ∈ Ring ∧ (π‘ˆ ∈ 𝐡 ∧ π‘Š ∈ 𝐡) ∧ 𝐾 ∈ β„•0) β†’ ((π‘ˆ(.rβ€˜πΆ)π‘Š) decompPMat 𝐾) = (𝐴 Ξ£g (π‘˜ ∈ (0...𝐾) ↦ ((π‘ˆ decompPMat π‘˜)(.rβ€˜π΄)(π‘Š decompPMat (𝐾 βˆ’ π‘˜))))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  βˆ€wral 3055  Vcvv 3468  βŸ¨cotp 4631   ↦ cmpt 5224   Γ— cxp 5667  β€˜cfv 6537  (class class class)co 7405   ∈ cmpo 7407   ↑m cmap 8822  Fincfn 8941  0cc0 11112   βˆ’ cmin 11448  β„•0cn0 12476  ...cfz 13490  Basecbs 17153  .rcmulr 17207  0gc0g 17394   Ξ£g cgsu 17395  CMndccmn 19700  Ringcrg 20138  Poly1cpl1 22051  coe1cco1 22052   maMul cmmul 22240   Mat cmat 22262   decompPMat cdecpmat 22619
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-ot 4632  df-uni 4903  df-int 4944  df-iun 4992  df-iin 4993  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7667  df-ofr 7668  df-om 7853  df-1st 7974  df-2nd 7975  df-supp 8147  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-er 8705  df-map 8824  df-pm 8825  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-sup 9439  df-oi 9507  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-fz 13491  df-fzo 13634  df-seq 13973  df-hash 14296  df-struct 17089  df-sets 17106  df-slot 17124  df-ndx 17136  df-base 17154  df-ress 17183  df-plusg 17219  df-mulr 17220  df-sca 17222  df-vsca 17223  df-ip 17224  df-tset 17225  df-ple 17226  df-ds 17228  df-hom 17230  df-cco 17231  df-0g 17396  df-gsum 17397  df-prds 17402  df-pws 17404  df-mre 17539  df-mrc 17540  df-acs 17542  df-mgm 18573  df-sgrp 18652  df-mnd 18668  df-mhm 18713  df-submnd 18714  df-grp 18866  df-minusg 18867  df-sbg 18868  df-mulg 18996  df-subg 19050  df-ghm 19139  df-cntz 19233  df-cmn 19702  df-abl 19703  df-mgp 20040  df-rng 20058  df-ur 20087  df-ring 20140  df-subrng 20446  df-subrg 20471  df-lmod 20708  df-lss 20779  df-sra 21021  df-rgmod 21022  df-dsmm 21627  df-frlm 21642  df-psr 21803  df-mpl 21805  df-opsr 21807  df-psr1 22054  df-ply1 22056  df-coe1 22057  df-mamu 22241  df-mat 22263  df-decpmat 22620
This theorem is referenced by:  decpmatmulsumfsupp  22630  pm2mpmhmlem1  22675  pm2mpmhmlem2  22676
  Copyright terms: Public domain W3C validator