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

Theorem conjnmz 19271
Description: A subgroup is unchanged under conjugation by an element of its 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
conjnmz ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) → 𝑆 = ran 𝐹)
Distinct variable groups:   𝑥,𝑦,   𝑥,𝑧, + ,𝑦   𝑥,𝐴,𝑦,𝑧   𝑦,𝐹,𝑧   𝑥,𝑁   𝑥,𝐺,𝑦,𝑧   𝑥,𝑆,𝑦,𝑧   𝑥,𝑋,𝑦,𝑧
Allowed substitution hints:   𝐹(𝑥)   (𝑧)   𝑁(𝑦,𝑧)

Proof of Theorem conjnmz
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 conjghm.x . . . . . . . . 9 𝑋 = (Base‘𝐺)
2 conjghm.p . . . . . . . . 9 + = (+g𝐺)
3 subgrcl 19150 . . . . . . . . . 10 (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)
43ad2antrr 726 . . . . . . . . 9 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → 𝐺 ∈ Grp)
5 eqid 2736 . . . . . . . . . 10 (invg𝐺) = (invg𝐺)
6 conjnmz.1 . . . . . . . . . . . 12 𝑁 = {𝑦𝑋 ∣ ∀𝑧𝑋 ((𝑦 + 𝑧) ∈ 𝑆 ↔ (𝑧 + 𝑦) ∈ 𝑆)}
76ssrab3 4081 . . . . . . . . . . 11 𝑁𝑋
8 simplr 768 . . . . . . . . . . 11 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → 𝐴𝑁)
97, 8sselid 3980 . . . . . . . . . 10 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → 𝐴𝑋)
101, 5, 4, 9grpinvcld 19007 . . . . . . . . 9 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → ((invg𝐺)‘𝐴) ∈ 𝑋)
111subgss 19146 . . . . . . . . . . 11 (𝑆 ∈ (SubGrp‘𝐺) → 𝑆𝑋)
1211adantr 480 . . . . . . . . . 10 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) → 𝑆𝑋)
1312sselda 3982 . . . . . . . . 9 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → 𝑤𝑋)
141, 2, 4, 10, 13, 9grpassd 18964 . . . . . . . 8 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → ((((invg𝐺)‘𝐴) + 𝑤) + 𝐴) = (((invg𝐺)‘𝐴) + (𝑤 + 𝐴)))
15 eqid 2736 . . . . . . . . . . . . 13 (0g𝐺) = (0g𝐺)
161, 2, 15, 5, 4, 9grprinvd 19014 . . . . . . . . . . . 12 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → (𝐴 + ((invg𝐺)‘𝐴)) = (0g𝐺))
1716oveq1d 7447 . . . . . . . . . . 11 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → ((𝐴 + ((invg𝐺)‘𝐴)) + 𝑤) = ((0g𝐺) + 𝑤))
181, 2, 4, 9, 10, 13grpassd 18964 . . . . . . . . . . 11 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → ((𝐴 + ((invg𝐺)‘𝐴)) + 𝑤) = (𝐴 + (((invg𝐺)‘𝐴) + 𝑤)))
191, 2, 15, 4, 13grplidd 18988 . . . . . . . . . . 11 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → ((0g𝐺) + 𝑤) = 𝑤)
2017, 18, 193eqtr3d 2784 . . . . . . . . . 10 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → (𝐴 + (((invg𝐺)‘𝐴) + 𝑤)) = 𝑤)
21 simpr 484 . . . . . . . . . 10 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → 𝑤𝑆)
2220, 21eqeltrd 2840 . . . . . . . . 9 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → (𝐴 + (((invg𝐺)‘𝐴) + 𝑤)) ∈ 𝑆)
231, 2, 4, 10, 13grpcld 18966 . . . . . . . . . 10 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → (((invg𝐺)‘𝐴) + 𝑤) ∈ 𝑋)
246nmzbi 19183 . . . . . . . . . 10 ((𝐴𝑁 ∧ (((invg𝐺)‘𝐴) + 𝑤) ∈ 𝑋) → ((𝐴 + (((invg𝐺)‘𝐴) + 𝑤)) ∈ 𝑆 ↔ ((((invg𝐺)‘𝐴) + 𝑤) + 𝐴) ∈ 𝑆))
258, 23, 24syl2anc 584 . . . . . . . . 9 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → ((𝐴 + (((invg𝐺)‘𝐴) + 𝑤)) ∈ 𝑆 ↔ ((((invg𝐺)‘𝐴) + 𝑤) + 𝐴) ∈ 𝑆))
2622, 25mpbid 232 . . . . . . . 8 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → ((((invg𝐺)‘𝐴) + 𝑤) + 𝐴) ∈ 𝑆)
2714, 26eqeltrrd 2841 . . . . . . 7 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → (((invg𝐺)‘𝐴) + (𝑤 + 𝐴)) ∈ 𝑆)
28 oveq2 7440 . . . . . . . . 9 (𝑥 = (((invg𝐺)‘𝐴) + (𝑤 + 𝐴)) → (𝐴 + 𝑥) = (𝐴 + (((invg𝐺)‘𝐴) + (𝑤 + 𝐴))))
2928oveq1d 7447 . . . . . . . 8 (𝑥 = (((invg𝐺)‘𝐴) + (𝑤 + 𝐴)) → ((𝐴 + 𝑥) 𝐴) = ((𝐴 + (((invg𝐺)‘𝐴) + (𝑤 + 𝐴))) 𝐴))
30 conjsubg.f . . . . . . . 8 𝐹 = (𝑥𝑆 ↦ ((𝐴 + 𝑥) 𝐴))
31 ovex 7465 . . . . . . . 8 ((𝐴 + (((invg𝐺)‘𝐴) + (𝑤 + 𝐴))) 𝐴) ∈ V
3229, 30, 31fvmpt 7015 . . . . . . 7 ((((invg𝐺)‘𝐴) + (𝑤 + 𝐴)) ∈ 𝑆 → (𝐹‘(((invg𝐺)‘𝐴) + (𝑤 + 𝐴))) = ((𝐴 + (((invg𝐺)‘𝐴) + (𝑤 + 𝐴))) 𝐴))
3327, 32syl 17 . . . . . 6 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → (𝐹‘(((invg𝐺)‘𝐴) + (𝑤 + 𝐴))) = ((𝐴 + (((invg𝐺)‘𝐴) + (𝑤 + 𝐴))) 𝐴))
3416oveq1d 7447 . . . . . . . 8 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → ((𝐴 + ((invg𝐺)‘𝐴)) + (𝑤 + 𝐴)) = ((0g𝐺) + (𝑤 + 𝐴)))
351, 2, 4, 13, 9grpcld 18966 . . . . . . . . 9 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → (𝑤 + 𝐴) ∈ 𝑋)
361, 2, 4, 9, 10, 35grpassd 18964 . . . . . . . 8 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → ((𝐴 + ((invg𝐺)‘𝐴)) + (𝑤 + 𝐴)) = (𝐴 + (((invg𝐺)‘𝐴) + (𝑤 + 𝐴))))
371, 2, 15, 4, 35grplidd 18988 . . . . . . . 8 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → ((0g𝐺) + (𝑤 + 𝐴)) = (𝑤 + 𝐴))
3834, 36, 373eqtr3d 2784 . . . . . . 7 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → (𝐴 + (((invg𝐺)‘𝐴) + (𝑤 + 𝐴))) = (𝑤 + 𝐴))
3938oveq1d 7447 . . . . . 6 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → ((𝐴 + (((invg𝐺)‘𝐴) + (𝑤 + 𝐴))) 𝐴) = ((𝑤 + 𝐴) 𝐴))
40 conjghm.m . . . . . . . 8 = (-g𝐺)
411, 2, 40grppncan 19050 . . . . . . 7 ((𝐺 ∈ Grp ∧ 𝑤𝑋𝐴𝑋) → ((𝑤 + 𝐴) 𝐴) = 𝑤)
424, 13, 9, 41syl3anc 1372 . . . . . 6 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → ((𝑤 + 𝐴) 𝐴) = 𝑤)
4333, 39, 423eqtrd 2780 . . . . 5 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → (𝐹‘(((invg𝐺)‘𝐴) + (𝑤 + 𝐴))) = 𝑤)
44 ovex 7465 . . . . . . 7 ((𝐴 + 𝑥) 𝐴) ∈ V
4544, 30fnmpti 6710 . . . . . 6 𝐹 Fn 𝑆
46 fnfvelrn 7099 . . . . . 6 ((𝐹 Fn 𝑆 ∧ (((invg𝐺)‘𝐴) + (𝑤 + 𝐴)) ∈ 𝑆) → (𝐹‘(((invg𝐺)‘𝐴) + (𝑤 + 𝐴))) ∈ ran 𝐹)
4745, 27, 46sylancr 587 . . . . 5 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → (𝐹‘(((invg𝐺)‘𝐴) + (𝑤 + 𝐴))) ∈ ran 𝐹)
4843, 47eqeltrrd 2841 . . . 4 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑤𝑆) → 𝑤 ∈ ran 𝐹)
4948ex 412 . . 3 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) → (𝑤𝑆𝑤 ∈ ran 𝐹))
5049ssrdv 3988 . 2 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) → 𝑆 ⊆ ran 𝐹)
513ad2antrr 726 . . . . . 6 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑥𝑆) → 𝐺 ∈ Grp)
52 simplr 768 . . . . . . 7 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑥𝑆) → 𝐴𝑁)
537, 52sselid 3980 . . . . . 6 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑥𝑆) → 𝐴𝑋)
5412sselda 3982 . . . . . 6 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑥𝑆) → 𝑥𝑋)
551, 2, 40grpaddsubass 19049 . . . . . 6 ((𝐺 ∈ Grp ∧ (𝐴𝑋𝑥𝑋𝐴𝑋)) → ((𝐴 + 𝑥) 𝐴) = (𝐴 + (𝑥 𝐴)))
5651, 53, 54, 53, 55syl13anc 1373 . . . . 5 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑥𝑆) → ((𝐴 + 𝑥) 𝐴) = (𝐴 + (𝑥 𝐴)))
571, 2, 40grpnpcan 19051 . . . . . . . 8 ((𝐺 ∈ Grp ∧ 𝑥𝑋𝐴𝑋) → ((𝑥 𝐴) + 𝐴) = 𝑥)
5851, 54, 53, 57syl3anc 1372 . . . . . . 7 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑥𝑆) → ((𝑥 𝐴) + 𝐴) = 𝑥)
59 simpr 484 . . . . . . 7 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑥𝑆) → 𝑥𝑆)
6058, 59eqeltrd 2840 . . . . . 6 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑥𝑆) → ((𝑥 𝐴) + 𝐴) ∈ 𝑆)
611, 40grpsubcl 19039 . . . . . . . 8 ((𝐺 ∈ Grp ∧ 𝑥𝑋𝐴𝑋) → (𝑥 𝐴) ∈ 𝑋)
6251, 54, 53, 61syl3anc 1372 . . . . . . 7 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑥𝑆) → (𝑥 𝐴) ∈ 𝑋)
636nmzbi 19183 . . . . . . 7 ((𝐴𝑁 ∧ (𝑥 𝐴) ∈ 𝑋) → ((𝐴 + (𝑥 𝐴)) ∈ 𝑆 ↔ ((𝑥 𝐴) + 𝐴) ∈ 𝑆))
6452, 62, 63syl2anc 584 . . . . . 6 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑥𝑆) → ((𝐴 + (𝑥 𝐴)) ∈ 𝑆 ↔ ((𝑥 𝐴) + 𝐴) ∈ 𝑆))
6560, 64mpbird 257 . . . . 5 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑥𝑆) → (𝐴 + (𝑥 𝐴)) ∈ 𝑆)
6656, 65eqeltrd 2840 . . . 4 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) ∧ 𝑥𝑆) → ((𝐴 + 𝑥) 𝐴) ∈ 𝑆)
6766, 30fmptd 7133 . . 3 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) → 𝐹:𝑆𝑆)
6867frnd 6743 . 2 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) → ran 𝐹𝑆)
6950, 68eqssd 4000 1 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑁) → 𝑆 = ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1539  wcel 2107  wral 3060  {crab 3435  wss 3950  cmpt 5224  ran crn 5685   Fn wfn 6555  cfv 6560  (class class class)co 7432  Basecbs 17248  +gcplusg 17298  0gc0g 17485  Grpcgrp 18952  invgcminusg 18953  -gcsg 18954  SubGrpcsubg 19139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-fv 6568  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-1st 8015  df-2nd 8016  df-0g 17487  df-mgm 18654  df-sgrp 18733  df-mnd 18749  df-grp 18955  df-minusg 18956  df-sbg 18957  df-subg 19142
This theorem is referenced by:  conjnmzb  19272  conjnsg  19273  sylow3lem2  19647
  Copyright terms: Public domain W3C validator