![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > gsum0 | Structured version Visualization version GIF version |
Description: Value of the empty group sum. (Contributed by Mario Carneiro, 7-Dec-2014.) |
Ref | Expression |
---|---|
gsum0.z | ⊢ 0 = (0g‘𝐺) |
Ref | Expression |
---|---|
gsum0 | ⊢ (𝐺 Σg ∅) = 0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2797 | . . 3 ⊢ (Base‘𝐺) = (Base‘𝐺) | |
2 | gsum0.z | . . 3 ⊢ 0 = (0g‘𝐺) | |
3 | eqid 2797 | . . 3 ⊢ (+g‘𝐺) = (+g‘𝐺) | |
4 | eqid 2797 | . . 3 ⊢ {𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)} = {𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)} | |
5 | id 22 | . . 3 ⊢ (𝐺 ∈ V → 𝐺 ∈ V) | |
6 | 0ex 5109 | . . . 4 ⊢ ∅ ∈ V | |
7 | 6 | a1i 11 | . . 3 ⊢ (𝐺 ∈ V → ∅ ∈ V) |
8 | f0 6435 | . . . 4 ⊢ ∅:∅⟶{𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)} | |
9 | 8 | a1i 11 | . . 3 ⊢ (𝐺 ∈ V → ∅:∅⟶{𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)}) |
10 | 1, 2, 3, 4, 5, 7, 9 | gsumval1 17720 | . 2 ⊢ (𝐺 ∈ V → (𝐺 Σg ∅) = 0 ) |
11 | df-gsum 16549 | . . . . 5 ⊢ Σg = (𝑤 ∈ V, 𝑓 ∈ V ↦ ⦋{𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)} / 𝑜⦌if(ran 𝑓 ⊆ 𝑜, (0g‘𝑤), if(dom 𝑓 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))), (℩𝑥∃𝑔[(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦))))))) | |
12 | 11 | reldmmpo 7148 | . . . 4 ⊢ Rel dom Σg |
13 | 12 | ovprc1 7061 | . . 3 ⊢ (¬ 𝐺 ∈ V → (𝐺 Σg ∅) = ∅) |
14 | fvprc 6538 | . . . 4 ⊢ (¬ 𝐺 ∈ V → (0g‘𝐺) = ∅) | |
15 | 2, 14 | syl5eq 2845 | . . 3 ⊢ (¬ 𝐺 ∈ V → 0 = ∅) |
16 | 13, 15 | eqtr4d 2836 | . 2 ⊢ (¬ 𝐺 ∈ V → (𝐺 Σg ∅) = 0 ) |
17 | 10, 16 | pm2.61i 183 | 1 ⊢ (𝐺 Σg ∅) = 0 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 396 = wceq 1525 ∃wex 1765 ∈ wcel 2083 ∀wral 3107 ∃wrex 3108 {crab 3111 Vcvv 3440 [wsbc 3711 ⦋csb 3817 ∖ cdif 3862 ⊆ wss 3865 ∅c0 4217 ifcif 4387 ◡ccnv 5449 dom cdm 5450 ran crn 5451 “ cima 5453 ∘ ccom 5454 ℩cio 6194 ⟶wf 6228 –1-1-onto→wf1o 6231 ‘cfv 6232 (class class class)co 7023 1c1 10391 ℤ≥cuz 12097 ...cfz 12746 seqcseq 13223 ♯chash 13544 Basecbs 16316 +gcplusg 16398 0gc0g 16546 Σg cgsu 16547 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 ax-un 7326 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ral 3112 df-rex 3113 df-rab 3116 df-v 3442 df-sbc 3712 df-csb 3818 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-nul 4218 df-if 4388 df-pw 4461 df-sn 4479 df-pr 4481 df-op 4485 df-uni 4752 df-br 4969 df-opab 5031 df-mpt 5048 df-id 5355 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-pred 6030 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-f1 6237 df-fo 6238 df-f1o 6239 df-fv 6240 df-ov 7026 df-oprab 7027 df-mpo 7028 df-wrecs 7805 df-recs 7867 df-rdg 7905 df-seq 13224 df-gsum 16549 |
This theorem is referenced by: gsumwsubmcl 17818 gsumccat 17821 gsumwmhm 17825 gsumwspan 17826 frmdgsum 17842 frmdup1 17844 gsumwrev 18239 gsmsymgrfix 18291 gsmsymgreq 18295 psgnunilem2 18358 psgn0fv0 18374 psgnsn 18383 psgnprfval1 18385 gsumconst 18778 mplmonmul 19936 mplcoe1 19937 mplcoe5 19940 coe1fzgsumd 20157 evl1gsumd 20206 gsumfsum 20298 mdet0pr 20889 madugsum 20940 tmdgsum 22391 xrge0gsumle 23128 xrge0tsms 23129 jensen 25252 cyc3genpmlem 30427 gsumle 30490 gsumvsca1 30493 gsumvsca2 30494 xrge0tsmsd 30499 esumnul 30920 esumsnf 30936 sitg0 31217 mrsub0 32373 matunitlindflem1 34440 lincval0 43972 |
Copyright terms: Public domain | W3C validator |