Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. 2
โข
(Baseโ(๐บ
โพs ๐)) =
(Baseโ(๐บ
โพs ๐)) |
2 | | eqid 2733 |
. 2
โข
(.gโ(๐บ โพs ๐)) = (.gโ(๐บ โพs ๐)) |
3 | | cycsubgcyg.s |
. . . 4
โข ๐ = ran (๐ฅ โ โค โฆ (๐ฅ ยท ๐ด)) |
4 | | cycsubgcyg.x |
. . . . . 6
โข ๐ = (Baseโ๐บ) |
5 | | cycsubgcyg.t |
. . . . . 6
โข ยท =
(.gโ๐บ) |
6 | | eqid 2733 |
. . . . . 6
โข (๐ฅ โ โค โฆ (๐ฅ ยท ๐ด)) = (๐ฅ โ โค โฆ (๐ฅ ยท ๐ด)) |
7 | 4, 5, 6 | cycsubgcl 19007 |
. . . . 5
โข ((๐บ โ Grp โง ๐ด โ ๐) โ (ran (๐ฅ โ โค โฆ (๐ฅ ยท ๐ด)) โ (SubGrpโ๐บ) โง ๐ด โ ran (๐ฅ โ โค โฆ (๐ฅ ยท ๐ด)))) |
8 | 7 | simpld 496 |
. . . 4
โข ((๐บ โ Grp โง ๐ด โ ๐) โ ran (๐ฅ โ โค โฆ (๐ฅ ยท ๐ด)) โ (SubGrpโ๐บ)) |
9 | 3, 8 | eqeltrid 2838 |
. . 3
โข ((๐บ โ Grp โง ๐ด โ ๐) โ ๐ โ (SubGrpโ๐บ)) |
10 | | eqid 2733 |
. . . 4
โข (๐บ โพs ๐) = (๐บ โพs ๐) |
11 | 10 | subggrp 18939 |
. . 3
โข (๐ โ (SubGrpโ๐บ) โ (๐บ โพs ๐) โ Grp) |
12 | 9, 11 | syl 17 |
. 2
โข ((๐บ โ Grp โง ๐ด โ ๐) โ (๐บ โพs ๐) โ Grp) |
13 | 7 | simprd 497 |
. . . 4
โข ((๐บ โ Grp โง ๐ด โ ๐) โ ๐ด โ ran (๐ฅ โ โค โฆ (๐ฅ ยท ๐ด))) |
14 | 13, 3 | eleqtrrdi 2845 |
. . 3
โข ((๐บ โ Grp โง ๐ด โ ๐) โ ๐ด โ ๐) |
15 | 10 | subgbas 18940 |
. . . 4
โข (๐ โ (SubGrpโ๐บ) โ ๐ = (Baseโ(๐บ โพs ๐))) |
16 | 9, 15 | syl 17 |
. . 3
โข ((๐บ โ Grp โง ๐ด โ ๐) โ ๐ = (Baseโ(๐บ โพs ๐))) |
17 | 14, 16 | eleqtrd 2836 |
. 2
โข ((๐บ โ Grp โง ๐ด โ ๐) โ ๐ด โ (Baseโ(๐บ โพs ๐))) |
18 | 16 | eleq2d 2820 |
. . . 4
โข ((๐บ โ Grp โง ๐ด โ ๐) โ (๐ฆ โ ๐ โ ๐ฆ โ (Baseโ(๐บ โพs ๐)))) |
19 | 18 | biimpar 479 |
. . 3
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ฆ โ (Baseโ(๐บ โพs ๐))) โ ๐ฆ โ ๐) |
20 | | simpr 486 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ฆ โ ๐) โ ๐ฆ โ ๐) |
21 | 20, 3 | eleqtrdi 2844 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ฆ โ ๐) โ ๐ฆ โ ran (๐ฅ โ โค โฆ (๐ฅ ยท ๐ด))) |
22 | | oveq1 7368 |
. . . . . . 7
โข (๐ฅ = ๐ โ (๐ฅ ยท ๐ด) = (๐ ยท ๐ด)) |
23 | 22 | cbvmptv 5222 |
. . . . . 6
โข (๐ฅ โ โค โฆ (๐ฅ ยท ๐ด)) = (๐ โ โค โฆ (๐ ยท ๐ด)) |
24 | | ovex 7394 |
. . . . . 6
โข (๐ ยท ๐ด) โ V |
25 | 23, 24 | elrnmpti 5919 |
. . . . 5
โข (๐ฆ โ ran (๐ฅ โ โค โฆ (๐ฅ ยท ๐ด)) โ โ๐ โ โค ๐ฆ = (๐ ยท ๐ด)) |
26 | 21, 25 | sylib 217 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ฆ โ ๐) โ โ๐ โ โค ๐ฆ = (๐ ยท ๐ด)) |
27 | 9 | ad2antrr 725 |
. . . . . . 7
โข ((((๐บ โ Grp โง ๐ด โ ๐) โง ๐ฆ โ ๐) โง ๐ โ โค) โ ๐ โ (SubGrpโ๐บ)) |
28 | | simpr 486 |
. . . . . . 7
โข ((((๐บ โ Grp โง ๐ด โ ๐) โง ๐ฆ โ ๐) โง ๐ โ โค) โ ๐ โ โค) |
29 | 14 | ad2antrr 725 |
. . . . . . 7
โข ((((๐บ โ Grp โง ๐ด โ ๐) โง ๐ฆ โ ๐) โง ๐ โ โค) โ ๐ด โ ๐) |
30 | 5, 10, 2 | subgmulg 18950 |
. . . . . . 7
โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ โค โง ๐ด โ ๐) โ (๐ ยท ๐ด) = (๐(.gโ(๐บ โพs ๐))๐ด)) |
31 | 27, 28, 29, 30 | syl3anc 1372 |
. . . . . 6
โข ((((๐บ โ Grp โง ๐ด โ ๐) โง ๐ฆ โ ๐) โง ๐ โ โค) โ (๐ ยท ๐ด) = (๐(.gโ(๐บ โพs ๐))๐ด)) |
32 | 31 | eqeq2d 2744 |
. . . . 5
โข ((((๐บ โ Grp โง ๐ด โ ๐) โง ๐ฆ โ ๐) โง ๐ โ โค) โ (๐ฆ = (๐ ยท ๐ด) โ ๐ฆ = (๐(.gโ(๐บ โพs ๐))๐ด))) |
33 | 32 | rexbidva 3170 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ฆ โ ๐) โ (โ๐ โ โค ๐ฆ = (๐ ยท ๐ด) โ โ๐ โ โค ๐ฆ = (๐(.gโ(๐บ โพs ๐))๐ด))) |
34 | 26, 33 | mpbid 231 |
. . 3
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ฆ โ ๐) โ โ๐ โ โค ๐ฆ = (๐(.gโ(๐บ โพs ๐))๐ด)) |
35 | 19, 34 | syldan 592 |
. 2
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ฆ โ (Baseโ(๐บ โพs ๐))) โ โ๐ โ โค ๐ฆ = (๐(.gโ(๐บ โพs ๐))๐ด)) |
36 | 1, 2, 12, 17, 35 | iscygd 19672 |
1
โข ((๐บ โ Grp โง ๐ด โ ๐) โ (๐บ โพs ๐) โ CycGrp) |