Step |
Hyp |
Ref |
Expression |
1 |
|
cycsubg.x |
โข ๐ = ( Base โ ๐บ ) |
2 |
|
cycsubg.t |
โข ยท = ( .g โ ๐บ ) |
3 |
|
cycsubg.f |
โข ๐น = ( ๐ฅ โ โค โฆ ( ๐ฅ ยท ๐ด ) ) |
4 |
|
ssintab |
โข ( ran ๐น โ โฉ { ๐ โฃ ( ๐ โ ( SubGrp โ ๐บ ) โง ๐ด โ ๐ ) } โ โ ๐ ( ( ๐ โ ( SubGrp โ ๐บ ) โง ๐ด โ ๐ ) โ ran ๐น โ ๐ ) ) |
5 |
1 2 3
|
cycsubgss |
โข ( ( ๐ โ ( SubGrp โ ๐บ ) โง ๐ด โ ๐ ) โ ran ๐น โ ๐ ) |
6 |
4 5
|
mpgbir |
โข ran ๐น โ โฉ { ๐ โฃ ( ๐ โ ( SubGrp โ ๐บ ) โง ๐ด โ ๐ ) } |
7 |
|
df-rab |
โข { ๐ โ ( SubGrp โ ๐บ ) โฃ ๐ด โ ๐ } = { ๐ โฃ ( ๐ โ ( SubGrp โ ๐บ ) โง ๐ด โ ๐ ) } |
8 |
7
|
inteqi |
โข โฉ { ๐ โ ( SubGrp โ ๐บ ) โฃ ๐ด โ ๐ } = โฉ { ๐ โฃ ( ๐ โ ( SubGrp โ ๐บ ) โง ๐ด โ ๐ ) } |
9 |
6 8
|
sseqtrri |
โข ran ๐น โ โฉ { ๐ โ ( SubGrp โ ๐บ ) โฃ ๐ด โ ๐ } |
10 |
9
|
a1i |
โข ( ( ๐บ โ Grp โง ๐ด โ ๐ ) โ ran ๐น โ โฉ { ๐ โ ( SubGrp โ ๐บ ) โฃ ๐ด โ ๐ } ) |
11 |
1 2 3
|
cycsubgcl |
โข ( ( ๐บ โ Grp โง ๐ด โ ๐ ) โ ( ran ๐น โ ( SubGrp โ ๐บ ) โง ๐ด โ ran ๐น ) ) |
12 |
|
eleq2 |
โข ( ๐ = ran ๐น โ ( ๐ด โ ๐ โ ๐ด โ ran ๐น ) ) |
13 |
12
|
elrab |
โข ( ran ๐น โ { ๐ โ ( SubGrp โ ๐บ ) โฃ ๐ด โ ๐ } โ ( ran ๐น โ ( SubGrp โ ๐บ ) โง ๐ด โ ran ๐น ) ) |
14 |
11 13
|
sylibr |
โข ( ( ๐บ โ Grp โง ๐ด โ ๐ ) โ ran ๐น โ { ๐ โ ( SubGrp โ ๐บ ) โฃ ๐ด โ ๐ } ) |
15 |
|
intss1 |
โข ( ran ๐น โ { ๐ โ ( SubGrp โ ๐บ ) โฃ ๐ด โ ๐ } โ โฉ { ๐ โ ( SubGrp โ ๐บ ) โฃ ๐ด โ ๐ } โ ran ๐น ) |
16 |
14 15
|
syl |
โข ( ( ๐บ โ Grp โง ๐ด โ ๐ ) โ โฉ { ๐ โ ( SubGrp โ ๐บ ) โฃ ๐ด โ ๐ } โ ran ๐น ) |
17 |
10 16
|
eqssd |
โข ( ( ๐บ โ Grp โง ๐ด โ ๐ ) โ ran ๐น = โฉ { ๐ โ ( SubGrp โ ๐บ ) โฃ ๐ด โ ๐ } ) |