Metamath Proof Explorer


Theorem isnsg3

Description: A subgroup is normal iff the conjugation of all the elements of the subgroup is in the subgroup. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypotheses isnsg3.1 X = Base G
isnsg3.2 + ˙ = + G
isnsg3.3 - ˙ = - G
Assertion isnsg3 S NrmSGrp G S SubGrp G x X y S x + ˙ y - ˙ x S

Proof

Step Hyp Ref Expression
1 isnsg3.1 X = Base G
2 isnsg3.2 + ˙ = + G
3 isnsg3.3 - ˙ = - G
4 nsgsubg S NrmSGrp G S SubGrp G
5 1 2 3 nsgconj S NrmSGrp G x X y S x + ˙ y - ˙ x S
6 5 3expb S NrmSGrp G x X y S x + ˙ y - ˙ x S
7 6 ralrimivva S NrmSGrp G x X y S x + ˙ y - ˙ x S
8 4 7 jca S NrmSGrp G S SubGrp G x X y S x + ˙ y - ˙ x S
9 simpl S SubGrp G x X y S x + ˙ y - ˙ x S S SubGrp G
10 subgrcl S SubGrp G G Grp
11 10 ad2antrr S SubGrp G x X y S x + ˙ y - ˙ x S z X w X z + ˙ w S G Grp
12 simprll S SubGrp G x X y S x + ˙ y - ˙ x S z X w X z + ˙ w S z X
13 eqid 0 G = 0 G
14 eqid inv g G = inv g G
15 1 2 13 14 grplinv G Grp z X inv g G z + ˙ z = 0 G
16 11 12 15 syl2anc S SubGrp G x X y S x + ˙ y - ˙ x S z X w X z + ˙ w S inv g G z + ˙ z = 0 G
17 16 oveq1d S SubGrp G x X y S x + ˙ y - ˙ x S z X w X z + ˙ w S inv g G z + ˙ z + ˙ w = 0 G + ˙ w
18 1 14 grpinvcl G Grp z X inv g G z X
19 11 12 18 syl2anc S SubGrp G x X y S x + ˙ y - ˙ x S z X w X z + ˙ w S inv g G z X
20 simprlr S SubGrp G x X y S x + ˙ y - ˙ x S z X w X z + ˙ w S w X
21 1 2 grpass G Grp inv g G z X z X w X inv g G z + ˙ z + ˙ w = inv g G z + ˙ z + ˙ w
22 11 19 12 20 21 syl13anc S SubGrp G x X y S x + ˙ y - ˙ x S z X w X z + ˙ w S inv g G z + ˙ z + ˙ w = inv g G z + ˙ z + ˙ w
23 1 2 13 grplid G Grp w X 0 G + ˙ w = w
24 11 20 23 syl2anc S SubGrp G x X y S x + ˙ y - ˙ x S z X w X z + ˙ w S 0 G + ˙ w = w
25 17 22 24 3eqtr3d S SubGrp G x X y S x + ˙ y - ˙ x S z X w X z + ˙ w S inv g G z + ˙ z + ˙ w = w
26 25 oveq1d S SubGrp G x X y S x + ˙ y - ˙ x S z X w X z + ˙ w S inv g G z + ˙ z + ˙ w - ˙ inv g G z = w - ˙ inv g G z
27 1 2 3 14 11 20 12 grpsubinv S SubGrp G x X y S x + ˙ y - ˙ x S z X w X z + ˙ w S w - ˙ inv g G z = w + ˙ z
28 26 27 eqtrd S SubGrp G x X y S x + ˙ y - ˙ x S z X w X z + ˙ w S inv g G z + ˙ z + ˙ w - ˙ inv g G z = w + ˙ z
29 simprr S SubGrp G x X y S x + ˙ y - ˙ x S z X w X z + ˙ w S z + ˙ w S
30 simplr S SubGrp G x X y S x + ˙ y - ˙ x S z X w X z + ˙ w S x X y S x + ˙ y - ˙ x S
31 oveq1 x = inv g G z x + ˙ y = inv g G z + ˙ y
32 id x = inv g G z x = inv g G z
33 31 32 oveq12d x = inv g G z x + ˙ y - ˙ x = inv g G z + ˙ y - ˙ inv g G z
34 33 eleq1d x = inv g G z x + ˙ y - ˙ x S inv g G z + ˙ y - ˙ inv g G z S
35 oveq2 y = z + ˙ w inv g G z + ˙ y = inv g G z + ˙ z + ˙ w
36 35 oveq1d y = z + ˙ w inv g G z + ˙ y - ˙ inv g G z = inv g G z + ˙ z + ˙ w - ˙ inv g G z
37 36 eleq1d y = z + ˙ w inv g G z + ˙ y - ˙ inv g G z S inv g G z + ˙ z + ˙ w - ˙ inv g G z S
38 34 37 rspc2va inv g G z X z + ˙ w S x X y S x + ˙ y - ˙ x S inv g G z + ˙ z + ˙ w - ˙ inv g G z S
39 19 29 30 38 syl21anc S SubGrp G x X y S x + ˙ y - ˙ x S z X w X z + ˙ w S inv g G z + ˙ z + ˙ w - ˙ inv g G z S
40 28 39 eqeltrrd S SubGrp G x X y S x + ˙ y - ˙ x S z X w X z + ˙ w S w + ˙ z S
41 40 expr S SubGrp G x X y S x + ˙ y - ˙ x S z X w X z + ˙ w S w + ˙ z S
42 41 ralrimivva S SubGrp G x X y S x + ˙ y - ˙ x S z X w X z + ˙ w S w + ˙ z S
43 1 2 isnsg2 S NrmSGrp G S SubGrp G z X w X z + ˙ w S w + ˙ z S
44 9 42 43 sylanbrc S SubGrp G x X y S x + ˙ y - ˙ x S S NrmSGrp G
45 8 44 impbii S NrmSGrp G S SubGrp G x X y S x + ˙ y - ˙ x S