Step |
Hyp |
Ref |
Expression |
1 |
|
nvdif.1 |
⊢ 𝑋 = ( BaseSet ‘ 𝑈 ) |
2 |
|
nvdif.2 |
⊢ 𝐺 = ( +𝑣 ‘ 𝑈 ) |
3 |
|
nvdif.4 |
⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 ) |
4 |
|
nvdif.6 |
⊢ 𝑁 = ( normCV ‘ 𝑈 ) |
5 |
|
simp1 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝑈 ∈ NrmCVec ) |
6 |
|
ax-icn |
⊢ i ∈ ℂ |
7 |
1 3
|
nvscl |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ i ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( i 𝑆 𝐵 ) ∈ 𝑋 ) |
8 |
6 7
|
mp3an2 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( i 𝑆 𝐵 ) ∈ 𝑋 ) |
9 |
8
|
3adant2 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i 𝑆 𝐵 ) ∈ 𝑋 ) |
10 |
1 2
|
nvgcl |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( i 𝑆 𝐵 ) ∈ 𝑋 ) → ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ∈ 𝑋 ) |
11 |
9 10
|
syld3an3 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ∈ 𝑋 ) |
12 |
1 4
|
nvcl |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ∈ ℝ ) |
13 |
5 11 12
|
syl2anc |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ∈ ℝ ) |
14 |
13
|
recnd |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ∈ ℂ ) |
15 |
14
|
mulid2d |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 1 · ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) |
16 |
6
|
absnegi |
⊢ ( abs ‘ - i ) = ( abs ‘ i ) |
17 |
|
absi |
⊢ ( abs ‘ i ) = 1 |
18 |
16 17
|
eqtri |
⊢ ( abs ‘ - i ) = 1 |
19 |
18
|
oveq1i |
⊢ ( ( abs ‘ - i ) · ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) = ( 1 · ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) |
20 |
|
negicn |
⊢ - i ∈ ℂ |
21 |
1 3 4
|
nvs |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ - i ∈ ℂ ∧ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ∈ 𝑋 ) → ( 𝑁 ‘ ( - i 𝑆 ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) = ( ( abs ‘ - i ) · ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) ) |
22 |
20 21
|
mp3an2 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ∈ 𝑋 ) → ( 𝑁 ‘ ( - i 𝑆 ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) = ( ( abs ‘ - i ) · ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) ) |
23 |
5 11 22
|
syl2anc |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( - i 𝑆 ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) = ( ( abs ‘ - i ) · ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) ) |
24 |
|
simp2 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 ) |
25 |
1 2 3
|
nvdi |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( - i ∈ ℂ ∧ 𝐴 ∈ 𝑋 ∧ ( i 𝑆 𝐵 ) ∈ 𝑋 ) ) → ( - i 𝑆 ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) = ( ( - i 𝑆 𝐴 ) 𝐺 ( - i 𝑆 ( i 𝑆 𝐵 ) ) ) ) |
26 |
20 25
|
mp3anr1 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ ( i 𝑆 𝐵 ) ∈ 𝑋 ) ) → ( - i 𝑆 ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) = ( ( - i 𝑆 𝐴 ) 𝐺 ( - i 𝑆 ( i 𝑆 𝐵 ) ) ) ) |
27 |
5 24 9 26
|
syl12anc |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - i 𝑆 ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) = ( ( - i 𝑆 𝐴 ) 𝐺 ( - i 𝑆 ( i 𝑆 𝐵 ) ) ) ) |
28 |
6 6
|
mulneg1i |
⊢ ( - i · i ) = - ( i · i ) |
29 |
|
ixi |
⊢ ( i · i ) = - 1 |
30 |
29
|
negeqi |
⊢ - ( i · i ) = - - 1 |
31 |
|
negneg1e1 |
⊢ - - 1 = 1 |
32 |
30 31
|
eqtri |
⊢ - ( i · i ) = 1 |
33 |
28 32
|
eqtri |
⊢ ( - i · i ) = 1 |
34 |
33
|
oveq1i |
⊢ ( ( - i · i ) 𝑆 𝐵 ) = ( 1 𝑆 𝐵 ) |
35 |
1 3
|
nvsass |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( - i ∈ ℂ ∧ i ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → ( ( - i · i ) 𝑆 𝐵 ) = ( - i 𝑆 ( i 𝑆 𝐵 ) ) ) |
36 |
20 35
|
mp3anr1 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( i ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → ( ( - i · i ) 𝑆 𝐵 ) = ( - i 𝑆 ( i 𝑆 𝐵 ) ) ) |
37 |
6 36
|
mpanr1 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( ( - i · i ) 𝑆 𝐵 ) = ( - i 𝑆 ( i 𝑆 𝐵 ) ) ) |
38 |
1 3
|
nvsid |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( 1 𝑆 𝐵 ) = 𝐵 ) |
39 |
34 37 38
|
3eqtr3a |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( - i 𝑆 ( i 𝑆 𝐵 ) ) = 𝐵 ) |
40 |
39
|
3adant2 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - i 𝑆 ( i 𝑆 𝐵 ) ) = 𝐵 ) |
41 |
40
|
oveq2d |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( - i 𝑆 𝐴 ) 𝐺 ( - i 𝑆 ( i 𝑆 𝐵 ) ) ) = ( ( - i 𝑆 𝐴 ) 𝐺 𝐵 ) ) |
42 |
1 3
|
nvscl |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ - i ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( - i 𝑆 𝐴 ) ∈ 𝑋 ) |
43 |
20 42
|
mp3an2 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( - i 𝑆 𝐴 ) ∈ 𝑋 ) |
44 |
43
|
3adant3 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - i 𝑆 𝐴 ) ∈ 𝑋 ) |
45 |
1 2
|
nvcom |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( - i 𝑆 𝐴 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( - i 𝑆 𝐴 ) 𝐺 𝐵 ) = ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) |
46 |
44 45
|
syld3an2 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( - i 𝑆 𝐴 ) 𝐺 𝐵 ) = ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) |
47 |
27 41 46
|
3eqtrd |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - i 𝑆 ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) = ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) |
48 |
47
|
fveq2d |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( - i 𝑆 ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) = ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ) |
49 |
23 48
|
eqtr3d |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( abs ‘ - i ) · ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) = ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ) |
50 |
19 49
|
eqtr3id |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 1 · ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) = ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ) |
51 |
15 50
|
eqtr3d |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) ) |