Step | Hyp | Ref
| Expression |
1 | | sspm.h |
. . . . . . . 8
β’ π» = (SubSpβπ) |
2 | 1 | sspnv 29710 |
. . . . . . 7
β’ ((π β NrmCVec β§ π β π») β π β NrmCVec) |
3 | | neg1cn 12272 |
. . . . . . . . 9
β’ -1 β
β |
4 | | sspm.y |
. . . . . . . . . 10
β’ π = (BaseSetβπ) |
5 | | eqid 2733 |
. . . . . . . . . 10
β’ (
Β·π OLD βπ) = ( Β·π OLD
βπ) |
6 | 4, 5 | nvscl 29610 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ -1 β
β β§ π΅ β
π) β (-1(
Β·π OLD βπ)π΅) β π) |
7 | 3, 6 | mp3an2 1450 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΅ β π) β (-1(
Β·π OLD βπ)π΅) β π) |
8 | 7 | ex 414 |
. . . . . . 7
β’ (π β NrmCVec β (π΅ β π β (-1(
Β·π OLD βπ)π΅) β π)) |
9 | 2, 8 | syl 17 |
. . . . . 6
β’ ((π β NrmCVec β§ π β π») β (π΅ β π β (-1(
Β·π OLD βπ)π΅) β π)) |
10 | 9 | anim2d 613 |
. . . . 5
β’ ((π β NrmCVec β§ π β π») β ((π΄ β π β§ π΅ β π) β (π΄ β π β§ (-1(
Β·π OLD βπ)π΅) β π))) |
11 | 10 | imp 408 |
. . . 4
β’ (((π β NrmCVec β§ π β π») β§ (π΄ β π β§ π΅ β π)) β (π΄ β π β§ (-1(
Β·π OLD βπ)π΅) β π)) |
12 | | eqid 2733 |
. . . . 5
β’ (
+π£ βπ) = ( +π£ βπ) |
13 | | eqid 2733 |
. . . . 5
β’ (
+π£ βπ) = ( +π£ βπ) |
14 | 4, 12, 13, 1 | sspgval 29713 |
. . . 4
β’ (((π β NrmCVec β§ π β π») β§ (π΄ β π β§ (-1(
Β·π OLD βπ)π΅) β π)) β (π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)) = (π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅))) |
15 | 11, 14 | syldan 592 |
. . 3
β’ (((π β NrmCVec β§ π β π») β§ (π΄ β π β§ π΅ β π)) β (π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)) = (π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅))) |
16 | | eqid 2733 |
. . . . . . 7
β’ (
Β·π OLD βπ) = ( Β·π OLD
βπ) |
17 | 4, 16, 5, 1 | sspsval 29715 |
. . . . . 6
β’ (((π β NrmCVec β§ π β π») β§ (-1 β β β§ π΅ β π)) β (-1(
Β·π OLD βπ)π΅) = (-1(
Β·π OLD βπ)π΅)) |
18 | 3, 17 | mpanr1 702 |
. . . . 5
β’ (((π β NrmCVec β§ π β π») β§ π΅ β π) β (-1(
Β·π OLD βπ)π΅) = (-1(
Β·π OLD βπ)π΅)) |
19 | 18 | adantrl 715 |
. . . 4
β’ (((π β NrmCVec β§ π β π») β§ (π΄ β π β§ π΅ β π)) β (-1(
Β·π OLD βπ)π΅) = (-1(
Β·π OLD βπ)π΅)) |
20 | 19 | oveq2d 7374 |
. . 3
β’ (((π β NrmCVec β§ π β π») β§ (π΄ β π β§ π΅ β π)) β (π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)) = (π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅))) |
21 | 15, 20 | eqtrd 2773 |
. 2
β’ (((π β NrmCVec β§ π β π») β§ (π΄ β π β§ π΅ β π)) β (π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)) = (π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅))) |
22 | | sspm.l |
. . . . 5
β’ πΏ = ( βπ£
βπ) |
23 | 4, 13, 5, 22 | nvmval 29626 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄πΏπ΅) = (π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅))) |
24 | 23 | 3expb 1121 |
. . 3
β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π)) β (π΄πΏπ΅) = (π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅))) |
25 | 2, 24 | sylan 581 |
. 2
β’ (((π β NrmCVec β§ π β π») β§ (π΄ β π β§ π΅ β π)) β (π΄πΏπ΅) = (π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅))) |
26 | | eqid 2733 |
. . . . . . 7
β’
(BaseSetβπ) =
(BaseSetβπ) |
27 | 26, 4, 1 | sspba 29711 |
. . . . . 6
β’ ((π β NrmCVec β§ π β π») β π β (BaseSetβπ)) |
28 | 27 | sseld 3944 |
. . . . 5
β’ ((π β NrmCVec β§ π β π») β (π΄ β π β π΄ β (BaseSetβπ))) |
29 | 27 | sseld 3944 |
. . . . 5
β’ ((π β NrmCVec β§ π β π») β (π΅ β π β π΅ β (BaseSetβπ))) |
30 | 28, 29 | anim12d 610 |
. . . 4
β’ ((π β NrmCVec β§ π β π») β ((π΄ β π β§ π΅ β π) β (π΄ β (BaseSetβπ) β§ π΅ β (BaseSetβπ)))) |
31 | 30 | imp 408 |
. . 3
β’ (((π β NrmCVec β§ π β π») β§ (π΄ β π β§ π΅ β π)) β (π΄ β (BaseSetβπ) β§ π΅ β (BaseSetβπ))) |
32 | | sspm.m |
. . . . . 6
β’ π = ( βπ£
βπ) |
33 | 26, 12, 16, 32 | nvmval 29626 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β (BaseSetβπ) β§ π΅ β (BaseSetβπ)) β (π΄ππ΅) = (π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅))) |
34 | 33 | 3expb 1121 |
. . . 4
β’ ((π β NrmCVec β§ (π΄ β (BaseSetβπ) β§ π΅ β (BaseSetβπ))) β (π΄ππ΅) = (π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅))) |
35 | 34 | adantlr 714 |
. . 3
β’ (((π β NrmCVec β§ π β π») β§ (π΄ β (BaseSetβπ) β§ π΅ β (BaseSetβπ))) β (π΄ππ΅) = (π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅))) |
36 | 31, 35 | syldan 592 |
. 2
β’ (((π β NrmCVec β§ π β π») β§ (π΄ β π β§ π΅ β π)) β (π΄ππ΅) = (π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅))) |
37 | 21, 25, 36 | 3eqtr4d 2783 |
1
β’ (((π β NrmCVec β§ π β π») β§ (π΄ β π β§ π΅ β π)) β (π΄πΏπ΅) = (π΄ππ΅)) |