Step | Hyp | Ref
| Expression |
1 | | normlem3.6 |
. . 3
โข ๐ถ = (๐น ยทih ๐น) |
2 | | normlem3.5 |
. . . . . . 7
โข ๐ด = (๐บ ยทih ๐บ) |
3 | | normlem1.3 |
. . . . . . . 8
โข ๐บ โ โ |
4 | 3, 3 | hicli 30372 |
. . . . . . 7
โข (๐บ
ยทih ๐บ) โ โ |
5 | 2, 4 | eqeltri 2829 |
. . . . . 6
โข ๐ด โ โ |
6 | | normlem3.7 |
. . . . . . . 8
โข ๐
โ โ |
7 | 6 | recni 11230 |
. . . . . . 7
โข ๐
โ โ |
8 | 7 | sqcli 14147 |
. . . . . 6
โข (๐
โ2) โ
โ |
9 | 5, 8 | mulcli 11223 |
. . . . 5
โข (๐ด ยท (๐
โ2)) โ โ |
10 | | normlem1.1 |
. . . . . . . 8
โข ๐ โ โ |
11 | | normlem1.2 |
. . . . . . . 8
โข ๐น โ โ |
12 | | normlem2.4 |
. . . . . . . 8
โข ๐ต = -(((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น))) |
13 | 10, 11, 3, 12 | normlem2 30402 |
. . . . . . 7
โข ๐ต โ โ |
14 | 13 | recni 11230 |
. . . . . 6
โข ๐ต โ โ |
15 | 14, 7 | mulcli 11223 |
. . . . 5
โข (๐ต ยท ๐
) โ โ |
16 | 9, 15 | addcomi 11407 |
. . . 4
โข ((๐ด ยท (๐
โ2)) + (๐ต ยท ๐
)) = ((๐ต ยท ๐
) + (๐ด ยท (๐
โ2))) |
17 | 10 | cjcli 15118 |
. . . . . . . . . 10
โข
(โโ๐)
โ โ |
18 | 11, 3 | hicli 30372 |
. . . . . . . . . 10
โข (๐น
ยทih ๐บ) โ โ |
19 | 17, 18 | mulcli 11223 |
. . . . . . . . 9
โข
((โโ๐)
ยท (๐น
ยทih ๐บ)) โ โ |
20 | 3, 11 | hicli 30372 |
. . . . . . . . . 10
โข (๐บ
ยทih ๐น) โ โ |
21 | 10, 20 | mulcli 11223 |
. . . . . . . . 9
โข (๐ ยท (๐บ ยทih ๐น)) โ
โ |
22 | 19, 21 | addcli 11222 |
. . . . . . . 8
โข
(((โโ๐)
ยท (๐น
ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น))) โ
โ |
23 | 22, 7 | mulneg1i 11662 |
. . . . . . 7
โข
(-(((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น))) ยท ๐
) = -((((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น))) ยท ๐
) |
24 | 12 | oveq1i 7421 |
. . . . . . 7
โข (๐ต ยท ๐
) = (-(((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น))) ยท ๐
) |
25 | 22, 7 | mulneg2i 11663 |
. . . . . . 7
โข
((((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น))) ยท -๐
) = -((((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น))) ยท ๐
) |
26 | 23, 24, 25 | 3eqtr4i 2770 |
. . . . . 6
โข (๐ต ยท ๐
) = ((((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น))) ยท -๐
) |
27 | 7 | negcli 11530 |
. . . . . . 7
โข -๐
โ โ |
28 | 19, 21, 27 | adddiri 11229 |
. . . . . 6
โข
((((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น))) ยท -๐
) = ((((โโ๐) ยท (๐น ยทih ๐บ)) ยท -๐
) + ((๐ ยท (๐บ ยทih ๐น)) ยท -๐
)) |
29 | 17, 18, 27 | mul32i 11412 |
. . . . . . 7
โข
(((โโ๐)
ยท (๐น
ยทih ๐บ)) ยท -๐
) = (((โโ๐) ยท -๐
) ยท (๐น ยทih ๐บ)) |
30 | 10, 20, 27 | mul32i 11412 |
. . . . . . 7
โข ((๐ ยท (๐บ ยทih ๐น)) ยท -๐
) = ((๐ ยท -๐
) ยท (๐บ ยทih ๐น)) |
31 | 29, 30 | oveq12i 7423 |
. . . . . 6
โข
((((โโ๐) ยท (๐น ยทih ๐บ)) ยท -๐
) + ((๐ ยท (๐บ ยทih ๐น)) ยท -๐
)) = ((((โโ๐) ยท -๐
) ยท (๐น ยทih ๐บ)) + ((๐ ยท -๐
) ยท (๐บ ยทih ๐น))) |
32 | 26, 28, 31 | 3eqtri 2764 |
. . . . 5
โข (๐ต ยท ๐
) = ((((โโ๐) ยท -๐
) ยท (๐น ยทih ๐บ)) + ((๐ ยท -๐
) ยท (๐บ ยทih ๐น))) |
33 | 2 | oveq2i 7422 |
. . . . . 6
โข ((๐
โ2) ยท ๐ด) = ((๐
โ2) ยท (๐บ ยทih ๐บ)) |
34 | 8, 5, 33 | mulcomli 11225 |
. . . . 5
โข (๐ด ยท (๐
โ2)) = ((๐
โ2) ยท (๐บ ยทih ๐บ)) |
35 | 32, 34 | oveq12i 7423 |
. . . 4
โข ((๐ต ยท ๐
) + (๐ด ยท (๐
โ2))) = (((((โโ๐) ยท -๐
) ยท (๐น ยทih ๐บ)) + ((๐ ยท -๐
) ยท (๐บ ยทih ๐น))) + ((๐
โ2) ยท (๐บ ยทih ๐บ))) |
36 | 17, 27 | mulcli 11223 |
. . . . . 6
โข
((โโ๐)
ยท -๐
) โ
โ |
37 | 36, 18 | mulcli 11223 |
. . . . 5
โข
(((โโ๐)
ยท -๐
) ยท
(๐น
ยทih ๐บ)) โ โ |
38 | 10, 27 | mulcli 11223 |
. . . . . 6
โข (๐ ยท -๐
) โ โ |
39 | 38, 20 | mulcli 11223 |
. . . . 5
โข ((๐ ยท -๐
) ยท (๐บ ยทih ๐น)) โ
โ |
40 | 8, 4 | mulcli 11223 |
. . . . 5
โข ((๐
โ2) ยท (๐บ
ยทih ๐บ)) โ โ |
41 | 37, 39, 40 | addassi 11226 |
. . . 4
โข
(((((โโ๐) ยท -๐
) ยท (๐น ยทih ๐บ)) + ((๐ ยท -๐
) ยท (๐บ ยทih ๐น))) + ((๐
โ2) ยท (๐บ ยทih ๐บ))) = ((((โโ๐) ยท -๐
) ยท (๐น ยทih ๐บ)) + (((๐ ยท -๐
) ยท (๐บ ยทih ๐น)) + ((๐
โ2) ยท (๐บ ยทih ๐บ)))) |
42 | 16, 35, 41 | 3eqtri 2764 |
. . 3
โข ((๐ด ยท (๐
โ2)) + (๐ต ยท ๐
)) = ((((โโ๐) ยท -๐
) ยท (๐น ยทih ๐บ)) + (((๐ ยท -๐
) ยท (๐บ ยทih ๐น)) + ((๐
โ2) ยท (๐บ ยทih ๐บ)))) |
43 | 1, 42 | oveq12i 7423 |
. 2
โข (๐ถ + ((๐ด ยท (๐
โ2)) + (๐ต ยท ๐
))) = ((๐น ยทih ๐น) + ((((โโ๐) ยท -๐
) ยท (๐น ยทih ๐บ)) + (((๐ ยท -๐
) ยท (๐บ ยทih ๐น)) + ((๐
โ2) ยท (๐บ ยทih ๐บ))))) |
44 | 9, 15 | addcli 11222 |
. . 3
โข ((๐ด ยท (๐
โ2)) + (๐ต ยท ๐
)) โ โ |
45 | 11, 11 | hicli 30372 |
. . . 4
โข (๐น
ยทih ๐น) โ โ |
46 | 1, 45 | eqeltri 2829 |
. . 3
โข ๐ถ โ โ |
47 | 44, 46 | addcomi 11407 |
. 2
โข (((๐ด ยท (๐
โ2)) + (๐ต ยท ๐
)) + ๐ถ) = (๐ถ + ((๐ด ยท (๐
โ2)) + (๐ต ยท ๐
))) |
48 | 39, 40 | addcli 11222 |
. . 3
โข (((๐ ยท -๐
) ยท (๐บ ยทih ๐น)) + ((๐
โ2) ยท (๐บ ยทih ๐บ))) โ
โ |
49 | 45, 37, 48 | addassi 11226 |
. 2
โข (((๐น
ยทih ๐น) + (((โโ๐) ยท -๐
) ยท (๐น ยทih ๐บ))) + (((๐ ยท -๐
) ยท (๐บ ยทih ๐น)) + ((๐
โ2) ยท (๐บ ยทih ๐บ)))) = ((๐น ยทih ๐น) + ((((โโ๐) ยท -๐
) ยท (๐น ยทih ๐บ)) + (((๐ ยท -๐
) ยท (๐บ ยทih ๐น)) + ((๐
โ2) ยท (๐บ ยทih ๐บ))))) |
50 | 43, 47, 49 | 3eqtr4i 2770 |
1
โข (((๐ด ยท (๐
โ2)) + (๐ต ยท ๐
)) + ๐ถ) = (((๐น ยทih ๐น) + (((โโ๐) ยท -๐
) ยท (๐น ยทih ๐บ))) + (((๐ ยท -๐
) ยท (๐บ ยทih ๐น)) + ((๐
โ2) ยท (๐บ ยทih ๐บ)))) |