Metamath Proof Explorer


Theorem ipval3

Description: Expansion of the inner product value ipval . (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses dipfval.1 𝑋 = ( BaseSet ‘ 𝑈 )
dipfval.2 𝐺 = ( +𝑣𝑈 )
dipfval.4 𝑆 = ( ·𝑠OLD𝑈 )
dipfval.6 𝑁 = ( normCV𝑈 )
dipfval.7 𝑃 = ( ·𝑖OLD𝑈 )
ipval3.3 𝑀 = ( −𝑣𝑈 )
Assertion ipval3 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐴 𝑃 𝐵 ) = ( ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝑀 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) )

Proof

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 ) )