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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
conjghm.p ⊢ + = ( +g ‘ 𝐺 )
conjghm.m ⊢ − = ( -g ‘ 𝐺 )
conjsubg.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) )
conjnmz.1 ⊢ 𝑁 = { 𝑦 ∈ 𝑋 ∣ ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑦 ) ∈ 𝑆 ) }
Assertion conjnmz ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) → 𝑆 = ran 𝐹 )

Proof

Step Hyp Ref Expression
1 conjghm.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 conjghm.p ⊢ + = ( +g ‘ 𝐺 )
3 conjghm.m ⊢ − = ( -g ‘ 𝐺 )
4 conjsubg.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) )
5 conjnmz.1 ⊢ 𝑁 = { 𝑦 ∈ 𝑋 ∣ ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑦 ) ∈ 𝑆 ) }
6 subgrcl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
7 6 ad2antrr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → 𝐺 ∈ Grp )
8 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
9 5 ssrab3 ⊢ 𝑁 ⊆ 𝑋
10 simplr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → 𝐴 ∈ 𝑁 )
11 9 10 sselid ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → 𝐴 ∈ 𝑋 )
12 1 8 7 11 grpinvcld ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 )
13 1 subgss ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ 𝑋 )
14 13 adantr ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) → 𝑆 ⊆ 𝑋 )
15 14 sselda ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → 𝑤 ∈ 𝑋 )
16 1 2 7 12 15 11 grpassd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) + 𝐴 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) )
17 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
18 1 2 17 8 7 11 grprinvd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝐴 + ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) = ( 0g ‘ 𝐺 ) )
19 18 oveq1d ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝐴 + ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) + 𝑤 ) = ( ( 0g ‘ 𝐺 ) + 𝑤 ) )
20 1 2 7 11 12 15 grpassd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝐴 + ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) + 𝑤 ) = ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) ) )
21 1 2 17 7 15 grplidd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 0g ‘ 𝐺 ) + 𝑤 ) = 𝑤 )
22 19 20 21 3eqtr3d ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) ) = 𝑤 )
23 simpr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → 𝑤 ∈ 𝑆 )
24 22 23 eqeltrd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) ) ∈ 𝑆 )
25 1 2 7 12 15 grpcld ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) ∈ 𝑋 )
26 5 nmzbi ⊢ ( ( 𝐴 ∈ 𝑁 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) ∈ 𝑋 ) → ( ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) ) ∈ 𝑆 ↔ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) + 𝐴 ) ∈ 𝑆 ) )
27 10 25 26 syl2anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) ) ∈ 𝑆 ↔ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) + 𝐴 ) ∈ 𝑆 ) )
28 24 27 mpbid ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) + 𝐴 ) ∈ 𝑆 )
29 16 28 eqeltrrd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ∈ 𝑆 )
30 oveq2 ⊢ ( 𝑥 = ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) → ( 𝐴 + 𝑥 ) = ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) )
31 30 oveq1d ⊢ ( 𝑥 = ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) → ( ( 𝐴 + 𝑥 ) − 𝐴 ) = ( ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) − 𝐴 ) )
32 ovex ⊢ ( ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) − 𝐴 ) ∈ V
33 31 4 32 fvmpt ⊢ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ∈ 𝑆 → ( 𝐹 ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) = ( ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) − 𝐴 ) )
34 29 33 syl ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝐹 ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) = ( ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) − 𝐴 ) )
35 18 oveq1d ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝐴 + ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) + ( 𝑤 + 𝐴 ) ) = ( ( 0g ‘ 𝐺 ) + ( 𝑤 + 𝐴 ) ) )
36 1 2 7 15 11 grpcld ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝑤 + 𝐴 ) ∈ 𝑋 )
37 1 2 7 11 12 36 grpassd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝐴 + ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) + ( 𝑤 + 𝐴 ) ) = ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) )
38 1 2 17 7 36 grplidd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 0g ‘ 𝐺 ) + ( 𝑤 + 𝐴 ) ) = ( 𝑤 + 𝐴 ) )
39 35 37 38 3eqtr3d ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) = ( 𝑤 + 𝐴 ) )
40 39 oveq1d ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) − 𝐴 ) = ( ( 𝑤 + 𝐴 ) − 𝐴 ) )
41 1 2 3 grppncan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑤 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑤 + 𝐴 ) − 𝐴 ) = 𝑤 )
42 7 15 11 41 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝑤 + 𝐴 ) − 𝐴 ) = 𝑤 )
43 34 40 42 3eqtrd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝐹 ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) = 𝑤 )
44 ovex ⊢ ( ( 𝐴 + 𝑥 ) − 𝐴 ) ∈ V
45 44 4 fnmpti ⊢ 𝐹 Fn 𝑆
46 fnfvelrn ⊢ ( ( 𝐹 Fn 𝑆 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ∈ 𝑆 ) → ( 𝐹 ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) ∈ ran 𝐹 )
47 45 29 46 sylancr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝐹 ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) ∈ ran 𝐹 )
48 43 47 eqeltrrd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → 𝑤 ∈ ran 𝐹 )
49 48 ex ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) → ( 𝑤 ∈ 𝑆 → 𝑤 ∈ ran 𝐹 ) )
50 49 ssrdv ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) → 𝑆 ⊆ ran 𝐹 )
51 6 ad2antrr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → 𝐺 ∈ Grp )
52 simplr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ 𝑁 )
53 9 52 sselid ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ 𝑋 )
54 14 sselda ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑋 )
55 1 2 3 grpaddsubass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝐴 + 𝑥 ) − 𝐴 ) = ( 𝐴 + ( 𝑥 − 𝐴 ) ) )
56 51 53 54 53 55 syl13anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐴 + 𝑥 ) − 𝐴 ) = ( 𝐴 + ( 𝑥 − 𝐴 ) ) )
57 1 2 3 grpnpcan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑥 − 𝐴 ) + 𝐴 ) = 𝑥 )
58 51 54 53 57 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑥 − 𝐴 ) + 𝐴 ) = 𝑥 )
59 simpr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
60 58 59 eqeltrd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑥 − 𝐴 ) + 𝐴 ) ∈ 𝑆 )
61 1 3 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑥 − 𝐴 ) ∈ 𝑋 )
62 51 54 53 61 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 − 𝐴 ) ∈ 𝑋 )
63 5 nmzbi ⊢ ( ( 𝐴 ∈ 𝑁 ∧ ( 𝑥 − 𝐴 ) ∈ 𝑋 ) → ( ( 𝐴 + ( 𝑥 − 𝐴 ) ) ∈ 𝑆 ↔ ( ( 𝑥 − 𝐴 ) + 𝐴 ) ∈ 𝑆 ) )
64 52 62 63 syl2anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐴 + ( 𝑥 − 𝐴 ) ) ∈ 𝑆 ↔ ( ( 𝑥 − 𝐴 ) + 𝐴 ) ∈ 𝑆 ) )
65 60 64 mpbird ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐴 + ( 𝑥 − 𝐴 ) ) ∈ 𝑆 )
66 56 65 eqeltrd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐴 + 𝑥 ) − 𝐴 ) ∈ 𝑆 )
67 66 4 fmptd ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) → 𝐹 : 𝑆 ⟶ 𝑆 )
68 67 frnd ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) → ran 𝐹 ⊆ 𝑆 )
69 50 68 eqssd ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) → 𝑆 = ran 𝐹 )