Step | Hyp | Ref
| Expression |
1 | | normlem1.1 |
. . . 4
โข ๐ โ โ |
2 | | normlem1.4 |
. . . . 5
โข ๐
โ โ |
3 | 2 | recni 11177 |
. . . 4
โข ๐
โ โ |
4 | 1, 3 | mulcli 11170 |
. . 3
โข (๐ ยท ๐
) โ โ |
5 | | normlem1.2 |
. . 3
โข ๐น โ โ |
6 | | normlem1.3 |
. . 3
โข ๐บ โ โ |
7 | 4, 5, 6 | normlem0 30100 |
. 2
โข ((๐น โโ
((๐ ยท ๐
)
ยทโ ๐บ)) ยทih
(๐น
โโ ((๐ ยท ๐
) ยทโ ๐บ))) = (((๐น ยทih ๐น) + (-(โโ(๐ ยท ๐
)) ยท (๐น ยทih ๐บ))) + ((-(๐ ยท ๐
) ยท (๐บ ยทih ๐น)) + (((๐ ยท ๐
) ยท (โโ(๐ ยท ๐
))) ยท (๐บ ยทih ๐บ)))) |
8 | 1, 3 | cjmuli 15083 |
. . . . . . . 8
โข
(โโ(๐
ยท ๐
)) =
((โโ๐)
ยท (โโ๐
)) |
9 | 3 | cjrebi 15068 |
. . . . . . . . . 10
โข (๐
โ โ โ
(โโ๐
) = ๐
) |
10 | 2, 9 | mpbi 229 |
. . . . . . . . 9
โข
(โโ๐
) =
๐
|
11 | 10 | oveq2i 7372 |
. . . . . . . 8
โข
((โโ๐)
ยท (โโ๐
)) = ((โโ๐) ยท ๐
) |
12 | 8, 11 | eqtri 2761 |
. . . . . . 7
โข
(โโ(๐
ยท ๐
)) =
((โโ๐)
ยท ๐
) |
13 | 12 | negeqi 11402 |
. . . . . 6
โข
-(โโ(๐
ยท ๐
)) =
-((โโ๐)
ยท ๐
) |
14 | 1 | cjcli 15063 |
. . . . . . 7
โข
(โโ๐)
โ โ |
15 | 14, 3 | mulneg2i 11610 |
. . . . . 6
โข
((โโ๐)
ยท -๐
) =
-((โโ๐)
ยท ๐
) |
16 | 13, 15 | eqtr4i 2764 |
. . . . 5
โข
-(โโ(๐
ยท ๐
)) =
((โโ๐)
ยท -๐
) |
17 | 16 | oveq1i 7371 |
. . . 4
โข
(-(โโ(๐
ยท ๐
)) ยท
(๐น
ยทih ๐บ)) = (((โโ๐) ยท -๐
) ยท (๐น ยทih ๐บ)) |
18 | 17 | oveq2i 7372 |
. . 3
โข ((๐น
ยทih ๐น) + (-(โโ(๐ ยท ๐
)) ยท (๐น ยทih ๐บ))) = ((๐น ยทih ๐น) + (((โโ๐) ยท -๐
) ยท (๐น ยทih ๐บ))) |
19 | 1, 3 | mulneg2i 11610 |
. . . . . 6
โข (๐ ยท -๐
) = -(๐ ยท ๐
) |
20 | 19 | eqcomi 2742 |
. . . . 5
โข -(๐ ยท ๐
) = (๐ ยท -๐
) |
21 | 20 | oveq1i 7371 |
. . . 4
โข (-(๐ ยท ๐
) ยท (๐บ ยทih ๐น)) = ((๐ ยท -๐
) ยท (๐บ ยทih ๐น)) |
22 | 8 | oveq2i 7372 |
. . . . . . 7
โข ((๐ ยท ๐
) ยท (โโ(๐ ยท ๐
))) = ((๐ ยท ๐
) ยท ((โโ๐) ยท (โโ๐
))) |
23 | 3 | cjcli 15063 |
. . . . . . . . 9
โข
(โโ๐
)
โ โ |
24 | 1, 3, 14, 23 | mul4i 11360 |
. . . . . . . 8
โข ((๐ ยท ๐
) ยท ((โโ๐) ยท (โโ๐
))) = ((๐ ยท (โโ๐)) ยท (๐
ยท (โโ๐
))) |
25 | | normlem1.5 |
. . . . . . . . . . . 12
โข
(absโ๐) =
1 |
26 | 25 | oveq1i 7371 |
. . . . . . . . . . 11
โข
((absโ๐)โ2) = (1โ2) |
27 | 1 | absvalsqi 15287 |
. . . . . . . . . . 11
โข
((absโ๐)โ2) = (๐ ยท (โโ๐)) |
28 | | sq1 14108 |
. . . . . . . . . . 11
โข
(1โ2) = 1 |
29 | 26, 27, 28 | 3eqtr3i 2769 |
. . . . . . . . . 10
โข (๐ ยท (โโ๐)) = 1 |
30 | 10 | oveq2i 7372 |
. . . . . . . . . 10
โข (๐
ยท (โโ๐
)) = (๐
ยท ๐
) |
31 | 29, 30 | oveq12i 7373 |
. . . . . . . . 9
โข ((๐ ยท (โโ๐)) ยท (๐
ยท (โโ๐
))) = (1 ยท (๐
ยท ๐
)) |
32 | 3, 3 | mulcli 11170 |
. . . . . . . . . 10
โข (๐
ยท ๐
) โ โ |
33 | 32 | mulid2i 11168 |
. . . . . . . . 9
โข (1
ยท (๐
ยท ๐
)) = (๐
ยท ๐
) |
34 | 31, 33 | eqtri 2761 |
. . . . . . . 8
โข ((๐ ยท (โโ๐)) ยท (๐
ยท (โโ๐
))) = (๐
ยท ๐
) |
35 | 24, 34 | eqtri 2761 |
. . . . . . 7
โข ((๐ ยท ๐
) ยท ((โโ๐) ยท (โโ๐
))) = (๐
ยท ๐
) |
36 | 22, 35 | eqtri 2761 |
. . . . . 6
โข ((๐ ยท ๐
) ยท (โโ(๐ ยท ๐
))) = (๐
ยท ๐
) |
37 | 3 | sqvali 14093 |
. . . . . 6
โข (๐
โ2) = (๐
ยท ๐
) |
38 | 36, 37 | eqtr4i 2764 |
. . . . 5
โข ((๐ ยท ๐
) ยท (โโ(๐ ยท ๐
))) = (๐
โ2) |
39 | 38 | oveq1i 7371 |
. . . 4
โข (((๐ ยท ๐
) ยท (โโ(๐ ยท ๐
))) ยท (๐บ ยทih ๐บ)) = ((๐
โ2) ยท (๐บ ยทih ๐บ)) |
40 | 21, 39 | oveq12i 7373 |
. . 3
โข ((-(๐ ยท ๐
) ยท (๐บ ยทih ๐น)) + (((๐ ยท ๐
) ยท (โโ(๐ ยท ๐
))) ยท (๐บ ยทih ๐บ))) = (((๐ ยท -๐
) ยท (๐บ ยทih ๐น)) + ((๐
โ2) ยท (๐บ ยทih ๐บ))) |
41 | 18, 40 | oveq12i 7373 |
. 2
โข (((๐น
ยทih ๐น) + (-(โโ(๐ ยท ๐
)) ยท (๐น ยทih ๐บ))) + ((-(๐ ยท ๐
) ยท (๐บ ยทih ๐น)) + (((๐ ยท ๐
) ยท (โโ(๐ ยท ๐
))) ยท (๐บ ยทih ๐บ)))) = (((๐น ยทih ๐น) + (((โโ๐) ยท -๐
) ยท (๐น ยทih ๐บ))) + (((๐ ยท -๐
) ยท (๐บ ยทih ๐น)) + ((๐
โ2) ยท (๐บ ยทih ๐บ)))) |
42 | 7, 41 | eqtri 2761 |
1
โข ((๐น โโ
((๐ ยท ๐
)
ยทโ ๐บ)) ยทih
(๐น
โโ ((๐ ยท ๐
) ยทโ ๐บ))) = (((๐น ยทih ๐น) + (((โโ๐) ยท -๐
) ยท (๐น ยทih ๐บ))) + (((๐ ยท -๐
) ยท (๐บ ยทih ๐น)) + ((๐
โ2) ยท (๐บ ยทih ๐บ)))) |