Metamath Proof Explorer

Theorem nmzsubg

Description: The normalizer N_G(S) of a subset S of the group is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypotheses elnmz.1 ⊢ 𝑁 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) }
nmzsubg.2 ⊢ 𝑋 = ( Base ‘ 𝐺 )
nmzsubg.3 ⊢ + = ( +g ‘ 𝐺 )
Assertion nmzsubg ( 𝐺 ∈ Grp → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 elnmz.1 ⊢ 𝑁 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) }
2 nmzsubg.2 ⊢ 𝑋 = ( Base ‘ 𝐺 )
3 nmzsubg.3 ⊢ + = ( +g ‘ 𝐺 )
4 1 ssrab3 ⊢ 𝑁 ⊆ 𝑋
5 4 a1i ⊢ ( 𝐺 ∈ Grp → 𝑁 ⊆ 𝑋 )
6 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
7 2 6 grpidcl ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
8 2 3 6 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) + 𝑧 ) = 𝑧 )
9 2 3 6 grprid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 + ( 0g ‘ 𝐺 ) ) = 𝑧 )
10 8 9 eqtr4d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) + 𝑧 ) = ( 𝑧 + ( 0g ‘ 𝐺 ) ) )
11 10 eleq1d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ) → ( ( ( 0g ‘ 𝐺 ) + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + ( 0g ‘ 𝐺 ) ) ∈ 𝑆 ) )
12 11 ralrimiva ⊢ ( 𝐺 ∈ Grp → ∀ 𝑧 ∈ 𝑋 ( ( ( 0g ‘ 𝐺 ) + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + ( 0g ‘ 𝐺 ) ) ∈ 𝑆 ) )
13 1 elnmz ⊢ ( ( 0g ‘ 𝐺 ) ∈ 𝑁 ↔ ( ( 0g ‘ 𝐺 ) ∈ 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ( ( ( 0g ‘ 𝐺 ) + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + ( 0g ‘ 𝐺 ) ) ∈ 𝑆 ) ) )
14 7 12 13 sylanbrc ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝑁 )
15 14 ne0d ⊢ ( 𝐺 ∈ Grp → 𝑁 ≠ ∅ )
16 id ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Grp )
17 4 sseli ⊢ ( 𝑧 ∈ 𝑁 → 𝑧 ∈ 𝑋 )
18 4 sseli ⊢ ( 𝑤 ∈ 𝑁 → 𝑤 ∈ 𝑋 )
19 2 3 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑧 + 𝑤 ) ∈ 𝑋 )
20 16 17 18 19 syl3an ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) → ( 𝑧 + 𝑤 ) ∈ 𝑋 )
21 simpl1 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → 𝐺 ∈ Grp )
22 simpl2 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → 𝑧 ∈ 𝑁 )
23 4 22 sseldi ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → 𝑧 ∈ 𝑋 )
24 simpl3 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → 𝑤 ∈ 𝑁 )
25 4 24 sseldi ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → 𝑤 ∈ 𝑋 )
26 simpr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → 𝑢 ∈ 𝑋 )
27 2 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ) ) → ( ( 𝑧 + 𝑤 ) + 𝑢 ) = ( 𝑧 + ( 𝑤 + 𝑢 ) ) )
28 21 23 25 26 27 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑧 + 𝑤 ) + 𝑢 ) = ( 𝑧 + ( 𝑤 + 𝑢 ) ) )
29 28 eleq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( 𝑧 + 𝑤 ) + 𝑢 ) ∈ 𝑆 ↔ ( 𝑧 + ( 𝑤 + 𝑢 ) ) ∈ 𝑆 ) )
30 2 3 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ) → ( 𝑤 + 𝑢 ) ∈ 𝑋 )
31 21 25 26 30 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( 𝑤 + 𝑢 ) ∈ 𝑋 )
32 1 nmzbi ⊢ ( ( 𝑧 ∈ 𝑁 ∧ ( 𝑤 + 𝑢 ) ∈ 𝑋 ) → ( ( 𝑧 + ( 𝑤 + 𝑢 ) ) ∈ 𝑆 ↔ ( ( 𝑤 + 𝑢 ) + 𝑧 ) ∈ 𝑆 ) )
33 22 31 32 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑧 + ( 𝑤 + 𝑢 ) ) ∈ 𝑆 ↔ ( ( 𝑤 + 𝑢 ) + 𝑧 ) ∈ 𝑆 ) )
34 2 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑤 + 𝑢 ) + 𝑧 ) = ( 𝑤 + ( 𝑢 + 𝑧 ) ) )
35 21 25 26 23 34 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑤 + 𝑢 ) + 𝑧 ) = ( 𝑤 + ( 𝑢 + 𝑧 ) ) )
36 35 eleq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( 𝑤 + 𝑢 ) + 𝑧 ) ∈ 𝑆 ↔ ( 𝑤 + ( 𝑢 + 𝑧 ) ) ∈ 𝑆 ) )
37 2 3 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑢 + 𝑧 ) ∈ 𝑋 )
38 21 26 23 37 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( 𝑢 + 𝑧 ) ∈ 𝑋 )
39 1 nmzbi ⊢ ( ( 𝑤 ∈ 𝑁 ∧ ( 𝑢 + 𝑧 ) ∈ 𝑋 ) → ( ( 𝑤 + ( 𝑢 + 𝑧 ) ) ∈ 𝑆 ↔ ( ( 𝑢 + 𝑧 ) + 𝑤 ) ∈ 𝑆 ) )
40 24 38 39 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑤 + ( 𝑢 + 𝑧 ) ) ∈ 𝑆 ↔ ( ( 𝑢 + 𝑧 ) + 𝑤 ) ∈ 𝑆 ) )
41 33 36 40 3bitrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑧 + ( 𝑤 + 𝑢 ) ) ∈ 𝑆 ↔ ( ( 𝑢 + 𝑧 ) + 𝑤 ) ∈ 𝑆 ) )
42 2 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝑢 + 𝑧 ) + 𝑤 ) = ( 𝑢 + ( 𝑧 + 𝑤 ) ) )
43 21 26 23 25 42 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑢 + 𝑧 ) + 𝑤 ) = ( 𝑢 + ( 𝑧 + 𝑤 ) ) )
44 43 eleq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( 𝑢 + 𝑧 ) + 𝑤 ) ∈ 𝑆 ↔ ( 𝑢 + ( 𝑧 + 𝑤 ) ) ∈ 𝑆 ) )
45 29 41 44 3bitrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( 𝑧 + 𝑤 ) + 𝑢 ) ∈ 𝑆 ↔ ( 𝑢 + ( 𝑧 + 𝑤 ) ) ∈ 𝑆 ) )
46 45 ralrimiva ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) → ∀ 𝑢 ∈ 𝑋 ( ( ( 𝑧 + 𝑤 ) + 𝑢 ) ∈ 𝑆 ↔ ( 𝑢 + ( 𝑧 + 𝑤 ) ) ∈ 𝑆 ) )
47 1 elnmz ⊢ ( ( 𝑧 + 𝑤 ) ∈ 𝑁 ↔ ( ( 𝑧 + 𝑤 ) ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑋 ( ( ( 𝑧 + 𝑤 ) + 𝑢 ) ∈ 𝑆 ↔ ( 𝑢 + ( 𝑧 + 𝑤 ) ) ∈ 𝑆 ) ) )
48 20 46 47 sylanbrc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) → ( 𝑧 + 𝑤 ) ∈ 𝑁 )
49 48 3expa ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑁 ) → ( 𝑧 + 𝑤 ) ∈ 𝑁 )
50 49 ralrimiva ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) → ∀ 𝑤 ∈ 𝑁 ( 𝑧 + 𝑤 ) ∈ 𝑁 )
51 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
52 2 51 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 )
53 17 52 sylan2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 )
54 simplr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → 𝑧 ∈ 𝑁 )
55 simpll ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → 𝐺 ∈ Grp )
56 53 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 )
57 simpr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → 𝑢 ∈ 𝑋 )
58 2 3 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 ) → ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑋 )
59 55 57 56 58 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑋 )
60 2 3 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 ∧ ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) ∈ 𝑋 )
61 55 56 59 60 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) ∈ 𝑋 )
62 1 nmzbi ⊢ ( ( 𝑧 ∈ 𝑁 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) ∈ 𝑋 ) → ( ( 𝑧 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) ) ∈ 𝑆 ↔ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) + 𝑧 ) ∈ 𝑆 ) )
63 54 61 62 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑧 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) ) ∈ 𝑆 ↔ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) + 𝑧 ) ∈ 𝑆 ) )
64 4 54 sseldi ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → 𝑧 ∈ 𝑋 )
65 2 3 6 51 grprinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) = ( 0g ‘ 𝐺 ) )
66 55 64 65 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( 𝑧 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) = ( 0g ‘ 𝐺 ) )
67 66 oveq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑧 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) = ( ( 0g ‘ 𝐺 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) )
68 2 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑧 ∈ 𝑋 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 ∧ ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑋 ) ) → ( ( 𝑧 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) = ( 𝑧 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) ) )
69 55 64 56 59 68 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑧 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) = ( 𝑧 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) ) )
70 2 3 6 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) = ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) )
71 55 59 70 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) = ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) )
72 67 69 71 3eqtr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( 𝑧 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) ) = ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) )
73 72 eleq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑧 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) ) ∈ 𝑆 ↔ ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑆 ) )
74 2 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 ∧ ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) + 𝑧 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) + 𝑧 ) ) )
75 55 56 59 64 74 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) + 𝑧 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) + 𝑧 ) ) )
76 2 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑢 ∈ 𝑋 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) + 𝑧 ) = ( 𝑢 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑧 ) ) )
77 55 57 56 64 76 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) + 𝑧 ) = ( 𝑢 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑧 ) ) )
78 2 3 6 51 grplinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑧 ) = ( 0g ‘ 𝐺 ) )
79 55 64 78 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑧 ) = ( 0g ‘ 𝐺 ) )
80 79 oveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( 𝑢 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑧 ) ) = ( 𝑢 + ( 0g ‘ 𝐺 ) ) )
81 2 3 6 grprid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ) → ( 𝑢 + ( 0g ‘ 𝐺 ) ) = 𝑢 )
82 55 57 81 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( 𝑢 + ( 0g ‘ 𝐺 ) ) = 𝑢 )
83 77 80 82 3eqtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) + 𝑧 ) = 𝑢 )
84 83 oveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) + 𝑧 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑢 ) )
85 75 84 eqtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) + 𝑧 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑢 ) )
86 85 eleq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) + 𝑧 ) ∈ 𝑆 ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑢 ) ∈ 𝑆 ) )
87 63 73 86 3bitr3rd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑢 ) ∈ 𝑆 ↔ ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑆 ) )
88 87 ralrimiva ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) → ∀ 𝑢 ∈ 𝑋 ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑢 ) ∈ 𝑆 ↔ ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑆 ) )
89 1 elnmz ⊢ ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑁 ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑋 ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑢 ) ∈ 𝑆 ↔ ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑆 ) ) )
90 53 88 89 sylanbrc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑁 )
91 50 90 jca ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) → ( ∀ 𝑤 ∈ 𝑁 ( 𝑧 + 𝑤 ) ∈ 𝑁 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑁 ) )
92 91 ralrimiva ⊢ ( 𝐺 ∈ Grp → ∀ 𝑧 ∈ 𝑁 ( ∀ 𝑤 ∈ 𝑁 ( 𝑧 + 𝑤 ) ∈ 𝑁 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑁 ) )
93 2 3 51 issubg2 ⊢ ( 𝐺 ∈ Grp → ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑁 ⊆ 𝑋 ∧ 𝑁 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑁 ( ∀ 𝑤 ∈ 𝑁 ( 𝑧 + 𝑤 ) ∈ 𝑁 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑁 ) ) ) )
94 5 15 92 93 mpbir3and ⊢ ( 𝐺 ∈ Grp → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )