Step | Hyp | Ref
| Expression |
1 | | h1de2.2 |
. . . . . . . . 9
โข ๐ต โ โ |
2 | 1, 1 | hicli 30065 |
. . . . . . . 8
โข (๐ต
ยทih ๐ต) โ โ |
3 | | h1de2.1 |
. . . . . . . 8
โข ๐ด โ โ |
4 | 2, 3 | hvmulcli 29998 |
. . . . . . 7
โข ((๐ต
ยทih ๐ต) ยทโ ๐ด) โ
โ |
5 | 3, 1 | hicli 30065 |
. . . . . . . 8
โข (๐ด
ยทih ๐ต) โ โ |
6 | 5, 1 | hvmulcli 29998 |
. . . . . . 7
โข ((๐ด
ยทih ๐ต) ยทโ ๐ต) โ
โ |
7 | | his2sub 30076 |
. . . . . . 7
โข ((((๐ต
ยทih ๐ต) ยทโ ๐ด) โ โ โง ((๐ด
ยทih ๐ต) ยทโ ๐ต) โ โ โง ๐ด โ โ) โ
((((๐ต
ยทih ๐ต) ยทโ ๐ด) โโ
((๐ด
ยทih ๐ต) ยทโ ๐ต))
ยทih ๐ด) = ((((๐ต ยทih ๐ต)
ยทโ ๐ด) ยทih ๐ด) โ (((๐ด ยทih ๐ต)
ยทโ ๐ต) ยทih ๐ด))) |
8 | 4, 6, 3, 7 | mp3an 1462 |
. . . . . 6
โข ((((๐ต
ยทih ๐ต) ยทโ ๐ด) โโ
((๐ด
ยทih ๐ต) ยทโ ๐ต))
ยทih ๐ด) = ((((๐ต ยทih ๐ต)
ยทโ ๐ด) ยทih ๐ด) โ (((๐ด ยทih ๐ต)
ยทโ ๐ต) ยทih ๐ด)) |
9 | | ax-his3 30068 |
. . . . . . . . 9
โข (((๐ต
ยทih ๐ต) โ โ โง ๐ด โ โ โง ๐ด โ โ) โ (((๐ต ยทih ๐ต)
ยทโ ๐ด) ยทih ๐ด) = ((๐ต ยทih ๐ต) ยท (๐ด ยทih ๐ด))) |
10 | 2, 3, 3, 9 | mp3an 1462 |
. . . . . . . 8
โข (((๐ต
ยทih ๐ต) ยทโ ๐ด)
ยทih ๐ด) = ((๐ต ยทih ๐ต) ยท (๐ด ยทih ๐ด)) |
11 | 3, 3 | hicli 30065 |
. . . . . . . . 9
โข (๐ด
ยทih ๐ด) โ โ |
12 | 2, 11 | mulcomi 11170 |
. . . . . . . 8
โข ((๐ต
ยทih ๐ต) ยท (๐ด ยทih ๐ด)) = ((๐ด ยทih ๐ด) ยท (๐ต ยทih ๐ต)) |
13 | 10, 12 | eqtri 2765 |
. . . . . . 7
โข (((๐ต
ยทih ๐ต) ยทโ ๐ด)
ยทih ๐ด) = ((๐ด ยทih ๐ด) ยท (๐ต ยทih ๐ต)) |
14 | | ax-his3 30068 |
. . . . . . . 8
โข (((๐ด
ยทih ๐ต) โ โ โง ๐ต โ โ โง ๐ด โ โ) โ (((๐ด ยทih ๐ต)
ยทโ ๐ต) ยทih ๐ด) = ((๐ด ยทih ๐ต) ยท (๐ต ยทih ๐ด))) |
15 | 5, 1, 3, 14 | mp3an 1462 |
. . . . . . 7
โข (((๐ด
ยทih ๐ต) ยทโ ๐ต)
ยทih ๐ด) = ((๐ด ยทih ๐ต) ยท (๐ต ยทih ๐ด)) |
16 | 13, 15 | oveq12i 7374 |
. . . . . 6
โข ((((๐ต
ยทih ๐ต) ยทโ ๐ด)
ยทih ๐ด) โ (((๐ด ยทih ๐ต)
ยทโ ๐ต) ยทih ๐ด)) = (((๐ด ยทih ๐ด) ยท (๐ต ยทih ๐ต)) โ ((๐ด ยทih ๐ต) ยท (๐ต ยทih ๐ด))) |
17 | 8, 16 | eqtr2i 2766 |
. . . . 5
โข (((๐ด
ยทih ๐ด) ยท (๐ต ยทih ๐ต)) โ ((๐ด ยทih ๐ต) ยท (๐ต ยทih ๐ด))) = ((((๐ต ยทih ๐ต)
ยทโ ๐ด) โโ ((๐ด
ยทih ๐ต) ยทโ ๐ต))
ยทih ๐ด) |
18 | | his2sub 30076 |
. . . . . . . 8
โข ((((๐ต
ยทih ๐ต) ยทโ ๐ด) โ โ โง ((๐ด
ยทih ๐ต) ยทโ ๐ต) โ โ โง ๐ต โ โ) โ
((((๐ต
ยทih ๐ต) ยทโ ๐ด) โโ
((๐ด
ยทih ๐ต) ยทโ ๐ต))
ยทih ๐ต) = ((((๐ต ยทih ๐ต)
ยทโ ๐ด) ยทih ๐ต) โ (((๐ด ยทih ๐ต)
ยทโ ๐ต) ยทih ๐ต))) |
19 | 4, 6, 1, 18 | mp3an 1462 |
. . . . . . 7
โข ((((๐ต
ยทih ๐ต) ยทโ ๐ด) โโ
((๐ด
ยทih ๐ต) ยทโ ๐ต))
ยทih ๐ต) = ((((๐ต ยทih ๐ต)
ยทโ ๐ด) ยทih ๐ต) โ (((๐ด ยทih ๐ต)
ยทโ ๐ต) ยทih ๐ต)) |
20 | 2, 5 | mulcomi 11170 |
. . . . . . . . 9
โข ((๐ต
ยทih ๐ต) ยท (๐ด ยทih ๐ต)) = ((๐ด ยทih ๐ต) ยท (๐ต ยทih ๐ต)) |
21 | | ax-his3 30068 |
. . . . . . . . . 10
โข (((๐ต
ยทih ๐ต) โ โ โง ๐ด โ โ โง ๐ต โ โ) โ (((๐ต ยทih ๐ต)
ยทโ ๐ด) ยทih ๐ต) = ((๐ต ยทih ๐ต) ยท (๐ด ยทih ๐ต))) |
22 | 2, 3, 1, 21 | mp3an 1462 |
. . . . . . . . 9
โข (((๐ต
ยทih ๐ต) ยทโ ๐ด)
ยทih ๐ต) = ((๐ต ยทih ๐ต) ยท (๐ด ยทih ๐ต)) |
23 | | ax-his3 30068 |
. . . . . . . . . 10
โข (((๐ด
ยทih ๐ต) โ โ โง ๐ต โ โ โง ๐ต โ โ) โ (((๐ด ยทih ๐ต)
ยทโ ๐ต) ยทih ๐ต) = ((๐ด ยทih ๐ต) ยท (๐ต ยทih ๐ต))) |
24 | 5, 1, 1, 23 | mp3an 1462 |
. . . . . . . . 9
โข (((๐ด
ยทih ๐ต) ยทโ ๐ต)
ยทih ๐ต) = ((๐ด ยทih ๐ต) ยท (๐ต ยทih ๐ต)) |
25 | 20, 22, 24 | 3eqtr4i 2775 |
. . . . . . . 8
โข (((๐ต
ยทih ๐ต) ยทโ ๐ด)
ยทih ๐ต) = (((๐ด ยทih ๐ต)
ยทโ ๐ต) ยทih ๐ต) |
26 | 4, 1 | hicli 30065 |
. . . . . . . . 9
โข (((๐ต
ยทih ๐ต) ยทโ ๐ด)
ยทih ๐ต) โ โ |
27 | 6, 1 | hicli 30065 |
. . . . . . . . 9
โข (((๐ด
ยทih ๐ต) ยทโ ๐ต)
ยทih ๐ต) โ โ |
28 | 26, 27 | subeq0i 11488 |
. . . . . . . 8
โข
(((((๐ต
ยทih ๐ต) ยทโ ๐ด)
ยทih ๐ต) โ (((๐ด ยทih ๐ต)
ยทโ ๐ต) ยทih ๐ต)) = 0 โ (((๐ต
ยทih ๐ต) ยทโ ๐ด)
ยทih ๐ต) = (((๐ด ยทih ๐ต)
ยทโ ๐ต) ยทih ๐ต)) |
29 | 25, 28 | mpbir 230 |
. . . . . . 7
โข ((((๐ต
ยทih ๐ต) ยทโ ๐ด)
ยทih ๐ต) โ (((๐ด ยทih ๐ต)
ยทโ ๐ต) ยทih ๐ต)) = 0 |
30 | 19, 29 | eqtri 2765 |
. . . . . 6
โข ((((๐ต
ยทih ๐ต) ยทโ ๐ด) โโ
((๐ด
ยทih ๐ต) ยทโ ๐ต))
ยทih ๐ต) = 0 |
31 | 1 | h1dei 30534 |
. . . . . . . . 9
โข (๐ด โ
(โฅโ(โฅโ{๐ต})) โ (๐ด โ โ โง โ๐ฅ โ โ ((๐ต
ยทih ๐ฅ) = 0 โ (๐ด ยทih ๐ฅ) = 0))) |
32 | 3, 31 | mpbiran 708 |
. . . . . . . 8
โข (๐ด โ
(โฅโ(โฅโ{๐ต})) โ โ๐ฅ โ โ ((๐ต ยทih ๐ฅ) = 0 โ (๐ด ยทih ๐ฅ) = 0)) |
33 | 4, 6 | hvsubcli 30005 |
. . . . . . . . 9
โข (((๐ต
ยทih ๐ต) ยทโ ๐ด) โโ
((๐ด
ยทih ๐ต) ยทโ ๐ต)) โ
โ |
34 | | oveq2 7370 |
. . . . . . . . . . . 12
โข (๐ฅ = (((๐ต ยทih ๐ต)
ยทโ ๐ด) โโ ((๐ด
ยทih ๐ต) ยทโ ๐ต)) โ (๐ต ยทih ๐ฅ) = (๐ต ยทih
(((๐ต
ยทih ๐ต) ยทโ ๐ด) โโ
((๐ด
ยทih ๐ต) ยทโ ๐ต)))) |
35 | 34 | eqeq1d 2739 |
. . . . . . . . . . 11
โข (๐ฅ = (((๐ต ยทih ๐ต)
ยทโ ๐ด) โโ ((๐ด
ยทih ๐ต) ยทโ ๐ต)) โ ((๐ต ยทih ๐ฅ) = 0 โ (๐ต ยทih
(((๐ต
ยทih ๐ต) ยทโ ๐ด) โโ
((๐ด
ยทih ๐ต) ยทโ ๐ต))) = 0)) |
36 | | oveq2 7370 |
. . . . . . . . . . . 12
โข (๐ฅ = (((๐ต ยทih ๐ต)
ยทโ ๐ด) โโ ((๐ด
ยทih ๐ต) ยทโ ๐ต)) โ (๐ด ยทih ๐ฅ) = (๐ด ยทih
(((๐ต
ยทih ๐ต) ยทโ ๐ด) โโ
((๐ด
ยทih ๐ต) ยทโ ๐ต)))) |
37 | 36 | eqeq1d 2739 |
. . . . . . . . . . 11
โข (๐ฅ = (((๐ต ยทih ๐ต)
ยทโ ๐ด) โโ ((๐ด
ยทih ๐ต) ยทโ ๐ต)) โ ((๐ด ยทih ๐ฅ) = 0 โ (๐ด ยทih
(((๐ต
ยทih ๐ต) ยทโ ๐ด) โโ
((๐ด
ยทih ๐ต) ยทโ ๐ต))) = 0)) |
38 | 35, 37 | imbi12d 345 |
. . . . . . . . . 10
โข (๐ฅ = (((๐ต ยทih ๐ต)
ยทโ ๐ด) โโ ((๐ด
ยทih ๐ต) ยทโ ๐ต)) โ (((๐ต ยทih ๐ฅ) = 0 โ (๐ด ยทih ๐ฅ) = 0) โ ((๐ต
ยทih (((๐ต ยทih ๐ต)
ยทโ ๐ด) โโ ((๐ด
ยทih ๐ต) ยทโ ๐ต))) = 0 โ (๐ด
ยทih (((๐ต ยทih ๐ต)
ยทโ ๐ด) โโ ((๐ด
ยทih ๐ต) ยทโ ๐ต))) = 0))) |
39 | 38 | rspcv 3580 |
. . . . . . . . 9
โข ((((๐ต
ยทih ๐ต) ยทโ ๐ด) โโ
((๐ด
ยทih ๐ต) ยทโ ๐ต)) โ โ โ
(โ๐ฅ โ โ
((๐ต
ยทih ๐ฅ) = 0 โ (๐ด ยทih ๐ฅ) = 0) โ ((๐ต
ยทih (((๐ต ยทih ๐ต)
ยทโ ๐ด) โโ ((๐ด
ยทih ๐ต) ยทโ ๐ต))) = 0 โ (๐ด
ยทih (((๐ต ยทih ๐ต)
ยทโ ๐ด) โโ ((๐ด
ยทih ๐ต) ยทโ ๐ต))) = 0))) |
40 | 33, 39 | ax-mp 5 |
. . . . . . . 8
โข
(โ๐ฅ โ
โ ((๐ต
ยทih ๐ฅ) = 0 โ (๐ด ยทih ๐ฅ) = 0) โ ((๐ต
ยทih (((๐ต ยทih ๐ต)
ยทโ ๐ด) โโ ((๐ด
ยทih ๐ต) ยทโ ๐ต))) = 0 โ (๐ด
ยทih (((๐ต ยทih ๐ต)
ยทโ ๐ด) โโ ((๐ด
ยทih ๐ต) ยทโ ๐ต))) = 0)) |
41 | 32, 40 | sylbi 216 |
. . . . . . 7
โข (๐ด โ
(โฅโ(โฅโ{๐ต})) โ ((๐ต ยทih
(((๐ต
ยทih ๐ต) ยทโ ๐ด) โโ
((๐ด
ยทih ๐ต) ยทโ ๐ต))) = 0 โ (๐ด
ยทih (((๐ต ยทih ๐ต)
ยทโ ๐ด) โโ ((๐ด
ยทih ๐ต) ยทโ ๐ต))) = 0)) |
42 | | orthcom 30092 |
. . . . . . . 8
โข
(((((๐ต
ยทih ๐ต) ยทโ ๐ด) โโ
((๐ด
ยทih ๐ต) ยทโ ๐ต)) โ โ โง ๐ต โ โ) โ
(((((๐ต
ยทih ๐ต) ยทโ ๐ด) โโ
((๐ด
ยทih ๐ต) ยทโ ๐ต))
ยทih ๐ต) = 0 โ (๐ต ยทih
(((๐ต
ยทih ๐ต) ยทโ ๐ด) โโ
((๐ด
ยทih ๐ต) ยทโ ๐ต))) = 0)) |
43 | 33, 1, 42 | mp2an 691 |
. . . . . . 7
โข
(((((๐ต
ยทih ๐ต) ยทโ ๐ด) โโ
((๐ด
ยทih ๐ต) ยทโ ๐ต))
ยทih ๐ต) = 0 โ (๐ต ยทih
(((๐ต
ยทih ๐ต) ยทโ ๐ด) โโ
((๐ด
ยทih ๐ต) ยทโ ๐ต))) = 0) |
44 | | orthcom 30092 |
. . . . . . . 8
โข
(((((๐ต
ยทih ๐ต) ยทโ ๐ด) โโ
((๐ด
ยทih ๐ต) ยทโ ๐ต)) โ โ โง ๐ด โ โ) โ
(((((๐ต
ยทih ๐ต) ยทโ ๐ด) โโ
((๐ด
ยทih ๐ต) ยทโ ๐ต))
ยทih ๐ด) = 0 โ (๐ด ยทih
(((๐ต
ยทih ๐ต) ยทโ ๐ด) โโ
((๐ด
ยทih ๐ต) ยทโ ๐ต))) = 0)) |
45 | 33, 3, 44 | mp2an 691 |
. . . . . . 7
โข
(((((๐ต
ยทih ๐ต) ยทโ ๐ด) โโ
((๐ด
ยทih ๐ต) ยทโ ๐ต))
ยทih ๐ด) = 0 โ (๐ด ยทih
(((๐ต
ยทih ๐ต) ยทโ ๐ด) โโ
((๐ด
ยทih ๐ต) ยทโ ๐ต))) = 0) |
46 | 41, 43, 45 | 3imtr4g 296 |
. . . . . 6
โข (๐ด โ
(โฅโ(โฅโ{๐ต})) โ (((((๐ต ยทih ๐ต)
ยทโ ๐ด) โโ ((๐ด
ยทih ๐ต) ยทโ ๐ต))
ยทih ๐ต) = 0 โ ((((๐ต ยทih ๐ต)
ยทโ ๐ด) โโ ((๐ด
ยทih ๐ต) ยทโ ๐ต))
ยทih ๐ด) = 0)) |
47 | 30, 46 | mpi 20 |
. . . . 5
โข (๐ด โ
(โฅโ(โฅโ{๐ต})) โ ((((๐ต ยทih ๐ต)
ยทโ ๐ด) โโ ((๐ด
ยทih ๐ต) ยทโ ๐ต))
ยทih ๐ด) = 0) |
48 | 17, 47 | eqtrid 2789 |
. . . 4
โข (๐ด โ
(โฅโ(โฅโ{๐ต})) โ (((๐ด ยทih ๐ด) ยท (๐ต ยทih ๐ต)) โ ((๐ด ยทih ๐ต) ยท (๐ต ยทih ๐ด))) = 0) |
49 | 11, 2 | mulcli 11169 |
. . . . 5
โข ((๐ด
ยทih ๐ด) ยท (๐ต ยทih ๐ต)) โ
โ |
50 | 1, 3 | hicli 30065 |
. . . . . 6
โข (๐ต
ยทih ๐ด) โ โ |
51 | 5, 50 | mulcli 11169 |
. . . . 5
โข ((๐ด
ยทih ๐ต) ยท (๐ต ยทih ๐ด)) โ
โ |
52 | 49, 51 | subeq0i 11488 |
. . . 4
โข ((((๐ด
ยทih ๐ด) ยท (๐ต ยทih ๐ต)) โ ((๐ด ยทih ๐ต) ยท (๐ต ยทih ๐ด))) = 0 โ ((๐ด
ยทih ๐ด) ยท (๐ต ยทih ๐ต)) = ((๐ด ยทih ๐ต) ยท (๐ต ยทih ๐ด))) |
53 | 48, 52 | sylib 217 |
. . 3
โข (๐ด โ
(โฅโ(โฅโ{๐ต})) โ ((๐ด ยทih ๐ด) ยท (๐ต ยทih ๐ต)) = ((๐ด ยทih ๐ต) ยท (๐ต ยทih ๐ด))) |
54 | 53 | eqcomd 2743 |
. 2
โข (๐ด โ
(โฅโ(โฅโ{๐ต})) โ ((๐ด ยทih ๐ต) ยท (๐ต ยทih ๐ด)) = ((๐ด ยทih ๐ด) ยท (๐ต ยทih ๐ต))) |
55 | 3, 1 | bcseqi 30104 |
. 2
โข (((๐ด
ยทih ๐ต) ยท (๐ต ยทih ๐ด)) = ((๐ด ยทih ๐ด) ยท (๐ต ยทih ๐ต)) โ ((๐ต ยทih ๐ต)
ยทโ ๐ด) = ((๐ด ยทih ๐ต)
ยทโ ๐ต)) |
56 | 54, 55 | sylib 217 |
1
โข (๐ด โ
(โฅโ(โฅโ{๐ต})) โ ((๐ต ยทih ๐ต)
ยทโ ๐ด) = ((๐ด ยทih ๐ต)
ยทโ ๐ต)) |