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 5 ssrab3 ⊢ 𝑁 ⊆ 𝑋
9 simplr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → 𝐴 ∈ 𝑁 )
10 8 9 sselid ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → 𝐴 ∈ 𝑋 )
11 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
12 1 11 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 )
13 7 10 12 syl2anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 )
14 1 subgss ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ 𝑋 )
15 14 adantr ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) → 𝑆 ⊆ 𝑋 )
16 15 sselda ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → 𝑤 ∈ 𝑋 )
17 1 2 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) + 𝐴 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) )
18 7 13 16 10 17 syl13anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) + 𝐴 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) )
19 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
20 1 2 19 11 grprinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 + ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) = ( 0g ‘ 𝐺 ) )
21 7 10 20 syl2anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝐴 + ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) = ( 0g ‘ 𝐺 ) )
22 21 oveq1d ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝐴 + ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) + 𝑤 ) = ( ( 0g ‘ 𝐺 ) + 𝑤 ) )
23 1 2 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝐴 ∈ 𝑋 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝐴 + ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) + 𝑤 ) = ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) ) )
24 7 10 13 16 23 syl13anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝐴 + ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) + 𝑤 ) = ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) ) )
25 1 2 19 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑤 ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) + 𝑤 ) = 𝑤 )
26 7 16 25 syl2anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 0g ‘ 𝐺 ) + 𝑤 ) = 𝑤 )
27 22 24 26 3eqtr3d ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) ) = 𝑤 )
28 simpr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → 𝑤 ∈ 𝑆 )
29 27 28 eqeltrd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) ) ∈ 𝑆 )
30 1 2 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) ∈ 𝑋 )
31 7 13 16 30 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) ∈ 𝑋 )
32 5 nmzbi ⊢ ( ( 𝐴 ∈ 𝑁 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) ∈ 𝑋 ) → ( ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) ) ∈ 𝑆 ↔ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) + 𝐴 ) ∈ 𝑆 ) )
33 9 31 32 syl2anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) ) ∈ 𝑆 ↔ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) + 𝐴 ) ∈ 𝑆 ) )
34 29 33 mpbid ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑤 ) + 𝐴 ) ∈ 𝑆 )
35 18 34 eqeltrrd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ∈ 𝑆 )
36 oveq2 ⊢ ( 𝑥 = ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) → ( 𝐴 + 𝑥 ) = ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) )
37 36 oveq1d ⊢ ( 𝑥 = ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) → ( ( 𝐴 + 𝑥 ) − 𝐴 ) = ( ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) − 𝐴 ) )
38 ovex ⊢ ( ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) − 𝐴 ) ∈ V
39 37 4 38 fvmpt ⊢ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ∈ 𝑆 → ( 𝐹 ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) = ( ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) − 𝐴 ) )
40 35 39 syl ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝐹 ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) = ( ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) − 𝐴 ) )
41 21 oveq1d ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝐴 + ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) + ( 𝑤 + 𝐴 ) ) = ( ( 0g ‘ 𝐺 ) + ( 𝑤 + 𝐴 ) ) )
42 1 2 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑤 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑤 + 𝐴 ) ∈ 𝑋 )
43 7 16 10 42 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝑤 + 𝐴 ) ∈ 𝑋 )
44 1 2 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝐴 ∈ 𝑋 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 ∧ ( 𝑤 + 𝐴 ) ∈ 𝑋 ) ) → ( ( 𝐴 + ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) + ( 𝑤 + 𝐴 ) ) = ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) )
45 7 10 13 43 44 syl13anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝐴 + ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) + ( 𝑤 + 𝐴 ) ) = ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) )
46 1 2 19 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑤 + 𝐴 ) ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) + ( 𝑤 + 𝐴 ) ) = ( 𝑤 + 𝐴 ) )
47 7 43 46 syl2anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 0g ‘ 𝐺 ) + ( 𝑤 + 𝐴 ) ) = ( 𝑤 + 𝐴 ) )
48 41 45 47 3eqtr3d ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) = ( 𝑤 + 𝐴 ) )
49 48 oveq1d ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝐴 + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) − 𝐴 ) = ( ( 𝑤 + 𝐴 ) − 𝐴 ) )
50 1 2 3 grppncan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑤 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑤 + 𝐴 ) − 𝐴 ) = 𝑤 )
51 7 16 10 50 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝑤 + 𝐴 ) − 𝐴 ) = 𝑤 )
52 40 49 51 3eqtrd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝐹 ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) = 𝑤 )
53 ovex ⊢ ( ( 𝐴 + 𝑥 ) − 𝐴 ) ∈ V
54 53 4 fnmpti ⊢ 𝐹 Fn 𝑆
55 fnfvelrn ⊢ ( ( 𝐹 Fn 𝑆 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ∈ 𝑆 ) → ( 𝐹 ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) ∈ ran 𝐹 )
56 54 35 55 sylancr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝐹 ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝑤 + 𝐴 ) ) ) ∈ ran 𝐹 )
57 52 56 eqeltrrd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑆 ) → 𝑤 ∈ ran 𝐹 )
58 57 ex ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) → ( 𝑤 ∈ 𝑆 → 𝑤 ∈ ran 𝐹 ) )
59 58 ssrdv ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) → 𝑆 ⊆ ran 𝐹 )
60 6 ad2antrr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → 𝐺 ∈ Grp )
61 simplr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ 𝑁 )
62 8 61 sselid ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ 𝑋 )
63 15 sselda ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑋 )
64 1 2 3 grpaddsubass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝐴 + 𝑥 ) − 𝐴 ) = ( 𝐴 + ( 𝑥 − 𝐴 ) ) )
65 60 62 63 62 64 syl13anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐴 + 𝑥 ) − 𝐴 ) = ( 𝐴 + ( 𝑥 − 𝐴 ) ) )
66 1 2 3 grpnpcan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑥 − 𝐴 ) + 𝐴 ) = 𝑥 )
67 60 63 62 66 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑥 − 𝐴 ) + 𝐴 ) = 𝑥 )
68 simpr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
69 67 68 eqeltrd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑥 − 𝐴 ) + 𝐴 ) ∈ 𝑆 )
70 1 3 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑥 − 𝐴 ) ∈ 𝑋 )
71 60 63 62 70 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 − 𝐴 ) ∈ 𝑋 )
72 5 nmzbi ⊢ ( ( 𝐴 ∈ 𝑁 ∧ ( 𝑥 − 𝐴 ) ∈ 𝑋 ) → ( ( 𝐴 + ( 𝑥 − 𝐴 ) ) ∈ 𝑆 ↔ ( ( 𝑥 − 𝐴 ) + 𝐴 ) ∈ 𝑆 ) )
73 61 71 72 syl2anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐴 + ( 𝑥 − 𝐴 ) ) ∈ 𝑆 ↔ ( ( 𝑥 − 𝐴 ) + 𝐴 ) ∈ 𝑆 ) )
74 69 73 mpbird ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐴 + ( 𝑥 − 𝐴 ) ) ∈ 𝑆 )
75 65 74 eqeltrd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐴 + 𝑥 ) − 𝐴 ) ∈ 𝑆 )
76 75 4 fmptd ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) → 𝐹 : 𝑆 ⟶ 𝑆 )
77 76 frnd ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) → ran 𝐹 ⊆ 𝑆 )
78 59 77 eqssd ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) → 𝑆 = ran 𝐹 )