| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > dprdgrp | Structured version Visualization version GIF version | ||
| Description: Reverse closure for the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) |
| Ref | Expression |
|---|---|
| dprdgrp | ⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | reldmdprd 19921 | . . . . . 6 ⊢ Rel dom DProd | |
| 2 | 1 | brrelex2i 5678 | . . . . 5 ⊢ (𝐺dom DProd 𝑆 → 𝑆 ∈ V) |
| 3 | 2 | dmexd 7842 | . . . 4 ⊢ (𝐺dom DProd 𝑆 → dom 𝑆 ∈ V) |
| 4 | eqid 2733 | . . . 4 ⊢ dom 𝑆 = dom 𝑆 | |
| 5 | eqid 2733 | . . . . 5 ⊢ (Cntz‘𝐺) = (Cntz‘𝐺) | |
| 6 | eqid 2733 | . . . . 5 ⊢ (0g‘𝐺) = (0g‘𝐺) | |
| 7 | eqid 2733 | . . . . 5 ⊢ (mrCls‘(SubGrp‘𝐺)) = (mrCls‘(SubGrp‘𝐺)) | |
| 8 | 5, 6, 7 | dmdprd 19922 | . . . 4 ⊢ ((dom 𝑆 ∈ V ∧ dom 𝑆 = dom 𝑆) → (𝐺dom DProd 𝑆 ↔ (𝐺 ∈ Grp ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (dom 𝑆 ∖ {𝑥})))) = {(0g‘𝐺)})))) |
| 9 | 3, 4, 8 | sylancl 586 | . . 3 ⊢ (𝐺dom DProd 𝑆 → (𝐺dom DProd 𝑆 ↔ (𝐺 ∈ Grp ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (dom 𝑆 ∖ {𝑥})))) = {(0g‘𝐺)})))) |
| 10 | 9 | ibi 267 | . 2 ⊢ (𝐺dom DProd 𝑆 → (𝐺 ∈ Grp ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (dom 𝑆 ∖ {𝑥})))) = {(0g‘𝐺)}))) |
| 11 | 10 | simp1d 1142 | 1 ⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ∀wral 3049 Vcvv 3438 ∖ cdif 3896 ∩ cin 3898 ⊆ wss 3899 {csn 4577 ∪ cuni 4860 class class class wbr 5095 dom cdm 5621 “ cima 5624 ⟶wf 6485 ‘cfv 6489 0gc0g 17353 mrClscmrc 17495 Grpcgrp 18856 SubGrpcsubg 19043 Cntzccntz 19237 DProd cdprd 19917 |
| 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 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7677 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2883 df-ne 2931 df-ral 3050 df-rex 3059 df-reu 3349 df-rab 3398 df-v 3440 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4861 df-iun 4945 df-br 5096 df-opab 5158 df-mpt 5177 df-id 5516 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-oprab 7359 df-mpo 7360 df-1st 7930 df-2nd 7931 df-ixp 8831 df-dprd 19919 |
| This theorem is referenced by: dprdssv 19940 dprdfid 19941 dprdfinv 19943 dprdfadd 19944 dprdfsub 19945 dprdfeq0 19946 dprdf11 19947 dprdsubg 19948 dprdlub 19950 dprdspan 19951 dprdres 19952 dprdss 19953 dprdf1o 19956 dmdprdsplitlem 19961 dprdcntz2 19962 dprddisj2 19963 dprd2dlem1 19965 dprd2da 19966 dmdprdsplit2lem 19969 dmdprdsplit2 19970 dpjfval 19979 dpjidcl 19982 |
| Copyright terms: Public domain | W3C validator |