Step | Hyp | Ref
| Expression |
1 | | neg1cn 12272 |
. . . 4
β’ -1 β
β |
2 | | lnosub.1 |
. . . . 5
β’ π = (BaseSetβπ) |
3 | | eqid 2733 |
. . . . 5
β’
(BaseSetβπ) =
(BaseSetβπ) |
4 | | eqid 2733 |
. . . . 5
β’ (
+π£ βπ) = ( +π£ βπ) |
5 | | eqid 2733 |
. . . . 5
β’ (
+π£ βπ) = ( +π£ βπ) |
6 | | eqid 2733 |
. . . . 5
β’ (
Β·π OLD βπ) = ( Β·π OLD
βπ) |
7 | | eqid 2733 |
. . . . 5
β’ (
Β·π OLD βπ) = ( Β·π OLD
βπ) |
8 | | lnosub.7 |
. . . . 5
β’ πΏ = (π LnOp π) |
9 | 2, 3, 4, 5, 6, 7, 8 | lnolin 29738 |
. . . 4
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (-1 β β β§ π΅ β π β§ π΄ β π)) β (πβ((-1(
Β·π OLD βπ)π΅)( +π£ βπ)π΄)) = ((-1(
Β·π OLD βπ)(πβπ΅))( +π£ βπ)(πβπ΄))) |
10 | 1, 9 | mp3anr1 1459 |
. . 3
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΅ β π β§ π΄ β π)) β (πβ((-1(
Β·π OLD βπ)π΅)( +π£ βπ)π΄)) = ((-1(
Β·π OLD βπ)(πβπ΅))( +π£ βπ)(πβπ΄))) |
11 | 10 | ancom2s 649 |
. 2
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β π β§ π΅ β π)) β (πβ((-1(
Β·π OLD βπ)π΅)( +π£ βπ)π΄)) = ((-1(
Β·π OLD βπ)(πβπ΅))( +π£ βπ)(πβπ΄))) |
12 | | lnosub.5 |
. . . . . 6
β’ π = ( βπ£
βπ) |
13 | 2, 4, 6, 12 | nvmval2 29627 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄ππ΅) = ((-1(
Β·π OLD βπ)π΅)( +π£ βπ)π΄)) |
14 | 13 | 3expb 1121 |
. . . 4
β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π)) β (π΄ππ΅) = ((-1(
Β·π OLD βπ)π΅)( +π£ βπ)π΄)) |
15 | 14 | 3ad2antl1 1186 |
. . 3
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β π β§ π΅ β π)) β (π΄ππ΅) = ((-1(
Β·π OLD βπ)π΅)( +π£ βπ)π΄)) |
16 | 15 | fveq2d 6847 |
. 2
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β π β§ π΅ β π)) β (πβ(π΄ππ΅)) = (πβ((-1(
Β·π OLD βπ)π΅)( +π£ βπ)π΄))) |
17 | | simpl2 1193 |
. . 3
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β π β§ π΅ β π)) β π β NrmCVec) |
18 | 2, 3, 8 | lnof 29739 |
. . . 4
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β π:πβΆ(BaseSetβπ)) |
19 | | simpl 484 |
. . . 4
β’ ((π΄ β π β§ π΅ β π) β π΄ β π) |
20 | | ffvelcdm 7033 |
. . . 4
β’ ((π:πβΆ(BaseSetβπ) β§ π΄ β π) β (πβπ΄) β (BaseSetβπ)) |
21 | 18, 19, 20 | syl2an 597 |
. . 3
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β π β§ π΅ β π)) β (πβπ΄) β (BaseSetβπ)) |
22 | | simpr 486 |
. . . 4
β’ ((π΄ β π β§ π΅ β π) β π΅ β π) |
23 | | ffvelcdm 7033 |
. . . 4
β’ ((π:πβΆ(BaseSetβπ) β§ π΅ β π) β (πβπ΅) β (BaseSetβπ)) |
24 | 18, 22, 23 | syl2an 597 |
. . 3
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β π β§ π΅ β π)) β (πβπ΅) β (BaseSetβπ)) |
25 | | lnosub.6 |
. . . 4
β’ π = ( βπ£
βπ) |
26 | 3, 5, 7, 25 | nvmval2 29627 |
. . 3
β’ ((π β NrmCVec β§ (πβπ΄) β (BaseSetβπ) β§ (πβπ΅) β (BaseSetβπ)) β ((πβπ΄)π(πβπ΅)) = ((-1(
Β·π OLD βπ)(πβπ΅))( +π£ βπ)(πβπ΄))) |
27 | 17, 21, 24, 26 | syl3anc 1372 |
. 2
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β π β§ π΅ β π)) β ((πβπ΄)π(πβπ΅)) = ((-1(
Β·π OLD βπ)(πβπ΅))( +π£ βπ)(πβπ΄))) |
28 | 11, 16, 27 | 3eqtr4d 2783 |
1
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β π β§ π΅ β π)) β (πβ(π΄ππ΅)) = ((πβπ΄)π(πβπ΅))) |