Step | Hyp | Ref
| Expression |
1 | | neg1cn 12272 |
. . . . 5
β’ -1 β
β |
2 | 1 | a1i 11 |
. . . 4
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β -1 β β) |
3 | | lno0.1 |
. . . . . 6
β’ π = (BaseSetβπ) |
4 | | lno0.5 |
. . . . . 6
β’ π = (0vecβπ) |
5 | 3, 4 | nvzcl 29618 |
. . . . 5
β’ (π β NrmCVec β π β π) |
6 | 5 | 3ad2ant1 1134 |
. . . 4
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β π β π) |
7 | 2, 6, 6 | 3jca 1129 |
. . 3
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β (-1 β β β§ π β π β§ π β π)) |
8 | | lno0.2 |
. . . 4
β’ π = (BaseSetβπ) |
9 | | eqid 2733 |
. . . 4
β’ (
+π£ βπ) = ( +π£ βπ) |
10 | | eqid 2733 |
. . . 4
β’ (
+π£ βπ) = ( +π£ βπ) |
11 | | eqid 2733 |
. . . 4
β’ (
Β·π OLD βπ) = ( Β·π OLD
βπ) |
12 | | eqid 2733 |
. . . 4
β’ (
Β·π OLD βπ) = ( Β·π OLD
βπ) |
13 | | lno0.7 |
. . . 4
β’ πΏ = (π LnOp π) |
14 | 3, 8, 9, 10, 11, 12, 13 | lnolin 29738 |
. . 3
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (-1 β β β§ π β π β§ π β π)) β (πβ((-1(
Β·π OLD βπ)π)( +π£ βπ)π)) = ((-1(
Β·π OLD βπ)(πβπ))( +π£ βπ)(πβπ))) |
15 | 7, 14 | mpdan 686 |
. 2
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β (πβ((-1(
Β·π OLD βπ)π)( +π£ βπ)π)) = ((-1(
Β·π OLD βπ)(πβπ))( +π£ βπ)(πβπ))) |
16 | 3, 9, 11, 4 | nvlinv 29636 |
. . . . 5
β’ ((π β NrmCVec β§ π β π) β ((-1(
Β·π OLD βπ)π)( +π£ βπ)π) = π) |
17 | 5, 16 | mpdan 686 |
. . . 4
β’ (π β NrmCVec β ((-1(
Β·π OLD βπ)π)( +π£ βπ)π) = π) |
18 | 17 | fveq2d 6847 |
. . 3
β’ (π β NrmCVec β (πβ((-1(
Β·π OLD βπ)π)( +π£ βπ)π)) = (πβπ)) |
19 | 18 | 3ad2ant1 1134 |
. 2
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β (πβ((-1(
Β·π OLD βπ)π)( +π£ βπ)π)) = (πβπ)) |
20 | | simp2 1138 |
. . 3
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β π β NrmCVec) |
21 | 3, 8, 13 | lnof 29739 |
. . . 4
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β π:πβΆπ) |
22 | 21, 6 | ffvelcdmd 7037 |
. . 3
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β (πβπ) β π) |
23 | | lno0.z |
. . . 4
β’ π = (0vecβπ) |
24 | 8, 10, 12, 23 | nvlinv 29636 |
. . 3
β’ ((π β NrmCVec β§ (πβπ) β π) β ((-1(
Β·π OLD βπ)(πβπ))( +π£ βπ)(πβπ)) = π) |
25 | 20, 22, 24 | syl2anc 585 |
. 2
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β ((-1(
Β·π OLD βπ)(πβπ))( +π£ βπ)(πβπ)) = π) |
26 | 15, 19, 25 | 3eqtr3d 2781 |
1
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β (πβπ) = π) |