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 )