# Metamath Proof Explorer

## Theorem conjnmz

Description: A subgroup is unchanged under conjugation by an element of its normalizer. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypotheses conjghm.x ${⊢}{X}={\mathrm{Base}}_{{G}}$
conjghm.p
conjghm.m
conjsubg.f
conjnmz.1
Assertion conjnmz ${⊢}\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {A}\in {N}\right)\to {S}=\mathrm{ran}{F}$

### Proof

Step Hyp Ref Expression
1 conjghm.x ${⊢}{X}={\mathrm{Base}}_{{G}}$
2 conjghm.p
3 conjghm.m
4 conjsubg.f
5 conjnmz.1
6 subgrcl ${⊢}{S}\in \mathrm{SubGrp}\left({G}\right)\to {G}\in \mathrm{Grp}$
7 6 ad2antrr ${⊢}\left(\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {A}\in {N}\right)\wedge {w}\in {S}\right)\to {G}\in \mathrm{Grp}$
8 5 ssrab3 ${⊢}{N}\subseteq {X}$
9 simplr ${⊢}\left(\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {A}\in {N}\right)\wedge {w}\in {S}\right)\to {A}\in {N}$
10 8 9 sseldi ${⊢}\left(\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {A}\in {N}\right)\wedge {w}\in {S}\right)\to {A}\in {X}$
11 eqid ${⊢}{inv}_{g}\left({G}\right)={inv}_{g}\left({G}\right)$
12 1 11 grpinvcl ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\right)\to {inv}_{g}\left({G}\right)\left({A}\right)\in {X}$
13 7 10 12 syl2anc ${⊢}\left(\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {A}\in {N}\right)\wedge {w}\in {S}\right)\to {inv}_{g}\left({G}\right)\left({A}\right)\in {X}$
14 1 subgss ${⊢}{S}\in \mathrm{SubGrp}\left({G}\right)\to {S}\subseteq {X}$
15 14 adantr ${⊢}\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {A}\in {N}\right)\to {S}\subseteq {X}$
16 15 sselda ${⊢}\left(\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {A}\in {N}\right)\wedge {w}\in {S}\right)\to {w}\in {X}$
17 1 2 grpass
18 7 13 16 10 17 syl13anc
19 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
20 1 2 19 11 grprinv
21 7 10 20 syl2anc
22 21 oveq1d
23 1 2 grpass
24 7 10 13 16 23 syl13anc
25 1 2 19 grplid
26 7 16 25 syl2anc
27 22 24 26 3eqtr3d
28 simpr ${⊢}\left(\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {A}\in {N}\right)\wedge {w}\in {S}\right)\to {w}\in {S}$
29 27 28 eqeltrd
30 1 2 grpcl
31 7 13 16 30 syl3anc
32 5 nmzbi
33 9 31 32 syl2anc
34 29 33 mpbid
35 18 34 eqeltrrd
36 oveq2
37 36 oveq1d
38 ovex
39 37 4 38 fvmpt
40 35 39 syl
41 21 oveq1d
42 1 2 grpcl
43 7 16 10 42 syl3anc
44 1 2 grpass
45 7 10 13 43 44 syl13anc
46 1 2 19 grplid
47 7 43 46 syl2anc
48 41 45 47 3eqtr3d
49 48 oveq1d
50 1 2 3 grppncan
51 7 16 10 50 syl3anc
52 40 49 51 3eqtrd
53 ovex
54 53 4 fnmpti ${⊢}{F}Fn{S}$
55 fnfvelrn
56 54 35 55 sylancr
57 52 56 eqeltrrd ${⊢}\left(\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {A}\in {N}\right)\wedge {w}\in {S}\right)\to {w}\in \mathrm{ran}{F}$
58 57 ex ${⊢}\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {A}\in {N}\right)\to \left({w}\in {S}\to {w}\in \mathrm{ran}{F}\right)$
59 58 ssrdv ${⊢}\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {A}\in {N}\right)\to {S}\subseteq \mathrm{ran}{F}$
60 6 ad2antrr ${⊢}\left(\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {A}\in {N}\right)\wedge {x}\in {S}\right)\to {G}\in \mathrm{Grp}$
61 simplr ${⊢}\left(\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {A}\in {N}\right)\wedge {x}\in {S}\right)\to {A}\in {N}$
62 8 61 sseldi ${⊢}\left(\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {A}\in {N}\right)\wedge {x}\in {S}\right)\to {A}\in {X}$
63 15 sselda ${⊢}\left(\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {A}\in {N}\right)\wedge {x}\in {S}\right)\to {x}\in {X}$
65 60 62 63 62 64 syl13anc
66 1 2 3 grpnpcan
67 60 63 62 66 syl3anc
68 simpr ${⊢}\left(\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {A}\in {N}\right)\wedge {x}\in {S}\right)\to {x}\in {S}$
69 67 68 eqeltrd
70 1 3 grpsubcl
71 60 63 62 70 syl3anc
72 5 nmzbi
73 61 71 72 syl2anc
74 69 73 mpbird
75 65 74 eqeltrd
76 75 4 fmptd ${⊢}\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {A}\in {N}\right)\to {F}:{S}⟶{S}$
77 76 frnd ${⊢}\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {A}\in {N}\right)\to \mathrm{ran}{F}\subseteq {S}$
78 59 77 eqssd ${⊢}\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {A}\in {N}\right)\to {S}=\mathrm{ran}{F}$