Step | Hyp | Ref
| Expression |
1 | | oveq2 7366 |
. . . 4
โข ((๐โ๐ต) = (๐ท ยทโ ๐ต) โ (๐ด ยทih (๐โ๐ต)) = (๐ด ยทih (๐ท
ยทโ ๐ต))) |
2 | | eigorthi.4 |
. . . . 5
โข ๐ท โ โ |
3 | | eigorthi.1 |
. . . . 5
โข ๐ด โ โ |
4 | | eigorthi.2 |
. . . . 5
โข ๐ต โ โ |
5 | | his5 30070 |
. . . . 5
โข ((๐ท โ โ โง ๐ด โ โ โง ๐ต โ โ) โ (๐ด
ยทih (๐ท ยทโ ๐ต)) = ((โโ๐ท) ยท (๐ด ยทih ๐ต))) |
6 | 2, 3, 4, 5 | mp3an 1462 |
. . . 4
โข (๐ด
ยทih (๐ท ยทโ ๐ต)) = ((โโ๐ท) ยท (๐ด ยทih ๐ต)) |
7 | 1, 6 | eqtrdi 2789 |
. . 3
โข ((๐โ๐ต) = (๐ท ยทโ ๐ต) โ (๐ด ยทih (๐โ๐ต)) = ((โโ๐ท) ยท (๐ด ยทih ๐ต))) |
8 | | oveq1 7365 |
. . . 4
โข ((๐โ๐ด) = (๐ถ ยทโ ๐ด) โ ((๐โ๐ด) ยทih ๐ต) = ((๐ถ ยทโ ๐ด)
ยทih ๐ต)) |
9 | | eigorthi.3 |
. . . . 5
โข ๐ถ โ โ |
10 | | ax-his3 30068 |
. . . . 5
โข ((๐ถ โ โ โง ๐ด โ โ โง ๐ต โ โ) โ ((๐ถ
ยทโ ๐ด) ยทih ๐ต) = (๐ถ ยท (๐ด ยทih ๐ต))) |
11 | 9, 3, 4, 10 | mp3an 1462 |
. . . 4
โข ((๐ถ
ยทโ ๐ด) ยทih ๐ต) = (๐ถ ยท (๐ด ยทih ๐ต)) |
12 | 8, 11 | eqtrdi 2789 |
. . 3
โข ((๐โ๐ด) = (๐ถ ยทโ ๐ด) โ ((๐โ๐ด) ยทih ๐ต) = (๐ถ ยท (๐ด ยทih ๐ต))) |
13 | 7, 12 | eqeqan12rd 2748 |
. 2
โข (((๐โ๐ด) = (๐ถ ยทโ ๐ด) โง (๐โ๐ต) = (๐ท ยทโ ๐ต)) โ ((๐ด ยทih (๐โ๐ต)) = ((๐โ๐ด) ยทih ๐ต) โ ((โโ๐ท) ยท (๐ด ยทih ๐ต)) = (๐ถ ยท (๐ด ยทih ๐ต)))) |
14 | 3, 4 | hicli 30065 |
. . . . . . . 8
โข (๐ด
ยทih ๐ต) โ โ |
15 | 2 | cjcli 15060 |
. . . . . . . . 9
โข
(โโ๐ท)
โ โ |
16 | | mulcan2 11798 |
. . . . . . . . 9
โข
(((โโ๐ท)
โ โ โง ๐ถ
โ โ โง ((๐ด
ยทih ๐ต) โ โ โง (๐ด ยทih ๐ต) โ 0)) โ
(((โโ๐ท)
ยท (๐ด
ยทih ๐ต)) = (๐ถ ยท (๐ด ยทih ๐ต)) โ (โโ๐ท) = ๐ถ)) |
17 | 15, 9, 16 | mp3an12 1452 |
. . . . . . . 8
โข (((๐ด
ยทih ๐ต) โ โ โง (๐ด ยทih ๐ต) โ 0) โ
(((โโ๐ท)
ยท (๐ด
ยทih ๐ต)) = (๐ถ ยท (๐ด ยทih ๐ต)) โ (โโ๐ท) = ๐ถ)) |
18 | 14, 17 | mpan 689 |
. . . . . . 7
โข ((๐ด
ยทih ๐ต) โ 0 โ (((โโ๐ท) ยท (๐ด ยทih ๐ต)) = (๐ถ ยท (๐ด ยทih ๐ต)) โ (โโ๐ท) = ๐ถ)) |
19 | | eqcom 2740 |
. . . . . . 7
โข
((โโ๐ท)
= ๐ถ โ ๐ถ = (โโ๐ท)) |
20 | 18, 19 | bitrdi 287 |
. . . . . 6
โข ((๐ด
ยทih ๐ต) โ 0 โ (((โโ๐ท) ยท (๐ด ยทih ๐ต)) = (๐ถ ยท (๐ด ยทih ๐ต)) โ ๐ถ = (โโ๐ท))) |
21 | 20 | biimpcd 249 |
. . . . 5
โข
(((โโ๐ท)
ยท (๐ด
ยทih ๐ต)) = (๐ถ ยท (๐ด ยทih ๐ต)) โ ((๐ด ยทih ๐ต) โ 0 โ ๐ถ = (โโ๐ท))) |
22 | 21 | necon1d 2962 |
. . . 4
โข
(((โโ๐ท)
ยท (๐ด
ยทih ๐ต)) = (๐ถ ยท (๐ด ยทih ๐ต)) โ (๐ถ โ (โโ๐ท) โ (๐ด ยทih ๐ต) = 0)) |
23 | 22 | com12 32 |
. . 3
โข (๐ถ โ (โโ๐ท) โ (((โโ๐ท) ยท (๐ด ยทih ๐ต)) = (๐ถ ยท (๐ด ยทih ๐ต)) โ (๐ด ยทih ๐ต) = 0)) |
24 | | oveq2 7366 |
. . . 4
โข ((๐ด
ยทih ๐ต) = 0 โ ((โโ๐ท) ยท (๐ด ยทih ๐ต)) = ((โโ๐ท) ยท 0)) |
25 | | oveq2 7366 |
. . . . 5
โข ((๐ด
ยทih ๐ต) = 0 โ (๐ถ ยท (๐ด ยทih ๐ต)) = (๐ถ ยท 0)) |
26 | 9 | mul01i 11350 |
. . . . . 6
โข (๐ถ ยท 0) =
0 |
27 | 15 | mul01i 11350 |
. . . . . 6
โข
((โโ๐ท)
ยท 0) = 0 |
28 | 26, 27 | eqtr4i 2764 |
. . . . 5
โข (๐ถ ยท 0) =
((โโ๐ท)
ยท 0) |
29 | 25, 28 | eqtrdi 2789 |
. . . 4
โข ((๐ด
ยทih ๐ต) = 0 โ (๐ถ ยท (๐ด ยทih ๐ต)) = ((โโ๐ท) ยท 0)) |
30 | 24, 29 | eqtr4d 2776 |
. . 3
โข ((๐ด
ยทih ๐ต) = 0 โ ((โโ๐ท) ยท (๐ด ยทih ๐ต)) = (๐ถ ยท (๐ด ยทih ๐ต))) |
31 | 23, 30 | impbid1 224 |
. 2
โข (๐ถ โ (โโ๐ท) โ (((โโ๐ท) ยท (๐ด ยทih ๐ต)) = (๐ถ ยท (๐ด ยทih ๐ต)) โ (๐ด ยทih ๐ต) = 0)) |
32 | 13, 31 | sylan9bb 511 |
1
โข ((((๐โ๐ด) = (๐ถ ยทโ ๐ด) โง (๐โ๐ต) = (๐ท ยทโ ๐ต)) โง ๐ถ โ (โโ๐ท)) โ ((๐ด ยทih (๐โ๐ต)) = ((๐โ๐ด) ยทih ๐ต) โ (๐ด ยทih ๐ต) = 0)) |