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