Step |
Hyp |
Ref |
Expression |
1 |
|
dipfval.1 |
⊢ 𝑋 = ( BaseSet ‘ 𝑈 ) |
2 |
|
dipfval.2 |
⊢ 𝐺 = ( +𝑣 ‘ 𝑈 ) |
3 |
|
dipfval.4 |
⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 ) |
4 |
|
dipfval.6 |
⊢ 𝑁 = ( normCV ‘ 𝑈 ) |
5 |
|
dipfval.7 |
⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 ) |
6 |
|
ipval3.3 |
⊢ 𝑀 = ( −𝑣 ‘ 𝑈 ) |
7 |
1 2 3 4 5
|
ipval2 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) = ( ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) ) |
8 |
1 2 3 6
|
nvmval |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐵 ) = ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) |
9 |
8
|
fveq2d |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ) |
10 |
9
|
oveq1d |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) |
11 |
10
|
oveq2d |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) |
12 |
|
ax-icn |
⊢ i ∈ ℂ |
13 |
1 3
|
nvscl |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ i ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( i 𝑆 𝐵 ) ∈ 𝑋 ) |
14 |
12 13
|
mp3an2 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( i 𝑆 𝐵 ) ∈ 𝑋 ) |
15 |
14
|
3adant2 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i 𝑆 𝐵 ) ∈ 𝑋 ) |
16 |
1 2 3 6
|
nvmval |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( i 𝑆 𝐵 ) ∈ 𝑋 ) → ( 𝐴 𝑀 ( i 𝑆 𝐵 ) ) = ( 𝐴 𝐺 ( - 1 𝑆 ( i 𝑆 𝐵 ) ) ) ) |
17 |
15 16
|
syld3an3 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑀 ( i 𝑆 𝐵 ) ) = ( 𝐴 𝐺 ( - 1 𝑆 ( i 𝑆 𝐵 ) ) ) ) |
18 |
|
neg1cn |
⊢ - 1 ∈ ℂ |
19 |
1 3
|
nvsass |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( - 1 ∈ ℂ ∧ i ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → ( ( - 1 · i ) 𝑆 𝐵 ) = ( - 1 𝑆 ( i 𝑆 𝐵 ) ) ) |
20 |
18 19
|
mp3anr1 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( i ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → ( ( - 1 · i ) 𝑆 𝐵 ) = ( - 1 𝑆 ( i 𝑆 𝐵 ) ) ) |
21 |
12 20
|
mpanr1 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( ( - 1 · i ) 𝑆 𝐵 ) = ( - 1 𝑆 ( i 𝑆 𝐵 ) ) ) |
22 |
12
|
mulm1i |
⊢ ( - 1 · i ) = - i |
23 |
22
|
oveq1i |
⊢ ( ( - 1 · i ) 𝑆 𝐵 ) = ( - i 𝑆 𝐵 ) |
24 |
21 23
|
eqtr3di |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 ( i 𝑆 𝐵 ) ) = ( - i 𝑆 𝐵 ) ) |
25 |
24
|
3adant2 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 ( i 𝑆 𝐵 ) ) = ( - i 𝑆 𝐵 ) ) |
26 |
25
|
oveq2d |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 1 𝑆 ( i 𝑆 𝐵 ) ) ) = ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) |
27 |
17 26
|
eqtrd |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑀 ( i 𝑆 𝐵 ) ) = ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) |
28 |
27
|
fveq2d |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝑀 ( i 𝑆 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ) |
29 |
28
|
oveq1d |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 𝑀 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) |
30 |
29
|
oveq2d |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝑀 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) |
31 |
30
|
oveq2d |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝑀 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) = ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ) |
32 |
11 31
|
oveq12d |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝑀 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ) = ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ) ) |
33 |
32
|
oveq1d |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝑀 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) = ( ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) ) |
34 |
7 33
|
eqtr4d |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) = ( ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝑀 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) ) |