Step | Hyp | Ref
| Expression |
1 | | simp1 1133 |
. . 3
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β π β NrmCVec) |
2 | | nvpncan2.1 |
. . . 4
β’ π = (BaseSetβπ) |
3 | | nvpncan2.2 |
. . . 4
β’ πΊ = ( +π£
βπ) |
4 | 2, 3 | nvgcl 30382 |
. . 3
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) β π) |
5 | | simp2 1134 |
. . 3
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β π΄ β π) |
6 | | eqid 2726 |
. . . 4
β’ (
Β·π OLD βπ) = ( Β·π OLD
βπ) |
7 | | nvpncan2.3 |
. . . 4
β’ π = ( βπ£
βπ) |
8 | 2, 3, 6, 7 | nvmval 30404 |
. . 3
β’ ((π β NrmCVec β§ (π΄πΊπ΅) β π β§ π΄ β π) β ((π΄πΊπ΅)ππ΄) = ((π΄πΊπ΅)πΊ(-1( Β·π OLD
βπ)π΄))) |
9 | 1, 4, 5, 8 | syl3anc 1368 |
. 2
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((π΄πΊπ΅)ππ΄) = ((π΄πΊπ΅)πΊ(-1( Β·π OLD
βπ)π΄))) |
10 | | simp3 1135 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β π΅ β π) |
11 | | neg1cn 12330 |
. . . . . 6
β’ -1 β
β |
12 | 2, 6 | nvscl 30388 |
. . . . . 6
β’ ((π β NrmCVec β§ -1 β
β β§ π΄ β
π) β (-1(
Β·π OLD βπ)π΄) β π) |
13 | 11, 12 | mp3an2 1445 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π) β (-1(
Β·π OLD βπ)π΄) β π) |
14 | 13 | 3adant3 1129 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (-1(
Β·π OLD βπ)π΄) β π) |
15 | 2, 3 | nvadd32 30385 |
. . . 4
β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π β§ (-1(
Β·π OLD βπ)π΄) β π)) β ((π΄πΊπ΅)πΊ(-1( Β·π OLD
βπ)π΄)) = ((π΄πΊ(-1( Β·π OLD
βπ)π΄))πΊπ΅)) |
16 | 1, 5, 10, 14, 15 | syl13anc 1369 |
. . 3
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((π΄πΊπ΅)πΊ(-1( Β·π OLD
βπ)π΄)) = ((π΄πΊ(-1( Β·π OLD
βπ)π΄))πΊπ΅)) |
17 | | eqid 2726 |
. . . . . . 7
β’
(0vecβπ) = (0vecβπ) |
18 | 2, 3, 6, 17 | nvrinv 30413 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π) β (π΄πΊ(-1( Β·π OLD
βπ)π΄)) = (0vecβπ)) |
19 | 18 | 3adant3 1129 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄πΊ(-1( Β·π OLD
βπ)π΄)) = (0vecβπ)) |
20 | 19 | oveq1d 7420 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((π΄πΊ(-1( Β·π OLD
βπ)π΄))πΊπ΅) = ((0vecβπ)πΊπ΅)) |
21 | 2, 3, 17 | nv0lid 30398 |
. . . . 5
β’ ((π β NrmCVec β§ π΅ β π) β ((0vecβπ)πΊπ΅) = π΅) |
22 | 21 | 3adant2 1128 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((0vecβπ)πΊπ΅) = π΅) |
23 | 20, 22 | eqtrd 2766 |
. . 3
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((π΄πΊ(-1( Β·π OLD
βπ)π΄))πΊπ΅) = π΅) |
24 | 16, 23 | eqtrd 2766 |
. 2
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((π΄πΊπ΅)πΊ(-1( Β·π OLD
βπ)π΄)) = π΅) |
25 | 9, 24 | eqtrd 2766 |
1
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((π΄πΊπ΅)ππ΄) = π΅) |