Step | Hyp | Ref
| Expression |
1 | | nn0cn 12478 |
. . . . 5
β’ (π β β0
β π β
β) |
2 | 1 | negcld 11554 |
. . . 4
β’ (π β β0
β -π β
β) |
3 | | ip1i.9 |
. . . . . 6
β’ π β
CPreHilOLD |
4 | 3 | phnvi 30056 |
. . . . 5
β’ π β NrmCVec |
5 | | ipasslem1.b |
. . . . 5
β’ π΅ β π |
6 | | ip1i.1 |
. . . . . 6
β’ π = (BaseSetβπ) |
7 | | ip1i.7 |
. . . . . 6
β’ π =
(Β·πOLDβπ) |
8 | 6, 7 | dipcl 29952 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄ππ΅) β β) |
9 | 4, 5, 8 | mp3an13 1452 |
. . . 4
β’ (π΄ β π β (π΄ππ΅) β β) |
10 | | mulcl 11190 |
. . . 4
β’ ((-π β β β§ (π΄ππ΅) β β) β (-π Β· (π΄ππ΅)) β β) |
11 | 2, 9, 10 | syl2an 596 |
. . 3
β’ ((π β β0
β§ π΄ β π) β (-π Β· (π΄ππ΅)) β β) |
12 | | ip1i.4 |
. . . . . . 7
β’ π = (
Β·π OLD βπ) |
13 | 6, 12 | nvscl 29866 |
. . . . . 6
β’ ((π β NrmCVec β§ -π β β β§ π΄ β π) β (-πππ΄) β π) |
14 | 4, 13 | mp3an1 1448 |
. . . . 5
β’ ((-π β β β§ π΄ β π) β (-πππ΄) β π) |
15 | 2, 14 | sylan 580 |
. . . 4
β’ ((π β β0
β§ π΄ β π) β (-πππ΄) β π) |
16 | 6, 7 | dipcl 29952 |
. . . . 5
β’ ((π β NrmCVec β§ (-πππ΄) β π β§ π΅ β π) β ((-πππ΄)ππ΅) β β) |
17 | 4, 5, 16 | mp3an13 1452 |
. . . 4
β’ ((-πππ΄) β π β ((-πππ΄)ππ΅) β β) |
18 | 15, 17 | syl 17 |
. . 3
β’ ((π β β0
β§ π΄ β π) β ((-πππ΄)ππ΅) β β) |
19 | | ax-1cn 11164 |
. . . . . . . . . . . . 13
β’ 1 β
β |
20 | | mulneg2 11647 |
. . . . . . . . . . . . 13
β’ ((π β β β§ 1 β
β) β (π Β·
-1) = -(π Β·
1)) |
21 | 19, 20 | mpan2 689 |
. . . . . . . . . . . 12
β’ (π β β β (π Β· -1) = -(π Β· 1)) |
22 | | mulrid 11208 |
. . . . . . . . . . . . 13
β’ (π β β β (π Β· 1) = π) |
23 | 22 | negeqd 11450 |
. . . . . . . . . . . 12
β’ (π β β β -(π Β· 1) = -π) |
24 | 21, 23 | eqtr2d 2773 |
. . . . . . . . . . 11
β’ (π β β β -π = (π Β· -1)) |
25 | 24 | adantr 481 |
. . . . . . . . . 10
β’ ((π β β β§ π΄ β π) β -π = (π Β· -1)) |
26 | 25 | oveq1d 7420 |
. . . . . . . . 9
β’ ((π β β β§ π΄ β π) β (-πππ΄) = ((π Β· -1)ππ΄)) |
27 | | neg1cn 12322 |
. . . . . . . . . 10
β’ -1 β
β |
28 | 6, 12 | nvsass 29868 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ (π β β β§ -1 β
β β§ π΄ β
π)) β ((π Β· -1)ππ΄) = (ππ(-1ππ΄))) |
29 | 4, 28 | mpan 688 |
. . . . . . . . . 10
β’ ((π β β β§ -1 β
β β§ π΄ β
π) β ((π Β· -1)ππ΄) = (ππ(-1ππ΄))) |
30 | 27, 29 | mp3an2 1449 |
. . . . . . . . 9
β’ ((π β β β§ π΄ β π) β ((π Β· -1)ππ΄) = (ππ(-1ππ΄))) |
31 | 26, 30 | eqtrd 2772 |
. . . . . . . 8
β’ ((π β β β§ π΄ β π) β (-πππ΄) = (ππ(-1ππ΄))) |
32 | 1, 31 | sylan 580 |
. . . . . . 7
β’ ((π β β0
β§ π΄ β π) β (-πππ΄) = (ππ(-1ππ΄))) |
33 | 32 | oveq1d 7420 |
. . . . . 6
β’ ((π β β0
β§ π΄ β π) β ((-πππ΄)ππ΅) = ((ππ(-1ππ΄))ππ΅)) |
34 | 6, 12 | nvscl 29866 |
. . . . . . . 8
β’ ((π β NrmCVec β§ -1 β
β β§ π΄ β
π) β (-1ππ΄) β π) |
35 | 4, 27, 34 | mp3an12 1451 |
. . . . . . 7
β’ (π΄ β π β (-1ππ΄) β π) |
36 | | ip1i.2 |
. . . . . . . 8
β’ πΊ = ( +π£
βπ) |
37 | 6, 36, 12, 7, 3, 5 | ipasslem1 30071 |
. . . . . . 7
β’ ((π β β0
β§ (-1ππ΄) β π) β ((ππ(-1ππ΄))ππ΅) = (π Β· ((-1ππ΄)ππ΅))) |
38 | 35, 37 | sylan2 593 |
. . . . . 6
β’ ((π β β0
β§ π΄ β π) β ((ππ(-1ππ΄))ππ΅) = (π Β· ((-1ππ΄)ππ΅))) |
39 | 33, 38 | eqtrd 2772 |
. . . . 5
β’ ((π β β0
β§ π΄ β π) β ((-πππ΄)ππ΅) = (π Β· ((-1ππ΄)ππ΅))) |
40 | 39 | oveq2d 7421 |
. . . 4
β’ ((π β β0
β§ π΄ β π) β ((-π Β· (π΄ππ΅)) β ((-πππ΄)ππ΅)) = ((-π Β· (π΄ππ΅)) β (π Β· ((-1ππ΄)ππ΅)))) |
41 | 6, 7 | dipcl 29952 |
. . . . . . . 8
β’ ((π β NrmCVec β§ (-1ππ΄) β π β§ π΅ β π) β ((-1ππ΄)ππ΅) β β) |
42 | 4, 5, 41 | mp3an13 1452 |
. . . . . . 7
β’ ((-1ππ΄) β π β ((-1ππ΄)ππ΅) β β) |
43 | 35, 42 | syl 17 |
. . . . . 6
β’ (π΄ β π β ((-1ππ΄)ππ΅) β β) |
44 | | mulcl 11190 |
. . . . . 6
β’ ((π β β β§ ((-1ππ΄)ππ΅) β β) β (π Β· ((-1ππ΄)ππ΅)) β β) |
45 | 1, 43, 44 | syl2an 596 |
. . . . 5
β’ ((π β β0
β§ π΄ β π) β (π Β· ((-1ππ΄)ππ΅)) β β) |
46 | 11, 45 | negsubd 11573 |
. . . 4
β’ ((π β β0
β§ π΄ β π) β ((-π Β· (π΄ππ΅)) + -(π Β· ((-1ππ΄)ππ΅))) = ((-π Β· (π΄ππ΅)) β (π Β· ((-1ππ΄)ππ΅)))) |
47 | | mulneg1 11646 |
. . . . . . 7
β’ ((π β β β§ ((-1ππ΄)ππ΅) β β) β (-π Β· ((-1ππ΄)ππ΅)) = -(π Β· ((-1ππ΄)ππ΅))) |
48 | 1, 43, 47 | syl2an 596 |
. . . . . 6
β’ ((π β β0
β§ π΄ β π) β (-π Β· ((-1ππ΄)ππ΅)) = -(π Β· ((-1ππ΄)ππ΅))) |
49 | 48 | oveq2d 7421 |
. . . . 5
β’ ((π β β0
β§ π΄ β π) β ((-π Β· (π΄ππ΅)) + (-π Β· ((-1ππ΄)ππ΅))) = ((-π Β· (π΄ππ΅)) + -(π Β· ((-1ππ΄)ππ΅)))) |
50 | 2 | adantr 481 |
. . . . . . 7
β’ ((π β β0
β§ π΄ β π) β -π β β) |
51 | 9 | adantl 482 |
. . . . . . 7
β’ ((π β β0
β§ π΄ β π) β (π΄ππ΅) β β) |
52 | 43 | adantl 482 |
. . . . . . 7
β’ ((π β β0
β§ π΄ β π) β ((-1ππ΄)ππ΅) β β) |
53 | 50, 51, 52 | adddid 11234 |
. . . . . 6
β’ ((π β β0
β§ π΄ β π) β (-π Β· ((π΄ππ΅) + ((-1ππ΄)ππ΅))) = ((-π Β· (π΄ππ΅)) + (-π Β· ((-1ππ΄)ππ΅)))) |
54 | 6, 36, 12, 7, 3 | ipdiri 30070 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ (-1ππ΄) β π β§ π΅ β π) β ((π΄πΊ(-1ππ΄))ππ΅) = ((π΄ππ΅) + ((-1ππ΄)ππ΅))) |
55 | 5, 54 | mp3an3 1450 |
. . . . . . . . . 10
β’ ((π΄ β π β§ (-1ππ΄) β π) β ((π΄πΊ(-1ππ΄))ππ΅) = ((π΄ππ΅) + ((-1ππ΄)ππ΅))) |
56 | 35, 55 | mpdan 685 |
. . . . . . . . 9
β’ (π΄ β π β ((π΄πΊ(-1ππ΄))ππ΅) = ((π΄ππ΅) + ((-1ππ΄)ππ΅))) |
57 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(0vecβπ) = (0vecβπ) |
58 | 6, 36, 12, 57 | nvrinv 29891 |
. . . . . . . . . . . 12
β’ ((π β NrmCVec β§ π΄ β π) β (π΄πΊ(-1ππ΄)) = (0vecβπ)) |
59 | 4, 58 | mpan 688 |
. . . . . . . . . . 11
β’ (π΄ β π β (π΄πΊ(-1ππ΄)) = (0vecβπ)) |
60 | 59 | oveq1d 7420 |
. . . . . . . . . 10
β’ (π΄ β π β ((π΄πΊ(-1ππ΄))ππ΅) = ((0vecβπ)ππ΅)) |
61 | 6, 57, 7 | dip0l 29958 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π΅ β π) β ((0vecβπ)ππ΅) = 0) |
62 | 4, 5, 61 | mp2an 690 |
. . . . . . . . . 10
β’
((0vecβπ)ππ΅) = 0 |
63 | 60, 62 | eqtrdi 2788 |
. . . . . . . . 9
β’ (π΄ β π β ((π΄πΊ(-1ππ΄))ππ΅) = 0) |
64 | 56, 63 | eqtr3d 2774 |
. . . . . . . 8
β’ (π΄ β π β ((π΄ππ΅) + ((-1ππ΄)ππ΅)) = 0) |
65 | 64 | oveq2d 7421 |
. . . . . . 7
β’ (π΄ β π β (-π Β· ((π΄ππ΅) + ((-1ππ΄)ππ΅))) = (-π Β· 0)) |
66 | 2 | mul01d 11409 |
. . . . . . 7
β’ (π β β0
β (-π Β· 0) =
0) |
67 | 65, 66 | sylan9eqr 2794 |
. . . . . 6
β’ ((π β β0
β§ π΄ β π) β (-π Β· ((π΄ππ΅) + ((-1ππ΄)ππ΅))) = 0) |
68 | 53, 67 | eqtr3d 2774 |
. . . . 5
β’ ((π β β0
β§ π΄ β π) β ((-π Β· (π΄ππ΅)) + (-π Β· ((-1ππ΄)ππ΅))) = 0) |
69 | 49, 68 | eqtr3d 2774 |
. . . 4
β’ ((π β β0
β§ π΄ β π) β ((-π Β· (π΄ππ΅)) + -(π Β· ((-1ππ΄)ππ΅))) = 0) |
70 | 40, 46, 69 | 3eqtr2d 2778 |
. . 3
β’ ((π β β0
β§ π΄ β π) β ((-π Β· (π΄ππ΅)) β ((-πππ΄)ππ΅)) = 0) |
71 | 11, 18, 70 | subeq0d 11575 |
. 2
β’ ((π β β0
β§ π΄ β π) β (-π Β· (π΄ππ΅)) = ((-πππ΄)ππ΅)) |
72 | 71 | eqcomd 2738 |
1
β’ ((π β β0
β§ π΄ β π) β ((-πππ΄)ππ΅) = (-π Β· (π΄ππ΅))) |