This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem conjsubgen

Description: A conjugated subgroup is equinumerous to the original subgroup. (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 ) )
Assertion conjsubgen 
|- ( ( S e. ( SubGrp ` G ) /\ 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 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
6 eqid 
 |-  ( x e. X |-> ( ( A .+ x ) .- A ) ) = ( x e. X |-> ( ( A .+ x ) .- A ) )
7 1 2 3 6 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 ) )
8 5 7 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 ) )
9 f1of1 
 |-  ( ( x e. X |-> ( ( A .+ x ) .- A ) ) : X -1-1-onto-> X -> ( x e. X |-> ( ( A .+ x ) .- A ) ) : X -1-1-> X )
10 8 9 simpl2im 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. X ) -> ( x e. X |-> ( ( A .+ x ) .- A ) ) : X -1-1-> X )
11 1 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ X )
12 11 adantr 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. X ) -> S C_ X )
13 f1ssres 
 |-  ( ( ( x e. X |-> ( ( A .+ x ) .- A ) ) : X -1-1-> X /\ S C_ X ) -> ( ( x e. X |-> ( ( A .+ x ) .- A ) ) |` S ) : S -1-1-> X )
14 10 12 13 syl2anc 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. X ) -> ( ( x e. X |-> ( ( A .+ x ) .- A ) ) |` S ) : S -1-1-> X )
15 12 resmptd 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. X ) -> ( ( x e. X |-> ( ( A .+ x ) .- A ) ) |` S ) = ( x e. S |-> ( ( A .+ x ) .- A ) ) )
16 15 4 eqtr4di 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. X ) -> ( ( x e. X |-> ( ( A .+ x ) .- A ) ) |` S ) = F )
17 f1eq1 
 |-  ( ( ( x e. X |-> ( ( A .+ x ) .- A ) ) |` S ) = F -> ( ( ( x e. X |-> ( ( A .+ x ) .- A ) ) |` S ) : S -1-1-> X <-> F : S -1-1-> X ) )
18 16 17 syl 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. X ) -> ( ( ( x e. X |-> ( ( A .+ x ) .- A ) ) |` S ) : S -1-1-> X <-> F : S -1-1-> X ) )
19 14 18 mpbid 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. X ) -> F : S -1-1-> X )
20 f1f1orn 
 |-  ( F : S -1-1-> X -> F : S -1-1-onto-> ran F )
21 19 20 syl 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. X ) -> F : S -1-1-onto-> ran F )
22 f1oeng 
 |-  ( ( S e. ( SubGrp ` G ) /\ F : S -1-1-onto-> ran F ) -> S ~~ ran F )
23 21 22 syldan 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. X ) -> S ~~ ran F )