Step | Hyp | Ref
| Expression |
1 | | 3simpc 1151 |
. . 3
โข ((๐
โ Domn โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ โ ๐ต โง ๐ โ ๐ต)) |
2 | | domneq0.b |
. . . . . 6
โข ๐ต = (Baseโ๐
) |
3 | | domneq0.t |
. . . . . 6
โข ยท =
(.rโ๐
) |
4 | | domneq0.z |
. . . . . 6
โข 0 =
(0gโ๐
) |
5 | 2, 3, 4 | isdomn 20780 |
. . . . 5
โข (๐
โ Domn โ (๐
โ NzRing โง
โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐ฅ ยท ๐ฆ) = 0 โ (๐ฅ = 0 โจ ๐ฆ = 0 )))) |
6 | 5 | simprbi 498 |
. . . 4
โข (๐
โ Domn โ
โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐ฅ ยท ๐ฆ) = 0 โ (๐ฅ = 0 โจ ๐ฆ = 0 ))) |
7 | 6 | 3ad2ant1 1134 |
. . 3
โข ((๐
โ Domn โง ๐ โ ๐ต โง ๐ โ ๐ต) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐ฅ ยท ๐ฆ) = 0 โ (๐ฅ = 0 โจ ๐ฆ = 0 ))) |
8 | | oveq1 7365 |
. . . . . 6
โข (๐ฅ = ๐ โ (๐ฅ ยท ๐ฆ) = (๐ ยท ๐ฆ)) |
9 | 8 | eqeq1d 2735 |
. . . . 5
โข (๐ฅ = ๐ โ ((๐ฅ ยท ๐ฆ) = 0 โ (๐ ยท ๐ฆ) = 0 )) |
10 | | eqeq1 2737 |
. . . . . 6
โข (๐ฅ = ๐ โ (๐ฅ = 0 โ ๐ = 0 )) |
11 | 10 | orbi1d 916 |
. . . . 5
โข (๐ฅ = ๐ โ ((๐ฅ = 0 โจ ๐ฆ = 0 ) โ (๐ = 0 โจ ๐ฆ = 0 ))) |
12 | 9, 11 | imbi12d 345 |
. . . 4
โข (๐ฅ = ๐ โ (((๐ฅ ยท ๐ฆ) = 0 โ (๐ฅ = 0 โจ ๐ฆ = 0 )) โ ((๐ ยท ๐ฆ) = 0 โ (๐ = 0 โจ ๐ฆ = 0 )))) |
13 | | oveq2 7366 |
. . . . . 6
โข (๐ฆ = ๐ โ (๐ ยท ๐ฆ) = (๐ ยท ๐)) |
14 | 13 | eqeq1d 2735 |
. . . . 5
โข (๐ฆ = ๐ โ ((๐ ยท ๐ฆ) = 0 โ (๐ ยท ๐) = 0 )) |
15 | | eqeq1 2737 |
. . . . . 6
โข (๐ฆ = ๐ โ (๐ฆ = 0 โ ๐ = 0 )) |
16 | 15 | orbi2d 915 |
. . . . 5
โข (๐ฆ = ๐ โ ((๐ = 0 โจ ๐ฆ = 0 ) โ (๐ = 0 โจ ๐ = 0 ))) |
17 | 14, 16 | imbi12d 345 |
. . . 4
โข (๐ฆ = ๐ โ (((๐ ยท ๐ฆ) = 0 โ (๐ = 0 โจ ๐ฆ = 0 )) โ ((๐ ยท ๐) = 0 โ (๐ = 0 โจ ๐ = 0 )))) |
18 | 12, 17 | rspc2va 3590 |
. . 3
โข (((๐ โ ๐ต โง ๐ โ ๐ต) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐ฅ ยท ๐ฆ) = 0 โ (๐ฅ = 0 โจ ๐ฆ = 0 ))) โ ((๐ ยท ๐) = 0 โ (๐ = 0 โจ ๐ = 0 ))) |
19 | 1, 7, 18 | syl2anc 585 |
. 2
โข ((๐
โ Domn โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ((๐ ยท ๐) = 0 โ (๐ = 0 โจ ๐ = 0 ))) |
20 | | domnring 20782 |
. . . . . 6
โข (๐
โ Domn โ ๐
โ Ring) |
21 | 20 | 3ad2ant1 1134 |
. . . . 5
โข ((๐
โ Domn โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ๐
โ Ring) |
22 | | simp3 1139 |
. . . . 5
โข ((๐
โ Domn โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
23 | 2, 3, 4 | ringlz 20016 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ( 0 ยท ๐) = 0 ) |
24 | 21, 22, 23 | syl2anc 585 |
. . . 4
โข ((๐
โ Domn โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ( 0 ยท ๐) = 0 ) |
25 | | oveq1 7365 |
. . . . 5
โข (๐ = 0 โ (๐ ยท ๐) = ( 0 ยท ๐)) |
26 | 25 | eqeq1d 2735 |
. . . 4
โข (๐ = 0 โ ((๐ ยท ๐) = 0 โ ( 0 ยท ๐) = 0 )) |
27 | 24, 26 | syl5ibrcom 247 |
. . 3
โข ((๐
โ Domn โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ = 0 โ (๐ ยท ๐) = 0 )) |
28 | | simp2 1138 |
. . . . 5
โข ((๐
โ Domn โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
29 | 2, 3, 4 | ringrz 20017 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (๐ ยท 0 ) = 0 ) |
30 | 21, 28, 29 | syl2anc 585 |
. . . 4
โข ((๐
โ Domn โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ ยท 0 ) = 0 ) |
31 | | oveq2 7366 |
. . . . 5
โข (๐ = 0 โ (๐ ยท ๐) = (๐ ยท 0 )) |
32 | 31 | eqeq1d 2735 |
. . . 4
โข (๐ = 0 โ ((๐ ยท ๐) = 0 โ (๐ ยท 0 ) = 0 )) |
33 | 30, 32 | syl5ibrcom 247 |
. . 3
โข ((๐
โ Domn โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ = 0 โ (๐ ยท ๐) = 0 )) |
34 | 27, 33 | jaod 858 |
. 2
โข ((๐
โ Domn โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ((๐ = 0 โจ ๐ = 0 ) โ (๐ ยท ๐) = 0 )) |
35 | 19, 34 | impbid 211 |
1
โข ((๐
โ Domn โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ((๐ ยท ๐) = 0 โ (๐ = 0 โจ ๐ = 0 ))) |