Step | Hyp | Ref
| Expression |
1 | | normpar.1 |
. . . . 5
โข ๐ด โ โ |
2 | | normpar.2 |
. . . . 5
โข ๐ต โ โ |
3 | 1, 2 | hvsubcli 30005 |
. . . 4
โข (๐ด โโ
๐ต) โ
โ |
4 | 3 | normsqi 30116 |
. . 3
โข
((normโโ(๐ด โโ ๐ต))โ2) = ((๐ด โโ ๐ต)
ยทih (๐ด โโ ๐ต)) |
5 | 1, 2 | hvaddcli 30002 |
. . . 4
โข (๐ด +โ ๐ต) โ
โ |
6 | 5 | normsqi 30116 |
. . 3
โข
((normโโ(๐ด +โ ๐ต))โ2) = ((๐ด +โ ๐ต) ยทih (๐ด +โ ๐ต)) |
7 | 4, 6 | oveq12i 7374 |
. 2
โข
(((normโโ(๐ด โโ ๐ต))โ2) +
((normโโ(๐ด +โ ๐ต))โ2)) = (((๐ด โโ ๐ต)
ยทih (๐ด โโ ๐ต)) + ((๐ด +โ ๐ต) ยทih (๐ด +โ ๐ต))) |
8 | 1 | normsqi 30116 |
. . . . . 6
โข
((normโโ๐ด)โ2) = (๐ด ยทih ๐ด) |
9 | 8 | oveq2i 7373 |
. . . . 5
โข (2
ยท ((normโโ๐ด)โ2)) = (2 ยท (๐ด ยทih ๐ด)) |
10 | 1, 1 | hicli 30065 |
. . . . . 6
โข (๐ด
ยทih ๐ด) โ โ |
11 | 10 | 2timesi 12298 |
. . . . 5
โข (2
ยท (๐ด
ยทih ๐ด)) = ((๐ด ยทih ๐ด) + (๐ด ยทih ๐ด)) |
12 | 9, 11 | eqtri 2765 |
. . . 4
โข (2
ยท ((normโโ๐ด)โ2)) = ((๐ด ยทih ๐ด) + (๐ด ยทih ๐ด)) |
13 | 2 | normsqi 30116 |
. . . . . 6
โข
((normโโ๐ต)โ2) = (๐ต ยทih ๐ต) |
14 | 13 | oveq2i 7373 |
. . . . 5
โข (2
ยท ((normโโ๐ต)โ2)) = (2 ยท (๐ต ยทih ๐ต)) |
15 | 2, 2 | hicli 30065 |
. . . . . 6
โข (๐ต
ยทih ๐ต) โ โ |
16 | 15 | 2timesi 12298 |
. . . . 5
โข (2
ยท (๐ต
ยทih ๐ต)) = ((๐ต ยทih ๐ต) + (๐ต ยทih ๐ต)) |
17 | 14, 16 | eqtri 2765 |
. . . 4
โข (2
ยท ((normโโ๐ต)โ2)) = ((๐ต ยทih ๐ต) + (๐ต ยทih ๐ต)) |
18 | 12, 17 | oveq12i 7374 |
. . 3
โข ((2
ยท ((normโโ๐ด)โ2)) + (2 ยท
((normโโ๐ต)โ2))) = (((๐ด ยทih ๐ด) + (๐ด ยทih ๐ด)) + ((๐ต ยทih ๐ต) + (๐ต ยทih ๐ต))) |
19 | 1, 2, 1, 2 | normlem9 30102 |
. . . . . 6
โข ((๐ด โโ
๐ต)
ยทih (๐ด โโ ๐ต)) = (((๐ด ยทih ๐ด) + (๐ต ยทih ๐ต)) โ ((๐ด ยทih ๐ต) + (๐ต ยทih ๐ด))) |
20 | 10, 15 | addcli 11168 |
. . . . . . 7
โข ((๐ด
ยทih ๐ด) + (๐ต ยทih ๐ต)) โ
โ |
21 | 1, 2 | hicli 30065 |
. . . . . . . 8
โข (๐ด
ยทih ๐ต) โ โ |
22 | 2, 1 | hicli 30065 |
. . . . . . . 8
โข (๐ต
ยทih ๐ด) โ โ |
23 | 21, 22 | addcli 11168 |
. . . . . . 7
โข ((๐ด
ยทih ๐ต) + (๐ต ยทih ๐ด)) โ
โ |
24 | 20, 23 | negsubi 11486 |
. . . . . 6
โข (((๐ด
ยทih ๐ด) + (๐ต ยทih ๐ต)) + -((๐ด ยทih ๐ต) + (๐ต ยทih ๐ด))) = (((๐ด ยทih ๐ด) + (๐ต ยทih ๐ต)) โ ((๐ด ยทih ๐ต) + (๐ต ยทih ๐ด))) |
25 | 19, 24 | eqtr4i 2768 |
. . . . 5
โข ((๐ด โโ
๐ต)
ยทih (๐ด โโ ๐ต)) = (((๐ด ยทih ๐ด) + (๐ต ยทih ๐ต)) + -((๐ด ยทih ๐ต) + (๐ต ยทih ๐ด))) |
26 | 1, 2, 1, 2 | normlem8 30101 |
. . . . 5
โข ((๐ด +โ ๐ต)
ยทih (๐ด +โ ๐ต)) = (((๐ด ยทih ๐ด) + (๐ต ยทih ๐ต)) + ((๐ด ยทih ๐ต) + (๐ต ยทih ๐ด))) |
27 | 25, 26 | oveq12i 7374 |
. . . 4
โข (((๐ด โโ
๐ต)
ยทih (๐ด โโ ๐ต)) + ((๐ด +โ ๐ต) ยทih (๐ด +โ ๐ต))) = ((((๐ด ยทih ๐ด) + (๐ต ยทih ๐ต)) + -((๐ด ยทih ๐ต) + (๐ต ยทih ๐ด))) + (((๐ด ยทih ๐ด) + (๐ต ยทih ๐ต)) + ((๐ด ยทih ๐ต) + (๐ต ยทih ๐ด)))) |
28 | 23 | negcli 11476 |
. . . . 5
โข -((๐ด
ยทih ๐ต) + (๐ต ยทih ๐ด)) โ
โ |
29 | 20, 28, 20, 23 | add42i 11387 |
. . . 4
โข ((((๐ด
ยทih ๐ด) + (๐ต ยทih ๐ต)) + -((๐ด ยทih ๐ต) + (๐ต ยทih ๐ด))) + (((๐ด ยทih ๐ด) + (๐ต ยทih ๐ต)) + ((๐ด ยทih ๐ต) + (๐ต ยทih ๐ด)))) = ((((๐ด ยทih ๐ด) + (๐ต ยทih ๐ต)) + ((๐ด ยทih ๐ด) + (๐ต ยทih ๐ต))) + (((๐ด ยทih ๐ต) + (๐ต ยทih ๐ด)) + -((๐ด ยทih ๐ต) + (๐ต ยทih ๐ด)))) |
30 | 23 | negidi 11477 |
. . . . . 6
โข (((๐ด
ยทih ๐ต) + (๐ต ยทih ๐ด)) + -((๐ด ยทih ๐ต) + (๐ต ยทih ๐ด))) = 0 |
31 | 30 | oveq2i 7373 |
. . . . 5
โข ((((๐ด
ยทih ๐ด) + (๐ต ยทih ๐ต)) + ((๐ด ยทih ๐ด) + (๐ต ยทih ๐ต))) + (((๐ด ยทih ๐ต) + (๐ต ยทih ๐ด)) + -((๐ด ยทih ๐ต) + (๐ต ยทih ๐ด)))) = ((((๐ด ยทih ๐ด) + (๐ต ยทih ๐ต)) + ((๐ด ยทih ๐ด) + (๐ต ยทih ๐ต))) + 0) |
32 | 20, 20 | addcli 11168 |
. . . . . 6
โข (((๐ด
ยทih ๐ด) + (๐ต ยทih ๐ต)) + ((๐ด ยทih ๐ด) + (๐ต ยทih ๐ต))) โ
โ |
33 | 32 | addid1i 11349 |
. . . . 5
โข ((((๐ด
ยทih ๐ด) + (๐ต ยทih ๐ต)) + ((๐ด ยทih ๐ด) + (๐ต ยทih ๐ต))) + 0) = (((๐ด ยทih ๐ด) + (๐ต ยทih ๐ต)) + ((๐ด ยทih ๐ด) + (๐ต ยทih ๐ต))) |
34 | 10, 15, 10, 15 | add4i 11386 |
. . . . 5
โข (((๐ด
ยทih ๐ด) + (๐ต ยทih ๐ต)) + ((๐ด ยทih ๐ด) + (๐ต ยทih ๐ต))) = (((๐ด ยทih ๐ด) + (๐ด ยทih ๐ด)) + ((๐ต ยทih ๐ต) + (๐ต ยทih ๐ต))) |
35 | 31, 33, 34 | 3eqtri 2769 |
. . . 4
โข ((((๐ด
ยทih ๐ด) + (๐ต ยทih ๐ต)) + ((๐ด ยทih ๐ด) + (๐ต ยทih ๐ต))) + (((๐ด ยทih ๐ต) + (๐ต ยทih ๐ด)) + -((๐ด ยทih ๐ต) + (๐ต ยทih ๐ด)))) = (((๐ด ยทih ๐ด) + (๐ด ยทih ๐ด)) + ((๐ต ยทih ๐ต) + (๐ต ยทih ๐ต))) |
36 | 27, 29, 35 | 3eqtri 2769 |
. . 3
โข (((๐ด โโ
๐ต)
ยทih (๐ด โโ ๐ต)) + ((๐ด +โ ๐ต) ยทih (๐ด +โ ๐ต))) = (((๐ด ยทih ๐ด) + (๐ด ยทih ๐ด)) + ((๐ต ยทih ๐ต) + (๐ต ยทih ๐ต))) |
37 | 18, 36 | eqtr4i 2768 |
. 2
โข ((2
ยท ((normโโ๐ด)โ2)) + (2 ยท
((normโโ๐ต)โ2))) = (((๐ด โโ ๐ต)
ยทih (๐ด โโ ๐ต)) + ((๐ด +โ ๐ต) ยทih (๐ด +โ ๐ต))) |
38 | 7, 37 | eqtr4i 2768 |
1
โข
(((normโโ(๐ด โโ ๐ต))โ2) +
((normโโ(๐ด +โ ๐ต))โ2)) = ((2 ยท
((normโโ๐ด)โ2)) + (2 ยท
((normโโ๐ต)โ2))) |