Step | Hyp | Ref
| Expression |
1 | | normlem1.2 |
. . . . 5
โข ๐น โ โ |
2 | | normlem1.1 |
. . . . . 6
โข ๐ โ โ |
3 | | normlem1.3 |
. . . . . 6
โข ๐บ โ โ |
4 | 2, 3 | hvmulcli 30267 |
. . . . 5
โข (๐
ยทโ ๐บ) โ โ |
5 | 1, 4 | hvsubvali 30273 |
. . . 4
โข (๐น โโ
(๐
ยทโ ๐บ)) = (๐น +โ (-1
ยทโ (๐ ยทโ ๐บ))) |
6 | 2 | mulm1i 11659 |
. . . . . . 7
โข (-1
ยท ๐) = -๐ |
7 | 6 | oveq1i 7419 |
. . . . . 6
โข ((-1
ยท ๐)
ยทโ ๐บ) = (-๐ ยทโ ๐บ) |
8 | | neg1cn 12326 |
. . . . . . 7
โข -1 โ
โ |
9 | 8, 2, 3 | hvmulassi 30299 |
. . . . . 6
โข ((-1
ยท ๐)
ยทโ ๐บ) = (-1 ยทโ
(๐
ยทโ ๐บ)) |
10 | 7, 9 | eqtr3i 2763 |
. . . . 5
โข (-๐
ยทโ ๐บ) = (-1 ยทโ
(๐
ยทโ ๐บ)) |
11 | 10 | oveq2i 7420 |
. . . 4
โข (๐น +โ (-๐
ยทโ ๐บ)) = (๐น +โ (-1
ยทโ (๐ ยทโ ๐บ))) |
12 | 5, 11 | eqtr4i 2764 |
. . 3
โข (๐น โโ
(๐
ยทโ ๐บ)) = (๐น +โ (-๐ ยทโ ๐บ)) |
13 | 12, 12 | oveq12i 7421 |
. 2
โข ((๐น โโ
(๐
ยทโ ๐บ)) ยทih
(๐น
โโ (๐ ยทโ ๐บ))) = ((๐น +โ (-๐ ยทโ ๐บ))
ยทih (๐น +โ (-๐ ยทโ ๐บ))) |
14 | 2 | negcli 11528 |
. . . 4
โข -๐ โ โ |
15 | 14, 3 | hvmulcli 30267 |
. . 3
โข (-๐
ยทโ ๐บ) โ โ |
16 | 1, 15 | hvaddcli 30271 |
. . 3
โข (๐น +โ (-๐
ยทโ ๐บ)) โ โ |
17 | | ax-his2 30336 |
. . 3
โข ((๐น โ โ โง (-๐
ยทโ ๐บ) โ โ โง (๐น +โ (-๐ ยทโ ๐บ)) โ โ) โ
((๐น +โ
(-๐
ยทโ ๐บ)) ยทih
(๐น +โ
(-๐
ยทโ ๐บ))) = ((๐น ยทih (๐น +โ (-๐
ยทโ ๐บ))) + ((-๐ ยทโ ๐บ)
ยทih (๐น +โ (-๐ ยทโ ๐บ))))) |
18 | 1, 15, 16, 17 | mp3an 1462 |
. 2
โข ((๐น +โ (-๐
ยทโ ๐บ)) ยทih
(๐น +โ
(-๐
ยทโ ๐บ))) = ((๐น ยทih (๐น +โ (-๐
ยทโ ๐บ))) + ((-๐ ยทโ ๐บ)
ยทih (๐น +โ (-๐ ยทโ ๐บ)))) |
19 | | his7 30343 |
. . . . 5
โข ((๐น โ โ โง ๐น โ โ โง (-๐
ยทโ ๐บ) โ โ) โ (๐น ยทih (๐น +โ (-๐
ยทโ ๐บ))) = ((๐น ยทih ๐น) + (๐น ยทih (-๐
ยทโ ๐บ)))) |
20 | 1, 1, 15, 19 | mp3an 1462 |
. . . 4
โข (๐น
ยทih (๐น +โ (-๐ ยทโ ๐บ))) = ((๐น ยทih ๐น) + (๐น ยทih (-๐
ยทโ ๐บ))) |
21 | | his5 30339 |
. . . . . . 7
โข ((-๐ โ โ โง ๐น โ โ โง ๐บ โ โ) โ (๐น
ยทih (-๐ ยทโ ๐บ)) = ((โโ-๐) ยท (๐น ยทih ๐บ))) |
22 | 14, 1, 3, 21 | mp3an 1462 |
. . . . . 6
โข (๐น
ยทih (-๐ ยทโ ๐บ)) = ((โโ-๐) ยท (๐น ยทih ๐บ)) |
23 | 2 | cjnegi 15129 |
. . . . . . 7
โข
(โโ-๐)
= -(โโ๐) |
24 | 23 | oveq1i 7419 |
. . . . . 6
โข
((โโ-๐)
ยท (๐น
ยทih ๐บ)) = (-(โโ๐) ยท (๐น ยทih ๐บ)) |
25 | 22, 24 | eqtri 2761 |
. . . . 5
โข (๐น
ยทih (-๐ ยทโ ๐บ)) = (-(โโ๐) ยท (๐น ยทih ๐บ)) |
26 | 25 | oveq2i 7420 |
. . . 4
โข ((๐น
ยทih ๐น) + (๐น ยทih (-๐
ยทโ ๐บ))) = ((๐น ยทih ๐น) + (-(โโ๐) ยท (๐น ยทih ๐บ))) |
27 | 20, 26 | eqtri 2761 |
. . 3
โข (๐น
ยทih (๐น +โ (-๐ ยทโ ๐บ))) = ((๐น ยทih ๐น) + (-(โโ๐) ยท (๐น ยทih ๐บ))) |
28 | | ax-his3 30337 |
. . . . 5
โข ((-๐ โ โ โง ๐บ โ โ โง (๐น +โ (-๐
ยทโ ๐บ)) โ โ) โ ((-๐
ยทโ ๐บ) ยทih (๐น +โ (-๐
ยทโ ๐บ))) = (-๐ ยท (๐บ ยทih (๐น +โ (-๐
ยทโ ๐บ))))) |
29 | 14, 3, 16, 28 | mp3an 1462 |
. . . 4
โข ((-๐
ยทโ ๐บ) ยทih (๐น +โ (-๐
ยทโ ๐บ))) = (-๐ ยท (๐บ ยทih (๐น +โ (-๐
ยทโ ๐บ)))) |
30 | | his7 30343 |
. . . . . . 7
โข ((๐บ โ โ โง ๐น โ โ โง (-๐
ยทโ ๐บ) โ โ) โ (๐บ ยทih (๐น +โ (-๐
ยทโ ๐บ))) = ((๐บ ยทih ๐น) + (๐บ ยทih (-๐
ยทโ ๐บ)))) |
31 | 3, 1, 15, 30 | mp3an 1462 |
. . . . . 6
โข (๐บ
ยทih (๐น +โ (-๐ ยทโ ๐บ))) = ((๐บ ยทih ๐น) + (๐บ ยทih (-๐
ยทโ ๐บ))) |
32 | | his5 30339 |
. . . . . . . 8
โข ((-๐ โ โ โง ๐บ โ โ โง ๐บ โ โ) โ (๐บ
ยทih (-๐ ยทโ ๐บ)) = ((โโ-๐) ยท (๐บ ยทih ๐บ))) |
33 | 14, 3, 3, 32 | mp3an 1462 |
. . . . . . 7
โข (๐บ
ยทih (-๐ ยทโ ๐บ)) = ((โโ-๐) ยท (๐บ ยทih ๐บ)) |
34 | 33 | oveq2i 7420 |
. . . . . 6
โข ((๐บ
ยทih ๐น) + (๐บ ยทih (-๐
ยทโ ๐บ))) = ((๐บ ยทih ๐น) + ((โโ-๐) ยท (๐บ ยทih ๐บ))) |
35 | 31, 34 | eqtri 2761 |
. . . . 5
โข (๐บ
ยทih (๐น +โ (-๐ ยทโ ๐บ))) = ((๐บ ยทih ๐น) + ((โโ-๐) ยท (๐บ ยทih ๐บ))) |
36 | 35 | oveq2i 7420 |
. . . 4
โข (-๐ ยท (๐บ ยทih (๐น +โ (-๐
ยทโ ๐บ)))) = (-๐ ยท ((๐บ ยทih ๐น) + ((โโ-๐) ยท (๐บ ยทih ๐บ)))) |
37 | 3, 1 | hicli 30334 |
. . . . . 6
โข (๐บ
ยทih ๐น) โ โ |
38 | 14 | cjcli 15116 |
. . . . . . 7
โข
(โโ-๐)
โ โ |
39 | 3, 3 | hicli 30334 |
. . . . . . 7
โข (๐บ
ยทih ๐บ) โ โ |
40 | 38, 39 | mulcli 11221 |
. . . . . 6
โข
((โโ-๐)
ยท (๐บ
ยทih ๐บ)) โ โ |
41 | 14, 37, 40 | adddii 11226 |
. . . . 5
โข (-๐ ยท ((๐บ ยทih ๐น) + ((โโ-๐) ยท (๐บ ยทih ๐บ)))) = ((-๐ ยท (๐บ ยทih ๐น)) + (-๐ ยท ((โโ-๐) ยท (๐บ ยทih ๐บ)))) |
42 | 14, 38, 39 | mulassi 11225 |
. . . . . . 7
โข ((-๐ ยท (โโ-๐)) ยท (๐บ ยทih ๐บ)) = (-๐ ยท ((โโ-๐) ยท (๐บ ยทih ๐บ))) |
43 | 23 | oveq2i 7420 |
. . . . . . . . 9
โข (-๐ ยท (โโ-๐)) = (-๐ ยท -(โโ๐)) |
44 | 2 | cjcli 15116 |
. . . . . . . . . 10
โข
(โโ๐)
โ โ |
45 | 2, 44 | mul2negi 11662 |
. . . . . . . . 9
โข (-๐ ยท -(โโ๐)) = (๐ ยท (โโ๐)) |
46 | 43, 45 | eqtri 2761 |
. . . . . . . 8
โข (-๐ ยท (โโ-๐)) = (๐ ยท (โโ๐)) |
47 | 46 | oveq1i 7419 |
. . . . . . 7
โข ((-๐ ยท (โโ-๐)) ยท (๐บ ยทih ๐บ)) = ((๐ ยท (โโ๐)) ยท (๐บ ยทih ๐บ)) |
48 | 42, 47 | eqtr3i 2763 |
. . . . . 6
โข (-๐ ยท
((โโ-๐)
ยท (๐บ
ยทih ๐บ))) = ((๐ ยท (โโ๐)) ยท (๐บ ยทih ๐บ)) |
49 | 48 | oveq2i 7420 |
. . . . 5
โข ((-๐ ยท (๐บ ยทih ๐น)) + (-๐ ยท ((โโ-๐) ยท (๐บ ยทih ๐บ)))) = ((-๐ ยท (๐บ ยทih ๐น)) + ((๐ ยท (โโ๐)) ยท (๐บ ยทih ๐บ))) |
50 | 41, 49 | eqtri 2761 |
. . . 4
โข (-๐ ยท ((๐บ ยทih ๐น) + ((โโ-๐) ยท (๐บ ยทih ๐บ)))) = ((-๐ ยท (๐บ ยทih ๐น)) + ((๐ ยท (โโ๐)) ยท (๐บ ยทih ๐บ))) |
51 | 29, 36, 50 | 3eqtri 2765 |
. . 3
โข ((-๐
ยทโ ๐บ) ยทih (๐น +โ (-๐
ยทโ ๐บ))) = ((-๐ ยท (๐บ ยทih ๐น)) + ((๐ ยท (โโ๐)) ยท (๐บ ยทih ๐บ))) |
52 | 27, 51 | oveq12i 7421 |
. 2
โข ((๐น
ยทih (๐น +โ (-๐ ยทโ ๐บ))) + ((-๐ ยทโ ๐บ)
ยทih (๐น +โ (-๐ ยทโ ๐บ)))) = (((๐น ยทih ๐น) + (-(โโ๐) ยท (๐น ยทih ๐บ))) + ((-๐ ยท (๐บ ยทih ๐น)) + ((๐ ยท (โโ๐)) ยท (๐บ ยทih ๐บ)))) |
53 | 13, 18, 52 | 3eqtri 2765 |
1
โข ((๐น โโ
(๐
ยทโ ๐บ)) ยทih
(๐น
โโ (๐ ยทโ ๐บ))) = (((๐น ยทih ๐น) + (-(โโ๐) ยท (๐น ยทih ๐บ))) + ((-๐ ยท (๐บ ยทih ๐น)) + ((๐ ยท (โโ๐)) ยท (๐บ ยทih ๐บ)))) |