Step | Hyp | Ref
| Expression |
1 | | df-ne 2942 |
. . . . 5
โข (๐ด โ 0 โ ยฌ ๐ด = 0) |
2 | | biorf 936 |
. . . . 5
โข (ยฌ
๐ด = 0 โ ((๐ต โโ
๐ถ) = 0โ
โ (๐ด = 0 โจ (๐ต โโ
๐ถ) =
0โ))) |
3 | 1, 2 | sylbi 216 |
. . . 4
โข (๐ด โ 0 โ ((๐ต โโ
๐ถ) = 0โ
โ (๐ด = 0 โจ (๐ต โโ
๐ถ) =
0โ))) |
4 | 3 | ad2antlr 726 |
. . 3
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โ ((๐ต โโ ๐ถ) = 0โ โ
(๐ด = 0 โจ (๐ต โโ
๐ถ) =
0โ))) |
5 | 4 | 3adant3 1133 |
. 2
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ต โโ ๐ถ) = 0โ โ
(๐ด = 0 โจ (๐ต โโ
๐ถ) =
0โ))) |
6 | | hvsubeq0 30321 |
. . 3
โข ((๐ต โ โ โง ๐ถ โ โ) โ ((๐ต โโ
๐ถ) = 0โ
โ ๐ต = ๐ถ)) |
7 | 6 | 3adant1 1131 |
. 2
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ต โโ ๐ถ) = 0โ โ
๐ต = ๐ถ)) |
8 | | hvsubdistr1 30302 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด
ยทโ (๐ต โโ ๐ถ)) = ((๐ด ยทโ ๐ต) โโ
(๐ด
ยทโ ๐ถ))) |
9 | 8 | eqeq1d 2735 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด
ยทโ (๐ต โโ ๐ถ)) = 0โ โ
((๐ด
ยทโ ๐ต) โโ (๐ด
ยทโ ๐ถ)) = 0โ)) |
10 | | hvsubcl 30270 |
. . . . . 6
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต โโ
๐ถ) โ
โ) |
11 | | hvmul0or 30278 |
. . . . . 6
โข ((๐ด โ โ โง (๐ต โโ
๐ถ) โ โ) โ
((๐ด
ยทโ (๐ต โโ ๐ถ)) = 0โ โ
(๐ด = 0 โจ (๐ต โโ
๐ถ) =
0โ))) |
12 | 10, 11 | sylan2 594 |
. . . . 5
โข ((๐ด โ โ โง (๐ต โ โ โง ๐ถ โ โ)) โ ((๐ด
ยทโ (๐ต โโ ๐ถ)) = 0โ โ
(๐ด = 0 โจ (๐ต โโ
๐ถ) =
0โ))) |
13 | 12 | 3impb 1116 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด
ยทโ (๐ต โโ ๐ถ)) = 0โ โ
(๐ด = 0 โจ (๐ต โโ
๐ถ) =
0โ))) |
14 | | hvmulcl 30266 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด
ยทโ ๐ต) โ โ) |
15 | 14 | 3adant3 1133 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด
ยทโ ๐ต) โ โ) |
16 | | hvmulcl 30266 |
. . . . . 6
โข ((๐ด โ โ โง ๐ถ โ โ) โ (๐ด
ยทโ ๐ถ) โ โ) |
17 | 16 | 3adant2 1132 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด
ยทโ ๐ถ) โ โ) |
18 | | hvsubeq0 30321 |
. . . . 5
โข (((๐ด
ยทโ ๐ต) โ โ โง (๐ด ยทโ ๐ถ) โ โ) โ
(((๐ด
ยทโ ๐ต) โโ (๐ด
ยทโ ๐ถ)) = 0โ โ (๐ด
ยทโ ๐ต) = (๐ด ยทโ ๐ถ))) |
19 | 15, 17, 18 | syl2anc 585 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (((๐ด
ยทโ ๐ต) โโ (๐ด
ยทโ ๐ถ)) = 0โ โ (๐ด
ยทโ ๐ต) = (๐ด ยทโ ๐ถ))) |
20 | 9, 13, 19 | 3bitr3d 309 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด = 0 โจ (๐ต โโ ๐ถ) = 0โ) โ
(๐ด
ยทโ ๐ต) = (๐ด ยทโ ๐ถ))) |
21 | 20 | 3adant1r 1178 |
. 2
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด = 0 โจ (๐ต โโ ๐ถ) = 0โ) โ
(๐ด
ยทโ ๐ต) = (๐ด ยทโ ๐ถ))) |
22 | 5, 7, 21 | 3bitr3rd 310 |
1
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด ยทโ ๐ต) = (๐ด ยทโ ๐ถ) โ ๐ต = ๐ถ)) |