Metamath Proof Explorer


Theorem isnsg

Description: Property of being a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypotheses isnsg.1
|- X = ( Base ` G )
isnsg.2
|- .+ = ( +g ` G )
Assertion isnsg
|- ( S e. ( NrmSGrp ` G ) <-> ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) ) )

Proof

Step Hyp Ref Expression
1 isnsg.1
 |-  X = ( Base ` G )
2 isnsg.2
 |-  .+ = ( +g ` G )
3 df-nsg
 |-  NrmSGrp = ( g e. Grp |-> { s e. ( SubGrp ` g ) | [. ( Base ` g ) / b ]. [. ( +g ` g ) / p ]. A. x e. b A. y e. b ( ( x p y ) e. s <-> ( y p x ) e. s ) } )
4 3 mptrcl
 |-  ( S e. ( NrmSGrp ` G ) -> G e. Grp )
5 subgrcl
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
6 5 adantr
 |-  ( ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) ) -> G e. Grp )
7 fveq2
 |-  ( g = G -> ( SubGrp ` g ) = ( SubGrp ` G ) )
8 fvexd
 |-  ( g = G -> ( Base ` g ) e. _V )
9 fveq2
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
10 9 1 eqtr4di
 |-  ( g = G -> ( Base ` g ) = X )
11 fvexd
 |-  ( ( g = G /\ b = X ) -> ( +g ` g ) e. _V )
12 simpl
 |-  ( ( g = G /\ b = X ) -> g = G )
13 12 fveq2d
 |-  ( ( g = G /\ b = X ) -> ( +g ` g ) = ( +g ` G ) )
14 13 2 eqtr4di
 |-  ( ( g = G /\ b = X ) -> ( +g ` g ) = .+ )
15 simplr
 |-  ( ( ( g = G /\ b = X ) /\ p = .+ ) -> b = X )
16 simpr
 |-  ( ( ( g = G /\ b = X ) /\ p = .+ ) -> p = .+ )
17 16 oveqd
 |-  ( ( ( g = G /\ b = X ) /\ p = .+ ) -> ( x p y ) = ( x .+ y ) )
18 17 eleq1d
 |-  ( ( ( g = G /\ b = X ) /\ p = .+ ) -> ( ( x p y ) e. s <-> ( x .+ y ) e. s ) )
19 16 oveqd
 |-  ( ( ( g = G /\ b = X ) /\ p = .+ ) -> ( y p x ) = ( y .+ x ) )
20 19 eleq1d
 |-  ( ( ( g = G /\ b = X ) /\ p = .+ ) -> ( ( y p x ) e. s <-> ( y .+ x ) e. s ) )
21 18 20 bibi12d
 |-  ( ( ( g = G /\ b = X ) /\ p = .+ ) -> ( ( ( x p y ) e. s <-> ( y p x ) e. s ) <-> ( ( x .+ y ) e. s <-> ( y .+ x ) e. s ) ) )
22 15 21 raleqbidv
 |-  ( ( ( g = G /\ b = X ) /\ p = .+ ) -> ( A. y e. b ( ( x p y ) e. s <-> ( y p x ) e. s ) <-> A. y e. X ( ( x .+ y ) e. s <-> ( y .+ x ) e. s ) ) )
23 15 22 raleqbidv
 |-  ( ( ( g = G /\ b = X ) /\ p = .+ ) -> ( A. x e. b A. y e. b ( ( x p y ) e. s <-> ( y p x ) e. s ) <-> A. x e. X A. y e. X ( ( x .+ y ) e. s <-> ( y .+ x ) e. s ) ) )
24 11 14 23 sbcied2
 |-  ( ( g = G /\ b = X ) -> ( [. ( +g ` g ) / p ]. A. x e. b A. y e. b ( ( x p y ) e. s <-> ( y p x ) e. s ) <-> A. x e. X A. y e. X ( ( x .+ y ) e. s <-> ( y .+ x ) e. s ) ) )
25 8 10 24 sbcied2
 |-  ( g = G -> ( [. ( Base ` g ) / b ]. [. ( +g ` g ) / p ]. A. x e. b A. y e. b ( ( x p y ) e. s <-> ( y p x ) e. s ) <-> A. x e. X A. y e. X ( ( x .+ y ) e. s <-> ( y .+ x ) e. s ) ) )
26 7 25 rabeqbidv
 |-  ( g = G -> { s e. ( SubGrp ` g ) | [. ( Base ` g ) / b ]. [. ( +g ` g ) / p ]. A. x e. b A. y e. b ( ( x p y ) e. s <-> ( y p x ) e. s ) } = { s e. ( SubGrp ` G ) | A. x e. X A. y e. X ( ( x .+ y ) e. s <-> ( y .+ x ) e. s ) } )
27 fvex
 |-  ( SubGrp ` G ) e. _V
28 27 rabex
 |-  { s e. ( SubGrp ` G ) | A. x e. X A. y e. X ( ( x .+ y ) e. s <-> ( y .+ x ) e. s ) } e. _V
29 26 3 28 fvmpt
 |-  ( G e. Grp -> ( NrmSGrp ` G ) = { s e. ( SubGrp ` G ) | A. x e. X A. y e. X ( ( x .+ y ) e. s <-> ( y .+ x ) e. s ) } )
30 29 eleq2d
 |-  ( G e. Grp -> ( S e. ( NrmSGrp ` G ) <-> S e. { s e. ( SubGrp ` G ) | A. x e. X A. y e. X ( ( x .+ y ) e. s <-> ( y .+ x ) e. s ) } ) )
31 eleq2
 |-  ( s = S -> ( ( x .+ y ) e. s <-> ( x .+ y ) e. S ) )
32 eleq2
 |-  ( s = S -> ( ( y .+ x ) e. s <-> ( y .+ x ) e. S ) )
33 31 32 bibi12d
 |-  ( s = S -> ( ( ( x .+ y ) e. s <-> ( y .+ x ) e. s ) <-> ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) ) )
34 33 2ralbidv
 |-  ( s = S -> ( A. x e. X A. y e. X ( ( x .+ y ) e. s <-> ( y .+ x ) e. s ) <-> A. x e. X A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) ) )
35 34 elrab
 |-  ( S e. { s e. ( SubGrp ` G ) | A. x e. X A. y e. X ( ( x .+ y ) e. s <-> ( y .+ x ) e. s ) } <-> ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) ) )
36 30 35 bitrdi
 |-  ( G e. Grp -> ( S e. ( NrmSGrp ` G ) <-> ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) ) ) )
37 4 6 36 pm5.21nii
 |-  ( S e. ( NrmSGrp ` G ) <-> ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) ) )