Metamath Proof Explorer

Theorem conjnmzb

Description: Alternative condition for elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypotheses conjghm.x 
|- X = ( Base ` G )
conjghm.p 
|- .+ = ( +g ` G )
conjghm.m 
|- .- = ( -g ` G )
conjsubg.f 
|- F = ( x e. S |-> ( ( A .+ x ) .- A ) )
conjnmz.1 
|- N = { y e. X | A. z e. X ( ( y .+ z ) e. S <-> ( z .+ y ) e. S ) }
Assertion conjnmzb 
|- ( S e. ( SubGrp ` G ) -> ( A e. N <-> ( A e. X /\ S = ran F ) ) )

Proof

Step Hyp Ref Expression
1 conjghm.x 
 |-  X = ( Base ` G )
2 conjghm.p 
 |-  .+ = ( +g ` G )
3 conjghm.m 
 |-  .- = ( -g ` G )
4 conjsubg.f 
 |-  F = ( x e. S |-> ( ( A .+ x ) .- A ) )
5 conjnmz.1 
 |-  N = { y e. X | A. z e. X ( ( y .+ z ) e. S <-> ( z .+ y ) e. S ) }
6 5 ssrab3 
 |-  N C_ X
7 simpr 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. N ) -> A e. N )
8 6 7 sseldi 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. N ) -> A e. X )
9 1 2 3 4 5 conjnmz 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. N ) -> S = ran F )
10 8 9 jca 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. N ) -> ( A e. X /\ S = ran F ) )
11 simprl 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( A e. X /\ S = ran F ) ) -> A e. X )
12 simplrr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( A e. X /\ S = ran F ) ) /\ w e. X ) -> S = ran F )
13 12 eleq2d 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( A e. X /\ S = ran F ) ) /\ w e. X ) -> ( ( A .+ w ) e. S <-> ( A .+ w ) e. ran F ) )
14 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
15 14 ad3antrrr 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ A e. X ) /\ w e. X ) /\ x e. S ) -> G e. Grp )
16 simpllr 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ A e. X ) /\ w e. X ) /\ x e. S ) -> A e. X )
17 1 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ X )
18 17 ad2antrr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. X ) /\ w e. X ) -> S C_ X )
19 18 sselda 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ A e. X ) /\ w e. X ) /\ x e. S ) -> x e. X )
20 1 2 3 grpaddsubass 
 |-  ( ( G e. Grp /\ ( A e. X /\ x e. X /\ A e. X ) ) -> ( ( A .+ x ) .- A ) = ( A .+ ( x .- A ) ) )
21 15 16 19 16 20 syl13anc 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ A e. X ) /\ w e. X ) /\ x e. S ) -> ( ( A .+ x ) .- A ) = ( A .+ ( x .- A ) ) )
22 21 eqeq1d 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ A e. X ) /\ w e. X ) /\ x e. S ) -> ( ( ( A .+ x ) .- A ) = ( A .+ w ) <-> ( A .+ ( x .- A ) ) = ( A .+ w ) ) )
23 1 3 grpsubcl 
 |-  ( ( G e. Grp /\ x e. X /\ A e. X ) -> ( x .- A ) e. X )
24 15 19 16 23 syl3anc 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ A e. X ) /\ w e. X ) /\ x e. S ) -> ( x .- A ) e. X )
25 simplr 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ A e. X ) /\ w e. X ) /\ x e. S ) -> w e. X )
26 1 2 grplcan 
 |-  ( ( G e. Grp /\ ( ( x .- A ) e. X /\ w e. X /\ A e. X ) ) -> ( ( A .+ ( x .- A ) ) = ( A .+ w ) <-> ( x .- A ) = w ) )
27 15 24 25 16 26 syl13anc 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ A e. X ) /\ w e. X ) /\ x e. S ) -> ( ( A .+ ( x .- A ) ) = ( A .+ w ) <-> ( x .- A ) = w ) )
28 1 2 3 grpsubadd 
 |-  ( ( G e. Grp /\ ( x e. X /\ A e. X /\ w e. X ) ) -> ( ( x .- A ) = w <-> ( w .+ A ) = x ) )
29 15 19 16 25 28 syl13anc 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ A e. X ) /\ w e. X ) /\ x e. S ) -> ( ( x .- A ) = w <-> ( w .+ A ) = x ) )
30 22 27 29 3bitrd 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ A e. X ) /\ w e. X ) /\ x e. S ) -> ( ( ( A .+ x ) .- A ) = ( A .+ w ) <-> ( w .+ A ) = x ) )
31 eqcom 
 |-  ( ( A .+ w ) = ( ( A .+ x ) .- A ) <-> ( ( A .+ x ) .- A ) = ( A .+ w ) )
32 eqcom 
 |-  ( x = ( w .+ A ) <-> ( w .+ A ) = x )
33 30 31 32 3bitr4g 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ A e. X ) /\ w e. X ) /\ x e. S ) -> ( ( A .+ w ) = ( ( A .+ x ) .- A ) <-> x = ( w .+ A ) ) )
34 33 rexbidva 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. X ) /\ w e. X ) -> ( E. x e. S ( A .+ w ) = ( ( A .+ x ) .- A ) <-> E. x e. S x = ( w .+ A ) ) )
35 34 adantlrr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( A e. X /\ S = ran F ) ) /\ w e. X ) -> ( E. x e. S ( A .+ w ) = ( ( A .+ x ) .- A ) <-> E. x e. S x = ( w .+ A ) ) )
36 ovex 
 |-  ( A .+ w ) e. _V
37 eqeq1 
 |-  ( y = ( A .+ w ) -> ( y = ( ( A .+ x ) .- A ) <-> ( A .+ w ) = ( ( A .+ x ) .- A ) ) )
38 37 rexbidv 
 |-  ( y = ( A .+ w ) -> ( E. x e. S y = ( ( A .+ x ) .- A ) <-> E. x e. S ( A .+ w ) = ( ( A .+ x ) .- A ) ) )
39 4 rnmpt 
 |-  ran F = { y | E. x e. S y = ( ( A .+ x ) .- A ) }
40 36 38 39 elab2 
 |-  ( ( A .+ w ) e. ran F <-> E. x e. S ( A .+ w ) = ( ( A .+ x ) .- A ) )
41 risset 
 |-  ( ( w .+ A ) e. S <-> E. x e. S x = ( w .+ A ) )
42 35 40 41 3bitr4g 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( A e. X /\ S = ran F ) ) /\ w e. X ) -> ( ( A .+ w ) e. ran F <-> ( w .+ A ) e. S ) )
43 13 42 bitrd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( A e. X /\ S = ran F ) ) /\ w e. X ) -> ( ( A .+ w ) e. S <-> ( w .+ A ) e. S ) )
44 43 ralrimiva 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( A e. X /\ S = ran F ) ) -> A. w e. X ( ( A .+ w ) e. S <-> ( w .+ A ) e. S ) )
45 5 elnmz 
 |-  ( A e. N <-> ( A e. X /\ A. w e. X ( ( A .+ w ) e. S <-> ( w .+ A ) e. S ) ) )
46 11 44 45 sylanbrc 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( A e. X /\ S = ran F ) ) -> A e. N )
47 10 46 impbida 
 |-  ( S e. ( SubGrp ` G ) -> ( A e. N <-> ( A e. X /\ S = ran F ) ) )