Step | Hyp | Ref
| Expression |
1 | | df-ne 2935 |
. . . . 5
โข (๐ด โ 0 โ ยฌ ๐ด = 0) |
2 | | biorf 933 |
. . . . 5
โข (ยฌ
๐ด = 0 โ ((๐ต โโ
๐ถ) = 0โ
โ (๐ด = 0 โจ (๐ต โโ
๐ถ) =
0โ))) |
3 | 1, 2 | sylbi 216 |
. . . 4
โข (๐ด โ 0 โ ((๐ต โโ
๐ถ) = 0โ
โ (๐ด = 0 โจ (๐ต โโ
๐ถ) =
0โ))) |
4 | 3 | ad2antlr 724 |
. . 3
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โ ((๐ต โโ ๐ถ) = 0โ โ
(๐ด = 0 โจ (๐ต โโ
๐ถ) =
0โ))) |
5 | 4 | 3adant3 1129 |
. 2
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ต โโ ๐ถ) = 0โ โ
(๐ด = 0 โจ (๐ต โโ
๐ถ) =
0โ))) |
6 | | hvsubeq0 30830 |
. . 3
โข ((๐ต โ โ โง ๐ถ โ โ) โ ((๐ต โโ
๐ถ) = 0โ
โ ๐ต = ๐ถ)) |
7 | 6 | 3adant1 1127 |
. 2
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ต โโ ๐ถ) = 0โ โ
๐ต = ๐ถ)) |
8 | | hvsubdistr1 30811 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด
ยทโ (๐ต โโ ๐ถ)) = ((๐ด ยทโ ๐ต) โโ
(๐ด
ยทโ ๐ถ))) |
9 | 8 | eqeq1d 2728 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด
ยทโ (๐ต โโ ๐ถ)) = 0โ โ
((๐ด
ยทโ ๐ต) โโ (๐ด
ยทโ ๐ถ)) = 0โ)) |
10 | | hvsubcl 30779 |
. . . . . 6
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต โโ
๐ถ) โ
โ) |
11 | | hvmul0or 30787 |
. . . . . 6
โข ((๐ด โ โ โง (๐ต โโ
๐ถ) โ โ) โ
((๐ด
ยทโ (๐ต โโ ๐ถ)) = 0โ โ
(๐ด = 0 โจ (๐ต โโ
๐ถ) =
0โ))) |
12 | 10, 11 | sylan2 592 |
. . . . 5
โข ((๐ด โ โ โง (๐ต โ โ โง ๐ถ โ โ)) โ ((๐ด
ยทโ (๐ต โโ ๐ถ)) = 0โ โ
(๐ด = 0 โจ (๐ต โโ
๐ถ) =
0โ))) |
13 | 12 | 3impb 1112 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด
ยทโ (๐ต โโ ๐ถ)) = 0โ โ
(๐ด = 0 โจ (๐ต โโ
๐ถ) =
0โ))) |
14 | | hvmulcl 30775 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด
ยทโ ๐ต) โ โ) |
15 | 14 | 3adant3 1129 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด
ยทโ ๐ต) โ โ) |
16 | | hvmulcl 30775 |
. . . . . 6
โข ((๐ด โ โ โง ๐ถ โ โ) โ (๐ด
ยทโ ๐ถ) โ โ) |
17 | 16 | 3adant2 1128 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด
ยทโ ๐ถ) โ โ) |
18 | | hvsubeq0 30830 |
. . . . 5
โข (((๐ด
ยทโ ๐ต) โ โ โง (๐ด ยทโ ๐ถ) โ โ) โ
(((๐ด
ยทโ ๐ต) โโ (๐ด
ยทโ ๐ถ)) = 0โ โ (๐ด
ยทโ ๐ต) = (๐ด ยทโ ๐ถ))) |
19 | 15, 17, 18 | syl2anc 583 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (((๐ด
ยทโ ๐ต) โโ (๐ด
ยทโ ๐ถ)) = 0โ โ (๐ด
ยทโ ๐ต) = (๐ด ยทโ ๐ถ))) |
20 | 9, 13, 19 | 3bitr3d 309 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด = 0 โจ (๐ต โโ ๐ถ) = 0โ) โ
(๐ด
ยทโ ๐ต) = (๐ด ยทโ ๐ถ))) |
21 | 20 | 3adant1r 1174 |
. 2
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด = 0 โจ (๐ต โโ ๐ถ) = 0โ) โ
(๐ด
ยทโ ๐ต) = (๐ด ยทโ ๐ถ))) |
22 | 5, 7, 21 | 3bitr3rd 310 |
1
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด ยทโ ๐ต) = (๐ด ยทโ ๐ถ) โ ๐ต = ๐ถ)) |