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 ) ) )