This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 sselid ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → 𝑧 ∈ 𝑋 )
24 simpl3 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → 𝑤 ∈ 𝑁 )
25 4 24 sselid ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → 𝑤 ∈ 𝑋 )
26 simpr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → 𝑢 ∈ 𝑋 )
27 2 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ) ) → ( ( 𝑧 + 𝑤 ) + 𝑢 ) = ( 𝑧 + ( 𝑤 + 𝑢 ) ) )
28 21 23 25 26 27 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑧 + 𝑤 ) + 𝑢 ) = ( 𝑧 + ( 𝑤 + 𝑢 ) ) )
29 28 eleq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( 𝑧 + 𝑤 ) + 𝑢 ) ∈ 𝑆 ↔ ( 𝑧 + ( 𝑤 + 𝑢 ) ) ∈ 𝑆 ) )
30 2 3 21 25 26 grpcld ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( 𝑤 + 𝑢 ) ∈ 𝑋 )
31 1 nmzbi ⊢ ( ( 𝑧 ∈ 𝑁 ∧ ( 𝑤 + 𝑢 ) ∈ 𝑋 ) → ( ( 𝑧 + ( 𝑤 + 𝑢 ) ) ∈ 𝑆 ↔ ( ( 𝑤 + 𝑢 ) + 𝑧 ) ∈ 𝑆 ) )
32 22 30 31 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑧 + ( 𝑤 + 𝑢 ) ) ∈ 𝑆 ↔ ( ( 𝑤 + 𝑢 ) + 𝑧 ) ∈ 𝑆 ) )
33 2 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑤 + 𝑢 ) + 𝑧 ) = ( 𝑤 + ( 𝑢 + 𝑧 ) ) )
34 21 25 26 23 33 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑤 + 𝑢 ) + 𝑧 ) = ( 𝑤 + ( 𝑢 + 𝑧 ) ) )
35 34 eleq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( 𝑤 + 𝑢 ) + 𝑧 ) ∈ 𝑆 ↔ ( 𝑤 + ( 𝑢 + 𝑧 ) ) ∈ 𝑆 ) )
36 2 3 21 26 23 grpcld ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( 𝑢 + 𝑧 ) ∈ 𝑋 )
37 1 nmzbi ⊢ ( ( 𝑤 ∈ 𝑁 ∧ ( 𝑢 + 𝑧 ) ∈ 𝑋 ) → ( ( 𝑤 + ( 𝑢 + 𝑧 ) ) ∈ 𝑆 ↔ ( ( 𝑢 + 𝑧 ) + 𝑤 ) ∈ 𝑆 ) )
38 24 36 37 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑤 + ( 𝑢 + 𝑧 ) ) ∈ 𝑆 ↔ ( ( 𝑢 + 𝑧 ) + 𝑤 ) ∈ 𝑆 ) )
39 32 35 38 3bitrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑧 + ( 𝑤 + 𝑢 ) ) ∈ 𝑆 ↔ ( ( 𝑢 + 𝑧 ) + 𝑤 ) ∈ 𝑆 ) )
40 2 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝑢 + 𝑧 ) + 𝑤 ) = ( 𝑢 + ( 𝑧 + 𝑤 ) ) )
41 21 26 23 25 40 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑢 + 𝑧 ) + 𝑤 ) = ( 𝑢 + ( 𝑧 + 𝑤 ) ) )
42 41 eleq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( 𝑢 + 𝑧 ) + 𝑤 ) ∈ 𝑆 ↔ ( 𝑢 + ( 𝑧 + 𝑤 ) ) ∈ 𝑆 ) )
43 29 39 42 3bitrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( 𝑧 + 𝑤 ) + 𝑢 ) ∈ 𝑆 ↔ ( 𝑢 + ( 𝑧 + 𝑤 ) ) ∈ 𝑆 ) )
44 43 ralrimiva ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) → ∀ 𝑢 ∈ 𝑋 ( ( ( 𝑧 + 𝑤 ) + 𝑢 ) ∈ 𝑆 ↔ ( 𝑢 + ( 𝑧 + 𝑤 ) ) ∈ 𝑆 ) )
45 1 elnmz ⊢ ( ( 𝑧 + 𝑤 ) ∈ 𝑁 ↔ ( ( 𝑧 + 𝑤 ) ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑋 ( ( ( 𝑧 + 𝑤 ) + 𝑢 ) ∈ 𝑆 ↔ ( 𝑢 + ( 𝑧 + 𝑤 ) ) ∈ 𝑆 ) ) )
46 20 44 45 sylanbrc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) → ( 𝑧 + 𝑤 ) ∈ 𝑁 )
47 46 3expa ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑤 ∈ 𝑁 ) → ( 𝑧 + 𝑤 ) ∈ 𝑁 )
48 47 ralrimiva ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) → ∀ 𝑤 ∈ 𝑁 ( 𝑧 + 𝑤 ) ∈ 𝑁 )
49 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
50 2 49 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 )
51 17 50 sylan2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 )
52 simplr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → 𝑧 ∈ 𝑁 )
53 simpll ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → 𝐺 ∈ Grp )
54 51 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 )
55 simpr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → 𝑢 ∈ 𝑋 )
56 2 3 53 55 54 grpcld ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑋 )
57 2 3 53 54 56 grpcld ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) ∈ 𝑋 )
58 1 nmzbi ⊢ ( ( 𝑧 ∈ 𝑁 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) ∈ 𝑋 ) → ( ( 𝑧 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) ) ∈ 𝑆 ↔ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) + 𝑧 ) ∈ 𝑆 ) )
59 52 57 58 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑧 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) ) ∈ 𝑆 ↔ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) + 𝑧 ) ∈ 𝑆 ) )
60 4 52 sselid ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → 𝑧 ∈ 𝑋 )
61 2 3 6 49 grprinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) = ( 0g ‘ 𝐺 ) )
62 53 60 61 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( 𝑧 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) = ( 0g ‘ 𝐺 ) )
63 62 oveq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑧 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) = ( ( 0g ‘ 𝐺 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) )
64 2 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑧 ∈ 𝑋 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 ∧ ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑋 ) ) → ( ( 𝑧 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) = ( 𝑧 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) ) )
65 53 60 54 56 64 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑧 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) = ( 𝑧 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) ) )
66 2 3 6 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) = ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) )
67 53 56 66 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) = ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) )
68 63 65 67 3eqtr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( 𝑧 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) ) = ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) )
69 68 eleq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑧 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) ) ∈ 𝑆 ↔ ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑆 ) )
70 2 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 ∧ ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) + 𝑧 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) + 𝑧 ) ) )
71 53 54 56 60 70 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) + 𝑧 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) + 𝑧 ) ) )
72 2 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑢 ∈ 𝑋 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) + 𝑧 ) = ( 𝑢 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑧 ) ) )
73 53 55 54 60 72 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) + 𝑧 ) = ( 𝑢 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑧 ) ) )
74 2 3 6 49 grplinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑧 ) = ( 0g ‘ 𝐺 ) )
75 53 60 74 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑧 ) = ( 0g ‘ 𝐺 ) )
76 75 oveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( 𝑢 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑧 ) ) = ( 𝑢 + ( 0g ‘ 𝐺 ) ) )
77 2 3 6 grprid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ) → ( 𝑢 + ( 0g ‘ 𝐺 ) ) = 𝑢 )
78 53 55 77 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( 𝑢 + ( 0g ‘ 𝐺 ) ) = 𝑢 )
79 73 76 78 3eqtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) + 𝑧 ) = 𝑢 )
80 79 oveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) + 𝑧 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑢 ) )
81 71 80 eqtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) + 𝑧 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑢 ) )
82 81 eleq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) + 𝑧 ) ∈ 𝑆 ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑢 ) ∈ 𝑆 ) )
83 59 69 82 3bitr3rd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑢 ) ∈ 𝑆 ↔ ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑆 ) )
84 83 ralrimiva ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) → ∀ 𝑢 ∈ 𝑋 ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑢 ) ∈ 𝑆 ↔ ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑆 ) )
85 1 elnmz ⊢ ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑁 ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑋 ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑢 ) ∈ 𝑆 ↔ ( 𝑢 + ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑆 ) ) )
86 51 84 85 sylanbrc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑁 )
87 48 86 jca ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ) → ( ∀ 𝑤 ∈ 𝑁 ( 𝑧 + 𝑤 ) ∈ 𝑁 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑁 ) )
88 87 ralrimiva ⊢ ( 𝐺 ∈ Grp → ∀ 𝑧 ∈ 𝑁 ( ∀ 𝑤 ∈ 𝑁 ( 𝑧 + 𝑤 ) ∈ 𝑁 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑁 ) )
89 2 3 49 issubg2 ⊢ ( 𝐺 ∈ Grp → ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑁 ⊆ 𝑋 ∧ 𝑁 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑁 ( ∀ 𝑤 ∈ 𝑁 ( 𝑧 + 𝑤 ) ∈ 𝑁 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑁 ) ) ) )
90 5 15 88 89 mpbir3and ⊢ ( 𝐺 ∈ Grp → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )