Metamath Proof Explorer

Theorem ipval2

Description: Expansion of the inner product value ipval . (Contributed by NM, 31-Jan-2007) (Revised by Mario Carneiro, 5-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dipfval.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
dipfval.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
dipfval.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
dipfval.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
dipfval.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
Assertion ipval2 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) = ( ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 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 1 2 3 4 5 ipval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) = ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ) / 4 ) )
7 ax-icn ⊢ i ∈ ℂ
8 1 2 3 4 5 ipval2lem4 ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ i ∈ ℂ ) → ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
9 7 8 mpan2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
10 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ∈ ℂ ) → ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ )
11 7 9 10 sylancr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ )
12 neg1cn ⊢ - 1 ∈ ℂ
13 1 2 3 4 5 ipval2lem4 ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ - 1 ∈ ℂ ) → ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
14 12 13 mpan2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
15 11 14 subcld ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ )
16 negicn ⊢ - i ∈ ℂ
17 1 2 3 4 5 ipval2lem4 ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ - i ∈ ℂ ) → ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
18 16 17 mpan2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
19 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ∈ ℂ ) → ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ )
20 7 18 19 sylancr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ )
21 15 20 negsubd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) + - ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) − ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) )
22 14 mulm1d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) = - ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) )
23 22 oveq2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) + - ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) )
24 11 14 negsubd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) + - ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) )
25 23 24 eqtrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) )
26 mulneg1 ⊢ ( ( i ∈ ℂ ∧ ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ∈ ℂ ) → ( - i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) = - ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) )
27 7 18 26 sylancr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) = - ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) )
28 25 27 oveq12d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) + - ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) )
29 subdi ⊢ ( ( i ∈ ℂ ∧ ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ∈ ℂ ∧ ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ∈ ℂ ) → ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) − ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) )
30 7 29 mp3an1 ⊢ ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ∈ ℂ ∧ ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ∈ ℂ ) → ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) − ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) )
31 9 18 30 syl2anc ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) − ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) )
32 31 oveq1d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) − ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) )
33 11 20 14 sub32d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) − ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) − ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) )
34 32 33 eqtrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) − ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) )
35 21 28 34 3eqtr4d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) )
36 1 3 nvsid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( 1 𝑆 𝐵 ) = 𝐵 )
37 36 oveq2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( 1 𝑆 𝐵 ) ) = ( 𝐴 𝐺 𝐵 ) )
38 37 fveq2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( 1 𝑆 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) )
39 38 oveq1d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 1 𝑆 𝐵 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) )
40 39 3adant2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 1 𝑆 𝐵 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) )
41 40 oveq2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) ) )
42 1 2 3 4 5 ipval2lem3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) ∈ ℝ )
43 42 recnd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) ∈ ℂ )
44 43 mullidd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) ) = ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) )
45 41 44 eqtrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) )
46 35 45 oveq12d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) + ( 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) ) )
47 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
48 df-4 ⊢ 4 = ( 3 + 1 )
49 oveq2 ⊢ ( 𝑘 = 4 → ( i ↑ 𝑘 ) = ( i ↑ 4 ) )
50 i4 ⊢ ( i ↑ 4 ) = 1
51 49 50 eqtrdi ⊢ ( 𝑘 = 4 → ( i ↑ 𝑘 ) = 1 )
52 51 oveq1d ⊢ ( 𝑘 = 4 → ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) = ( 1 𝑆 𝐵 ) )
53 52 oveq2d ⊢ ( 𝑘 = 4 → ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) = ( 𝐴 𝐺 ( 1 𝑆 𝐵 ) ) )
54 53 fveq2d ⊢ ( 𝑘 = 4 → ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 ( 1 𝑆 𝐵 ) ) ) )
55 54 oveq1d ⊢ ( 𝑘 = 4 → ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 1 𝑆 𝐵 ) ) ) ↑ 2 ) )
56 51 55 oveq12d ⊢ ( 𝑘 = 4 → ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) )
57 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
58 expcl ⊢ ( ( i ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( i ↑ 𝑘 ) ∈ ℂ )
59 7 57 58 sylancr ⊢ ( 𝑘 ∈ ℕ → ( i ↑ 𝑘 ) ∈ ℂ )
60 59 adantl ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → ( i ↑ 𝑘 ) ∈ ℂ )
61 1 2 3 4 5 ipval2lem4 ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( i ↑ 𝑘 ) ∈ ℂ ) → ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
62 59 61 sylan2 ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
63 60 62 mulcld ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ )
64 df-3 ⊢ 3 = ( 2 + 1 )
65 oveq2 ⊢ ( 𝑘 = 3 → ( i ↑ 𝑘 ) = ( i ↑ 3 ) )
66 i3 ⊢ ( i ↑ 3 ) = - i
67 65 66 eqtrdi ⊢ ( 𝑘 = 3 → ( i ↑ 𝑘 ) = - i )
68 67 oveq1d ⊢ ( 𝑘 = 3 → ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) = ( - i 𝑆 𝐵 ) )
69 68 oveq2d ⊢ ( 𝑘 = 3 → ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) = ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) )
70 69 fveq2d ⊢ ( 𝑘 = 3 → ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) )
71 70 oveq1d ⊢ ( 𝑘 = 3 → ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) )
72 67 71 oveq12d ⊢ ( 𝑘 = 3 → ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( - i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) )
73 df-2 ⊢ 2 = ( 1 + 1 )
74 oveq2 ⊢ ( 𝑘 = 2 → ( i ↑ 𝑘 ) = ( i ↑ 2 ) )
75 i2 ⊢ ( i ↑ 2 ) = - 1
76 74 75 eqtrdi ⊢ ( 𝑘 = 2 → ( i ↑ 𝑘 ) = - 1 )
77 76 oveq1d ⊢ ( 𝑘 = 2 → ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) = ( - 1 𝑆 𝐵 ) )
78 77 oveq2d ⊢ ( 𝑘 = 2 → ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) = ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) )
79 78 fveq2d ⊢ ( 𝑘 = 2 → ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) )
80 79 oveq1d ⊢ ( 𝑘 = 2 → ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) )
81 76 80 oveq12d ⊢ ( 𝑘 = 2 → ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( - 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) )
82 1z ⊢ 1 ∈ ℤ
83 oveq2 ⊢ ( 𝑘 = 1 → ( i ↑ 𝑘 ) = ( i ↑ 1 ) )
84 exp1 ⊢ ( i ∈ ℂ → ( i ↑ 1 ) = i )
85 7 84 ax-mp ⊢ ( i ↑ 1 ) = i
86 83 85 eqtrdi ⊢ ( 𝑘 = 1 → ( i ↑ 𝑘 ) = i )
87 86 oveq1d ⊢ ( 𝑘 = 1 → ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) = ( i 𝑆 𝐵 ) )
88 87 oveq2d ⊢ ( 𝑘 = 1 → ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) = ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) )
89 88 fveq2d ⊢ ( 𝑘 = 1 → ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) )
90 89 oveq1d ⊢ ( 𝑘 = 1 → ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) )
91 86 90 oveq12d ⊢ ( 𝑘 = 1 → ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) )
92 91 fsum1 ⊢ ( ( 1 ∈ ℤ ∧ ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... 1 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) )
93 82 11 92 sylancr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → Σ 𝑘 ∈ ( 1 ... 1 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) )
94 1nn ⊢ 1 ∈ ℕ
95 93 94 jctil ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 1 ∈ ℕ ∧ Σ 𝑘 ∈ ( 1 ... 1 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) )
96 eqidd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) )
97 47 73 81 63 95 96 fsump1i ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 2 ∈ ℕ ∧ Σ 𝑘 ∈ ( 1 ... 2 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ) )
98 eqidd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) )
99 47 64 72 63 97 98 fsump1i ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 3 ∈ ℕ ∧ Σ 𝑘 ∈ ( 1 ... 3 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ) )
100 eqidd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) + ( 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) + ( 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) )
101 47 48 56 63 99 100 fsump1i ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 4 ∈ ℕ ∧ Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) + ( 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ) )
102 101 simprd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) + ( 1 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) )
103 43 14 subcld ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ )
104 9 18 subcld ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ )
105 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ ) → ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ∈ ℂ )
106 7 104 105 sylancr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ∈ ℂ )
107 103 106 addcomd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ) = ( ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) + ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) )
108 106 14 43 subadd23d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) ) = ( ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) + ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) )
109 107 108 eqtr4d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ) = ( ( ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) ) )
110 46 102 109 3eqtr4d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ) )
111 110 oveq1d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ) / 4 ) = ( ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) )
112 6 111 eqtrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) = ( ( ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - i 𝑆 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) )