Metamath Proof Explorer

Theorem nsgacs

Description: Normal subgroups form an algebraic closure system. (Contributed by Stefan O'Rear, 4-Sep-2015)

Ref Expression
Hypothesis subgacs.b 
|- B = ( Base ` G )
Assertion nsgacs 
|- ( G e. Grp -> ( NrmSGrp ` G ) e. ( ACS ` B ) )

Proof

Step Hyp Ref Expression
1 subgacs.b 
 |-  B = ( Base ` G )
2 1 subgss 
 |-  ( s e. ( SubGrp ` G ) -> s C_ B )
3 velpw 
 |-  ( s e. ~P B <-> s C_ B )
4 2 3 sylibr 
 |-  ( s e. ( SubGrp ` G ) -> s e. ~P B )
5 eleq2w 
 |-  ( z = s -> ( ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. z <-> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. s ) )
6 5 raleqbi1dv 
 |-  ( z = s -> ( A. y e. z ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. z <-> A. y e. s ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. s ) )
7 6 ralbidv 
 |-  ( z = s -> ( A. x e. B A. y e. z ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. z <-> A. x e. B A. y e. s ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. s ) )
8 7 elrab3 
 |-  ( s e. ~P B -> ( s e. { z e. ~P B | A. x e. B A. y e. z ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. z } <-> A. x e. B A. y e. s ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. s ) )
9 4 8 syl 
 |-  ( s e. ( SubGrp ` G ) -> ( s e. { z e. ~P B | A. x e. B A. y e. z ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. z } <-> A. x e. B A. y e. s ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. s ) )
10 9 bicomd 
 |-  ( s e. ( SubGrp ` G ) -> ( A. x e. B A. y e. s ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. s <-> s e. { z e. ~P B | A. x e. B A. y e. z ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. z } ) )
11 10 pm5.32i 
 |-  ( ( s e. ( SubGrp ` G ) /\ A. x e. B A. y e. s ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. s ) <-> ( s e. ( SubGrp ` G ) /\ s e. { z e. ~P B | A. x e. B A. y e. z ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. z } ) )
12 eqid 
 |-  ( +g ` G ) = ( +g ` G )
13 eqid 
 |-  ( -g ` G ) = ( -g ` G )
14 1 12 13 isnsg3 
 |-  ( s e. ( NrmSGrp ` G ) <-> ( s e. ( SubGrp ` G ) /\ A. x e. B A. y e. s ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. s ) )
15 elin 
 |-  ( s e. ( ( SubGrp ` G ) i^i { z e. ~P B | A. x e. B A. y e. z ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. z } ) <-> ( s e. ( SubGrp ` G ) /\ s e. { z e. ~P B | A. x e. B A. y e. z ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. z } ) )
16 11 14 15 3bitr4i 
 |-  ( s e. ( NrmSGrp ` G ) <-> s e. ( ( SubGrp ` G ) i^i { z e. ~P B | A. x e. B A. y e. z ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. z } ) )
17 16 eqriv 
 |-  ( NrmSGrp ` G ) = ( ( SubGrp ` G ) i^i { z e. ~P B | A. x e. B A. y e. z ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. z } )
18 1 fvexi 
 |-  B e. _V
19 mreacs 
 |-  ( B e. _V -> ( ACS ` B ) e. ( Moore ` ~P B ) )
20 18 19 mp1i 
 |-  ( G e. Grp -> ( ACS ` B ) e. ( Moore ` ~P B ) )
21 1 subgacs 
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` B ) )
22 simpl 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> G e. Grp )
23 1 12 grpcl 
 |-  ( ( G e. Grp /\ x e. B /\ y e. B ) -> ( x ( +g ` G ) y ) e. B )
24 23 3expb 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` G ) y ) e. B )
25 simprl 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> x e. B )
26 1 13 grpsubcl 
 |-  ( ( G e. Grp /\ ( x ( +g ` G ) y ) e. B /\ x e. B ) -> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. B )
27 22 24 25 26 syl3anc 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. B )
28 27 ralrimivva 
 |-  ( G e. Grp -> A. x e. B A. y e. B ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. B )
29 acsfn1c 
 |-  ( ( B e. _V /\ A. x e. B A. y e. B ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. B ) -> { z e. ~P B | A. x e. B A. y e. z ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. z } e. ( ACS ` B ) )
30 18 28 29 sylancr 
 |-  ( G e. Grp -> { z e. ~P B | A. x e. B A. y e. z ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. z } e. ( ACS ` B ) )
31 mreincl 
 |-  ( ( ( ACS ` B ) e. ( Moore ` ~P B ) /\ ( SubGrp ` G ) e. ( ACS ` B ) /\ { z e. ~P B | A. x e. B A. y e. z ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. z } e. ( ACS ` B ) ) -> ( ( SubGrp ` G ) i^i { z e. ~P B | A. x e. B A. y e. z ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. z } ) e. ( ACS ` B ) )
32 20 21 30 31 syl3anc 
 |-  ( G e. Grp -> ( ( SubGrp ` G ) i^i { z e. ~P B | A. x e. B A. y e. z ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. z } ) e. ( ACS ` B ) )
33 17 32 eqeltrid 
 |-  ( G e. Grp -> ( NrmSGrp ` G ) e. ( ACS ` B ) )