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

Theorem dprdsn 18635
 Description: A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.)
Assertion
Ref Expression
dprdsn ((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {⟨𝐴, 𝑆⟩} ∧ (𝐺 DProd {⟨𝐴, 𝑆⟩}) = 𝑆))

Proof of Theorem dprdsn
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2760 . . 3 (Cntz‘𝐺) = (Cntz‘𝐺)
2 eqid 2760 . . 3 (0g𝐺) = (0g𝐺)
3 eqid 2760 . . 3 (mrCls‘(SubGrp‘𝐺)) = (mrCls‘(SubGrp‘𝐺))
4 subgrcl 17800 . . . 4 (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)
54adantl 473 . . 3 ((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) → 𝐺 ∈ Grp)
6 snex 5057 . . . 4 {𝐴} ∈ V
76a1i 11 . . 3 ((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) → {𝐴} ∈ V)
8 f1osng 6338 . . . . 5 ((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) → {⟨𝐴, 𝑆⟩}:{𝐴}–1-1-onto→{𝑆})
9 f1of 6298 . . . . 5 ({⟨𝐴, 𝑆⟩}:{𝐴}–1-1-onto→{𝑆} → {⟨𝐴, 𝑆⟩}:{𝐴}⟶{𝑆})
108, 9syl 17 . . . 4 ((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) → {⟨𝐴, 𝑆⟩}:{𝐴}⟶{𝑆})
11 simpr 479 . . . . 5 ((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) → 𝑆 ∈ (SubGrp‘𝐺))
1211snssd 4485 . . . 4 ((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) → {𝑆} ⊆ (SubGrp‘𝐺))
1310, 12fssd 6218 . . 3 ((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) → {⟨𝐴, 𝑆⟩}:{𝐴}⟶(SubGrp‘𝐺))
14 simpr1 1234 . . . . . 6 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴} ∧ 𝑥𝑦)) → 𝑥 ∈ {𝐴})
15 elsni 4338 . . . . . 6 (𝑥 ∈ {𝐴} → 𝑥 = 𝐴)
1614, 15syl 17 . . . . 5 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴} ∧ 𝑥𝑦)) → 𝑥 = 𝐴)
17 simpr2 1236 . . . . . 6 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴} ∧ 𝑥𝑦)) → 𝑦 ∈ {𝐴})
18 elsni 4338 . . . . . 6 (𝑦 ∈ {𝐴} → 𝑦 = 𝐴)
1917, 18syl 17 . . . . 5 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴} ∧ 𝑥𝑦)) → 𝑦 = 𝐴)
2016, 19eqtr4d 2797 . . . 4 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴} ∧ 𝑥𝑦)) → 𝑥 = 𝑦)
21 simpr3 1238 . . . 4 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴} ∧ 𝑥𝑦)) → 𝑥𝑦)
2220, 21pm2.21ddne 3016 . . 3 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴} ∧ 𝑥𝑦)) → ({⟨𝐴, 𝑆⟩}‘𝑥) ⊆ ((Cntz‘𝐺)‘({⟨𝐴, 𝑆⟩}‘𝑦)))
235adantr 472 . . . . . . . 8 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → 𝐺 ∈ Grp)
24 eqid 2760 . . . . . . . . 9 (Base‘𝐺) = (Base‘𝐺)
2524subgacs 17830 . . . . . . . 8 (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)))
26 acsmre 16514 . . . . . . . 8 ((SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
2723, 25, 263syl 18 . . . . . . 7 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
2815adantl 473 . . . . . . . . . . . . . . 15 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → 𝑥 = 𝐴)
2928sneqd 4333 . . . . . . . . . . . . . 14 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → {𝑥} = {𝐴})
3029difeq2d 3871 . . . . . . . . . . . . 13 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → ({𝐴} ∖ {𝑥}) = ({𝐴} ∖ {𝐴}))
31 difid 4091 . . . . . . . . . . . . 13 ({𝐴} ∖ {𝐴}) = ∅
3230, 31syl6eq 2810 . . . . . . . . . . . 12 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → ({𝐴} ∖ {𝑥}) = ∅)
3332imaeq2d 5624 . . . . . . . . . . 11 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → ({⟨𝐴, 𝑆⟩} “ ({𝐴} ∖ {𝑥})) = ({⟨𝐴, 𝑆⟩} “ ∅))
34 ima0 5639 . . . . . . . . . . 11 ({⟨𝐴, 𝑆⟩} “ ∅) = ∅
3533, 34syl6eq 2810 . . . . . . . . . 10 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → ({⟨𝐴, 𝑆⟩} “ ({𝐴} ∖ {𝑥})) = ∅)
3635unieqd 4598 . . . . . . . . 9 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → ({⟨𝐴, 𝑆⟩} “ ({𝐴} ∖ {𝑥})) = ∅)
37 uni0 4617 . . . . . . . . 9 ∅ = ∅
3836, 37syl6eq 2810 . . . . . . . 8 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → ({⟨𝐴, 𝑆⟩} “ ({𝐴} ∖ {𝑥})) = ∅)
39 0ss 4115 . . . . . . . . 9 ∅ ⊆ {(0g𝐺)}
4039a1i 11 . . . . . . . 8 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → ∅ ⊆ {(0g𝐺)})
4138, 40eqsstrd 3780 . . . . . . 7 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → ({⟨𝐴, 𝑆⟩} “ ({𝐴} ∖ {𝑥})) ⊆ {(0g𝐺)})
4220subg 17820 . . . . . . . 8 (𝐺 ∈ Grp → {(0g𝐺)} ∈ (SubGrp‘𝐺))
4323, 42syl 17 . . . . . . 7 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → {(0g𝐺)} ∈ (SubGrp‘𝐺))
443mrcsscl 16482 . . . . . . 7 (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ ({⟨𝐴, 𝑆⟩} “ ({𝐴} ∖ {𝑥})) ⊆ {(0g𝐺)} ∧ {(0g𝐺)} ∈ (SubGrp‘𝐺)) → ((mrCls‘(SubGrp‘𝐺))‘ ({⟨𝐴, 𝑆⟩} “ ({𝐴} ∖ {𝑥}))) ⊆ {(0g𝐺)})
4527, 41, 43, 44syl3anc 1477 . . . . . 6 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → ((mrCls‘(SubGrp‘𝐺))‘ ({⟨𝐴, 𝑆⟩} “ ({𝐴} ∖ {𝑥}))) ⊆ {(0g𝐺)})
462subg0cl 17803 . . . . . . . . 9 (𝑆 ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ 𝑆)
4746ad2antlr 765 . . . . . . . 8 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → (0g𝐺) ∈ 𝑆)
4815fveq2d 6356 . . . . . . . . 9 (𝑥 ∈ {𝐴} → ({⟨𝐴, 𝑆⟩}‘𝑥) = ({⟨𝐴, 𝑆⟩}‘𝐴))
49 fvsng 6611 . . . . . . . . 9 ((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) → ({⟨𝐴, 𝑆⟩}‘𝐴) = 𝑆)
5048, 49sylan9eqr 2816 . . . . . . . 8 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → ({⟨𝐴, 𝑆⟩}‘𝑥) = 𝑆)
5147, 50eleqtrrd 2842 . . . . . . 7 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → (0g𝐺) ∈ ({⟨𝐴, 𝑆⟩}‘𝑥))
5251snssd 4485 . . . . . 6 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → {(0g𝐺)} ⊆ ({⟨𝐴, 𝑆⟩}‘𝑥))
5345, 52sstrd 3754 . . . . 5 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → ((mrCls‘(SubGrp‘𝐺))‘ ({⟨𝐴, 𝑆⟩} “ ({𝐴} ∖ {𝑥}))) ⊆ ({⟨𝐴, 𝑆⟩}‘𝑥))
54 sseqin2 3960 . . . . 5 (((mrCls‘(SubGrp‘𝐺))‘ ({⟨𝐴, 𝑆⟩} “ ({𝐴} ∖ {𝑥}))) ⊆ ({⟨𝐴, 𝑆⟩}‘𝑥) ↔ (({⟨𝐴, 𝑆⟩}‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘ ({⟨𝐴, 𝑆⟩} “ ({𝐴} ∖ {𝑥})))) = ((mrCls‘(SubGrp‘𝐺))‘ ({⟨𝐴, 𝑆⟩} “ ({𝐴} ∖ {𝑥}))))
5553, 54sylib 208 . . . 4 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → (({⟨𝐴, 𝑆⟩}‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘ ({⟨𝐴, 𝑆⟩} “ ({𝐴} ∖ {𝑥})))) = ((mrCls‘(SubGrp‘𝐺))‘ ({⟨𝐴, 𝑆⟩} “ ({𝐴} ∖ {𝑥}))))
5655, 45eqsstrd 3780 . . 3 (((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → (({⟨𝐴, 𝑆⟩}‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘ ({⟨𝐴, 𝑆⟩} “ ({𝐴} ∖ {𝑥})))) ⊆ {(0g𝐺)})
571, 2, 3, 5, 7, 13, 22, 56dmdprdd 18598 . 2 ((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) → 𝐺dom DProd {⟨𝐴, 𝑆⟩})
583dprdspan 18626 . . . 4 (𝐺dom DProd {⟨𝐴, 𝑆⟩} → (𝐺 DProd {⟨𝐴, 𝑆⟩}) = ((mrCls‘(SubGrp‘𝐺))‘ ran {⟨𝐴, 𝑆⟩}))
5957, 58syl 17 . . 3 ((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) → (𝐺 DProd {⟨𝐴, 𝑆⟩}) = ((mrCls‘(SubGrp‘𝐺))‘ ran {⟨𝐴, 𝑆⟩}))
60 rnsnopg 5773 . . . . . . . 8 (𝐴𝑉 → ran {⟨𝐴, 𝑆⟩} = {𝑆})
6160adantr 472 . . . . . . 7 ((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) → ran {⟨𝐴, 𝑆⟩} = {𝑆})
6261unieqd 4598 . . . . . 6 ((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) → ran {⟨𝐴, 𝑆⟩} = {𝑆})
63 unisng 4604 . . . . . . 7 (𝑆 ∈ (SubGrp‘𝐺) → {𝑆} = 𝑆)
6463adantl 473 . . . . . 6 ((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) → {𝑆} = 𝑆)
6562, 64eqtrd 2794 . . . . 5 ((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) → ran {⟨𝐴, 𝑆⟩} = 𝑆)
6665fveq2d 6356 . . . 4 ((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) → ((mrCls‘(SubGrp‘𝐺))‘ ran {⟨𝐴, 𝑆⟩}) = ((mrCls‘(SubGrp‘𝐺))‘𝑆))
675, 25, 263syl 18 . . . . 5 ((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
683mrcid 16475 . . . . 5 (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((mrCls‘(SubGrp‘𝐺))‘𝑆) = 𝑆)
6967, 68sylancom 704 . . . 4 ((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) → ((mrCls‘(SubGrp‘𝐺))‘𝑆) = 𝑆)
7066, 69eqtrd 2794 . . 3 ((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) → ((mrCls‘(SubGrp‘𝐺))‘ ran {⟨𝐴, 𝑆⟩}) = 𝑆)
7159, 70eqtrd 2794 . 2 ((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) → (𝐺 DProd {⟨𝐴, 𝑆⟩}) = 𝑆)
7257, 71jca 555 1 ((𝐴𝑉𝑆 ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {⟨𝐴, 𝑆⟩} ∧ (𝐺 DProd {⟨𝐴, 𝑆⟩}) = 𝑆))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072   = wceq 1632   ∈ wcel 2139   ≠ wne 2932  Vcvv 3340   ∖ cdif 3712   ∩ cin 3714   ⊆ wss 3715  ∅c0 4058  {csn 4321  ⟨cop 4327  ∪ cuni 4588   class class class wbr 4804  dom cdm 5266  ran crn 5267   “ cima 5269  ⟶wf 6045  –1-1-onto→wf1o 6048  ‘cfv 6049  (class class class)co 6813  Basecbs 16059  0gc0g 16302  Moorecmre 16444  mrClscmrc 16445  ACScacs 16447  Grpcgrp 17623  SubGrpcsubg 17789  Cntzccntz 17948   DProd cdprd 18592 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-of 7062  df-om 7231  df-1st 7333  df-2nd 7334  df-supp 7464  df-tpos 7521  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-oadd 7733  df-er 7911  df-map 8025  df-ixp 8075  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-fsupp 8441  df-oi 8580  df-card 8955  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-nn 11213  df-2 11271  df-n0 11485  df-z 11570  df-uz 11880  df-fz 12520  df-fzo 12660  df-seq 12996  df-hash 13312  df-ndx 16062  df-slot 16063  df-base 16065  df-sets 16066  df-ress 16067  df-plusg 16156  df-0g 16304  df-gsum 16305  df-mre 16448  df-mrc 16449  df-acs 16451  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-mhm 17536  df-submnd 17537  df-grp 17626  df-minusg 17627  df-sbg 17628  df-mulg 17742  df-subg 17792  df-ghm 17859  df-gim 17902  df-cntz 17950  df-oppg 17976  df-cmn 18395  df-dprd 18594 This theorem is referenced by:  dprd2da  18641  dmdprdpr  18648  dprdpr  18649  dpjlem  18650  pgpfaclem1  18680
 Copyright terms: Public domain W3C validator