Step | Hyp | Ref
| Expression |
1 | | dipfval.1 |
. . . 4
β’ π = (BaseSetβπ) |
2 | | dipfval.2 |
. . . 4
β’ πΊ = ( +π£
βπ) |
3 | | dipfval.4 |
. . . 4
β’ π = (
Β·π OLD βπ) |
4 | | dipfval.6 |
. . . 4
β’ π =
(normCVβπ) |
5 | | dipfval.7 |
. . . 4
β’ π =
(Β·πOLDβπ) |
6 | 1, 2, 3, 4, 5 | ipval2 29691 |
. . 3
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄ππ΅) = (((((πβ(π΄πΊπ΅))β2) β ((πβ(π΄πΊ(-1ππ΅)))β2)) + (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2)))) / 4)) |
7 | 6 | oveq2d 7374 |
. 2
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (4 Β· (π΄ππ΅)) = (4 Β· (((((πβ(π΄πΊπ΅))β2) β ((πβ(π΄πΊ(-1ππ΅)))β2)) + (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2)))) / 4))) |
8 | | simp1 1137 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β π β NrmCVec) |
9 | 1, 2 | nvgcl 29604 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) β π) |
10 | 1, 4 | nvcl 29645 |
. . . . . . . 8
β’ ((π β NrmCVec β§ (π΄πΊπ΅) β π) β (πβ(π΄πΊπ΅)) β β) |
11 | 8, 9, 10 | syl2anc 585 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (πβ(π΄πΊπ΅)) β β) |
12 | 11 | recnd 11188 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (πβ(π΄πΊπ΅)) β β) |
13 | 12 | sqcld 14055 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((πβ(π΄πΊπ΅))β2) β β) |
14 | | neg1cn 12272 |
. . . . . . . . . . 11
β’ -1 β
β |
15 | 1, 3 | nvscl 29610 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ -1 β
β β§ π΅ β
π) β (-1ππ΅) β π) |
16 | 14, 15 | mp3an2 1450 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π΅ β π) β (-1ππ΅) β π) |
17 | 16 | 3adant2 1132 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (-1ππ΅) β π) |
18 | 1, 2 | nvgcl 29604 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π΄ β π β§ (-1ππ΅) β π) β (π΄πΊ(-1ππ΅)) β π) |
19 | 17, 18 | syld3an3 1410 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄πΊ(-1ππ΅)) β π) |
20 | 1, 4 | nvcl 29645 |
. . . . . . . 8
β’ ((π β NrmCVec β§ (π΄πΊ(-1ππ΅)) β π) β (πβ(π΄πΊ(-1ππ΅))) β β) |
21 | 8, 19, 20 | syl2anc 585 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (πβ(π΄πΊ(-1ππ΅))) β β) |
22 | 21 | recnd 11188 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (πβ(π΄πΊ(-1ππ΅))) β β) |
23 | 22 | sqcld 14055 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((πβ(π΄πΊ(-1ππ΅)))β2) β β) |
24 | 13, 23 | subcld 11517 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (((πβ(π΄πΊπ΅))β2) β ((πβ(π΄πΊ(-1ππ΅)))β2)) β
β) |
25 | | ax-icn 11115 |
. . . . 5
β’ i β
β |
26 | 1, 3 | nvscl 29610 |
. . . . . . . . . . . 12
β’ ((π β NrmCVec β§ i β
β β§ π΅ β
π) β (iππ΅) β π) |
27 | 25, 26 | mp3an2 1450 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π΅ β π) β (iππ΅) β π) |
28 | 27 | 3adant2 1132 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (iππ΅) β π) |
29 | 1, 2 | nvgcl 29604 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π΄ β π β§ (iππ΅) β π) β (π΄πΊ(iππ΅)) β π) |
30 | 28, 29 | syld3an3 1410 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄πΊ(iππ΅)) β π) |
31 | 1, 4 | nvcl 29645 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ (π΄πΊ(iππ΅)) β π) β (πβ(π΄πΊ(iππ΅))) β β) |
32 | 8, 30, 31 | syl2anc 585 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (πβ(π΄πΊ(iππ΅))) β β) |
33 | 32 | recnd 11188 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (πβ(π΄πΊ(iππ΅))) β β) |
34 | 33 | sqcld 14055 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((πβ(π΄πΊ(iππ΅)))β2) β β) |
35 | | negicn 11407 |
. . . . . . . . . . . 12
β’ -i β
β |
36 | 1, 3 | nvscl 29610 |
. . . . . . . . . . . 12
β’ ((π β NrmCVec β§ -i β
β β§ π΅ β
π) β (-iππ΅) β π) |
37 | 35, 36 | mp3an2 1450 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π΅ β π) β (-iππ΅) β π) |
38 | 37 | 3adant2 1132 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (-iππ΅) β π) |
39 | 1, 2 | nvgcl 29604 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π΄ β π β§ (-iππ΅) β π) β (π΄πΊ(-iππ΅)) β π) |
40 | 38, 39 | syld3an3 1410 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄πΊ(-iππ΅)) β π) |
41 | 1, 4 | nvcl 29645 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ (π΄πΊ(-iππ΅)) β π) β (πβ(π΄πΊ(-iππ΅))) β β) |
42 | 8, 40, 41 | syl2anc 585 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (πβ(π΄πΊ(-iππ΅))) β β) |
43 | 42 | recnd 11188 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (πβ(π΄πΊ(-iππ΅))) β β) |
44 | 43 | sqcld 14055 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((πβ(π΄πΊ(-iππ΅)))β2) β β) |
45 | 34, 44 | subcld 11517 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2)) β
β) |
46 | | mulcl 11140 |
. . . . 5
β’ ((i
β β β§ (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2)) β β) β (i
Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2))) β
β) |
47 | 25, 45, 46 | sylancr 588 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2))) β
β) |
48 | 24, 47 | addcld 11179 |
. . 3
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((((πβ(π΄πΊπ΅))β2) β ((πβ(π΄πΊ(-1ππ΅)))β2)) + (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2)))) β
β) |
49 | | 4cn 12243 |
. . . 4
β’ 4 β
β |
50 | | 4ne0 12266 |
. . . 4
β’ 4 β
0 |
51 | | divcan2 11826 |
. . . 4
β’
((((((πβ(π΄πΊπ΅))β2) β ((πβ(π΄πΊ(-1ππ΅)))β2)) + (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2)))) β β β§ 4 β
β β§ 4 β 0) β (4 Β· (((((πβ(π΄πΊπ΅))β2) β ((πβ(π΄πΊ(-1ππ΅)))β2)) + (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2)))) / 4)) = ((((πβ(π΄πΊπ΅))β2) β ((πβ(π΄πΊ(-1ππ΅)))β2)) + (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2))))) |
52 | 49, 50, 51 | mp3an23 1454 |
. . 3
β’
(((((πβ(π΄πΊπ΅))β2) β ((πβ(π΄πΊ(-1ππ΅)))β2)) + (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2)))) β β β (4
Β· (((((πβ(π΄πΊπ΅))β2) β ((πβ(π΄πΊ(-1ππ΅)))β2)) + (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2)))) / 4)) = ((((πβ(π΄πΊπ΅))β2) β ((πβ(π΄πΊ(-1ππ΅)))β2)) + (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2))))) |
53 | 48, 52 | syl 17 |
. 2
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (4 Β· (((((πβ(π΄πΊπ΅))β2) β ((πβ(π΄πΊ(-1ππ΅)))β2)) + (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2)))) / 4)) = ((((πβ(π΄πΊπ΅))β2) β ((πβ(π΄πΊ(-1ππ΅)))β2)) + (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2))))) |
54 | 7, 53 | eqtrd 2773 |
1
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (4 Β· (π΄ππ΅)) = ((((πβ(π΄πΊπ΅))β2) β ((πβ(π΄πΊ(-1ππ΅)))β2)) + (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2))))) |