Step |
Hyp |
Ref |
Expression |
1 |
|
cycsubg.x |
|- X = ( Base ` G ) |
2 |
|
cycsubg.t |
|- .x. = ( .g ` G ) |
3 |
|
cycsubg.f |
|- F = ( x e. ZZ |-> ( x .x. A ) ) |
4 |
|
ssintab |
|- ( ran F C_ |^| { s | ( s e. ( SubGrp ` G ) /\ A e. s ) } <-> A. s ( ( s e. ( SubGrp ` G ) /\ A e. s ) -> ran F C_ s ) ) |
5 |
1 2 3
|
cycsubgss |
|- ( ( s e. ( SubGrp ` G ) /\ A e. s ) -> ran F C_ s ) |
6 |
4 5
|
mpgbir |
|- ran F C_ |^| { s | ( s e. ( SubGrp ` G ) /\ A e. s ) } |
7 |
|
df-rab |
|- { s e. ( SubGrp ` G ) | A e. s } = { s | ( s e. ( SubGrp ` G ) /\ A e. s ) } |
8 |
7
|
inteqi |
|- |^| { s e. ( SubGrp ` G ) | A e. s } = |^| { s | ( s e. ( SubGrp ` G ) /\ A e. s ) } |
9 |
6 8
|
sseqtrri |
|- ran F C_ |^| { s e. ( SubGrp ` G ) | A e. s } |
10 |
9
|
a1i |
|- ( ( G e. Grp /\ A e. X ) -> ran F C_ |^| { s e. ( SubGrp ` G ) | A e. s } ) |
11 |
1 2 3
|
cycsubgcl |
|- ( ( G e. Grp /\ A e. X ) -> ( ran F e. ( SubGrp ` G ) /\ A e. ran F ) ) |
12 |
|
eleq2 |
|- ( s = ran F -> ( A e. s <-> A e. ran F ) ) |
13 |
12
|
elrab |
|- ( ran F e. { s e. ( SubGrp ` G ) | A e. s } <-> ( ran F e. ( SubGrp ` G ) /\ A e. ran F ) ) |
14 |
11 13
|
sylibr |
|- ( ( G e. Grp /\ A e. X ) -> ran F e. { s e. ( SubGrp ` G ) | A e. s } ) |
15 |
|
intss1 |
|- ( ran F e. { s e. ( SubGrp ` G ) | A e. s } -> |^| { s e. ( SubGrp ` G ) | A e. s } C_ ran F ) |
16 |
14 15
|
syl |
|- ( ( G e. Grp /\ A e. X ) -> |^| { s e. ( SubGrp ` G ) | A e. s } C_ ran F ) |
17 |
10 16
|
eqssd |
|- ( ( G e. Grp /\ A e. X ) -> ran F = |^| { s e. ( SubGrp ` G ) | A e. s } ) |