Step | Hyp | Ref
| Expression |
1 | | odf1.1 |
. . . . . . . 8
โข ๐ = (Baseโ๐บ) |
2 | | odf1.3 |
. . . . . . . 8
โข ยท =
(.gโ๐บ) |
3 | 1, 2 | mulgcl 18971 |
. . . . . . 7
โข ((๐บ โ Grp โง ๐ฅ โ โค โง ๐ด โ ๐) โ (๐ฅ ยท ๐ด) โ ๐) |
4 | 3 | 3expa 1119 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ฅ โ โค) โง ๐ด โ ๐) โ (๐ฅ ยท ๐ด) โ ๐) |
5 | 4 | an32s 651 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ฅ โ โค) โ (๐ฅ ยท ๐ด) โ ๐) |
6 | | odf1.4 |
. . . . 5
โข ๐น = (๐ฅ โ โค โฆ (๐ฅ ยท ๐ด)) |
7 | 5, 6 | fmptd 7114 |
. . . 4
โข ((๐บ โ Grp โง ๐ด โ ๐) โ ๐น:โคโถ๐) |
8 | 7 | adantr 482 |
. . 3
โข (((๐บ โ Grp โง ๐ด โ ๐) โง (๐โ๐ด) = 0) โ ๐น:โคโถ๐) |
9 | | oveq1 7416 |
. . . . . . . . 9
โข (๐ฅ = ๐ฆ โ (๐ฅ ยท ๐ด) = (๐ฆ ยท ๐ด)) |
10 | | ovex 7442 |
. . . . . . . . 9
โข (๐ฅ ยท ๐ด) โ V |
11 | 9, 6, 10 | fvmpt3i 7004 |
. . . . . . . 8
โข (๐ฆ โ โค โ (๐นโ๐ฆ) = (๐ฆ ยท ๐ด)) |
12 | | oveq1 7416 |
. . . . . . . . 9
โข (๐ฅ = ๐ง โ (๐ฅ ยท ๐ด) = (๐ง ยท ๐ด)) |
13 | 12, 6, 10 | fvmpt3i 7004 |
. . . . . . . 8
โข (๐ง โ โค โ (๐นโ๐ง) = (๐ง ยท ๐ด)) |
14 | 11, 13 | eqeqan12d 2747 |
. . . . . . 7
โข ((๐ฆ โ โค โง ๐ง โ โค) โ ((๐นโ๐ฆ) = (๐นโ๐ง) โ (๐ฆ ยท ๐ด) = (๐ง ยท ๐ด))) |
15 | 14 | adantl 483 |
. . . . . 6
โข ((((๐บ โ Grp โง ๐ด โ ๐) โง (๐โ๐ด) = 0) โง (๐ฆ โ โค โง ๐ง โ โค)) โ ((๐นโ๐ฆ) = (๐นโ๐ง) โ (๐ฆ ยท ๐ด) = (๐ง ยท ๐ด))) |
16 | | simplr 768 |
. . . . . . . 8
โข ((((๐บ โ Grp โง ๐ด โ ๐) โง (๐โ๐ด) = 0) โง (๐ฆ โ โค โง ๐ง โ โค)) โ (๐โ๐ด) = 0) |
17 | 16 | breq1d 5159 |
. . . . . . 7
โข ((((๐บ โ Grp โง ๐ด โ ๐) โง (๐โ๐ด) = 0) โง (๐ฆ โ โค โง ๐ง โ โค)) โ ((๐โ๐ด) โฅ (๐ฆ โ ๐ง) โ 0 โฅ (๐ฆ โ ๐ง))) |
18 | | odf1.2 |
. . . . . . . . 9
โข ๐ = (odโ๐บ) |
19 | | eqid 2733 |
. . . . . . . . 9
โข
(0gโ๐บ) = (0gโ๐บ) |
20 | 1, 18, 2, 19 | odcong 19417 |
. . . . . . . 8
โข ((๐บ โ Grp โง ๐ด โ ๐ โง (๐ฆ โ โค โง ๐ง โ โค)) โ ((๐โ๐ด) โฅ (๐ฆ โ ๐ง) โ (๐ฆ ยท ๐ด) = (๐ง ยท ๐ด))) |
21 | 20 | ad4ant124 1174 |
. . . . . . 7
โข ((((๐บ โ Grp โง ๐ด โ ๐) โง (๐โ๐ด) = 0) โง (๐ฆ โ โค โง ๐ง โ โค)) โ ((๐โ๐ด) โฅ (๐ฆ โ ๐ง) โ (๐ฆ ยท ๐ด) = (๐ง ยท ๐ด))) |
22 | | zsubcl 12604 |
. . . . . . . . 9
โข ((๐ฆ โ โค โง ๐ง โ โค) โ (๐ฆ โ ๐ง) โ โค) |
23 | 22 | adantl 483 |
. . . . . . . 8
โข ((((๐บ โ Grp โง ๐ด โ ๐) โง (๐โ๐ด) = 0) โง (๐ฆ โ โค โง ๐ง โ โค)) โ (๐ฆ โ ๐ง) โ โค) |
24 | | 0dvds 16220 |
. . . . . . . 8
โข ((๐ฆ โ ๐ง) โ โค โ (0 โฅ (๐ฆ โ ๐ง) โ (๐ฆ โ ๐ง) = 0)) |
25 | 23, 24 | syl 17 |
. . . . . . 7
โข ((((๐บ โ Grp โง ๐ด โ ๐) โง (๐โ๐ด) = 0) โง (๐ฆ โ โค โง ๐ง โ โค)) โ (0 โฅ (๐ฆ โ ๐ง) โ (๐ฆ โ ๐ง) = 0)) |
26 | 17, 21, 25 | 3bitr3d 309 |
. . . . . 6
โข ((((๐บ โ Grp โง ๐ด โ ๐) โง (๐โ๐ด) = 0) โง (๐ฆ โ โค โง ๐ง โ โค)) โ ((๐ฆ ยท ๐ด) = (๐ง ยท ๐ด) โ (๐ฆ โ ๐ง) = 0)) |
27 | | zcn 12563 |
. . . . . . . 8
โข (๐ฆ โ โค โ ๐ฆ โ
โ) |
28 | | zcn 12563 |
. . . . . . . 8
โข (๐ง โ โค โ ๐ง โ
โ) |
29 | | subeq0 11486 |
. . . . . . . 8
โข ((๐ฆ โ โ โง ๐ง โ โ) โ ((๐ฆ โ ๐ง) = 0 โ ๐ฆ = ๐ง)) |
30 | 27, 28, 29 | syl2an 597 |
. . . . . . 7
โข ((๐ฆ โ โค โง ๐ง โ โค) โ ((๐ฆ โ ๐ง) = 0 โ ๐ฆ = ๐ง)) |
31 | 30 | adantl 483 |
. . . . . 6
โข ((((๐บ โ Grp โง ๐ด โ ๐) โง (๐โ๐ด) = 0) โง (๐ฆ โ โค โง ๐ง โ โค)) โ ((๐ฆ โ ๐ง) = 0 โ ๐ฆ = ๐ง)) |
32 | 15, 26, 31 | 3bitrd 305 |
. . . . 5
โข ((((๐บ โ Grp โง ๐ด โ ๐) โง (๐โ๐ด) = 0) โง (๐ฆ โ โค โง ๐ง โ โค)) โ ((๐นโ๐ฆ) = (๐นโ๐ง) โ ๐ฆ = ๐ง)) |
33 | 32 | biimpd 228 |
. . . 4
โข ((((๐บ โ Grp โง ๐ด โ ๐) โง (๐โ๐ด) = 0) โง (๐ฆ โ โค โง ๐ง โ โค)) โ ((๐นโ๐ฆ) = (๐นโ๐ง) โ ๐ฆ = ๐ง)) |
34 | 33 | ralrimivva 3201 |
. . 3
โข (((๐บ โ Grp โง ๐ด โ ๐) โง (๐โ๐ด) = 0) โ โ๐ฆ โ โค โ๐ง โ โค ((๐นโ๐ฆ) = (๐นโ๐ง) โ ๐ฆ = ๐ง)) |
35 | | dff13 7254 |
. . 3
โข (๐น:โคโ1-1โ๐ โ (๐น:โคโถ๐ โง โ๐ฆ โ โค โ๐ง โ โค ((๐นโ๐ฆ) = (๐นโ๐ง) โ ๐ฆ = ๐ง))) |
36 | 8, 34, 35 | sylanbrc 584 |
. 2
โข (((๐บ โ Grp โง ๐ด โ ๐) โง (๐โ๐ด) = 0) โ ๐น:โคโ1-1โ๐) |
37 | 1, 18, 2, 19 | odid 19406 |
. . . . . 6
โข (๐ด โ ๐ โ ((๐โ๐ด) ยท ๐ด) = (0gโ๐บ)) |
38 | 1, 19, 2 | mulg0 18957 |
. . . . . 6
โข (๐ด โ ๐ โ (0 ยท ๐ด) = (0gโ๐บ)) |
39 | 37, 38 | eqtr4d 2776 |
. . . . 5
โข (๐ด โ ๐ โ ((๐โ๐ด) ยท ๐ด) = (0 ยท ๐ด)) |
40 | 39 | ad2antlr 726 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐น:โคโ1-1โ๐) โ ((๐โ๐ด) ยท ๐ด) = (0 ยท ๐ด)) |
41 | 1, 18 | odcl 19404 |
. . . . . . 7
โข (๐ด โ ๐ โ (๐โ๐ด) โ
โ0) |
42 | 41 | ad2antlr 726 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐น:โคโ1-1โ๐) โ (๐โ๐ด) โ
โ0) |
43 | 42 | nn0zd 12584 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐น:โคโ1-1โ๐) โ (๐โ๐ด) โ โค) |
44 | | oveq1 7416 |
. . . . . 6
โข (๐ฅ = (๐โ๐ด) โ (๐ฅ ยท ๐ด) = ((๐โ๐ด) ยท ๐ด)) |
45 | 44, 6, 10 | fvmpt3i 7004 |
. . . . 5
โข ((๐โ๐ด) โ โค โ (๐นโ(๐โ๐ด)) = ((๐โ๐ด) ยท ๐ด)) |
46 | 43, 45 | syl 17 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐น:โคโ1-1โ๐) โ (๐นโ(๐โ๐ด)) = ((๐โ๐ด) ยท ๐ด)) |
47 | | 0zd 12570 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐น:โคโ1-1โ๐) โ 0 โ โค) |
48 | | oveq1 7416 |
. . . . . 6
โข (๐ฅ = 0 โ (๐ฅ ยท ๐ด) = (0 ยท ๐ด)) |
49 | 48, 6, 10 | fvmpt3i 7004 |
. . . . 5
โข (0 โ
โค โ (๐นโ0)
= (0 ยท ๐ด)) |
50 | 47, 49 | syl 17 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐น:โคโ1-1โ๐) โ (๐นโ0) = (0 ยท ๐ด)) |
51 | 40, 46, 50 | 3eqtr4d 2783 |
. . 3
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐น:โคโ1-1โ๐) โ (๐นโ(๐โ๐ด)) = (๐นโ0)) |
52 | | simpr 486 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐น:โคโ1-1โ๐) โ ๐น:โคโ1-1โ๐) |
53 | | f1fveq 7261 |
. . . 4
โข ((๐น:โคโ1-1โ๐ โง ((๐โ๐ด) โ โค โง 0 โ โค))
โ ((๐นโ(๐โ๐ด)) = (๐นโ0) โ (๐โ๐ด) = 0)) |
54 | 52, 43, 47, 53 | syl12anc 836 |
. . 3
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐น:โคโ1-1โ๐) โ ((๐นโ(๐โ๐ด)) = (๐นโ0) โ (๐โ๐ด) = 0)) |
55 | 51, 54 | mpbid 231 |
. 2
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐น:โคโ1-1โ๐) โ (๐โ๐ด) = 0) |
56 | 36, 55 | impbida 800 |
1
โข ((๐บ โ Grp โง ๐ด โ ๐) โ ((๐โ๐ด) = 0 โ ๐น:โคโ1-1โ๐)) |