Metamath Proof Explorer

Theorem conjsubg

Description: A conjugated subgroup is also a subgroup. (Contributed by Mario Carneiro, 13-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 ) )
Assertion conjsubg 
|- ( ( S e. ( SubGrp ` G ) /\ A e. X ) -> ran F e. ( SubGrp ` G ) )

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 1 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ X )
6 5 adantr 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. X ) -> S C_ X )
7 df-ima 
 |-  ( ( x e. X |-> ( ( A .+ x ) .- A ) ) " S ) = ran ( ( x e. X |-> ( ( A .+ x ) .- A ) ) |` S )
8 resmpt 
 |-  ( S C_ X -> ( ( x e. X |-> ( ( A .+ x ) .- A ) ) |` S ) = ( x e. S |-> ( ( A .+ x ) .- A ) ) )
9 8 4 eqtr4di 
 |-  ( S C_ X -> ( ( x e. X |-> ( ( A .+ x ) .- A ) ) |` S ) = F )
10 9 rneqd 
 |-  ( S C_ X -> ran ( ( x e. X |-> ( ( A .+ x ) .- A ) ) |` S ) = ran F )
11 7 10 syl5eq 
 |-  ( S C_ X -> ( ( x e. X |-> ( ( A .+ x ) .- A ) ) " S ) = ran F )
12 6 11 syl 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. X ) -> ( ( x e. X |-> ( ( A .+ x ) .- A ) ) " S ) = ran F )
13 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
14 eqid 
 |-  ( x e. X |-> ( ( A .+ x ) .- A ) ) = ( x e. X |-> ( ( A .+ x ) .- A ) )
15 1 2 3 14 conjghm 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( x e. X |-> ( ( A .+ x ) .- A ) ) e. ( G GrpHom G ) /\ ( x e. X |-> ( ( A .+ x ) .- A ) ) : X -1-1-onto-> X ) )
16 13 15 sylan 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. X ) -> ( ( x e. X |-> ( ( A .+ x ) .- A ) ) e. ( G GrpHom G ) /\ ( x e. X |-> ( ( A .+ x ) .- A ) ) : X -1-1-onto-> X ) )
17 16 simpld 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. X ) -> ( x e. X |-> ( ( A .+ x ) .- A ) ) e. ( G GrpHom G ) )
18 simpl 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. X ) -> S e. ( SubGrp ` G ) )
19 ghmima 
 |-  ( ( ( x e. X |-> ( ( A .+ x ) .- A ) ) e. ( G GrpHom G ) /\ S e. ( SubGrp ` G ) ) -> ( ( x e. X |-> ( ( A .+ x ) .- A ) ) " S ) e. ( SubGrp ` G ) )
20 17 18 19 syl2anc 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. X ) -> ( ( x e. X |-> ( ( A .+ x ) .- A ) ) " S ) e. ( SubGrp ` G ) )
21 12 20 eqeltrrd 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. X ) -> ran F e. ( SubGrp ` G ) )