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

Theorem conjnmzb 17635
Description: Alternative condition for elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.)
Hypotheses
Ref Expression
conjghm.x 𝑋 = (Base‘𝐺)
conjghm.p + = (+g𝐺)
conjghm.m = (-g𝐺)
conjsubg.f 𝐹 = (𝑥𝑆 ↦ ((𝐴 + 𝑥) 𝐴))
conjnmz.1 𝑁 = {𝑦𝑋 ∣ ∀𝑧𝑋 ((𝑦 + 𝑧) ∈ 𝑆 ↔ (𝑧 + 𝑦) ∈ 𝑆)}
Assertion
Ref Expression
conjnmzb (𝑆 ∈ (SubGrp‘𝐺) → (𝐴𝑁 ↔ (𝐴𝑋𝑆 = ran 𝐹)))
Distinct variable groups:   𝑥,𝑦,   𝑥,𝑧, + ,𝑦   𝑥,𝐴,𝑦,𝑧   𝑦,𝐹,𝑧   𝑥,𝑁   𝑥,𝐺,𝑦,𝑧   𝑥,𝑆,𝑦,𝑧   𝑥,𝑋,𝑦,𝑧
Allowed substitution hints:   𝐹(𝑥)   (𝑧)   𝑁(𝑦,𝑧)

Proof of Theorem conjnmzb
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 conjnmz.1 . . . . 5 𝑁 = {𝑦𝑋 ∣ ∀𝑧𝑋 ((𝑦 + 𝑧) ∈ 𝑆 ↔ (𝑧 + 𝑦) ∈ 𝑆)}
2 ssrab2 3672 . . . . 5 {𝑦𝑋 ∣ ∀𝑧𝑋 ((𝑦 + 𝑧) ∈ 𝑆 ↔ (𝑧 + 𝑦) ∈ 𝑆)} ⊆ 𝑋
31, 2eqsstri 3620 . . . 4 𝑁𝑋
4 simpr 477 . . . 4 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) → 𝐴𝑁)
53, 4sseldi 3586 . . 3 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) → 𝐴𝑋)
6 conjghm.x . . . 4 𝑋 = (Base‘𝐺)
7 conjghm.p . . . 4 + = (+g𝐺)
8 conjghm.m . . . 4 = (-g𝐺)
9 conjsubg.f . . . 4 𝐹 = (𝑥𝑆 ↦ ((𝐴 + 𝑥) 𝐴))
106, 7, 8, 9, 1conjnmz 17634 . . 3 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) → 𝑆 = ran 𝐹)
115, 10jca 554 . 2 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) → (𝐴𝑋𝑆 = ran 𝐹))
12 simprl 793 . . 3 ((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴𝑋𝑆 = ran 𝐹)) → 𝐴𝑋)
13 simplrr 800 . . . . . 6 (((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴𝑋𝑆 = ran 𝐹)) ∧ 𝑤𝑋) → 𝑆 = ran 𝐹)
1413eleq2d 2684 . . . . 5 (((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴𝑋𝑆 = ran 𝐹)) ∧ 𝑤𝑋) → ((𝐴 + 𝑤) ∈ 𝑆 ↔ (𝐴 + 𝑤) ∈ ran 𝐹))
15 subgrcl 17539 . . . . . . . . . . . . 13 (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)
1615ad3antrrr 765 . . . . . . . . . . . 12 ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑋) ∧ 𝑤𝑋) ∧ 𝑥𝑆) → 𝐺 ∈ Grp)
17 simpllr 798 . . . . . . . . . . . 12 ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑋) ∧ 𝑤𝑋) ∧ 𝑥𝑆) → 𝐴𝑋)
186subgss 17535 . . . . . . . . . . . . . 14 (𝑆 ∈ (SubGrp‘𝐺) → 𝑆𝑋)
1918ad2antrr 761 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑋) ∧ 𝑤𝑋) → 𝑆𝑋)
2019sselda 3588 . . . . . . . . . . . 12 ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑋) ∧ 𝑤𝑋) ∧ 𝑥𝑆) → 𝑥𝑋)
216, 7, 8grpaddsubass 17445 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ (𝐴𝑋𝑥𝑋𝐴𝑋)) → ((𝐴 + 𝑥) 𝐴) = (𝐴 + (𝑥 𝐴)))
2216, 17, 20, 17, 21syl13anc 1325 . . . . . . . . . . 11 ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑋) ∧ 𝑤𝑋) ∧ 𝑥𝑆) → ((𝐴 + 𝑥) 𝐴) = (𝐴 + (𝑥 𝐴)))
2322eqeq1d 2623 . . . . . . . . . 10 ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑋) ∧ 𝑤𝑋) ∧ 𝑥𝑆) → (((𝐴 + 𝑥) 𝐴) = (𝐴 + 𝑤) ↔ (𝐴 + (𝑥 𝐴)) = (𝐴 + 𝑤)))
246, 8grpsubcl 17435 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ 𝑥𝑋𝐴𝑋) → (𝑥 𝐴) ∈ 𝑋)
2516, 20, 17, 24syl3anc 1323 . . . . . . . . . . 11 ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑋) ∧ 𝑤𝑋) ∧ 𝑥𝑆) → (𝑥 𝐴) ∈ 𝑋)
26 simplr 791 . . . . . . . . . . 11 ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑋) ∧ 𝑤𝑋) ∧ 𝑥𝑆) → 𝑤𝑋)
276, 7grplcan 17417 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ ((𝑥 𝐴) ∈ 𝑋𝑤𝑋𝐴𝑋)) → ((𝐴 + (𝑥 𝐴)) = (𝐴 + 𝑤) ↔ (𝑥 𝐴) = 𝑤))
2816, 25, 26, 17, 27syl13anc 1325 . . . . . . . . . 10 ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑋) ∧ 𝑤𝑋) ∧ 𝑥𝑆) → ((𝐴 + (𝑥 𝐴)) = (𝐴 + 𝑤) ↔ (𝑥 𝐴) = 𝑤))
296, 7, 8grpsubadd 17443 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ (𝑥𝑋𝐴𝑋𝑤𝑋)) → ((𝑥 𝐴) = 𝑤 ↔ (𝑤 + 𝐴) = 𝑥))
3016, 20, 17, 26, 29syl13anc 1325 . . . . . . . . . 10 ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑋) ∧ 𝑤𝑋) ∧ 𝑥𝑆) → ((𝑥 𝐴) = 𝑤 ↔ (𝑤 + 𝐴) = 𝑥))
3123, 28, 303bitrd 294 . . . . . . . . 9 ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑋) ∧ 𝑤𝑋) ∧ 𝑥𝑆) → (((𝐴 + 𝑥) 𝐴) = (𝐴 + 𝑤) ↔ (𝑤 + 𝐴) = 𝑥))
32 eqcom 2628 . . . . . . . . 9 ((𝐴 + 𝑤) = ((𝐴 + 𝑥) 𝐴) ↔ ((𝐴 + 𝑥) 𝐴) = (𝐴 + 𝑤))
33 eqcom 2628 . . . . . . . . 9 (𝑥 = (𝑤 + 𝐴) ↔ (𝑤 + 𝐴) = 𝑥)
3431, 32, 333bitr4g 303 . . . . . . . 8 ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑋) ∧ 𝑤𝑋) ∧ 𝑥𝑆) → ((𝐴 + 𝑤) = ((𝐴 + 𝑥) 𝐴) ↔ 𝑥 = (𝑤 + 𝐴)))
3534rexbidva 3044 . . . . . . 7 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑋) ∧ 𝑤𝑋) → (∃𝑥𝑆 (𝐴 + 𝑤) = ((𝐴 + 𝑥) 𝐴) ↔ ∃𝑥𝑆 𝑥 = (𝑤 + 𝐴)))
3635adantlrr 756 . . . . . 6 (((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴𝑋𝑆 = ran 𝐹)) ∧ 𝑤𝑋) → (∃𝑥𝑆 (𝐴 + 𝑤) = ((𝐴 + 𝑥) 𝐴) ↔ ∃𝑥𝑆 𝑥 = (𝑤 + 𝐴)))
37 ovex 6643 . . . . . . 7 (𝐴 + 𝑤) ∈ V
38 eqeq1 2625 . . . . . . . 8 (𝑦 = (𝐴 + 𝑤) → (𝑦 = ((𝐴 + 𝑥) 𝐴) ↔ (𝐴 + 𝑤) = ((𝐴 + 𝑥) 𝐴)))
3938rexbidv 3047 . . . . . . 7 (𝑦 = (𝐴 + 𝑤) → (∃𝑥𝑆 𝑦 = ((𝐴 + 𝑥) 𝐴) ↔ ∃𝑥𝑆 (𝐴 + 𝑤) = ((𝐴 + 𝑥) 𝐴)))
409rnmpt 5341 . . . . . . 7 ran 𝐹 = {𝑦 ∣ ∃𝑥𝑆 𝑦 = ((𝐴 + 𝑥) 𝐴)}
4137, 39, 40elab2 3342 . . . . . 6 ((𝐴 + 𝑤) ∈ ran 𝐹 ↔ ∃𝑥𝑆 (𝐴 + 𝑤) = ((𝐴 + 𝑥) 𝐴))
42 risset 3057 . . . . . 6 ((𝑤 + 𝐴) ∈ 𝑆 ↔ ∃𝑥𝑆 𝑥 = (𝑤 + 𝐴))
4336, 41, 423bitr4g 303 . . . . 5 (((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴𝑋𝑆 = ran 𝐹)) ∧ 𝑤𝑋) → ((𝐴 + 𝑤) ∈ ran 𝐹 ↔ (𝑤 + 𝐴) ∈ 𝑆))
4414, 43bitrd 268 . . . 4 (((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴𝑋𝑆 = ran 𝐹)) ∧ 𝑤𝑋) → ((𝐴 + 𝑤) ∈ 𝑆 ↔ (𝑤 + 𝐴) ∈ 𝑆))
4544ralrimiva 2962 . . 3 ((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴𝑋𝑆 = ran 𝐹)) → ∀𝑤𝑋 ((𝐴 + 𝑤) ∈ 𝑆 ↔ (𝑤 + 𝐴) ∈ 𝑆))
461elnmz 17573 . . 3 (𝐴𝑁 ↔ (𝐴𝑋 ∧ ∀𝑤𝑋 ((𝐴 + 𝑤) ∈ 𝑆 ↔ (𝑤 + 𝐴) ∈ 𝑆)))
4712, 45, 46sylanbrc 697 . 2 ((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴𝑋𝑆 = ran 𝐹)) → 𝐴𝑁)
4811, 47impbida 876 1 (𝑆 ∈ (SubGrp‘𝐺) → (𝐴𝑁 ↔ (𝐴𝑋𝑆 = ran 𝐹)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wral 2908  wrex 2909  {crab 2912  wss 3560  cmpt 4683  ran crn 5085  cfv 5857  (class class class)co 6615  Basecbs 15800  +gcplusg 15881  Grpcgrp 17362  -gcsg 17364  SubGrpcsubg 17528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-id 4999  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-1st 7128  df-2nd 7129  df-0g 16042  df-mgm 17182  df-sgrp 17224  df-mnd 17235  df-grp 17365  df-minusg 17366  df-sbg 17367  df-subg 17531
This theorem is referenced by:  sylow3lem6  17987
  Copyright terms: Public domain W3C validator