![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dprdspan | Structured version Visualization version GIF version |
Description: The direct product is the span of the union of the factors. (Contributed by Mario Carneiro, 25-Apr-2016.) |
Ref | Expression |
---|---|
dprdspan.k | ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) |
Ref | Expression |
---|---|
dprdspan | ⊢ (𝐺dom DProd 𝑆 → (𝐺 DProd 𝑆) = (𝐾‘∪ ran 𝑆)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . . 3 ⊢ (𝐺dom DProd 𝑆 → 𝐺dom DProd 𝑆) | |
2 | eqidd 2795 | . . 3 ⊢ (𝐺dom DProd 𝑆 → dom 𝑆 = dom 𝑆) | |
3 | dprdgrp 18844 | . . . . 5 ⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp) | |
4 | eqid 2794 | . . . . . 6 ⊢ (Base‘𝐺) = (Base‘𝐺) | |
5 | 4 | subgacs 18068 | . . . . 5 ⊢ (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺))) |
6 | acsmre 16752 | . . . . 5 ⊢ ((SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) | |
7 | 3, 5, 6 | 3syl 18 | . . . 4 ⊢ (𝐺dom DProd 𝑆 → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
8 | dprdf 18845 | . . . . . . . 8 ⊢ (𝐺dom DProd 𝑆 → 𝑆:dom 𝑆⟶(SubGrp‘𝐺)) | |
9 | 8 | ffnd 6386 | . . . . . . 7 ⊢ (𝐺dom DProd 𝑆 → 𝑆 Fn dom 𝑆) |
10 | fniunfv 6874 | . . . . . . 7 ⊢ (𝑆 Fn dom 𝑆 → ∪ 𝑘 ∈ dom 𝑆(𝑆‘𝑘) = ∪ ran 𝑆) | |
11 | 9, 10 | syl 17 | . . . . . 6 ⊢ (𝐺dom DProd 𝑆 → ∪ 𝑘 ∈ dom 𝑆(𝑆‘𝑘) = ∪ ran 𝑆) |
12 | simpl 483 | . . . . . . . . 9 ⊢ ((𝐺dom DProd 𝑆 ∧ 𝑘 ∈ dom 𝑆) → 𝐺dom DProd 𝑆) | |
13 | eqidd 2795 | . . . . . . . . 9 ⊢ ((𝐺dom DProd 𝑆 ∧ 𝑘 ∈ dom 𝑆) → dom 𝑆 = dom 𝑆) | |
14 | simpr 485 | . . . . . . . . 9 ⊢ ((𝐺dom DProd 𝑆 ∧ 𝑘 ∈ dom 𝑆) → 𝑘 ∈ dom 𝑆) | |
15 | 12, 13, 14 | dprdub 18864 | . . . . . . . 8 ⊢ ((𝐺dom DProd 𝑆 ∧ 𝑘 ∈ dom 𝑆) → (𝑆‘𝑘) ⊆ (𝐺 DProd 𝑆)) |
16 | 15 | ralrimiva 3148 | . . . . . . 7 ⊢ (𝐺dom DProd 𝑆 → ∀𝑘 ∈ dom 𝑆(𝑆‘𝑘) ⊆ (𝐺 DProd 𝑆)) |
17 | iunss 4870 | . . . . . . 7 ⊢ (∪ 𝑘 ∈ dom 𝑆(𝑆‘𝑘) ⊆ (𝐺 DProd 𝑆) ↔ ∀𝑘 ∈ dom 𝑆(𝑆‘𝑘) ⊆ (𝐺 DProd 𝑆)) | |
18 | 16, 17 | sylibr 235 | . . . . . 6 ⊢ (𝐺dom DProd 𝑆 → ∪ 𝑘 ∈ dom 𝑆(𝑆‘𝑘) ⊆ (𝐺 DProd 𝑆)) |
19 | 11, 18 | eqsstrrd 3929 | . . . . 5 ⊢ (𝐺dom DProd 𝑆 → ∪ ran 𝑆 ⊆ (𝐺 DProd 𝑆)) |
20 | 4 | dprdssv 18855 | . . . . 5 ⊢ (𝐺 DProd 𝑆) ⊆ (Base‘𝐺) |
21 | 19, 20 | syl6ss 3903 | . . . 4 ⊢ (𝐺dom DProd 𝑆 → ∪ ran 𝑆 ⊆ (Base‘𝐺)) |
22 | dprdspan.k | . . . . 5 ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) | |
23 | 22 | mrccl 16711 | . . . 4 ⊢ (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ ∪ ran 𝑆 ⊆ (Base‘𝐺)) → (𝐾‘∪ ran 𝑆) ∈ (SubGrp‘𝐺)) |
24 | 7, 21, 23 | syl2anc 584 | . . 3 ⊢ (𝐺dom DProd 𝑆 → (𝐾‘∪ ran 𝑆) ∈ (SubGrp‘𝐺)) |
25 | eqimss 3946 | . . . . . . 7 ⊢ (∪ 𝑘 ∈ dom 𝑆(𝑆‘𝑘) = ∪ ran 𝑆 → ∪ 𝑘 ∈ dom 𝑆(𝑆‘𝑘) ⊆ ∪ ran 𝑆) | |
26 | 11, 25 | syl 17 | . . . . . 6 ⊢ (𝐺dom DProd 𝑆 → ∪ 𝑘 ∈ dom 𝑆(𝑆‘𝑘) ⊆ ∪ ran 𝑆) |
27 | iunss 4870 | . . . . . 6 ⊢ (∪ 𝑘 ∈ dom 𝑆(𝑆‘𝑘) ⊆ ∪ ran 𝑆 ↔ ∀𝑘 ∈ dom 𝑆(𝑆‘𝑘) ⊆ ∪ ran 𝑆) | |
28 | 26, 27 | sylib 219 | . . . . 5 ⊢ (𝐺dom DProd 𝑆 → ∀𝑘 ∈ dom 𝑆(𝑆‘𝑘) ⊆ ∪ ran 𝑆) |
29 | 28 | r19.21bi 3174 | . . . 4 ⊢ ((𝐺dom DProd 𝑆 ∧ 𝑘 ∈ dom 𝑆) → (𝑆‘𝑘) ⊆ ∪ ran 𝑆) |
30 | 7, 22, 21 | mrcssidd 16725 | . . . . 5 ⊢ (𝐺dom DProd 𝑆 → ∪ ran 𝑆 ⊆ (𝐾‘∪ ran 𝑆)) |
31 | 30 | adantr 481 | . . . 4 ⊢ ((𝐺dom DProd 𝑆 ∧ 𝑘 ∈ dom 𝑆) → ∪ ran 𝑆 ⊆ (𝐾‘∪ ran 𝑆)) |
32 | 29, 31 | sstrd 3901 | . . 3 ⊢ ((𝐺dom DProd 𝑆 ∧ 𝑘 ∈ dom 𝑆) → (𝑆‘𝑘) ⊆ (𝐾‘∪ ran 𝑆)) |
33 | 1, 2, 24, 32 | dprdlub 18865 | . 2 ⊢ (𝐺dom DProd 𝑆 → (𝐺 DProd 𝑆) ⊆ (𝐾‘∪ ran 𝑆)) |
34 | dprdsubg 18863 | . . 3 ⊢ (𝐺dom DProd 𝑆 → (𝐺 DProd 𝑆) ∈ (SubGrp‘𝐺)) | |
35 | 22 | mrcsscl 16720 | . . 3 ⊢ (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ ∪ ran 𝑆 ⊆ (𝐺 DProd 𝑆) ∧ (𝐺 DProd 𝑆) ∈ (SubGrp‘𝐺)) → (𝐾‘∪ ran 𝑆) ⊆ (𝐺 DProd 𝑆)) |
36 | 7, 19, 34, 35 | syl3anc 1364 | . 2 ⊢ (𝐺dom DProd 𝑆 → (𝐾‘∪ ran 𝑆) ⊆ (𝐺 DProd 𝑆)) |
37 | 33, 36 | eqssd 3908 | 1 ⊢ (𝐺dom DProd 𝑆 → (𝐺 DProd 𝑆) = (𝐾‘∪ ran 𝑆)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1522 ∈ wcel 2080 ∀wral 3104 ⊆ wss 3861 ∪ cuni 4747 ∪ ciun 4827 class class class wbr 4964 dom cdm 5446 ran crn 5447 Fn wfn 6223 ‘cfv 6228 (class class class)co 7019 Basecbs 16312 Moorecmre 16682 mrClscmrc 16683 ACScacs 16685 Grpcgrp 17861 SubGrpcsubg 18027 DProd cdprd 18832 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-8 2082 ax-9 2090 ax-10 2111 ax-11 2125 ax-12 2140 ax-13 2343 ax-ext 2768 ax-rep 5084 ax-sep 5097 ax-nul 5104 ax-pow 5160 ax-pr 5224 ax-un 7322 ax-cnex 10442 ax-resscn 10443 ax-1cn 10444 ax-icn 10445 ax-addcl 10446 ax-addrcl 10447 ax-mulcl 10448 ax-mulrcl 10449 ax-mulcom 10450 ax-addass 10451 ax-mulass 10452 ax-distr 10453 ax-i2m1 10454 ax-1ne0 10455 ax-1rid 10456 ax-rnegex 10457 ax-rrecex 10458 ax-cnre 10459 ax-pre-lttri 10460 ax-pre-lttrn 10461 ax-pre-ltadd 10462 ax-pre-mulgt0 10463 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1763 df-nf 1767 df-sb 2042 df-mo 2575 df-eu 2611 df-clab 2775 df-cleq 2787 df-clel 2862 df-nfc 2934 df-ne 2984 df-nel 3090 df-ral 3109 df-rex 3110 df-reu 3111 df-rmo 3112 df-rab 3113 df-v 3438 df-sbc 3708 df-csb 3814 df-dif 3864 df-un 3866 df-in 3868 df-ss 3876 df-pss 3878 df-nul 4214 df-if 4384 df-pw 4457 df-sn 4475 df-pr 4477 df-tp 4479 df-op 4481 df-uni 4748 df-int 4785 df-iun 4829 df-iin 4830 df-br 4965 df-opab 5027 df-mpt 5044 df-tr 5067 df-id 5351 df-eprel 5356 df-po 5365 df-so 5366 df-fr 5405 df-se 5406 df-we 5407 df-xp 5452 df-rel 5453 df-cnv 5454 df-co 5455 df-dm 5456 df-rn 5457 df-res 5458 df-ima 5459 df-pred 6026 df-ord 6072 df-on 6073 df-lim 6074 df-suc 6075 df-iota 6192 df-fun 6230 df-fn 6231 df-f 6232 df-f1 6233 df-fo 6234 df-f1o 6235 df-fv 6236 df-isom 6237 df-riota 6980 df-ov 7022 df-oprab 7023 df-mpo 7024 df-of 7270 df-om 7440 df-1st 7548 df-2nd 7549 df-supp 7685 df-tpos 7746 df-wrecs 7801 df-recs 7863 df-rdg 7901 df-1o 7956 df-oadd 7960 df-er 8142 df-map 8261 df-ixp 8314 df-en 8361 df-dom 8362 df-sdom 8363 df-fin 8364 df-fsupp 8683 df-oi 8823 df-card 9217 df-pnf 10526 df-mnf 10527 df-xr 10528 df-ltxr 10529 df-le 10530 df-sub 10721 df-neg 10722 df-nn 11489 df-2 11550 df-n0 11748 df-z 11832 df-uz 12094 df-fz 12743 df-fzo 12884 df-seq 13220 df-hash 13541 df-ndx 16315 df-slot 16316 df-base 16318 df-sets 16319 df-ress 16320 df-plusg 16407 df-0g 16544 df-gsum 16545 df-mre 16686 df-mrc 16687 df-acs 16689 df-mgm 17681 df-sgrp 17723 df-mnd 17734 df-mhm 17774 df-submnd 17775 df-grp 17864 df-minusg 17865 df-sbg 17866 df-mulg 17982 df-subg 18030 df-ghm 18097 df-gim 18140 df-cntz 18188 df-oppg 18215 df-cmn 18635 df-dprd 18834 |
This theorem is referenced by: dprdres 18867 dprdf1o 18871 subgdprd 18874 dprdsn 18875 dprd2dlem1 18880 dprd2da 18881 dprd2db 18882 dmdprdsplit2lem 18884 |
Copyright terms: Public domain | W3C validator |