Step | Hyp | Ref
| Expression |
1 | | fidomndrng.a |
. . . 4
โข (๐ โ ๐ด โ (๐ต โ { 0 })) |
2 | 1 | eldifad 3923 |
. . 3
โข (๐ โ ๐ด โ ๐ต) |
3 | | eldifsni 4751 |
. . . . . . . . . . . 12
โข (๐ด โ (๐ต โ { 0 }) โ ๐ด โ 0 ) |
4 | 1, 3 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ๐ด โ 0 ) |
5 | 4 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โง ๐ฆ โ ๐ต) โง (๐นโ๐ฆ) = 0 ) โ ๐ด โ 0 ) |
6 | | oveq1 7365 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ = ๐ฆ โ (๐ฅ ยท ๐ด) = (๐ฆ ยท ๐ด)) |
7 | | fidomndrng.f |
. . . . . . . . . . . . . . . . 17
โข ๐น = (๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐ด)) |
8 | | ovex 7391 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ ยท ๐ด) โ V |
9 | 6, 7, 8 | fvmpt 6949 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ ๐ต โ (๐นโ๐ฆ) = (๐ฆ ยท ๐ด)) |
10 | 9 | adantl 483 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฆ โ ๐ต) โ (๐นโ๐ฆ) = (๐ฆ ยท ๐ด)) |
11 | 10 | eqeq1d 2735 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฆ โ ๐ต) โ ((๐นโ๐ฆ) = 0 โ (๐ฆ ยท ๐ด) = 0 )) |
12 | | fidomndrng.r |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐
โ Domn) |
13 | 12 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฆ โ ๐ต) โ ๐
โ Domn) |
14 | | simpr 486 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฆ โ ๐ต) โ ๐ฆ โ ๐ต) |
15 | 2 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฆ โ ๐ต) โ ๐ด โ ๐ต) |
16 | | fidomndrng.b |
. . . . . . . . . . . . . . . 16
โข ๐ต = (Baseโ๐
) |
17 | | fidomndrng.t |
. . . . . . . . . . . . . . . 16
โข ยท =
(.rโ๐
) |
18 | | fidomndrng.z |
. . . . . . . . . . . . . . . 16
โข 0 =
(0gโ๐
) |
19 | 16, 17, 18 | domneq0 20783 |
. . . . . . . . . . . . . . 15
โข ((๐
โ Domn โง ๐ฆ โ ๐ต โง ๐ด โ ๐ต) โ ((๐ฆ ยท ๐ด) = 0 โ (๐ฆ = 0 โจ ๐ด = 0 ))) |
20 | 13, 14, 15, 19 | syl3anc 1372 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฆ โ ๐ต) โ ((๐ฆ ยท ๐ด) = 0 โ (๐ฆ = 0 โจ ๐ด = 0 ))) |
21 | 11, 20 | bitrd 279 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฆ โ ๐ต) โ ((๐นโ๐ฆ) = 0 โ (๐ฆ = 0 โจ ๐ด = 0 ))) |
22 | 21 | biimpa 478 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฆ โ ๐ต) โง (๐นโ๐ฆ) = 0 ) โ (๐ฆ = 0 โจ ๐ด = 0 )) |
23 | 22 | ord 863 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฆ โ ๐ต) โง (๐นโ๐ฆ) = 0 ) โ (ยฌ ๐ฆ = 0 โ ๐ด = 0 )) |
24 | 23 | necon1ad 2957 |
. . . . . . . . . 10
โข (((๐ โง ๐ฆ โ ๐ต) โง (๐นโ๐ฆ) = 0 ) โ (๐ด โ 0 โ ๐ฆ = 0 )) |
25 | 5, 24 | mpd 15 |
. . . . . . . . 9
โข (((๐ โง ๐ฆ โ ๐ต) โง (๐นโ๐ฆ) = 0 ) โ ๐ฆ = 0 ) |
26 | 25 | ex 414 |
. . . . . . . 8
โข ((๐ โง ๐ฆ โ ๐ต) โ ((๐นโ๐ฆ) = 0 โ ๐ฆ = 0 )) |
27 | 26 | ralrimiva 3140 |
. . . . . . 7
โข (๐ โ โ๐ฆ โ ๐ต ((๐นโ๐ฆ) = 0 โ ๐ฆ = 0 )) |
28 | | domnring 20782 |
. . . . . . . . . . 11
โข (๐
โ Domn โ ๐
โ Ring) |
29 | 12, 28 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ๐
โ Ring) |
30 | 16, 17 | ringrghm 20034 |
. . . . . . . . . 10
โข ((๐
โ Ring โง ๐ด โ ๐ต) โ (๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐ด)) โ (๐
GrpHom ๐
)) |
31 | 29, 2, 30 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐ด)) โ (๐
GrpHom ๐
)) |
32 | 7, 31 | eqeltrid 2838 |
. . . . . . . 8
โข (๐ โ ๐น โ (๐
GrpHom ๐
)) |
33 | 16, 16, 18, 18 | ghmf1 19042 |
. . . . . . . 8
โข (๐น โ (๐
GrpHom ๐
) โ (๐น:๐ตโ1-1โ๐ต โ โ๐ฆ โ ๐ต ((๐นโ๐ฆ) = 0 โ ๐ฆ = 0 ))) |
34 | 32, 33 | syl 17 |
. . . . . . 7
โข (๐ โ (๐น:๐ตโ1-1โ๐ต โ โ๐ฆ โ ๐ต ((๐นโ๐ฆ) = 0 โ ๐ฆ = 0 ))) |
35 | 27, 34 | mpbird 257 |
. . . . . 6
โข (๐ โ ๐น:๐ตโ1-1โ๐ต) |
36 | | fidomndrng.x |
. . . . . . . 8
โข (๐ โ ๐ต โ Fin) |
37 | | enrefg 8927 |
. . . . . . . 8
โข (๐ต โ Fin โ ๐ต โ ๐ต) |
38 | 36, 37 | syl 17 |
. . . . . . 7
โข (๐ โ ๐ต โ ๐ต) |
39 | | f1finf1o 9218 |
. . . . . . 7
โข ((๐ต โ ๐ต โง ๐ต โ Fin) โ (๐น:๐ตโ1-1โ๐ต โ ๐น:๐ตโ1-1-ontoโ๐ต)) |
40 | 38, 36, 39 | syl2anc 585 |
. . . . . 6
โข (๐ โ (๐น:๐ตโ1-1โ๐ต โ ๐น:๐ตโ1-1-ontoโ๐ต)) |
41 | 35, 40 | mpbid 231 |
. . . . 5
โข (๐ โ ๐น:๐ตโ1-1-ontoโ๐ต) |
42 | | f1ocnv 6797 |
. . . . 5
โข (๐น:๐ตโ1-1-ontoโ๐ต โ โก๐น:๐ตโ1-1-ontoโ๐ต) |
43 | | f1of 6785 |
. . . . 5
โข (โก๐น:๐ตโ1-1-ontoโ๐ต โ โก๐น:๐ตโถ๐ต) |
44 | 41, 42, 43 | 3syl 18 |
. . . 4
โข (๐ โ โก๐น:๐ตโถ๐ต) |
45 | | fidomndrng.o |
. . . . . 6
โข 1 =
(1rโ๐
) |
46 | 16, 45 | ringidcl 19994 |
. . . . 5
โข (๐
โ Ring โ 1 โ ๐ต) |
47 | 29, 46 | syl 17 |
. . . 4
โข (๐ โ 1 โ ๐ต) |
48 | 44, 47 | ffvelcdmd 7037 |
. . 3
โข (๐ โ (โก๐นโ 1 ) โ ๐ต) |
49 | | fidomndrng.d |
. . . 4
โข โฅ =
(โฅrโ๐
) |
50 | 16, 49, 17 | dvdsrmul 20082 |
. . 3
โข ((๐ด โ ๐ต โง (โก๐นโ 1 ) โ ๐ต) โ ๐ด โฅ ((โก๐นโ 1 ) ยท ๐ด)) |
51 | 2, 48, 50 | syl2anc 585 |
. 2
โข (๐ โ ๐ด โฅ ((โก๐นโ 1 ) ยท ๐ด)) |
52 | | oveq1 7365 |
. . . . 5
โข (๐ฆ = (โก๐นโ 1 ) โ (๐ฆ ยท ๐ด) = ((โก๐นโ 1 ) ยท ๐ด)) |
53 | 6 | cbvmptv 5219 |
. . . . . 6
โข (๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐ด)) = (๐ฆ โ ๐ต โฆ (๐ฆ ยท ๐ด)) |
54 | 7, 53 | eqtri 2761 |
. . . . 5
โข ๐น = (๐ฆ โ ๐ต โฆ (๐ฆ ยท ๐ด)) |
55 | | ovex 7391 |
. . . . 5
โข ((โก๐นโ 1 ) ยท ๐ด) โ V |
56 | 52, 54, 55 | fvmpt 6949 |
. . . 4
โข ((โก๐นโ 1 ) โ ๐ต โ (๐นโ(โก๐นโ 1 )) = ((โก๐นโ 1 ) ยท ๐ด)) |
57 | 48, 56 | syl 17 |
. . 3
โข (๐ โ (๐นโ(โก๐นโ 1 )) = ((โก๐นโ 1 ) ยท ๐ด)) |
58 | | f1ocnvfv2 7224 |
. . . 4
โข ((๐น:๐ตโ1-1-ontoโ๐ต โง 1 โ ๐ต) โ (๐นโ(โก๐นโ 1 )) = 1 ) |
59 | 41, 47, 58 | syl2anc 585 |
. . 3
โข (๐ โ (๐นโ(โก๐นโ 1 )) = 1 ) |
60 | 57, 59 | eqtr3d 2775 |
. 2
โข (๐ โ ((โก๐นโ 1 ) ยท ๐ด) = 1 ) |
61 | 51, 60 | breqtrd 5132 |
1
โข (๐ โ ๐ด โฅ 1 ) |