Step | Hyp | Ref
| Expression |
1 | | ringinvnzdiv.a |
. . 3
โข (๐ โ โ๐ โ ๐ต (๐ ยท ๐) = 1 ) |
2 | | ringinvnzdiv.r |
. . . . . . . . 9
โข (๐ โ ๐
โ Ring) |
3 | | ringinvnzdiv.y |
. . . . . . . . 9
โข (๐ โ ๐ โ ๐ต) |
4 | | ringinvnzdiv.b |
. . . . . . . . . 10
โข ๐ต = (Baseโ๐
) |
5 | | ringinvnzdiv.t |
. . . . . . . . . 10
โข ยท =
(.rโ๐
) |
6 | | ringinvnzdiv.u |
. . . . . . . . . 10
โข 1 =
(1rโ๐
) |
7 | 4, 5, 6 | ringlidm 20000 |
. . . . . . . . 9
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ( 1 ยท ๐) = ๐) |
8 | 2, 3, 7 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ ( 1 ยท ๐) = ๐) |
9 | 8 | eqcomd 2739 |
. . . . . . 7
โข (๐ โ ๐ = ( 1 ยท ๐)) |
10 | 9 | ad3antrrr 729 |
. . . . . 6
โข ((((๐ โง ๐ โ ๐ต) โง (๐ ยท ๐) = 1 ) โง (๐ ยท ๐) = 0 ) โ ๐ = ( 1 ยท ๐)) |
11 | | oveq1 7368 |
. . . . . . . . . 10
โข ( 1 = (๐ ยท ๐) โ ( 1 ยท ๐) = ((๐ ยท ๐) ยท ๐)) |
12 | 11 | eqcoms 2741 |
. . . . . . . . 9
โข ((๐ ยท ๐) = 1 โ ( 1 ยท ๐) = ((๐ ยท ๐) ยท ๐)) |
13 | 12 | adantl 483 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐ต) โง (๐ ยท ๐) = 1 ) โ ( 1 ยท ๐) = ((๐ ยท ๐) ยท ๐)) |
14 | 2 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ต) โ ๐
โ Ring) |
15 | | simpr 486 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
16 | | ringinvnzdiv.x |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ ๐ต) |
17 | 16 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
18 | 3 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
19 | 15, 17, 18 | 3jca 1129 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ต) โ (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) |
20 | 14, 19 | jca 513 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ต) โ (๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต))) |
21 | 20 | adantr 482 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐ต) โง (๐ ยท ๐) = 1 ) โ (๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต))) |
22 | 4, 5 | ringass 19992 |
. . . . . . . . 9
โข ((๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐ต) โง (๐ ยท ๐) = 1 ) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) |
24 | 13, 23 | eqtrd 2773 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐ต) โง (๐ ยท ๐) = 1 ) โ ( 1 ยท ๐) = (๐ ยท (๐ ยท ๐))) |
25 | 24 | adantr 482 |
. . . . . 6
โข ((((๐ โง ๐ โ ๐ต) โง (๐ ยท ๐) = 1 ) โง (๐ ยท ๐) = 0 ) โ ( 1 ยท ๐) = (๐ ยท (๐ ยท ๐))) |
26 | | oveq2 7369 |
. . . . . . 7
โข ((๐ ยท ๐) = 0 โ (๐ ยท (๐ ยท ๐)) = (๐ ยท 0 )) |
27 | | ringinvnzdiv.z |
. . . . . . . . . 10
โข 0 =
(0gโ๐
) |
28 | 4, 5, 27 | ringrz 20020 |
. . . . . . . . 9
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (๐ ยท 0 ) = 0 ) |
29 | 2, 28 | sylan 581 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ต) โ (๐ ยท 0 ) = 0 ) |
30 | 29 | adantr 482 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐ต) โง (๐ ยท ๐) = 1 ) โ (๐ ยท 0 ) = 0 ) |
31 | 26, 30 | sylan9eqr 2795 |
. . . . . 6
โข ((((๐ โง ๐ โ ๐ต) โง (๐ ยท ๐) = 1 ) โง (๐ ยท ๐) = 0 ) โ (๐ ยท (๐ ยท ๐)) = 0 ) |
32 | 10, 25, 31 | 3eqtrd 2777 |
. . . . 5
โข ((((๐ โง ๐ โ ๐ต) โง (๐ ยท ๐) = 1 ) โง (๐ ยท ๐) = 0 ) โ ๐ = 0 ) |
33 | 32 | exp31 421 |
. . . 4
โข ((๐ โง ๐ โ ๐ต) โ ((๐ ยท ๐) = 1 โ ((๐ ยท ๐) = 0 โ ๐ = 0 ))) |
34 | 33 | rexlimdva 3149 |
. . 3
โข (๐ โ (โ๐ โ ๐ต (๐ ยท ๐) = 1 โ ((๐ ยท ๐) = 0 โ ๐ = 0 ))) |
35 | 1, 34 | mpd 15 |
. 2
โข (๐ โ ((๐ ยท ๐) = 0 โ ๐ = 0 )) |
36 | | oveq2 7369 |
. . . 4
โข (๐ = 0 โ (๐ ยท ๐) = (๐ ยท 0 )) |
37 | 4, 5, 27 | ringrz 20020 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (๐ ยท 0 ) = 0 ) |
38 | 2, 16, 37 | syl2anc 585 |
. . . 4
โข (๐ โ (๐ ยท 0 ) = 0 ) |
39 | 36, 38 | sylan9eqr 2795 |
. . 3
โข ((๐ โง ๐ = 0 ) โ (๐ ยท ๐) = 0 ) |
40 | 39 | ex 414 |
. 2
โข (๐ โ (๐ = 0 โ (๐ ยท ๐) = 0 )) |
41 | 35, 40 | impbid 211 |
1
โข (๐ โ ((๐ ยท ๐) = 0 โ ๐ = 0 )) |