Step | Hyp | Ref
| Expression |
1 | | neg1cn 12326 |
. . . . . 6
β’ -1 β
β |
2 | | nvpncan2.1 |
. . . . . . 7
β’ π = (BaseSetβπ) |
3 | | nvpncan2.2 |
. . . . . . 7
β’ πΊ = ( +π£
βπ) |
4 | | eqid 2733 |
. . . . . . 7
β’ (
Β·π OLD βπ) = ( Β·π OLD
βπ) |
5 | 2, 3, 4 | nvdi 29883 |
. . . . . 6
β’ ((π β NrmCVec β§ (-1 β
β β§ πΆ β
π β§ π· β π)) β (-1(
Β·π OLD βπ)(πΆπΊπ·)) = ((-1(
Β·π OLD βπ)πΆ)πΊ(-1( Β·π OLD
βπ)π·))) |
6 | 1, 5 | mp3anr1 1459 |
. . . . 5
β’ ((π β NrmCVec β§ (πΆ β π β§ π· β π)) β (-1(
Β·π OLD βπ)(πΆπΊπ·)) = ((-1(
Β·π OLD βπ)πΆ)πΊ(-1( Β·π OLD
βπ)π·))) |
7 | 6 | 3adant2 1132 |
. . . 4
β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (-1(
Β·π OLD βπ)(πΆπΊπ·)) = ((-1(
Β·π OLD βπ)πΆ)πΊ(-1( Β·π OLD
βπ)π·))) |
8 | 7 | oveq2d 7425 |
. . 3
β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((π΄πΊπ΅)πΊ(-1( Β·π OLD
βπ)(πΆπΊπ·))) = ((π΄πΊπ΅)πΊ((-1( Β·π OLD
βπ)πΆ)πΊ(-1( Β·π OLD
βπ)π·)))) |
9 | 2, 4 | nvscl 29879 |
. . . . . . 7
β’ ((π β NrmCVec β§ -1 β
β β§ πΆ β
π) β (-1(
Β·π OLD βπ)πΆ) β π) |
10 | 1, 9 | mp3an2 1450 |
. . . . . 6
β’ ((π β NrmCVec β§ πΆ β π) β (-1(
Β·π OLD βπ)πΆ) β π) |
11 | 2, 4 | nvscl 29879 |
. . . . . . 7
β’ ((π β NrmCVec β§ -1 β
β β§ π· β
π) β (-1(
Β·π OLD βπ)π·) β π) |
12 | 1, 11 | mp3an2 1450 |
. . . . . 6
β’ ((π β NrmCVec β§ π· β π) β (-1(
Β·π OLD βπ)π·) β π) |
13 | 10, 12 | anim12dan 620 |
. . . . 5
β’ ((π β NrmCVec β§ (πΆ β π β§ π· β π)) β ((-1(
Β·π OLD βπ)πΆ) β π β§ (-1(
Β·π OLD βπ)π·) β π)) |
14 | 13 | 3adant2 1132 |
. . . 4
β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((-1(
Β·π OLD βπ)πΆ) β π β§ (-1(
Β·π OLD βπ)π·) β π)) |
15 | 2, 3 | nvadd4 29878 |
. . . 4
β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π) β§ ((-1(
Β·π OLD βπ)πΆ) β π β§ (-1(
Β·π OLD βπ)π·) β π)) β ((π΄πΊπ΅)πΊ((-1( Β·π OLD
βπ)πΆ)πΊ(-1( Β·π OLD
βπ)π·))) = ((π΄πΊ(-1( Β·π OLD
βπ)πΆ))πΊ(π΅πΊ(-1( Β·π OLD
βπ)π·)))) |
16 | 14, 15 | syld3an3 1410 |
. . 3
β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((π΄πΊπ΅)πΊ((-1( Β·π OLD
βπ)πΆ)πΊ(-1( Β·π OLD
βπ)π·))) = ((π΄πΊ(-1( Β·π OLD
βπ)πΆ))πΊ(π΅πΊ(-1( Β·π OLD
βπ)π·)))) |
17 | 8, 16 | eqtrd 2773 |
. 2
β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((π΄πΊπ΅)πΊ(-1( Β·π OLD
βπ)(πΆπΊπ·))) = ((π΄πΊ(-1( Β·π OLD
βπ)πΆ))πΊ(π΅πΊ(-1( Β·π OLD
βπ)π·)))) |
18 | | simp1 1137 |
. . 3
β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β π β NrmCVec) |
19 | 2, 3 | nvgcl 29873 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) β π) |
20 | 19 | 3expb 1121 |
. . . 4
β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π)) β (π΄πΊπ΅) β π) |
21 | 20 | 3adant3 1133 |
. . 3
β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (π΄πΊπ΅) β π) |
22 | 2, 3 | nvgcl 29873 |
. . . . 5
β’ ((π β NrmCVec β§ πΆ β π β§ π· β π) β (πΆπΊπ·) β π) |
23 | 22 | 3expb 1121 |
. . . 4
β’ ((π β NrmCVec β§ (πΆ β π β§ π· β π)) β (πΆπΊπ·) β π) |
24 | 23 | 3adant2 1132 |
. . 3
β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (πΆπΊπ·) β π) |
25 | | nvpncan2.3 |
. . . 4
β’ π = ( βπ£
βπ) |
26 | 2, 3, 4, 25 | nvmval 29895 |
. . 3
β’ ((π β NrmCVec β§ (π΄πΊπ΅) β π β§ (πΆπΊπ·) β π) β ((π΄πΊπ΅)π(πΆπΊπ·)) = ((π΄πΊπ΅)πΊ(-1( Β·π OLD
βπ)(πΆπΊπ·)))) |
27 | 18, 21, 24, 26 | syl3anc 1372 |
. 2
β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((π΄πΊπ΅)π(πΆπΊπ·)) = ((π΄πΊπ΅)πΊ(-1( Β·π OLD
βπ)(πΆπΊπ·)))) |
28 | 2, 3, 4, 25 | nvmval 29895 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π β§ πΆ β π) β (π΄ππΆ) = (π΄πΊ(-1( Β·π OLD
βπ)πΆ))) |
29 | 28 | 3adant3r 1182 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π β§ (πΆ β π β§ π· β π)) β (π΄ππΆ) = (π΄πΊ(-1( Β·π OLD
βπ)πΆ))) |
30 | 29 | 3adant2r 1180 |
. . 3
β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (π΄ππΆ) = (π΄πΊ(-1( Β·π OLD
βπ)πΆ))) |
31 | 2, 3, 4, 25 | nvmval 29895 |
. . . . 5
β’ ((π β NrmCVec β§ π΅ β π β§ π· β π) β (π΅ππ·) = (π΅πΊ(-1( Β·π OLD
βπ)π·))) |
32 | 31 | 3adant3l 1181 |
. . . 4
β’ ((π β NrmCVec β§ π΅ β π β§ (πΆ β π β§ π· β π)) β (π΅ππ·) = (π΅πΊ(-1( Β·π OLD
βπ)π·))) |
33 | 32 | 3adant2l 1179 |
. . 3
β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (π΅ππ·) = (π΅πΊ(-1( Β·π OLD
βπ)π·))) |
34 | 30, 33 | oveq12d 7427 |
. 2
β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((π΄ππΆ)πΊ(π΅ππ·)) = ((π΄πΊ(-1( Β·π OLD
βπ)πΆ))πΊ(π΅πΊ(-1( Β·π OLD
βπ)π·)))) |
35 | 17, 27, 34 | 3eqtr4d 2783 |
1
β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((π΄πΊπ΅)π(πΆπΊπ·)) = ((π΄ππΆ)πΊ(π΅ππ·))) |