Step | Hyp | Ref
| Expression |
1 | | iscyg.1 |
. . . . 5
โข ๐ต = (Baseโ๐บ) |
2 | | iscyg.2 |
. . . . 5
โข ยท =
(.gโ๐บ) |
3 | | iscyg3.e |
. . . . 5
โข ๐ธ = {๐ฅ โ ๐ต โฃ ran (๐ โ โค โฆ (๐ ยท ๐ฅ)) = ๐ต} |
4 | 1, 2, 3 | iscyggen2 19665 |
. . . 4
โข (๐บ โ Grp โ (๐ โ ๐ธ โ (๐ โ ๐ต โง โ๐ฆ โ ๐ต โ๐ โ โค ๐ฆ = (๐ ยท ๐)))) |
5 | 4 | simprbda 500 |
. . 3
โข ((๐บ โ Grp โง ๐ โ ๐ธ) โ ๐ โ ๐ต) |
6 | | cyggeninv.n |
. . . 4
โข ๐ = (invgโ๐บ) |
7 | 1, 6 | grpinvcl 18805 |
. . 3
โข ((๐บ โ Grp โง ๐ โ ๐ต) โ (๐โ๐) โ ๐ต) |
8 | 5, 7 | syldan 592 |
. 2
โข ((๐บ โ Grp โง ๐ โ ๐ธ) โ (๐โ๐) โ ๐ต) |
9 | 4 | simplbda 501 |
. . 3
โข ((๐บ โ Grp โง ๐ โ ๐ธ) โ โ๐ฆ โ ๐ต โ๐ โ โค ๐ฆ = (๐ ยท ๐)) |
10 | | oveq1 7369 |
. . . . . . 7
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
11 | 10 | eqeq2d 2748 |
. . . . . 6
โข (๐ = ๐ โ (๐ฆ = (๐ ยท ๐) โ ๐ฆ = (๐ ยท ๐))) |
12 | 11 | cbvrexvw 3229 |
. . . . 5
โข
(โ๐ โ
โค ๐ฆ = (๐ ยท ๐) โ โ๐ โ โค ๐ฆ = (๐ ยท ๐)) |
13 | | znegcl 12545 |
. . . . . . . . 9
โข (๐ โ โค โ -๐ โ
โค) |
14 | 13 | adantl 483 |
. . . . . . . 8
โข ((((๐บ โ Grp โง ๐ โ ๐ธ) โง ๐ฆ โ ๐ต) โง ๐ โ โค) โ -๐ โ โค) |
15 | | simpr 486 |
. . . . . . . . . . . 12
โข ((((๐บ โ Grp โง ๐ โ ๐ธ) โง ๐ฆ โ ๐ต) โง ๐ โ โค) โ ๐ โ โค) |
16 | 15 | zcnd 12615 |
. . . . . . . . . . 11
โข ((((๐บ โ Grp โง ๐ โ ๐ธ) โง ๐ฆ โ ๐ต) โง ๐ โ โค) โ ๐ โ โ) |
17 | 16 | negnegd 11510 |
. . . . . . . . . 10
โข ((((๐บ โ Grp โง ๐ โ ๐ธ) โง ๐ฆ โ ๐ต) โง ๐ โ โค) โ --๐ = ๐) |
18 | 17 | oveq1d 7377 |
. . . . . . . . 9
โข ((((๐บ โ Grp โง ๐ โ ๐ธ) โง ๐ฆ โ ๐ต) โง ๐ โ โค) โ (--๐ ยท ๐) = (๐ ยท ๐)) |
19 | | simplll 774 |
. . . . . . . . . 10
โข ((((๐บ โ Grp โง ๐ โ ๐ธ) โง ๐ฆ โ ๐ต) โง ๐ โ โค) โ ๐บ โ Grp) |
20 | 5 | ad2antrr 725 |
. . . . . . . . . 10
โข ((((๐บ โ Grp โง ๐ โ ๐ธ) โง ๐ฆ โ ๐ต) โง ๐ โ โค) โ ๐ โ ๐ต) |
21 | 1, 2, 6 | mulgneg2 18917 |
. . . . . . . . . 10
โข ((๐บ โ Grp โง -๐ โ โค โง ๐ โ ๐ต) โ (--๐ ยท ๐) = (-๐ ยท (๐โ๐))) |
22 | 19, 14, 20, 21 | syl3anc 1372 |
. . . . . . . . 9
โข ((((๐บ โ Grp โง ๐ โ ๐ธ) โง ๐ฆ โ ๐ต) โง ๐ โ โค) โ (--๐ ยท ๐) = (-๐ ยท (๐โ๐))) |
23 | 18, 22 | eqtr3d 2779 |
. . . . . . . 8
โข ((((๐บ โ Grp โง ๐ โ ๐ธ) โง ๐ฆ โ ๐ต) โง ๐ โ โค) โ (๐ ยท ๐) = (-๐ ยท (๐โ๐))) |
24 | | oveq1 7369 |
. . . . . . . . 9
โข (๐ = -๐ โ (๐ ยท (๐โ๐)) = (-๐ ยท (๐โ๐))) |
25 | 24 | rspceeqv 3600 |
. . . . . . . 8
โข ((-๐ โ โค โง (๐ ยท ๐) = (-๐ ยท (๐โ๐))) โ โ๐ โ โค (๐ ยท ๐) = (๐ ยท (๐โ๐))) |
26 | 14, 23, 25 | syl2anc 585 |
. . . . . . 7
โข ((((๐บ โ Grp โง ๐ โ ๐ธ) โง ๐ฆ โ ๐ต) โง ๐ โ โค) โ โ๐ โ โค (๐ ยท ๐) = (๐ ยท (๐โ๐))) |
27 | | eqeq1 2741 |
. . . . . . . 8
โข (๐ฆ = (๐ ยท ๐) โ (๐ฆ = (๐ ยท (๐โ๐)) โ (๐ ยท ๐) = (๐ ยท (๐โ๐)))) |
28 | 27 | rexbidv 3176 |
. . . . . . 7
โข (๐ฆ = (๐ ยท ๐) โ (โ๐ โ โค ๐ฆ = (๐ ยท (๐โ๐)) โ โ๐ โ โค (๐ ยท ๐) = (๐ ยท (๐โ๐)))) |
29 | 26, 28 | syl5ibrcom 247 |
. . . . . 6
โข ((((๐บ โ Grp โง ๐ โ ๐ธ) โง ๐ฆ โ ๐ต) โง ๐ โ โค) โ (๐ฆ = (๐ ยท ๐) โ โ๐ โ โค ๐ฆ = (๐ ยท (๐โ๐)))) |
30 | 29 | rexlimdva 3153 |
. . . . 5
โข (((๐บ โ Grp โง ๐ โ ๐ธ) โง ๐ฆ โ ๐ต) โ (โ๐ โ โค ๐ฆ = (๐ ยท ๐) โ โ๐ โ โค ๐ฆ = (๐ ยท (๐โ๐)))) |
31 | 12, 30 | biimtrid 241 |
. . . 4
โข (((๐บ โ Grp โง ๐ โ ๐ธ) โง ๐ฆ โ ๐ต) โ (โ๐ โ โค ๐ฆ = (๐ ยท ๐) โ โ๐ โ โค ๐ฆ = (๐ ยท (๐โ๐)))) |
32 | 31 | ralimdva 3165 |
. . 3
โข ((๐บ โ Grp โง ๐ โ ๐ธ) โ (โ๐ฆ โ ๐ต โ๐ โ โค ๐ฆ = (๐ ยท ๐) โ โ๐ฆ โ ๐ต โ๐ โ โค ๐ฆ = (๐ ยท (๐โ๐)))) |
33 | 9, 32 | mpd 15 |
. 2
โข ((๐บ โ Grp โง ๐ โ ๐ธ) โ โ๐ฆ โ ๐ต โ๐ โ โค ๐ฆ = (๐ ยท (๐โ๐))) |
34 | 1, 2, 3 | iscyggen2 19665 |
. . 3
โข (๐บ โ Grp โ ((๐โ๐) โ ๐ธ โ ((๐โ๐) โ ๐ต โง โ๐ฆ โ ๐ต โ๐ โ โค ๐ฆ = (๐ ยท (๐โ๐))))) |
35 | 34 | adantr 482 |
. 2
โข ((๐บ โ Grp โง ๐ โ ๐ธ) โ ((๐โ๐) โ ๐ธ โ ((๐โ๐) โ ๐ต โง โ๐ฆ โ ๐ต โ๐ โ โค ๐ฆ = (๐ ยท (๐โ๐))))) |
36 | 8, 33, 35 | mpbir2and 712 |
1
โข ((๐บ โ Grp โง ๐ โ ๐ธ) โ (๐โ๐) โ ๐ธ) |