Step | Hyp | Ref
| Expression |
1 | | simpl2 1192 |
. . 3
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ ๐ด โ ๐) |
2 | | simprl 769 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ ๐ โ 0) |
3 | | simpl3 1193 |
. . . . . . 7
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ ๐ โ
โค) |
4 | 3 | zcnd 12663 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ ๐ โ
โ) |
5 | | abs00 15232 |
. . . . . . 7
โข (๐ โ โ โ
((absโ๐) = 0 โ
๐ = 0)) |
6 | 5 | necon3bbid 2978 |
. . . . . 6
โข (๐ โ โ โ (ยฌ
(absโ๐) = 0 โ
๐ โ 0)) |
7 | 4, 6 | syl 17 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ (ยฌ
(absโ๐) = 0 โ
๐ โ 0)) |
8 | 2, 7 | mpbird 256 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ ยฌ
(absโ๐) =
0) |
9 | | nn0abscl 15255 |
. . . . . . 7
โข (๐ โ โค โ
(absโ๐) โ
โ0) |
10 | 3, 9 | syl 17 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ (absโ๐) โ
โ0) |
11 | | elnn0 12470 |
. . . . . 6
โข
((absโ๐)
โ โ0 โ ((absโ๐) โ โ โจ (absโ๐) = 0)) |
12 | 10, 11 | sylib 217 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ
((absโ๐) โ
โ โจ (absโ๐)
= 0)) |
13 | 12 | ord 862 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ (ยฌ
(absโ๐) โ
โ โ (absโ๐) = 0)) |
14 | 8, 13 | mt3d 148 |
. . 3
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ (absโ๐) โ
โ) |
15 | | simprr 771 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ (๐ ยท ๐ด) = 0 ) |
16 | | oveq1 7412 |
. . . . . 6
โข
((absโ๐) =
๐ โ ((absโ๐) ยท ๐ด) = (๐ ยท ๐ด)) |
17 | 16 | eqeq1d 2734 |
. . . . 5
โข
((absโ๐) =
๐ โ (((absโ๐) ยท ๐ด) = 0 โ (๐ ยท ๐ด) = 0 )) |
18 | 15, 17 | syl5ibrcom 246 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ
((absโ๐) = ๐ โ ((absโ๐) ยท ๐ด) = 0 )) |
19 | | simpl1 1191 |
. . . . . . 7
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ ๐บ โ Grp) |
20 | | odcl.1 |
. . . . . . . 8
โข ๐ = (Baseโ๐บ) |
21 | | odid.3 |
. . . . . . . 8
โข ยท =
(.gโ๐บ) |
22 | | eqid 2732 |
. . . . . . . 8
โข
(invgโ๐บ) = (invgโ๐บ) |
23 | 20, 21, 22 | mulgneg 18966 |
. . . . . . 7
โข ((๐บ โ Grp โง ๐ โ โค โง ๐ด โ ๐) โ (-๐ ยท ๐ด) = ((invgโ๐บ)โ(๐ ยท ๐ด))) |
24 | 19, 3, 1, 23 | syl3anc 1371 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ (-๐ ยท ๐ด) = ((invgโ๐บ)โ(๐ ยท ๐ด))) |
25 | 15 | fveq2d 6892 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ
((invgโ๐บ)โ(๐ ยท ๐ด)) = ((invgโ๐บ)โ 0 )) |
26 | | odid.4 |
. . . . . . . 8
โข 0 =
(0gโ๐บ) |
27 | 26, 22 | grpinvid 18880 |
. . . . . . 7
โข (๐บ โ Grp โ
((invgโ๐บ)โ 0 ) = 0 ) |
28 | 19, 27 | syl 17 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ
((invgโ๐บ)โ 0 ) = 0 ) |
29 | 24, 25, 28 | 3eqtrd 2776 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ (-๐ ยท ๐ด) = 0 ) |
30 | | oveq1 7412 |
. . . . . 6
โข
((absโ๐) =
-๐ โ ((absโ๐) ยท ๐ด) = (-๐ ยท ๐ด)) |
31 | 30 | eqeq1d 2734 |
. . . . 5
โข
((absโ๐) =
-๐ โ
(((absโ๐) ยท ๐ด) = 0 โ (-๐ ยท ๐ด) = 0 )) |
32 | 29, 31 | syl5ibrcom 246 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ
((absโ๐) = -๐ โ ((absโ๐) ยท ๐ด) = 0 )) |
33 | 3 | zred 12662 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ ๐ โ
โ) |
34 | 33 | absord 15358 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ
((absโ๐) = ๐ โจ (absโ๐) = -๐)) |
35 | 18, 32, 34 | mpjaod 858 |
. . 3
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ
((absโ๐) ยท ๐ด) = 0 ) |
36 | | odcl.2 |
. . . 4
โข ๐ = (odโ๐บ) |
37 | 20, 36, 21, 26 | odlem2 19401 |
. . 3
โข ((๐ด โ ๐ โง (absโ๐) โ โ โง ((absโ๐) ยท ๐ด) = 0 ) โ (๐โ๐ด) โ (1...(absโ๐))) |
38 | 1, 14, 35, 37 | syl3anc 1371 |
. 2
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ (๐โ๐ด) โ (1...(absโ๐))) |
39 | | elfznn 13526 |
. 2
โข ((๐โ๐ด) โ (1...(absโ๐)) โ (๐โ๐ด) โ โ) |
40 | 38, 39 | syl 17 |
1
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ (๐โ๐ด) โ โ) |