Step | Hyp | Ref
| Expression |
1 | | lnopunilem1.5 |
. . . 4
โข ๐ถ โ โ |
2 | | lnopunilem.3 |
. . . . . 6
โข ๐ด โ โ |
3 | | lnopunilem.1 |
. . . . . . . 8
โข ๐ โ LinOp |
4 | 3 | lnopfi 30960 |
. . . . . . 7
โข ๐: โโถ
โ |
5 | 4 | ffvelcdmi 7038 |
. . . . . 6
โข (๐ด โ โ โ (๐โ๐ด) โ โ) |
6 | 2, 5 | ax-mp 5 |
. . . . 5
โข (๐โ๐ด) โ โ |
7 | | lnopunilem.4 |
. . . . . 6
โข ๐ต โ โ |
8 | 4 | ffvelcdmi 7038 |
. . . . . 6
โข (๐ต โ โ โ (๐โ๐ต) โ โ) |
9 | 7, 8 | ax-mp 5 |
. . . . 5
โข (๐โ๐ต) โ โ |
10 | 6, 9 | hicli 30072 |
. . . 4
โข ((๐โ๐ด) ยทih (๐โ๐ต)) โ โ |
11 | 1, 10 | mulcli 11170 |
. . 3
โข (๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต))) โ โ |
12 | | reval 15000 |
. . 3
โข ((๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต))) โ โ โ
(โโ(๐ถ ยท
((๐โ๐ด) ยทih (๐โ๐ต)))) = (((๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต))) + (โโ(๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต))))) / 2)) |
13 | 11, 12 | ax-mp 5 |
. 2
โข
(โโ(๐ถ
ยท ((๐โ๐ด)
ยทih (๐โ๐ต)))) = (((๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต))) + (โโ(๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต))))) / 2) |
14 | 2, 7 | hicli 30072 |
. . . . 5
โข (๐ด
ยทih ๐ต) โ โ |
15 | 1, 14 | mulcli 11170 |
. . . 4
โข (๐ถ ยท (๐ด ยทih ๐ต)) โ
โ |
16 | | reval 15000 |
. . . 4
โข ((๐ถ ยท (๐ด ยทih ๐ต)) โ โ โ
(โโ(๐ถ ยท
(๐ด
ยทih ๐ต))) = (((๐ถ ยท (๐ด ยทih ๐ต)) + (โโ(๐ถ ยท (๐ด ยทih ๐ต)))) / 2)) |
17 | 15, 16 | ax-mp 5 |
. . 3
โข
(โโ(๐ถ
ยท (๐ด
ยทih ๐ต))) = (((๐ถ ยท (๐ด ยทih ๐ต)) + (โโ(๐ถ ยท (๐ด ยทih ๐ต)))) / 2) |
18 | | lnopunilem.2 |
. . . . . . . . . . . . 13
โข
โ๐ฅ โ
โ (normโโ(๐โ๐ฅ)) = (normโโ๐ฅ) |
19 | | 2fveq3 6851 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = ๐ฆ โ (normโโ(๐โ๐ฅ)) = (normโโ(๐โ๐ฆ))) |
20 | | fveq2 6846 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = ๐ฆ โ (normโโ๐ฅ) =
(normโโ๐ฆ)) |
21 | 19, 20 | eqeq12d 2749 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ฆ โ
((normโโ(๐โ๐ฅ)) = (normโโ๐ฅ) โ
(normโโ(๐โ๐ฆ)) = (normโโ๐ฆ))) |
22 | 21 | cbvralvw 3224 |
. . . . . . . . . . . . 13
โข
(โ๐ฅ โ
โ (normโโ(๐โ๐ฅ)) = (normโโ๐ฅ) โ โ๐ฆ โ โ
(normโโ(๐โ๐ฆ)) = (normโโ๐ฆ)) |
23 | 18, 22 | mpbi 229 |
. . . . . . . . . . . 12
โข
โ๐ฆ โ
โ (normโโ(๐โ๐ฆ)) = (normโโ๐ฆ) |
24 | | oveq1 7368 |
. . . . . . . . . . . . . 14
โข
((normโโ(๐โ๐ฆ)) = (normโโ๐ฆ) โ
((normโโ(๐โ๐ฆ))โ2) =
((normโโ๐ฆ)โ2)) |
25 | 4 | ffvelcdmi 7038 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ โ (๐โ๐ฆ) โ โ) |
26 | | normsq 30125 |
. . . . . . . . . . . . . . . 16
โข ((๐โ๐ฆ) โ โ โ
((normโโ(๐โ๐ฆ))โ2) = ((๐โ๐ฆ) ยทih (๐โ๐ฆ))) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ โ โ
((normโโ(๐โ๐ฆ))โ2) = ((๐โ๐ฆ) ยทih (๐โ๐ฆ))) |
28 | | normsq 30125 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ โ โ
((normโโ๐ฆ)โ2) = (๐ฆ ยทih ๐ฆ)) |
29 | 27, 28 | eqeq12d 2749 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ
(((normโโ(๐โ๐ฆ))โ2) =
((normโโ๐ฆ)โ2) โ ((๐โ๐ฆ) ยทih (๐โ๐ฆ)) = (๐ฆ ยทih ๐ฆ))) |
30 | 24, 29 | imbitrid 243 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ
((normโโ(๐โ๐ฆ)) = (normโโ๐ฆ) โ ((๐โ๐ฆ) ยทih (๐โ๐ฆ)) = (๐ฆ ยทih ๐ฆ))) |
31 | 30 | ralimia 3080 |
. . . . . . . . . . . 12
โข
(โ๐ฆ โ
โ (normโโ(๐โ๐ฆ)) = (normโโ๐ฆ) โ โ๐ฆ โ โ ((๐โ๐ฆ) ยทih (๐โ๐ฆ)) = (๐ฆ ยทih ๐ฆ)) |
32 | 23, 31 | ax-mp 5 |
. . . . . . . . . . 11
โข
โ๐ฆ โ
โ ((๐โ๐ฆ)
ยทih (๐โ๐ฆ)) = (๐ฆ ยทih ๐ฆ) |
33 | | fveq2 6846 |
. . . . . . . . . . . . . 14
โข (๐ฆ = ๐ด โ (๐โ๐ฆ) = (๐โ๐ด)) |
34 | 33, 33 | oveq12d 7379 |
. . . . . . . . . . . . 13
โข (๐ฆ = ๐ด โ ((๐โ๐ฆ) ยทih (๐โ๐ฆ)) = ((๐โ๐ด) ยทih (๐โ๐ด))) |
35 | | id 22 |
. . . . . . . . . . . . . 14
โข (๐ฆ = ๐ด โ ๐ฆ = ๐ด) |
36 | 35, 35 | oveq12d 7379 |
. . . . . . . . . . . . 13
โข (๐ฆ = ๐ด โ (๐ฆ ยทih ๐ฆ) = (๐ด ยทih ๐ด)) |
37 | 34, 36 | eqeq12d 2749 |
. . . . . . . . . . . 12
โข (๐ฆ = ๐ด โ (((๐โ๐ฆ) ยทih (๐โ๐ฆ)) = (๐ฆ ยทih ๐ฆ) โ ((๐โ๐ด) ยทih (๐โ๐ด)) = (๐ด ยทih ๐ด))) |
38 | 37 | rspcv 3579 |
. . . . . . . . . . 11
โข (๐ด โ โ โ
(โ๐ฆ โ โ
((๐โ๐ฆ)
ยทih (๐โ๐ฆ)) = (๐ฆ ยทih ๐ฆ) โ ((๐โ๐ด) ยทih (๐โ๐ด)) = (๐ด ยทih ๐ด))) |
39 | 2, 32, 38 | mp2 9 |
. . . . . . . . . 10
โข ((๐โ๐ด) ยทih (๐โ๐ด)) = (๐ด ยทih ๐ด) |
40 | 39 | oveq2i 7372 |
. . . . . . . . 9
โข
((โโ๐ถ)
ยท ((๐โ๐ด)
ยทih (๐โ๐ด))) = ((โโ๐ถ) ยท (๐ด ยทih ๐ด)) |
41 | 40 | oveq2i 7372 |
. . . . . . . 8
โข (๐ถ ยท ((โโ๐ถ) ยท ((๐โ๐ด) ยทih (๐โ๐ด)))) = (๐ถ ยท ((โโ๐ถ) ยท (๐ด ยทih ๐ด))) |
42 | | fveq2 6846 |
. . . . . . . . . . . 12
โข (๐ฆ = ๐ต โ (๐โ๐ฆ) = (๐โ๐ต)) |
43 | 42, 42 | oveq12d 7379 |
. . . . . . . . . . 11
โข (๐ฆ = ๐ต โ ((๐โ๐ฆ) ยทih (๐โ๐ฆ)) = ((๐โ๐ต) ยทih (๐โ๐ต))) |
44 | | id 22 |
. . . . . . . . . . . 12
โข (๐ฆ = ๐ต โ ๐ฆ = ๐ต) |
45 | 44, 44 | oveq12d 7379 |
. . . . . . . . . . 11
โข (๐ฆ = ๐ต โ (๐ฆ ยทih ๐ฆ) = (๐ต ยทih ๐ต)) |
46 | 43, 45 | eqeq12d 2749 |
. . . . . . . . . 10
โข (๐ฆ = ๐ต โ (((๐โ๐ฆ) ยทih (๐โ๐ฆ)) = (๐ฆ ยทih ๐ฆ) โ ((๐โ๐ต) ยทih (๐โ๐ต)) = (๐ต ยทih ๐ต))) |
47 | 46 | rspcv 3579 |
. . . . . . . . 9
โข (๐ต โ โ โ
(โ๐ฆ โ โ
((๐โ๐ฆ)
ยทih (๐โ๐ฆ)) = (๐ฆ ยทih ๐ฆ) โ ((๐โ๐ต) ยทih (๐โ๐ต)) = (๐ต ยทih ๐ต))) |
48 | 7, 32, 47 | mp2 9 |
. . . . . . . 8
โข ((๐โ๐ต) ยทih (๐โ๐ต)) = (๐ต ยทih ๐ต) |
49 | 41, 48 | oveq12i 7373 |
. . . . . . 7
โข ((๐ถ ยท ((โโ๐ถ) ยท ((๐โ๐ด) ยทih (๐โ๐ด)))) + ((๐โ๐ต) ยทih (๐โ๐ต))) = ((๐ถ ยท ((โโ๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) |
50 | 49 | oveq1i 7371 |
. . . . . 6
โข (((๐ถ ยท ((โโ๐ถ) ยท ((๐โ๐ด) ยทih (๐โ๐ด)))) + ((๐โ๐ต) ยทih (๐โ๐ต))) + ((๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต))) + (โโ(๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต)))))) = (((๐ถ ยท ((โโ๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต))) + (โโ(๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต)))))) |
51 | 1 | cjcli 15063 |
. . . . . . . . . 10
โข
(โโ๐ถ)
โ โ |
52 | 6, 6 | hicli 30072 |
. . . . . . . . . 10
โข ((๐โ๐ด) ยทih (๐โ๐ด)) โ โ |
53 | 51, 52 | mulcli 11170 |
. . . . . . . . 9
โข
((โโ๐ถ)
ยท ((๐โ๐ด)
ยทih (๐โ๐ด))) โ โ |
54 | 1, 53 | mulcli 11170 |
. . . . . . . 8
โข (๐ถ ยท ((โโ๐ถ) ยท ((๐โ๐ด) ยทih (๐โ๐ด)))) โ โ |
55 | 9, 9 | hicli 30072 |
. . . . . . . 8
โข ((๐โ๐ต) ยทih (๐โ๐ต)) โ โ |
56 | 11 | cjcli 15063 |
. . . . . . . 8
โข
(โโ(๐ถ
ยท ((๐โ๐ด)
ยทih (๐โ๐ต)))) โ โ |
57 | 54, 55, 11, 56 | add42i 11388 |
. . . . . . 7
โข (((๐ถ ยท ((โโ๐ถ) ยท ((๐โ๐ด) ยทih (๐โ๐ด)))) + ((๐โ๐ต) ยทih (๐โ๐ต))) + ((๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต))) + (โโ(๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต)))))) = (((๐ถ ยท ((โโ๐ถ) ยท ((๐โ๐ด) ยทih (๐โ๐ด)))) + (๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต)))) + ((โโ(๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต)))) + ((๐โ๐ต) ยทih (๐โ๐ต)))) |
58 | 2, 2 | hicli 30072 |
. . . . . . . . . . 11
โข (๐ด
ยทih ๐ด) โ โ |
59 | 51, 58 | mulcli 11170 |
. . . . . . . . . 10
โข
((โโ๐ถ)
ยท (๐ด
ยทih ๐ด)) โ โ |
60 | 1, 59 | mulcli 11170 |
. . . . . . . . 9
โข (๐ถ ยท ((โโ๐ถ) ยท (๐ด ยทih ๐ด))) โ
โ |
61 | 7, 7 | hicli 30072 |
. . . . . . . . 9
โข (๐ต
ยทih ๐ต) โ โ |
62 | 15 | cjcli 15063 |
. . . . . . . . 9
โข
(โโ(๐ถ
ยท (๐ด
ยทih ๐ต))) โ โ |
63 | 60, 61, 15, 62 | add42i 11388 |
. . . . . . . 8
โข (((๐ถ ยท ((โโ๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท (๐ด ยทih ๐ต)) + (โโ(๐ถ ยท (๐ด ยทih ๐ต))))) = (((๐ถ ยท ((โโ๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ถ ยท (๐ด ยทih ๐ต))) + ((โโ(๐ถ ยท (๐ด ยทih ๐ต))) + (๐ต ยทih ๐ต))) |
64 | 1, 2 | hvmulcli 30005 |
. . . . . . . . . . . 12
โข (๐ถ
ยทโ ๐ด) โ โ |
65 | 64, 7 | hvaddcli 30009 |
. . . . . . . . . . 11
โข ((๐ถ
ยทโ ๐ด) +โ ๐ต) โ โ |
66 | | fveq2 6846 |
. . . . . . . . . . . . . 14
โข (๐ฆ = ((๐ถ ยทโ ๐ด) +โ ๐ต) โ (๐โ๐ฆ) = (๐โ((๐ถ ยทโ ๐ด) +โ ๐ต))) |
67 | 66, 66 | oveq12d 7379 |
. . . . . . . . . . . . 13
โข (๐ฆ = ((๐ถ ยทโ ๐ด) +โ ๐ต) โ ((๐โ๐ฆ) ยทih (๐โ๐ฆ)) = ((๐โ((๐ถ ยทโ ๐ด) +โ ๐ต))
ยทih (๐โ((๐ถ ยทโ ๐ด) +โ ๐ต)))) |
68 | | id 22 |
. . . . . . . . . . . . . 14
โข (๐ฆ = ((๐ถ ยทโ ๐ด) +โ ๐ต) โ ๐ฆ = ((๐ถ ยทโ ๐ด) +โ ๐ต)) |
69 | 68, 68 | oveq12d 7379 |
. . . . . . . . . . . . 13
โข (๐ฆ = ((๐ถ ยทโ ๐ด) +โ ๐ต) โ (๐ฆ ยทih ๐ฆ) = (((๐ถ ยทโ ๐ด) +โ ๐ต)
ยทih ((๐ถ ยทโ ๐ด) +โ ๐ต))) |
70 | 67, 69 | eqeq12d 2749 |
. . . . . . . . . . . 12
โข (๐ฆ = ((๐ถ ยทโ ๐ด) +โ ๐ต) โ (((๐โ๐ฆ) ยทih (๐โ๐ฆ)) = (๐ฆ ยทih ๐ฆ) โ ((๐โ((๐ถ ยทโ ๐ด) +โ ๐ต))
ยทih (๐โ((๐ถ ยทโ ๐ด) +โ ๐ต))) = (((๐ถ ยทโ ๐ด) +โ ๐ต)
ยทih ((๐ถ ยทโ ๐ด) +โ ๐ต)))) |
71 | 70 | rspcv 3579 |
. . . . . . . . . . 11
โข (((๐ถ
ยทโ ๐ด) +โ ๐ต) โ โ โ (โ๐ฆ โ โ ((๐โ๐ฆ) ยทih (๐โ๐ฆ)) = (๐ฆ ยทih ๐ฆ) โ ((๐โ((๐ถ ยทโ ๐ด) +โ ๐ต))
ยทih (๐โ((๐ถ ยทโ ๐ด) +โ ๐ต))) = (((๐ถ ยทโ ๐ด) +โ ๐ต)
ยทih ((๐ถ ยทโ ๐ด) +โ ๐ต)))) |
72 | 65, 32, 71 | mp2 9 |
. . . . . . . . . 10
โข ((๐โ((๐ถ ยทโ ๐ด) +โ ๐ต))
ยทih (๐โ((๐ถ ยทโ ๐ด) +โ ๐ต))) = (((๐ถ ยทโ ๐ด) +โ ๐ต)
ยทih ((๐ถ ยทโ ๐ด) +โ ๐ต)) |
73 | | ax-his2 30074 |
. . . . . . . . . . 11
โข (((๐ถ
ยทโ ๐ด) โ โ โง ๐ต โ โ โง ((๐ถ ยทโ ๐ด) +โ ๐ต) โ โ) โ
(((๐ถ
ยทโ ๐ด) +โ ๐ต) ยทih
((๐ถ
ยทโ ๐ด) +โ ๐ต)) = (((๐ถ ยทโ ๐ด)
ยทih ((๐ถ ยทโ ๐ด) +โ ๐ต)) + (๐ต ยทih ((๐ถ
ยทโ ๐ด) +โ ๐ต)))) |
74 | 64, 7, 65, 73 | mp3an 1462 |
. . . . . . . . . 10
โข (((๐ถ
ยทโ ๐ด) +โ ๐ต) ยทih
((๐ถ
ยทโ ๐ด) +โ ๐ต)) = (((๐ถ ยทโ ๐ด)
ยทih ((๐ถ ยทโ ๐ด) +โ ๐ต)) + (๐ต ยทih ((๐ถ
ยทโ ๐ด) +โ ๐ต))) |
75 | | ax-his3 30075 |
. . . . . . . . . . . . 13
โข ((๐ถ โ โ โง ๐ด โ โ โง ((๐ถ
ยทโ ๐ด) +โ ๐ต) โ โ) โ ((๐ถ ยทโ ๐ด)
ยทih ((๐ถ ยทโ ๐ด) +โ ๐ต)) = (๐ถ ยท (๐ด ยทih ((๐ถ
ยทโ ๐ด) +โ ๐ต)))) |
76 | 1, 2, 65, 75 | mp3an 1462 |
. . . . . . . . . . . 12
โข ((๐ถ
ยทโ ๐ด) ยทih
((๐ถ
ยทโ ๐ด) +โ ๐ต)) = (๐ถ ยท (๐ด ยทih ((๐ถ
ยทโ ๐ด) +โ ๐ต))) |
77 | | his7 30081 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง (๐ถ
ยทโ ๐ด) โ โ โง ๐ต โ โ) โ (๐ด ยทih ((๐ถ
ยทโ ๐ด) +โ ๐ต)) = ((๐ด ยทih (๐ถ
ยทโ ๐ด)) + (๐ด ยทih ๐ต))) |
78 | 2, 64, 7, 77 | mp3an 1462 |
. . . . . . . . . . . . . 14
โข (๐ด
ยทih ((๐ถ ยทโ ๐ด) +โ ๐ต)) = ((๐ด ยทih (๐ถ
ยทโ ๐ด)) + (๐ด ยทih ๐ต)) |
79 | | his5 30077 |
. . . . . . . . . . . . . . . 16
โข ((๐ถ โ โ โง ๐ด โ โ โง ๐ด โ โ) โ (๐ด
ยทih (๐ถ ยทโ ๐ด)) = ((โโ๐ถ) ยท (๐ด ยทih ๐ด))) |
80 | 1, 2, 2, 79 | mp3an 1462 |
. . . . . . . . . . . . . . 15
โข (๐ด
ยทih (๐ถ ยทโ ๐ด)) = ((โโ๐ถ) ยท (๐ด ยทih ๐ด)) |
81 | 80 | oveq1i 7371 |
. . . . . . . . . . . . . 14
โข ((๐ด
ยทih (๐ถ ยทโ ๐ด)) + (๐ด ยทih ๐ต)) = (((โโ๐ถ) ยท (๐ด ยทih ๐ด)) + (๐ด ยทih ๐ต)) |
82 | 78, 81 | eqtri 2761 |
. . . . . . . . . . . . 13
โข (๐ด
ยทih ((๐ถ ยทโ ๐ด) +โ ๐ต)) = (((โโ๐ถ) ยท (๐ด ยทih ๐ด)) + (๐ด ยทih ๐ต)) |
83 | 82 | oveq2i 7372 |
. . . . . . . . . . . 12
โข (๐ถ ยท (๐ด ยทih ((๐ถ
ยทโ ๐ด) +โ ๐ต))) = (๐ถ ยท (((โโ๐ถ) ยท (๐ด ยทih ๐ด)) + (๐ด ยทih ๐ต))) |
84 | 1, 59, 14 | adddii 11175 |
. . . . . . . . . . . 12
โข (๐ถ ยท
(((โโ๐ถ)
ยท (๐ด
ยทih ๐ด)) + (๐ด ยทih ๐ต))) = ((๐ถ ยท ((โโ๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ถ ยท (๐ด ยทih ๐ต))) |
85 | 76, 83, 84 | 3eqtri 2765 |
. . . . . . . . . . 11
โข ((๐ถ
ยทโ ๐ด) ยทih
((๐ถ
ยทโ ๐ด) +โ ๐ต)) = ((๐ถ ยท ((โโ๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ถ ยท (๐ด ยทih ๐ต))) |
86 | | his7 30081 |
. . . . . . . . . . . . 13
โข ((๐ต โ โ โง (๐ถ
ยทโ ๐ด) โ โ โง ๐ต โ โ) โ (๐ต ยทih ((๐ถ
ยทโ ๐ด) +โ ๐ต)) = ((๐ต ยทih (๐ถ
ยทโ ๐ด)) + (๐ต ยทih ๐ต))) |
87 | 7, 64, 7, 86 | mp3an 1462 |
. . . . . . . . . . . 12
โข (๐ต
ยทih ((๐ถ ยทโ ๐ด) +โ ๐ต)) = ((๐ต ยทih (๐ถ
ยทโ ๐ด)) + (๐ต ยทih ๐ต)) |
88 | | his5 30077 |
. . . . . . . . . . . . . . 15
โข ((๐ถ โ โ โง ๐ต โ โ โง ๐ด โ โ) โ (๐ต
ยทih (๐ถ ยทโ ๐ด)) = ((โโ๐ถ) ยท (๐ต ยทih ๐ด))) |
89 | 1, 7, 2, 88 | mp3an 1462 |
. . . . . . . . . . . . . 14
โข (๐ต
ยทih (๐ถ ยทโ ๐ด)) = ((โโ๐ถ) ยท (๐ต ยทih ๐ด)) |
90 | 1, 14 | cjmuli 15083 |
. . . . . . . . . . . . . . 15
โข
(โโ(๐ถ
ยท (๐ด
ยทih ๐ต))) = ((โโ๐ถ) ยท (โโ(๐ด
ยทih ๐ต))) |
91 | 7, 2 | his1i 30091 |
. . . . . . . . . . . . . . . 16
โข (๐ต
ยทih ๐ด) = (โโ(๐ด ยทih ๐ต)) |
92 | 91 | oveq2i 7372 |
. . . . . . . . . . . . . . 15
โข
((โโ๐ถ)
ยท (๐ต
ยทih ๐ด)) = ((โโ๐ถ) ยท (โโ(๐ด
ยทih ๐ต))) |
93 | 90, 92 | eqtr4i 2764 |
. . . . . . . . . . . . . 14
โข
(โโ(๐ถ
ยท (๐ด
ยทih ๐ต))) = ((โโ๐ถ) ยท (๐ต ยทih ๐ด)) |
94 | 89, 93 | eqtr4i 2764 |
. . . . . . . . . . . . 13
โข (๐ต
ยทih (๐ถ ยทโ ๐ด)) = (โโ(๐ถ ยท (๐ด ยทih ๐ต))) |
95 | 94 | oveq1i 7371 |
. . . . . . . . . . . 12
โข ((๐ต
ยทih (๐ถ ยทโ ๐ด)) + (๐ต ยทih ๐ต)) = ((โโ(๐ถ ยท (๐ด ยทih ๐ต))) + (๐ต ยทih ๐ต)) |
96 | 87, 95 | eqtri 2761 |
. . . . . . . . . . 11
โข (๐ต
ยทih ((๐ถ ยทโ ๐ด) +โ ๐ต)) = ((โโ(๐ถ ยท (๐ด ยทih ๐ต))) + (๐ต ยทih ๐ต)) |
97 | 85, 96 | oveq12i 7373 |
. . . . . . . . . 10
โข (((๐ถ
ยทโ ๐ด) ยทih
((๐ถ
ยทโ ๐ด) +โ ๐ต)) + (๐ต ยทih ((๐ถ
ยทโ ๐ด) +โ ๐ต))) = (((๐ถ ยท ((โโ๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ถ ยท (๐ด ยทih ๐ต))) + ((โโ(๐ถ ยท (๐ด ยทih ๐ต))) + (๐ต ยทih ๐ต))) |
98 | 72, 74, 97 | 3eqtrri 2766 |
. . . . . . . . 9
โข (((๐ถ ยท ((โโ๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ถ ยท (๐ด ยทih ๐ต))) + ((โโ(๐ถ ยท (๐ด ยทih ๐ต))) + (๐ต ยทih ๐ต))) = ((๐โ((๐ถ ยทโ ๐ด) +โ ๐ต))
ยทih (๐โ((๐ถ ยทโ ๐ด) +โ ๐ต))) |
99 | 3 | lnopli 30959 |
. . . . . . . . . . . 12
โข ((๐ถ โ โ โง ๐ด โ โ โง ๐ต โ โ) โ (๐โ((๐ถ ยทโ ๐ด) +โ ๐ต)) = ((๐ถ ยทโ (๐โ๐ด)) +โ (๐โ๐ต))) |
100 | 1, 2, 7, 99 | mp3an 1462 |
. . . . . . . . . . 11
โข (๐โ((๐ถ ยทโ ๐ด) +โ ๐ต)) = ((๐ถ ยทโ (๐โ๐ด)) +โ (๐โ๐ต)) |
101 | 100, 100 | oveq12i 7373 |
. . . . . . . . . 10
โข ((๐โ((๐ถ ยทโ ๐ด) +โ ๐ต))
ยทih (๐โ((๐ถ ยทโ ๐ด) +โ ๐ต))) = (((๐ถ ยทโ (๐โ๐ด)) +โ (๐โ๐ต)) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต))) |
102 | 1, 6 | hvmulcli 30005 |
. . . . . . . . . . 11
โข (๐ถ
ยทโ (๐โ๐ด)) โ โ |
103 | 102, 9 | hvaddcli 30009 |
. . . . . . . . . . 11
โข ((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต)) โ โ |
104 | | ax-his2 30074 |
. . . . . . . . . . 11
โข (((๐ถ
ยทโ (๐โ๐ด)) โ โ โง (๐โ๐ต) โ โ โง ((๐ถ ยทโ (๐โ๐ด)) +โ (๐โ๐ต)) โ โ) โ (((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต)) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต))) = (((๐ถ ยทโ (๐โ๐ด)) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต))) + ((๐โ๐ต) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต))))) |
105 | 102, 9, 103, 104 | mp3an 1462 |
. . . . . . . . . 10
โข (((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต)) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต))) = (((๐ถ ยทโ (๐โ๐ด)) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต))) + ((๐โ๐ต) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต)))) |
106 | 101, 105 | eqtri 2761 |
. . . . . . . . 9
โข ((๐โ((๐ถ ยทโ ๐ด) +โ ๐ต))
ยทih (๐โ((๐ถ ยทโ ๐ด) +โ ๐ต))) = (((๐ถ ยทโ (๐โ๐ด)) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต))) + ((๐โ๐ต) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต)))) |
107 | | ax-his3 30075 |
. . . . . . . . . . . 12
โข ((๐ถ โ โ โง (๐โ๐ด) โ โ โง ((๐ถ ยทโ (๐โ๐ด)) +โ (๐โ๐ต)) โ โ) โ ((๐ถ
ยทโ (๐โ๐ด)) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต))) = (๐ถ ยท ((๐โ๐ด) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต))))) |
108 | 1, 6, 103, 107 | mp3an 1462 |
. . . . . . . . . . 11
โข ((๐ถ
ยทโ (๐โ๐ด)) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต))) = (๐ถ ยท ((๐โ๐ด) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต)))) |
109 | | his7 30081 |
. . . . . . . . . . . . . 14
โข (((๐โ๐ด) โ โ โง (๐ถ ยทโ (๐โ๐ด)) โ โ โง (๐โ๐ต) โ โ) โ ((๐โ๐ด) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต))) = (((๐โ๐ด) ยทih (๐ถ
ยทโ (๐โ๐ด))) + ((๐โ๐ด) ยทih (๐โ๐ต)))) |
110 | 6, 102, 9, 109 | mp3an 1462 |
. . . . . . . . . . . . 13
โข ((๐โ๐ด) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต))) = (((๐โ๐ด) ยทih (๐ถ
ยทโ (๐โ๐ด))) + ((๐โ๐ด) ยทih (๐โ๐ต))) |
111 | | his5 30077 |
. . . . . . . . . . . . . . 15
โข ((๐ถ โ โ โง (๐โ๐ด) โ โ โง (๐โ๐ด) โ โ) โ ((๐โ๐ด) ยทih (๐ถ
ยทโ (๐โ๐ด))) = ((โโ๐ถ) ยท ((๐โ๐ด) ยทih (๐โ๐ด)))) |
112 | 1, 6, 6, 111 | mp3an 1462 |
. . . . . . . . . . . . . 14
โข ((๐โ๐ด) ยทih (๐ถ
ยทโ (๐โ๐ด))) = ((โโ๐ถ) ยท ((๐โ๐ด) ยทih (๐โ๐ด))) |
113 | 112 | oveq1i 7371 |
. . . . . . . . . . . . 13
โข (((๐โ๐ด) ยทih (๐ถ
ยทโ (๐โ๐ด))) + ((๐โ๐ด) ยทih (๐โ๐ต))) = (((โโ๐ถ) ยท ((๐โ๐ด) ยทih (๐โ๐ด))) + ((๐โ๐ด) ยทih (๐โ๐ต))) |
114 | 110, 113 | eqtri 2761 |
. . . . . . . . . . . 12
โข ((๐โ๐ด) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต))) = (((โโ๐ถ) ยท ((๐โ๐ด) ยทih (๐โ๐ด))) + ((๐โ๐ด) ยทih (๐โ๐ต))) |
115 | 114 | oveq2i 7372 |
. . . . . . . . . . 11
โข (๐ถ ยท ((๐โ๐ด) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต)))) = (๐ถ ยท (((โโ๐ถ) ยท ((๐โ๐ด) ยทih (๐โ๐ด))) + ((๐โ๐ด) ยทih (๐โ๐ต)))) |
116 | 1, 53, 10 | adddii 11175 |
. . . . . . . . . . 11
โข (๐ถ ยท
(((โโ๐ถ)
ยท ((๐โ๐ด)
ยทih (๐โ๐ด))) + ((๐โ๐ด) ยทih (๐โ๐ต)))) = ((๐ถ ยท ((โโ๐ถ) ยท ((๐โ๐ด) ยทih (๐โ๐ด)))) + (๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต)))) |
117 | 108, 115,
116 | 3eqtri 2765 |
. . . . . . . . . 10
โข ((๐ถ
ยทโ (๐โ๐ด)) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต))) = ((๐ถ ยท ((โโ๐ถ) ยท ((๐โ๐ด) ยทih (๐โ๐ด)))) + (๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต)))) |
118 | | his7 30081 |
. . . . . . . . . . . 12
โข (((๐โ๐ต) โ โ โง (๐ถ ยทโ (๐โ๐ด)) โ โ โง (๐โ๐ต) โ โ) โ ((๐โ๐ต) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต))) = (((๐โ๐ต) ยทih (๐ถ
ยทโ (๐โ๐ด))) + ((๐โ๐ต) ยทih (๐โ๐ต)))) |
119 | 9, 102, 9, 118 | mp3an 1462 |
. . . . . . . . . . 11
โข ((๐โ๐ต) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต))) = (((๐โ๐ต) ยทih (๐ถ
ยทโ (๐โ๐ด))) + ((๐โ๐ต) ยทih (๐โ๐ต))) |
120 | | his5 30077 |
. . . . . . . . . . . . . 14
โข ((๐ถ โ โ โง (๐โ๐ต) โ โ โง (๐โ๐ด) โ โ) โ ((๐โ๐ต) ยทih (๐ถ
ยทโ (๐โ๐ด))) = ((โโ๐ถ) ยท ((๐โ๐ต) ยทih (๐โ๐ด)))) |
121 | 1, 9, 6, 120 | mp3an 1462 |
. . . . . . . . . . . . 13
โข ((๐โ๐ต) ยทih (๐ถ
ยทโ (๐โ๐ด))) = ((โโ๐ถ) ยท ((๐โ๐ต) ยทih (๐โ๐ด))) |
122 | 1, 10 | cjmuli 15083 |
. . . . . . . . . . . . . 14
โข
(โโ(๐ถ
ยท ((๐โ๐ด)
ยทih (๐โ๐ต)))) = ((โโ๐ถ) ยท (โโ((๐โ๐ด) ยทih (๐โ๐ต)))) |
123 | 9, 6 | his1i 30091 |
. . . . . . . . . . . . . . 15
โข ((๐โ๐ต) ยทih (๐โ๐ด)) = (โโ((๐โ๐ด) ยทih (๐โ๐ต))) |
124 | 123 | oveq2i 7372 |
. . . . . . . . . . . . . 14
โข
((โโ๐ถ)
ยท ((๐โ๐ต)
ยทih (๐โ๐ด))) = ((โโ๐ถ) ยท (โโ((๐โ๐ด) ยทih (๐โ๐ต)))) |
125 | 122, 124 | eqtr4i 2764 |
. . . . . . . . . . . . 13
โข
(โโ(๐ถ
ยท ((๐โ๐ด)
ยทih (๐โ๐ต)))) = ((โโ๐ถ) ยท ((๐โ๐ต) ยทih (๐โ๐ด))) |
126 | 121, 125 | eqtr4i 2764 |
. . . . . . . . . . . 12
โข ((๐โ๐ต) ยทih (๐ถ
ยทโ (๐โ๐ด))) = (โโ(๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต)))) |
127 | 126 | oveq1i 7371 |
. . . . . . . . . . 11
โข (((๐โ๐ต) ยทih (๐ถ
ยทโ (๐โ๐ด))) + ((๐โ๐ต) ยทih (๐โ๐ต))) = ((โโ(๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต)))) + ((๐โ๐ต) ยทih (๐โ๐ต))) |
128 | 119, 127 | eqtri 2761 |
. . . . . . . . . 10
โข ((๐โ๐ต) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต))) = ((โโ(๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต)))) + ((๐โ๐ต) ยทih (๐โ๐ต))) |
129 | 117, 128 | oveq12i 7373 |
. . . . . . . . 9
โข (((๐ถ
ยทโ (๐โ๐ด)) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต))) + ((๐โ๐ต) ยทih
((๐ถ
ยทโ (๐โ๐ด)) +โ (๐โ๐ต)))) = (((๐ถ ยท ((โโ๐ถ) ยท ((๐โ๐ด) ยทih (๐โ๐ด)))) + (๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต)))) + ((โโ(๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต)))) + ((๐โ๐ต) ยทih (๐โ๐ต)))) |
130 | 98, 106, 129 | 3eqtrri 2766 |
. . . . . . . 8
โข (((๐ถ ยท ((โโ๐ถ) ยท ((๐โ๐ด) ยทih (๐โ๐ด)))) + (๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต)))) + ((โโ(๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต)))) + ((๐โ๐ต) ยทih (๐โ๐ต)))) = (((๐ถ ยท ((โโ๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ถ ยท (๐ด ยทih ๐ต))) + ((โโ(๐ถ ยท (๐ด ยทih ๐ต))) + (๐ต ยทih ๐ต))) |
131 | 63, 130 | eqtr4i 2764 |
. . . . . . 7
โข (((๐ถ ยท ((โโ๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท (๐ด ยทih ๐ต)) + (โโ(๐ถ ยท (๐ด ยทih ๐ต))))) = (((๐ถ ยท ((โโ๐ถ) ยท ((๐โ๐ด) ยทih (๐โ๐ด)))) + (๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต)))) + ((โโ(๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต)))) + ((๐โ๐ต) ยทih (๐โ๐ต)))) |
132 | 57, 131 | eqtr4i 2764 |
. . . . . 6
โข (((๐ถ ยท ((โโ๐ถ) ยท ((๐โ๐ด) ยทih (๐โ๐ด)))) + ((๐โ๐ต) ยทih (๐โ๐ต))) + ((๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต))) + (โโ(๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต)))))) = (((๐ถ ยท ((โโ๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท (๐ด ยทih ๐ต)) + (โโ(๐ถ ยท (๐ด ยทih ๐ต))))) |
133 | 50, 132 | eqtr3i 2763 |
. . . . 5
โข (((๐ถ ยท ((โโ๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต))) + (โโ(๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต)))))) = (((๐ถ ยท ((โโ๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท (๐ด ยทih ๐ต)) + (โโ(๐ถ ยท (๐ด ยทih ๐ต))))) |
134 | 60, 61 | addcli 11169 |
. . . . . 6
โข ((๐ถ ยท ((โโ๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) โ
โ |
135 | 11, 56 | addcli 11169 |
. . . . . 6
โข ((๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต))) + (โโ(๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต))))) โ โ |
136 | 15, 62 | addcli 11169 |
. . . . . 6
โข ((๐ถ ยท (๐ด ยทih ๐ต)) + (โโ(๐ถ ยท (๐ด ยทih ๐ต)))) โ
โ |
137 | 134, 135,
136 | addcani 11356 |
. . . . 5
โข ((((๐ถ ยท ((โโ๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต))) + (โโ(๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต)))))) = (((๐ถ ยท ((โโ๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท (๐ด ยทih ๐ต)) + (โโ(๐ถ ยท (๐ด ยทih ๐ต))))) โ ((๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต))) + (โโ(๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต))))) = ((๐ถ ยท (๐ด ยทih ๐ต)) + (โโ(๐ถ ยท (๐ด ยทih ๐ต))))) |
138 | 133, 137 | mpbi 229 |
. . . 4
โข ((๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต))) + (โโ(๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต))))) = ((๐ถ ยท (๐ด ยทih ๐ต)) + (โโ(๐ถ ยท (๐ด ยทih ๐ต)))) |
139 | 138 | oveq1i 7371 |
. . 3
โข (((๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต))) + (โโ(๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต))))) / 2) = (((๐ถ ยท (๐ด ยทih ๐ต)) + (โโ(๐ถ ยท (๐ด ยทih ๐ต)))) / 2) |
140 | 17, 139 | eqtr4i 2764 |
. 2
โข
(โโ(๐ถ
ยท (๐ด
ยทih ๐ต))) = (((๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต))) + (โโ(๐ถ ยท ((๐โ๐ด) ยทih (๐โ๐ต))))) / 2) |
141 | 13, 140 | eqtr4i 2764 |
1
โข
(โโ(๐ถ
ยท ((๐โ๐ด)
ยทih (๐โ๐ต)))) = (โโ(๐ถ ยท (๐ด ยทih ๐ต))) |