Step | Hyp | Ref
| Expression |
1 | | simp1 1136 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β π β NrmCVec) |
2 | | ax-icn 11134 |
. . . . . . . 8
β’ i β
β |
3 | | nvdif.1 |
. . . . . . . . 9
β’ π = (BaseSetβπ) |
4 | | nvdif.4 |
. . . . . . . . 9
β’ π = (
Β·π OLD βπ) |
5 | 3, 4 | nvscl 29665 |
. . . . . . . 8
β’ ((π β NrmCVec β§ i β
β β§ π΅ β
π) β (iππ΅) β π) |
6 | 2, 5 | mp3an2 1449 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΅ β π) β (iππ΅) β π) |
7 | 6 | 3adant2 1131 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (iππ΅) β π) |
8 | | nvdif.2 |
. . . . . . 7
β’ πΊ = ( +π£
βπ) |
9 | 3, 8 | nvgcl 29659 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π β§ (iππ΅) β π) β (π΄πΊ(iππ΅)) β π) |
10 | 7, 9 | syld3an3 1409 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄πΊ(iππ΅)) β π) |
11 | | nvdif.6 |
. . . . . 6
β’ π =
(normCVβπ) |
12 | 3, 11 | nvcl 29700 |
. . . . 5
β’ ((π β NrmCVec β§ (π΄πΊ(iππ΅)) β π) β (πβ(π΄πΊ(iππ΅))) β β) |
13 | 1, 10, 12 | syl2anc 584 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (πβ(π΄πΊ(iππ΅))) β β) |
14 | 13 | recnd 11207 |
. . 3
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (πβ(π΄πΊ(iππ΅))) β β) |
15 | 14 | mullidd 11197 |
. 2
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (1 Β· (πβ(π΄πΊ(iππ΅)))) = (πβ(π΄πΊ(iππ΅)))) |
16 | 2 | absnegi 15312 |
. . . . 5
β’
(absβ-i) = (absβi) |
17 | | absi 15198 |
. . . . 5
β’
(absβi) = 1 |
18 | 16, 17 | eqtri 2759 |
. . . 4
β’
(absβ-i) = 1 |
19 | 18 | oveq1i 7387 |
. . 3
β’
((absβ-i) Β· (πβ(π΄πΊ(iππ΅)))) = (1 Β· (πβ(π΄πΊ(iππ΅)))) |
20 | | negicn 11426 |
. . . . . 6
β’ -i β
β |
21 | 3, 4, 11 | nvs 29702 |
. . . . . 6
β’ ((π β NrmCVec β§ -i β
β β§ (π΄πΊ(iππ΅)) β π) β (πβ(-iπ(π΄πΊ(iππ΅)))) = ((absβ-i) Β· (πβ(π΄πΊ(iππ΅))))) |
22 | 20, 21 | mp3an2 1449 |
. . . . 5
β’ ((π β NrmCVec β§ (π΄πΊ(iππ΅)) β π) β (πβ(-iπ(π΄πΊ(iππ΅)))) = ((absβ-i) Β· (πβ(π΄πΊ(iππ΅))))) |
23 | 1, 10, 22 | syl2anc 584 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (πβ(-iπ(π΄πΊ(iππ΅)))) = ((absβ-i) Β· (πβ(π΄πΊ(iππ΅))))) |
24 | | simp2 1137 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β π΄ β π) |
25 | 3, 8, 4 | nvdi 29669 |
. . . . . . . 8
β’ ((π β NrmCVec β§ (-i β
β β§ π΄ β
π β§ (iππ΅) β π)) β (-iπ(π΄πΊ(iππ΅))) = ((-iππ΄)πΊ(-iπ(iππ΅)))) |
26 | 20, 25 | mp3anr1 1458 |
. . . . . . 7
β’ ((π β NrmCVec β§ (π΄ β π β§ (iππ΅) β π)) β (-iπ(π΄πΊ(iππ΅))) = ((-iππ΄)πΊ(-iπ(iππ΅)))) |
27 | 1, 24, 7, 26 | syl12anc 835 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (-iπ(π΄πΊ(iππ΅))) = ((-iππ΄)πΊ(-iπ(iππ΅)))) |
28 | 2, 2 | mulneg1i 11625 |
. . . . . . . . . . 11
β’ (-i
Β· i) = -(i Β· i) |
29 | | ixi 11808 |
. . . . . . . . . . . . 13
β’ (i
Β· i) = -1 |
30 | 29 | negeqi 11418 |
. . . . . . . . . . . 12
β’ -(i
Β· i) = --1 |
31 | | negneg1e1 12295 |
. . . . . . . . . . . 12
β’ --1 =
1 |
32 | 30, 31 | eqtri 2759 |
. . . . . . . . . . 11
β’ -(i
Β· i) = 1 |
33 | 28, 32 | eqtri 2759 |
. . . . . . . . . 10
β’ (-i
Β· i) = 1 |
34 | 33 | oveq1i 7387 |
. . . . . . . . 9
β’ ((-i
Β· i)ππ΅) = (1ππ΅) |
35 | 3, 4 | nvsass 29667 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ (-i β
β β§ i β β β§ π΅ β π)) β ((-i Β· i)ππ΅) = (-iπ(iππ΅))) |
36 | 20, 35 | mp3anr1 1458 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ (i β
β β§ π΅ β
π)) β ((-i Β·
i)ππ΅) = (-iπ(iππ΅))) |
37 | 2, 36 | mpanr1 701 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π΅ β π) β ((-i Β· i)ππ΅) = (-iπ(iππ΅))) |
38 | 3, 4 | nvsid 29666 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π΅ β π) β (1ππ΅) = π΅) |
39 | 34, 37, 38 | 3eqtr3a 2795 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΅ β π) β (-iπ(iππ΅)) = π΅) |
40 | 39 | 3adant2 1131 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (-iπ(iππ΅)) = π΅) |
41 | 40 | oveq2d 7393 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((-iππ΄)πΊ(-iπ(iππ΅))) = ((-iππ΄)πΊπ΅)) |
42 | 3, 4 | nvscl 29665 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ -i β
β β§ π΄ β
π) β (-iππ΄) β π) |
43 | 20, 42 | mp3an2 1449 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π) β (-iππ΄) β π) |
44 | 43 | 3adant3 1132 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (-iππ΄) β π) |
45 | 3, 8 | nvcom 29660 |
. . . . . . 7
β’ ((π β NrmCVec β§ (-iππ΄) β π β§ π΅ β π) β ((-iππ΄)πΊπ΅) = (π΅πΊ(-iππ΄))) |
46 | 44, 45 | syld3an2 1411 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((-iππ΄)πΊπ΅) = (π΅πΊ(-iππ΄))) |
47 | 27, 41, 46 | 3eqtrd 2775 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (-iπ(π΄πΊ(iππ΅))) = (π΅πΊ(-iππ΄))) |
48 | 47 | fveq2d 6866 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (πβ(-iπ(π΄πΊ(iππ΅)))) = (πβ(π΅πΊ(-iππ΄)))) |
49 | 23, 48 | eqtr3d 2773 |
. . 3
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((absβ-i) Β· (πβ(π΄πΊ(iππ΅)))) = (πβ(π΅πΊ(-iππ΄)))) |
50 | 19, 49 | eqtr3id 2785 |
. 2
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (1 Β· (πβ(π΄πΊ(iππ΅)))) = (πβ(π΅πΊ(-iππ΄)))) |
51 | 15, 50 | eqtr3d 2773 |
1
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (πβ(π΄πΊ(iππ΅))) = (πβ(π΅πΊ(-iππ΄)))) |