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

Theorem matgsum 21931
Description: Finite commutative sums in a matrix algebra are taken componentwise. (Contributed by AV, 26-Sep-2019.)
Hypotheses
Ref Expression
matgsum.a 𝐴 = (𝑁 Mat 𝑅)
matgsum.b 𝐵 = (Base‘𝐴)
matgsum.z 0 = (0g𝐴)
matgsum.i (𝜑𝑁 ∈ Fin)
matgsum.j (𝜑𝐽𝑊)
matgsum.r (𝜑𝑅 ∈ Ring)
matgsum.f ((𝜑𝑦𝐽) → (𝑖𝑁, 𝑗𝑁𝑈) ∈ 𝐵)
matgsum.w (𝜑 → (𝑦𝐽 ↦ (𝑖𝑁, 𝑗𝑁𝑈)) finSupp 0 )
Assertion
Ref Expression
matgsum (𝜑 → (𝐴 Σg (𝑦𝐽 ↦ (𝑖𝑁, 𝑗𝑁𝑈))) = (𝑖𝑁, 𝑗𝑁 ↦ (𝑅 Σg (𝑦𝐽𝑈))))
Distinct variable groups:   𝑖,𝐽,𝑗,𝑦   𝑖,𝑁,𝑗,𝑦   𝑅,𝑖,𝑗,𝑦   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑖,𝑗)   𝐴(𝑦,𝑖,𝑗)   𝐵(𝑦,𝑖,𝑗)   𝑈(𝑦,𝑖,𝑗)   𝑊(𝑦,𝑖,𝑗)   0 (𝑦,𝑖,𝑗)

Proof of Theorem matgsum
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 matgsum.j . . . 4 (𝜑𝐽𝑊)
21mptexd 7223 . . 3 (𝜑 → (𝑦𝐽 ↦ (𝑖𝑁, 𝑗𝑁𝑈)) ∈ V)
3 matgsum.a . . . . 5 𝐴 = (𝑁 Mat 𝑅)
43ovexi 7440 . . . 4 𝐴 ∈ V
54a1i 11 . . 3 (𝜑𝐴 ∈ V)
6 ovexd 7441 . . 3 (𝜑 → (𝑅 freeLMod (𝑁 × 𝑁)) ∈ V)
7 matgsum.i . . . . 5 (𝜑𝑁 ∈ Fin)
8 matgsum.r . . . . 5 (𝜑𝑅 ∈ Ring)
9 eqid 2733 . . . . . 6 (𝑅 freeLMod (𝑁 × 𝑁)) = (𝑅 freeLMod (𝑁 × 𝑁))
103, 9matbas 21905 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (Base‘(𝑅 freeLMod (𝑁 × 𝑁))) = (Base‘𝐴))
117, 8, 10syl2anc 585 . . . 4 (𝜑 → (Base‘(𝑅 freeLMod (𝑁 × 𝑁))) = (Base‘𝐴))
1211eqcomd 2739 . . 3 (𝜑 → (Base‘𝐴) = (Base‘(𝑅 freeLMod (𝑁 × 𝑁))))
133, 9matplusg 21906 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (+g‘(𝑅 freeLMod (𝑁 × 𝑁))) = (+g𝐴))
147, 8, 13syl2anc 585 . . . 4 (𝜑 → (+g‘(𝑅 freeLMod (𝑁 × 𝑁))) = (+g𝐴))
1514eqcomd 2739 . . 3 (𝜑 → (+g𝐴) = (+g‘(𝑅 freeLMod (𝑁 × 𝑁))))
162, 5, 6, 12, 15gsumpropd 18594 . 2 (𝜑 → (𝐴 Σg (𝑦𝐽 ↦ (𝑖𝑁, 𝑗𝑁𝑈))) = ((𝑅 freeLMod (𝑁 × 𝑁)) Σg (𝑦𝐽 ↦ (𝑖𝑁, 𝑗𝑁𝑈))))
17 mpompts 8048 . . . . . 6 (𝑖𝑁, 𝑗𝑁𝑈) = (𝑧 ∈ (𝑁 × 𝑁) ↦ (1st𝑧) / 𝑖(2nd𝑧) / 𝑗𝑈)
1817a1i 11 . . . . 5 (𝜑 → (𝑖𝑁, 𝑗𝑁𝑈) = (𝑧 ∈ (𝑁 × 𝑁) ↦ (1st𝑧) / 𝑖(2nd𝑧) / 𝑗𝑈))
1918mpteq2dv 5250 . . . 4 (𝜑 → (𝑦𝐽 ↦ (𝑖𝑁, 𝑗𝑁𝑈)) = (𝑦𝐽 ↦ (𝑧 ∈ (𝑁 × 𝑁) ↦ (1st𝑧) / 𝑖(2nd𝑧) / 𝑗𝑈)))
2019oveq2d 7422 . . 3 (𝜑 → ((𝑅 freeLMod (𝑁 × 𝑁)) Σg (𝑦𝐽 ↦ (𝑖𝑁, 𝑗𝑁𝑈))) = ((𝑅 freeLMod (𝑁 × 𝑁)) Σg (𝑦𝐽 ↦ (𝑧 ∈ (𝑁 × 𝑁) ↦ (1st𝑧) / 𝑖(2nd𝑧) / 𝑗𝑈))))
21 eqid 2733 . . . 4 (Base‘(𝑅 freeLMod (𝑁 × 𝑁))) = (Base‘(𝑅 freeLMod (𝑁 × 𝑁)))
22 eqid 2733 . . . 4 (0g‘(𝑅 freeLMod (𝑁 × 𝑁))) = (0g‘(𝑅 freeLMod (𝑁 × 𝑁)))
23 xpfi 9314 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑁 ∈ Fin) → (𝑁 × 𝑁) ∈ Fin)
247, 7, 23syl2anc 585 . . . 4 (𝜑 → (𝑁 × 𝑁) ∈ Fin)
25 matgsum.f . . . . . 6 ((𝜑𝑦𝐽) → (𝑖𝑁, 𝑗𝑁𝑈) ∈ 𝐵)
26 matgsum.b . . . . . 6 𝐵 = (Base‘𝐴)
2725, 26eleqtrdi 2844 . . . . 5 ((𝜑𝑦𝐽) → (𝑖𝑁, 𝑗𝑁𝑈) ∈ (Base‘𝐴))
2817eqcomi 2742 . . . . . 6 (𝑧 ∈ (𝑁 × 𝑁) ↦ (1st𝑧) / 𝑖(2nd𝑧) / 𝑗𝑈) = (𝑖𝑁, 𝑗𝑁𝑈)
2928a1i 11 . . . . 5 ((𝜑𝑦𝐽) → (𝑧 ∈ (𝑁 × 𝑁) ↦ (1st𝑧) / 𝑖(2nd𝑧) / 𝑗𝑈) = (𝑖𝑁, 𝑗𝑁𝑈))
307, 8jca 513 . . . . . . 7 (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
3130adantr 482 . . . . . 6 ((𝜑𝑦𝐽) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
3231, 10syl 17 . . . . 5 ((𝜑𝑦𝐽) → (Base‘(𝑅 freeLMod (𝑁 × 𝑁))) = (Base‘𝐴))
3327, 29, 323eltr4d 2849 . . . 4 ((𝜑𝑦𝐽) → (𝑧 ∈ (𝑁 × 𝑁) ↦ (1st𝑧) / 𝑖(2nd𝑧) / 𝑗𝑈) ∈ (Base‘(𝑅 freeLMod (𝑁 × 𝑁))))
34 matgsum.w . . . . . 6 (𝜑 → (𝑦𝐽 ↦ (𝑖𝑁, 𝑗𝑁𝑈)) finSupp 0 )
3528mpteq2i 5253 . . . . . 6 (𝑦𝐽 ↦ (𝑧 ∈ (𝑁 × 𝑁) ↦ (1st𝑧) / 𝑖(2nd𝑧) / 𝑗𝑈)) = (𝑦𝐽 ↦ (𝑖𝑁, 𝑗𝑁𝑈))
36 matgsum.z . . . . . . 7 0 = (0g𝐴)
3736eqcomi 2742 . . . . . 6 (0g𝐴) = 0
3834, 35, 373brtr4g 5182 . . . . 5 (𝜑 → (𝑦𝐽 ↦ (𝑧 ∈ (𝑁 × 𝑁) ↦ (1st𝑧) / 𝑖(2nd𝑧) / 𝑗𝑈)) finSupp (0g𝐴))
393, 9mat0 21911 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0g‘(𝑅 freeLMod (𝑁 × 𝑁))) = (0g𝐴))
407, 8, 39syl2anc 585 . . . . 5 (𝜑 → (0g‘(𝑅 freeLMod (𝑁 × 𝑁))) = (0g𝐴))
4138, 40breqtrrd 5176 . . . 4 (𝜑 → (𝑦𝐽 ↦ (𝑧 ∈ (𝑁 × 𝑁) ↦ (1st𝑧) / 𝑖(2nd𝑧) / 𝑗𝑈)) finSupp (0g‘(𝑅 freeLMod (𝑁 × 𝑁))))
429, 21, 22, 24, 1, 8, 33, 41frlmgsum 21319 . . 3 (𝜑 → ((𝑅 freeLMod (𝑁 × 𝑁)) Σg (𝑦𝐽 ↦ (𝑧 ∈ (𝑁 × 𝑁) ↦ (1st𝑧) / 𝑖(2nd𝑧) / 𝑗𝑈))) = (𝑧 ∈ (𝑁 × 𝑁) ↦ (𝑅 Σg (𝑦𝐽(1st𝑧) / 𝑖(2nd𝑧) / 𝑗𝑈))))
4320, 42eqtrd 2773 . 2 (𝜑 → ((𝑅 freeLMod (𝑁 × 𝑁)) Σg (𝑦𝐽 ↦ (𝑖𝑁, 𝑗𝑁𝑈))) = (𝑧 ∈ (𝑁 × 𝑁) ↦ (𝑅 Σg (𝑦𝐽(1st𝑧) / 𝑖(2nd𝑧) / 𝑗𝑈))))
44 fvex 6902 . . . . . . . 8 (2nd𝑧) ∈ V
45 csbov2g 7452 . . . . . . . 8 ((2nd𝑧) ∈ V → (2nd𝑧) / 𝑗(𝑅 Σg (𝑦𝐽𝑈)) = (𝑅 Σg (2nd𝑧) / 𝑗(𝑦𝐽𝑈)))
4644, 45ax-mp 5 . . . . . . 7 (2nd𝑧) / 𝑗(𝑅 Σg (𝑦𝐽𝑈)) = (𝑅 Σg (2nd𝑧) / 𝑗(𝑦𝐽𝑈))
4746csbeq2i 3901 . . . . . 6 (1st𝑧) / 𝑖(2nd𝑧) / 𝑗(𝑅 Σg (𝑦𝐽𝑈)) = (1st𝑧) / 𝑖(𝑅 Σg (2nd𝑧) / 𝑗(𝑦𝐽𝑈))
48 fvex 6902 . . . . . . 7 (1st𝑧) ∈ V
49 csbov2g 7452 . . . . . . 7 ((1st𝑧) ∈ V → (1st𝑧) / 𝑖(𝑅 Σg (2nd𝑧) / 𝑗(𝑦𝐽𝑈)) = (𝑅 Σg (1st𝑧) / 𝑖(2nd𝑧) / 𝑗(𝑦𝐽𝑈)))
5048, 49ax-mp 5 . . . . . 6 (1st𝑧) / 𝑖(𝑅 Σg (2nd𝑧) / 𝑗(𝑦𝐽𝑈)) = (𝑅 Σg (1st𝑧) / 𝑖(2nd𝑧) / 𝑗(𝑦𝐽𝑈))
51 csbmpt2 5558 . . . . . . . . . 10 ((2nd𝑧) ∈ V → (2nd𝑧) / 𝑗(𝑦𝐽𝑈) = (𝑦𝐽(2nd𝑧) / 𝑗𝑈))
5244, 51ax-mp 5 . . . . . . . . 9 (2nd𝑧) / 𝑗(𝑦𝐽𝑈) = (𝑦𝐽(2nd𝑧) / 𝑗𝑈)
5352csbeq2i 3901 . . . . . . . 8 (1st𝑧) / 𝑖(2nd𝑧) / 𝑗(𝑦𝐽𝑈) = (1st𝑧) / 𝑖(𝑦𝐽(2nd𝑧) / 𝑗𝑈)
54 csbmpt2 5558 . . . . . . . . 9 ((1st𝑧) ∈ V → (1st𝑧) / 𝑖(𝑦𝐽(2nd𝑧) / 𝑗𝑈) = (𝑦𝐽(1st𝑧) / 𝑖(2nd𝑧) / 𝑗𝑈))
5548, 54ax-mp 5 . . . . . . . 8 (1st𝑧) / 𝑖(𝑦𝐽(2nd𝑧) / 𝑗𝑈) = (𝑦𝐽(1st𝑧) / 𝑖(2nd𝑧) / 𝑗𝑈)
5653, 55eqtri 2761 . . . . . . 7 (1st𝑧) / 𝑖(2nd𝑧) / 𝑗(𝑦𝐽𝑈) = (𝑦𝐽(1st𝑧) / 𝑖(2nd𝑧) / 𝑗𝑈)
5756oveq2i 7417 . . . . . 6 (𝑅 Σg (1st𝑧) / 𝑖(2nd𝑧) / 𝑗(𝑦𝐽𝑈)) = (𝑅 Σg (𝑦𝐽(1st𝑧) / 𝑖(2nd𝑧) / 𝑗𝑈))
5847, 50, 573eqtrri 2766 . . . . 5 (𝑅 Σg (𝑦𝐽(1st𝑧) / 𝑖(2nd𝑧) / 𝑗𝑈)) = (1st𝑧) / 𝑖(2nd𝑧) / 𝑗(𝑅 Σg (𝑦𝐽𝑈))
5958mpteq2i 5253 . . . 4 (𝑧 ∈ (𝑁 × 𝑁) ↦ (𝑅 Σg (𝑦𝐽(1st𝑧) / 𝑖(2nd𝑧) / 𝑗𝑈))) = (𝑧 ∈ (𝑁 × 𝑁) ↦ (1st𝑧) / 𝑖(2nd𝑧) / 𝑗(𝑅 Σg (𝑦𝐽𝑈)))
60 mpompts 8048 . . . 4 (𝑖𝑁, 𝑗𝑁 ↦ (𝑅 Σg (𝑦𝐽𝑈))) = (𝑧 ∈ (𝑁 × 𝑁) ↦ (1st𝑧) / 𝑖(2nd𝑧) / 𝑗(𝑅 Σg (𝑦𝐽𝑈)))
6159, 60eqtr4i 2764 . . 3 (𝑧 ∈ (𝑁 × 𝑁) ↦ (𝑅 Σg (𝑦𝐽(1st𝑧) / 𝑖(2nd𝑧) / 𝑗𝑈))) = (𝑖𝑁, 𝑗𝑁 ↦ (𝑅 Σg (𝑦𝐽𝑈)))
6261a1i 11 . 2 (𝜑 → (𝑧 ∈ (𝑁 × 𝑁) ↦ (𝑅 Σg (𝑦𝐽(1st𝑧) / 𝑖(2nd𝑧) / 𝑗𝑈))) = (𝑖𝑁, 𝑗𝑁 ↦ (𝑅 Σg (𝑦𝐽𝑈))))
6316, 43, 623eqtrd 2777 1 (𝜑 → (𝐴 Σg (𝑦𝐽 ↦ (𝑖𝑁, 𝑗𝑁𝑈))) = (𝑖𝑁, 𝑗𝑁 ↦ (𝑅 Σg (𝑦𝐽𝑈))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wcel 2107  Vcvv 3475  csb 3893   class class class wbr 5148  cmpt 5231   × cxp 5674  cfv 6541  (class class class)co 7406  cmpo 7408  1st c1st 7970  2nd c2nd 7971  Fincfn 8936   finSupp cfsupp 9358  Basecbs 17141  +gcplusg 17194  0gc0g 17382   Σg cgsu 17383  Ringcrg 20050   freeLMod cfrlm 21293   Mat cmat 21899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-ot 4637  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-supp 8144  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-er 8700  df-map 8819  df-ixp 8889  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fsupp 9359  df-sup 9434  df-oi 9502  df-card 9931  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-dec 12675  df-uz 12820  df-fz 13482  df-fzo 13625  df-seq 13964  df-hash 14288  df-struct 17077  df-sets 17094  df-slot 17112  df-ndx 17124  df-base 17142  df-ress 17171  df-plusg 17207  df-mulr 17208  df-sca 17210  df-vsca 17211  df-ip 17212  df-tset 17213  df-ple 17214  df-ds 17216  df-hom 17218  df-cco 17219  df-0g 17384  df-gsum 17385  df-prds 17390  df-pws 17392  df-mgm 18558  df-sgrp 18607  df-mnd 18623  df-mhm 18668  df-grp 18819  df-minusg 18820  df-sbg 18821  df-subg 18998  df-cntz 19176  df-cmn 19645  df-abl 19646  df-mgp 19983  df-ur 20000  df-ring 20052  df-subrg 20354  df-lmod 20466  df-lss 20536  df-sra 20778  df-rgmod 20779  df-dsmm 21279  df-frlm 21294  df-mat 21900
This theorem is referenced by:  decpmatmul  22266  pmatcollpw2  22272
  Copyright terms: Public domain W3C validator