Metamath Proof Explorer

Theorem 4ipval2

Description: Four times the inner product value ipval3 , useful for simplifying certain proofs. (Contributed by NM, 10-Apr-2007) (New usage is discouraged.)

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

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 1 2 3 4 5 ipval2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) = ( ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) )
7 6 oveq2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 4 · ( 𝐴 𝑃 𝐵 ) ) = ( 4 · ( ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) ) )
8 simp1 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝑈 ∈ NrmCVec )
9 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )
10 1 4 nvcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ∈ ℝ )
11 8 9 10 syl2anc ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ∈ ℝ )
12 11 recnd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ∈ ℂ )
13 12 sqcld ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) ∈ ℂ )
14 neg1cn ⊢ - 1 ∈ ℂ
15 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 𝐵 ) ∈ 𝑋 )
16 14 15 mp3an2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 𝐵 ) ∈ 𝑋 )
17 16 3adant2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 𝐵 ) ∈ 𝑋 )
18 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( - 1 𝑆 𝐵 ) ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 )
19 17 18 syld3an3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 )
20 1 4 nvcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ∈ ℝ )
21 8 19 20 syl2anc ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ∈ ℝ )
22 21 recnd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ∈ ℂ )
23 22 sqcld ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
24 13 23 subcld ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ )
25 ax-icn ⊢ i ∈ ℂ
26 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ i ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( i 𝑆 𝐵 ) ∈ 𝑋 )
27 25 26 mp3an2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( i 𝑆 𝐵 ) ∈ 𝑋 )
28 27 3adant2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i 𝑆 𝐵 ) ∈ 𝑋 )
29 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( i 𝑆 𝐵 ) ∈ 𝑋 ) → ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ∈ 𝑋 )
30 28 29 syld3an3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ∈ 𝑋 )
31 1 4 nvcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ∈ ℝ )
32 8 30 31 syl2anc ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ∈ ℝ )
33 32 recnd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ∈ ℂ )
34 33 sqcld ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
35 negicn ⊢ - i ∈ ℂ
36 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - i ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( - i 𝑆 𝐵 ) ∈ 𝑋 )
37 35 36 mp3an2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( - i 𝑆 𝐵 ) ∈ 𝑋 )
38 37 3adant2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - i 𝑆 𝐵 ) ∈ 𝑋 )
39 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( - i 𝑆 𝐵 ) ∈ 𝑋 ) → ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ∈ 𝑋 )
40 38 39 syld3an3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ∈ 𝑋 )
41 1 4 nvcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ∈ ℝ )
42 8 40 41 syl2anc ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ∈ ℝ )
43 42 recnd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ∈ ℂ )
44 43 sqcld ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
45 34 44 subcld ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ )
46 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ ) → ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ∈ ℂ )
47 25 45 46 sylancr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ∈ ℂ )
48 24 47 addcld ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ) ∈ ℂ )
49 4cn ⊢ 4 ∈ ℂ
50 4ne0 ⊢ 4 ≠ 0
51 divcan2 ⊢ ( ( ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 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 ⊢ ( ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 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 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 4 · ( ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) ) = ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ) )
54 7 53 eqtrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 4 · ( 𝐴 𝑃 𝐵 ) ) = ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ) )