Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dprdfinv | Structured version Visualization version GIF version |
Description: Take the inverse of a group sum over a family of elements of disjoint subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
Ref | Expression |
---|---|
eldprdi.0 | ⊢ 0 = (0g‘𝐺) |
eldprdi.w | ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } |
eldprdi.1 | ⊢ (𝜑 → 𝐺dom DProd 𝑆) |
eldprdi.2 | ⊢ (𝜑 → dom 𝑆 = 𝐼) |
eldprdi.3 | ⊢ (𝜑 → 𝐹 ∈ 𝑊) |
dprdfinv.b | ⊢ 𝑁 = (invg‘𝐺) |
Ref | Expression |
---|---|
dprdfinv | ⊢ (𝜑 → ((𝑁 ∘ 𝐹) ∈ 𝑊 ∧ (𝐺 Σg (𝑁 ∘ 𝐹)) = (𝑁‘(𝐺 Σg 𝐹)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldprdi.1 | . . . . . 6 ⊢ (𝜑 → 𝐺dom DProd 𝑆) | |
2 | dprdgrp 19105 | . . . . . 6 ⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp) | |
3 | 1, 2 | syl 17 | . . . . 5 ⊢ (𝜑 → 𝐺 ∈ Grp) |
4 | eqid 2820 | . . . . . 6 ⊢ (Base‘𝐺) = (Base‘𝐺) | |
5 | dprdfinv.b | . . . . . 6 ⊢ 𝑁 = (invg‘𝐺) | |
6 | 4, 5 | grpinvf 18128 | . . . . 5 ⊢ (𝐺 ∈ Grp → 𝑁:(Base‘𝐺)⟶(Base‘𝐺)) |
7 | 3, 6 | syl 17 | . . . 4 ⊢ (𝜑 → 𝑁:(Base‘𝐺)⟶(Base‘𝐺)) |
8 | eldprdi.w | . . . . 5 ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } | |
9 | eldprdi.2 | . . . . 5 ⊢ (𝜑 → dom 𝑆 = 𝐼) | |
10 | eldprdi.3 | . . . . 5 ⊢ (𝜑 → 𝐹 ∈ 𝑊) | |
11 | 8, 1, 9, 10, 4 | dprdff 19112 | . . . 4 ⊢ (𝜑 → 𝐹:𝐼⟶(Base‘𝐺)) |
12 | fcompt 6876 | . . . 4 ⊢ ((𝑁:(Base‘𝐺)⟶(Base‘𝐺) ∧ 𝐹:𝐼⟶(Base‘𝐺)) → (𝑁 ∘ 𝐹) = (𝑥 ∈ 𝐼 ↦ (𝑁‘(𝐹‘𝑥)))) | |
13 | 7, 11, 12 | syl2anc 586 | . . 3 ⊢ (𝜑 → (𝑁 ∘ 𝐹) = (𝑥 ∈ 𝐼 ↦ (𝑁‘(𝐹‘𝑥)))) |
14 | 1, 9 | dprdf2 19107 | . . . . . 6 ⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) |
15 | 14 | ffvelrnda 6832 | . . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑆‘𝑥) ∈ (SubGrp‘𝐺)) |
16 | 8, 1, 9, 10 | dprdfcl 19113 | . . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ (𝑆‘𝑥)) |
17 | 5 | subginvcl 18266 | . . . . 5 ⊢ (((𝑆‘𝑥) ∈ (SubGrp‘𝐺) ∧ (𝐹‘𝑥) ∈ (𝑆‘𝑥)) → (𝑁‘(𝐹‘𝑥)) ∈ (𝑆‘𝑥)) |
18 | 15, 16, 17 | syl2anc 586 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑁‘(𝐹‘𝑥)) ∈ (𝑆‘𝑥)) |
19 | 1, 9 | dprddomcld 19101 | . . . . . 6 ⊢ (𝜑 → 𝐼 ∈ V) |
20 | 19 | mptexd 6968 | . . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑁‘(𝐹‘𝑥))) ∈ V) |
21 | funmpt 6374 | . . . . . 6 ⊢ Fun (𝑥 ∈ 𝐼 ↦ (𝑁‘(𝐹‘𝑥))) | |
22 | 21 | a1i 11 | . . . . 5 ⊢ (𝜑 → Fun (𝑥 ∈ 𝐼 ↦ (𝑁‘(𝐹‘𝑥)))) |
23 | 8, 1, 9, 10 | dprdffsupp 19114 | . . . . 5 ⊢ (𝜑 → 𝐹 finSupp 0 ) |
24 | ssidd 3973 | . . . . . . . . 9 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐹 supp 0 )) | |
25 | eldprdi.0 | . . . . . . . . . . 11 ⊢ 0 = (0g‘𝐺) | |
26 | 25 | fvexi 6665 | . . . . . . . . . 10 ⊢ 0 ∈ V |
27 | 26 | a1i 11 | . . . . . . . . 9 ⊢ (𝜑 → 0 ∈ V) |
28 | 11, 24, 19, 27 | suppssr 7842 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ (𝐹 supp 0 ))) → (𝐹‘𝑥) = 0 ) |
29 | 28 | fveq2d 6655 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ (𝐹 supp 0 ))) → (𝑁‘(𝐹‘𝑥)) = (𝑁‘ 0 )) |
30 | 25, 5 | grpinvid 18138 | . . . . . . . . 9 ⊢ (𝐺 ∈ Grp → (𝑁‘ 0 ) = 0 ) |
31 | 3, 30 | syl 17 | . . . . . . . 8 ⊢ (𝜑 → (𝑁‘ 0 ) = 0 ) |
32 | 31 | adantr 483 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ (𝐹 supp 0 ))) → (𝑁‘ 0 ) = 0 ) |
33 | 29, 32 | eqtrd 2855 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ (𝐹 supp 0 ))) → (𝑁‘(𝐹‘𝑥)) = 0 ) |
34 | 33, 19 | suppss2 7845 | . . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ (𝑁‘(𝐹‘𝑥))) supp 0 ) ⊆ (𝐹 supp 0 )) |
35 | fsuppsssupp 8830 | . . . . 5 ⊢ ((((𝑥 ∈ 𝐼 ↦ (𝑁‘(𝐹‘𝑥))) ∈ V ∧ Fun (𝑥 ∈ 𝐼 ↦ (𝑁‘(𝐹‘𝑥)))) ∧ (𝐹 finSupp 0 ∧ ((𝑥 ∈ 𝐼 ↦ (𝑁‘(𝐹‘𝑥))) supp 0 ) ⊆ (𝐹 supp 0 ))) → (𝑥 ∈ 𝐼 ↦ (𝑁‘(𝐹‘𝑥))) finSupp 0 ) | |
36 | 20, 22, 23, 34, 35 | syl22anc 836 | . . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑁‘(𝐹‘𝑥))) finSupp 0 ) |
37 | 8, 1, 9, 18, 36 | dprdwd 19111 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑁‘(𝐹‘𝑥))) ∈ 𝑊) |
38 | 13, 37 | eqeltrd 2911 | . 2 ⊢ (𝜑 → (𝑁 ∘ 𝐹) ∈ 𝑊) |
39 | eqid 2820 | . . 3 ⊢ (Cntz‘𝐺) = (Cntz‘𝐺) | |
40 | 8, 1, 9, 10, 39 | dprdfcntz 19115 | . . 3 ⊢ (𝜑 → ran 𝐹 ⊆ ((Cntz‘𝐺)‘ran 𝐹)) |
41 | 4, 25, 39, 5, 3, 19, 11, 40, 23 | gsumzinv 19043 | . 2 ⊢ (𝜑 → (𝐺 Σg (𝑁 ∘ 𝐹)) = (𝑁‘(𝐺 Σg 𝐹))) |
42 | 38, 41 | jca 514 | 1 ⊢ (𝜑 → ((𝑁 ∘ 𝐹) ∈ 𝑊 ∧ (𝐺 Σg (𝑁 ∘ 𝐹)) = (𝑁‘(𝐺 Σg 𝐹)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1537 ∈ wcel 2114 {crab 3137 Vcvv 3481 ∖ cdif 3916 ⊆ wss 3919 class class class wbr 5047 ↦ cmpt 5127 dom cdm 5536 ∘ ccom 5540 Fun wfun 6330 ⟶wf 6332 ‘cfv 6336 (class class class)co 7137 supp csupp 7811 Xcixp 8442 finSupp cfsupp 8814 Basecbs 16461 0gc0g 16691 Σg cgsu 16692 Grpcgrp 18081 invgcminusg 18082 SubGrpcsubg 18251 Cntzccntz 18423 DProd cdprd 19093 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2792 ax-rep 5171 ax-sep 5184 ax-nul 5191 ax-pow 5247 ax-pr 5311 ax-un 7442 ax-cnex 10574 ax-resscn 10575 ax-1cn 10576 ax-icn 10577 ax-addcl 10578 ax-addrcl 10579 ax-mulcl 10580 ax-mulrcl 10581 ax-mulcom 10582 ax-addass 10583 ax-mulass 10584 ax-distr 10585 ax-i2m1 10586 ax-1ne0 10587 ax-1rid 10588 ax-rnegex 10589 ax-rrecex 10590 ax-cnre 10591 ax-pre-lttri 10592 ax-pre-lttrn 10593 ax-pre-ltadd 10594 ax-pre-mulgt0 10595 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2653 df-clab 2799 df-cleq 2813 df-clel 2891 df-nfc 2959 df-ne 3012 df-nel 3119 df-ral 3138 df-rex 3139 df-reu 3140 df-rmo 3141 df-rab 3142 df-v 3483 df-sbc 3759 df-csb 3867 df-dif 3922 df-un 3924 df-in 3926 df-ss 3935 df-pss 3937 df-nul 4275 df-if 4449 df-pw 4522 df-sn 4549 df-pr 4551 df-tp 4553 df-op 4555 df-uni 4820 df-int 4858 df-iun 4902 df-iin 4903 df-br 5048 df-opab 5110 df-mpt 5128 df-tr 5154 df-id 5441 df-eprel 5446 df-po 5455 df-so 5456 df-fr 5495 df-se 5496 df-we 5497 df-xp 5542 df-rel 5543 df-cnv 5544 df-co 5545 df-dm 5546 df-rn 5547 df-res 5548 df-ima 5549 df-pred 6129 df-ord 6175 df-on 6176 df-lim 6177 df-suc 6178 df-iota 6295 df-fun 6338 df-fn 6339 df-f 6340 df-f1 6341 df-fo 6342 df-f1o 6343 df-fv 6344 df-isom 6345 df-riota 7095 df-ov 7140 df-oprab 7141 df-mpo 7142 df-om 7562 df-1st 7670 df-2nd 7671 df-supp 7812 df-tpos 7873 df-wrecs 7928 df-recs 7989 df-rdg 8027 df-1o 8083 df-oadd 8087 df-er 8270 df-map 8389 df-ixp 8443 df-en 8491 df-dom 8492 df-sdom 8493 df-fin 8494 df-fsupp 8815 df-oi 8955 df-card 9349 df-pnf 10658 df-mnf 10659 df-xr 10660 df-ltxr 10661 df-le 10662 df-sub 10853 df-neg 10854 df-nn 11620 df-2 11682 df-n0 11880 df-z 11964 df-uz 12226 df-fz 12878 df-fzo 13019 df-seq 13355 df-hash 13676 df-ndx 16464 df-slot 16465 df-base 16467 df-sets 16468 df-ress 16469 df-plusg 16556 df-0g 16693 df-gsum 16694 df-mre 16835 df-mrc 16836 df-acs 16838 df-mgm 17830 df-sgrp 17879 df-mnd 17890 df-mhm 17934 df-submnd 17935 df-grp 18084 df-minusg 18085 df-subg 18254 df-ghm 18334 df-gim 18377 df-cntz 18425 df-oppg 18452 df-cmn 18886 df-dprd 19095 |
This theorem is referenced by: dprdfsub 19121 |
Copyright terms: Public domain | W3C validator |