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 12 mulm1i ⊢ ( - 1 · i ) = - i
19 18 oveq1i ⊢ ( ( - 1 · i ) 𝑆 𝐵 ) = ( - i 𝑆 𝐵 )
20 neg1cn ⊢ - 1 ∈ ℂ
21 1 3 nvsass ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( - 1 ∈ ℂ ∧ i ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → ( ( - 1 · i ) 𝑆 𝐵 ) = ( - 1 𝑆 ( i 𝑆 𝐵 ) ) )
22 20 21 mp3anr1 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( i ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) ) → ( ( - 1 · i ) 𝑆 𝐵 ) = ( - 1 𝑆 ( i 𝑆 𝐵 ) ) )
23 12 22 mpanr1 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( ( - 1 · i ) 𝑆 𝐵 ) = ( - 1 𝑆 ( i 𝑆 𝐵 ) ) )
24 19 23 syl5reqr ⊢ ( ( 𝑈 ∈ 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 ) )