Step | Hyp | Ref
| Expression |
1 | | dipfval.1 |
. . 3
β’ π = (BaseSetβπ) |
2 | | dipfval.2 |
. . 3
β’ πΊ = ( +π£
βπ) |
3 | | dipfval.4 |
. . 3
β’ π = (
Β·π OLD βπ) |
4 | | dipfval.6 |
. . 3
β’ π =
(normCVβπ) |
5 | | dipfval.7 |
. . 3
β’ π =
(Β·πOLDβπ) |
6 | 1, 2, 3, 4, 5 | ipval2 29691 |
. 2
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄ππ΅) = (((((πβ(π΄πΊπ΅))β2) β ((πβ(π΄πΊ(-1ππ΅)))β2)) + (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2)))) / 4)) |
7 | | ipval3.3 |
. . . . . . . 8
β’ π = ( βπ£
βπ) |
8 | 1, 2, 3, 7 | nvmval 29626 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄ππ΅) = (π΄πΊ(-1ππ΅))) |
9 | 8 | fveq2d 6847 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (πβ(π΄ππ΅)) = (πβ(π΄πΊ(-1ππ΅)))) |
10 | 9 | oveq1d 7373 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((πβ(π΄ππ΅))β2) = ((πβ(π΄πΊ(-1ππ΅)))β2)) |
11 | 10 | oveq2d 7374 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (((πβ(π΄πΊπ΅))β2) β ((πβ(π΄ππ΅))β2)) = (((πβ(π΄πΊπ΅))β2) β ((πβ(π΄πΊ(-1ππ΅)))β2))) |
12 | | ax-icn 11115 |
. . . . . . . . . . . 12
β’ i β
β |
13 | 1, 3 | nvscl 29610 |
. . . . . . . . . . . 12
β’ ((π β NrmCVec β§ i β
β β§ π΅ β
π) β (iππ΅) β π) |
14 | 12, 13 | mp3an2 1450 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π΅ β π) β (iππ΅) β π) |
15 | 14 | 3adant2 1132 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (iππ΅) β π) |
16 | 1, 2, 3, 7 | nvmval 29626 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π΄ β π β§ (iππ΅) β π) β (π΄π(iππ΅)) = (π΄πΊ(-1π(iππ΅)))) |
17 | 15, 16 | syld3an3 1410 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄π(iππ΅)) = (π΄πΊ(-1π(iππ΅)))) |
18 | | neg1cn 12272 |
. . . . . . . . . . . . . 14
β’ -1 β
β |
19 | 1, 3 | nvsass 29612 |
. . . . . . . . . . . . . 14
β’ ((π β NrmCVec β§ (-1 β
β β§ i β β β§ π΅ β π)) β ((-1 Β· i)ππ΅) = (-1π(iππ΅))) |
20 | 18, 19 | mp3anr1 1459 |
. . . . . . . . . . . . 13
β’ ((π β NrmCVec β§ (i β
β β§ π΅ β
π)) β ((-1 Β·
i)ππ΅) = (-1π(iππ΅))) |
21 | 12, 20 | mpanr1 702 |
. . . . . . . . . . . 12
β’ ((π β NrmCVec β§ π΅ β π) β ((-1 Β· i)ππ΅) = (-1π(iππ΅))) |
22 | 12 | mulm1i 11605 |
. . . . . . . . . . . . 13
β’ (-1
Β· i) = -i |
23 | 22 | oveq1i 7368 |
. . . . . . . . . . . 12
β’ ((-1
Β· i)ππ΅) = (-iππ΅) |
24 | 21, 23 | eqtr3di 2788 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π΅ β π) β (-1π(iππ΅)) = (-iππ΅)) |
25 | 24 | 3adant2 1132 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (-1π(iππ΅)) = (-iππ΅)) |
26 | 25 | oveq2d 7374 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄πΊ(-1π(iππ΅))) = (π΄πΊ(-iππ΅))) |
27 | 17, 26 | eqtrd 2773 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄π(iππ΅)) = (π΄πΊ(-iππ΅))) |
28 | 27 | fveq2d 6847 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (πβ(π΄π(iππ΅))) = (πβ(π΄πΊ(-iππ΅)))) |
29 | 28 | oveq1d 7373 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((πβ(π΄π(iππ΅)))β2) = ((πβ(π΄πΊ(-iππ΅)))β2)) |
30 | 29 | oveq2d 7374 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄π(iππ΅)))β2)) = (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2))) |
31 | 30 | oveq2d 7374 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄π(iππ΅)))β2))) = (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2)))) |
32 | 11, 31 | oveq12d 7376 |
. . 3
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((((πβ(π΄πΊπ΅))β2) β ((πβ(π΄ππ΅))β2)) + (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄π(iππ΅)))β2)))) = ((((πβ(π΄πΊπ΅))β2) β ((πβ(π΄πΊ(-1ππ΅)))β2)) + (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2))))) |
33 | 32 | oveq1d 7373 |
. 2
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (((((πβ(π΄πΊπ΅))β2) β ((πβ(π΄ππ΅))β2)) + (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄π(iππ΅)))β2)))) / 4) = (((((πβ(π΄πΊπ΅))β2) β ((πβ(π΄πΊ(-1ππ΅)))β2)) + (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2)))) / 4)) |
34 | 6, 33 | eqtr4d 2776 |
1
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄ππ΅) = (((((πβ(π΄πΊπ΅))β2) β ((πβ(π΄ππ΅))β2)) + (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄π(iππ΅)))β2)))) / 4)) |