Metamath Proof Explorer

Theorem cphipval

Description: Value of the inner product expressed by a sum of terms with the norm defined by the inner product. Equation 6.45 of Ponnusamy p. 361. (Contributed by NM, 31-Jan-2007) (Revised by AV, 18-Oct-2021)

Ref Expression
Hypotheses cphipfval.x ⊢ 𝑋 = ( Base ‘ 𝑊 )
cphipfval.p ⊢ + = ( +g ‘ 𝑊 )
cphipfval.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
cphipfval.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
cphipfval.i ⊢ , = ( ·𝑖 ‘ 𝑊 )
cphipval.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
cphipval.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion cphipval ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 , 𝐵 ) = ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) ) / 4 ) )

Proof

Step Hyp Ref Expression
1 cphipfval.x ⊢ 𝑋 = ( Base ‘ 𝑊 )
2 cphipfval.p ⊢ + = ( +g ‘ 𝑊 )
3 cphipfval.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
4 cphipfval.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
5 cphipfval.i ⊢ , = ( ·𝑖 ‘ 𝑊 )
6 cphipval.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
7 cphipval.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
8 eqid ⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
9 1 2 3 4 5 8 6 7 cphipval2 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 , 𝐵 ) = ( ( ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) )
10 ax-icn ⊢ i ∈ ℂ
11 10 a1i ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → i ∈ ℂ )
12 simp1l ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝑊 ∈ ℂPreHil )
13 cphngp ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp )
14 ngpgrp ⊢ ( 𝑊 ∈ NrmGrp → 𝑊 ∈ Grp )
15 13 14 syl ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ Grp )
16 15 adantr ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) → 𝑊 ∈ Grp )
17 16 3ad2ant1 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝑊 ∈ Grp )
18 simp2 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
19 cphlmod ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod )
20 19 3anim1i ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑊 ∈ LMod ∧ i ∈ 𝐾 ∧ 𝐵 ∈ 𝑋 ) )
21 20 3expa ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐵 ∈ 𝑋 ) → ( 𝑊 ∈ LMod ∧ i ∈ 𝐾 ∧ 𝐵 ∈ 𝑋 ) )
22 1 6 3 7 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ i ∈ 𝐾 ∧ 𝐵 ∈ 𝑋 ) → ( i · 𝐵 ) ∈ 𝑋 )
23 21 22 syl ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐵 ∈ 𝑋 ) → ( i · 𝐵 ) ∈ 𝑋 )
24 23 3adant2 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · 𝐵 ) ∈ 𝑋 )
25 1 2 grpcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( i · 𝐵 ) ∈ 𝑋 ) → ( 𝐴 + ( i · 𝐵 ) ) ∈ 𝑋 )
26 17 18 24 25 syl3anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 + ( i · 𝐵 ) ) ∈ 𝑋 )
27 1 5 4 nmsq ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 + ( i · 𝐵 ) ) ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝐴 + ( i · 𝐵 ) ) , ( 𝐴 + ( i · 𝐵 ) ) ) )
28 12 26 27 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝐴 + ( i · 𝐵 ) ) , ( 𝐴 + ( i · 𝐵 ) ) ) )
29 1 5 reipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 + ( i · 𝐵 ) ) ∈ 𝑋 ) → ( ( 𝐴 + ( i · 𝐵 ) ) , ( 𝐴 + ( i · 𝐵 ) ) ) ∈ ℝ )
30 12 26 29 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 + ( i · 𝐵 ) ) , ( 𝐴 + ( i · 𝐵 ) ) ) ∈ ℝ )
31 30 recnd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 + ( i · 𝐵 ) ) , ( 𝐴 + ( i · 𝐵 ) ) ) ∈ ℂ )
32 28 31 eqeltrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
33 11 32 mulcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ )
34 19 adantr ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) → 𝑊 ∈ LMod )
35 34 3ad2ant1 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝑊 ∈ LMod )
36 cphclm ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod )
37 6 7 clmneg1 ⊢ ( 𝑊 ∈ ℂMod → - 1 ∈ 𝐾 )
38 36 37 syl ⊢ ( 𝑊 ∈ ℂPreHil → - 1 ∈ 𝐾 )
39 38 adantr ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) → - 1 ∈ 𝐾 )
40 39 3ad2ant1 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → - 1 ∈ 𝐾 )
41 simp3 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
42 1 6 3 7 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ - 1 ∈ 𝐾 ∧ 𝐵 ∈ 𝑋 ) → ( - 1 · 𝐵 ) ∈ 𝑋 )
43 35 40 41 42 syl3anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - 1 · 𝐵 ) ∈ 𝑋 )
44 1 2 grpcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( - 1 · 𝐵 ) ∈ 𝑋 ) → ( 𝐴 + ( - 1 · 𝐵 ) ) ∈ 𝑋 )
45 17 18 43 44 syl3anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 + ( - 1 · 𝐵 ) ) ∈ 𝑋 )
46 1 5 4 nmsq ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 + ( - 1 · 𝐵 ) ) ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝐴 + ( - 1 · 𝐵 ) ) , ( 𝐴 + ( - 1 · 𝐵 ) ) ) )
47 12 45 46 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝐴 + ( - 1 · 𝐵 ) ) , ( 𝐴 + ( - 1 · 𝐵 ) ) ) )
48 1 5 reipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 + ( - 1 · 𝐵 ) ) ∈ 𝑋 ) → ( ( 𝐴 + ( - 1 · 𝐵 ) ) , ( 𝐴 + ( - 1 · 𝐵 ) ) ) ∈ ℝ )
49 12 45 48 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 + ( - 1 · 𝐵 ) ) , ( 𝐴 + ( - 1 · 𝐵 ) ) ) ∈ ℝ )
50 47 49 eqeltrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) ∈ ℝ )
51 50 recnd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
52 addneg1mul ⊢ ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ ∧ ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) ∈ ℂ ) → ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) ) )
53 33 51 52 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) ) )
54 36 adantr ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) → 𝑊 ∈ ℂMod )
55 1 2 8 6 3 clmvsubval ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) = ( 𝐴 + ( - 1 · 𝐵 ) ) )
56 55 eqcomd ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 + ( - 1 · 𝐵 ) ) = ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) )
57 54 56 syl3an1 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 + ( - 1 · 𝐵 ) ) = ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) )
58 57 fveq2d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) )
59 58 oveq1d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) )
60 59 oveq2d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) ) = ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) )
61 53 60 eqtrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) )
62 eqid ⊢ ( invg ‘ 𝑊 ) = ( invg ‘ 𝑊 )
63 54 3ad2ant1 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝑊 ∈ ℂMod )
64 simp1r ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → i ∈ 𝐾 )
65 1 6 3 62 7 63 41 64 clmvsneg ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( invg ‘ 𝑊 ) ‘ ( i · 𝐵 ) ) = ( - i · 𝐵 ) )
66 65 eqcomd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - i · 𝐵 ) = ( ( invg ‘ 𝑊 ) ‘ ( i · 𝐵 ) ) )
67 66 oveq2d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 + ( - i · 𝐵 ) ) = ( 𝐴 + ( ( invg ‘ 𝑊 ) ‘ ( i · 𝐵 ) ) ) )
68 1 2 62 8 grpsubval ⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( i · 𝐵 ) ∈ 𝑋 ) → ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) = ( 𝐴 + ( ( invg ‘ 𝑊 ) ‘ ( i · 𝐵 ) ) ) )
69 18 24 68 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) = ( 𝐴 + ( ( invg ‘ 𝑊 ) ‘ ( i · 𝐵 ) ) ) )
70 67 69 eqtr4d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 + ( - i · 𝐵 ) ) = ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) )
71 70 fveq2d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 + ( - i · 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) )
72 71 oveq1d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + ( - i · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) )
73 72 oveq2d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - i · ( ( 𝑁 ‘ ( 𝐴 + ( - i · 𝐵 ) ) ) ↑ 2 ) ) = ( - i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) )
74 61 73 oveq12d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 + ( - i · 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) )
75 54 anim1i ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐵 ∈ 𝑋 ) → ( 𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑋 ) )
76 75 3adant2 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑋 ) )
77 1 3 clmvs1 ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑋 ) → ( 1 · 𝐵 ) = 𝐵 )
78 76 77 syl ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 1 · 𝐵 ) = 𝐵 )
79 78 oveq2d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 + ( 1 · 𝐵 ) ) = ( 𝐴 + 𝐵 ) )
80 79 fveq2d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 + ( 1 · 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) )
81 80 oveq1d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + ( 1 · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) )
82 81 oveq2d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 1 · ( ( 𝑁 ‘ ( 𝐴 + ( 1 · 𝐵 ) ) ) ↑ 2 ) ) = ( 1 · ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) ) )
83 1 2 grpcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 + 𝐵 ) ∈ 𝑋 )
84 16 83 syl3an1 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 + 𝐵 ) ∈ 𝑋 )
85 1 5 4 nmsq ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 + 𝐵 ) ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 + 𝐵 ) , ( 𝐴 + 𝐵 ) ) )
86 12 84 85 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 + 𝐵 ) , ( 𝐴 + 𝐵 ) ) )
87 1 5 reipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 + 𝐵 ) ∈ 𝑋 ) → ( ( 𝐴 + 𝐵 ) , ( 𝐴 + 𝐵 ) ) ∈ ℝ )
88 12 84 87 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 + 𝐵 ) , ( 𝐴 + 𝐵 ) ) ∈ ℝ )
89 86 88 eqeltrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) ∈ ℝ )
90 89 recnd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) ∈ ℂ )
91 90 mullidd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 1 · ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) ) = ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) )
92 82 91 eqtrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 1 · ( ( 𝑁 ‘ ( 𝐴 + ( 1 · 𝐵 ) ) ) ↑ 2 ) ) = ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) )
93 74 92 oveq12d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 + ( - i · 𝐵 ) ) ) ↑ 2 ) ) ) + ( 1 · ( ( 𝑁 ‘ ( 𝐴 + ( 1 · 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) + ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) ) )
94 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
95 df-4 ⊢ 4 = ( 3 + 1 )
96 oveq2 ⊢ ( 𝑘 = 4 → ( i ↑ 𝑘 ) = ( i ↑ 4 ) )
97 i4 ⊢ ( i ↑ 4 ) = 1
98 96 97 eqtrdi ⊢ ( 𝑘 = 4 → ( i ↑ 𝑘 ) = 1 )
99 98 oveq1d ⊢ ( 𝑘 = 4 → ( ( i ↑ 𝑘 ) · 𝐵 ) = ( 1 · 𝐵 ) )
100 99 oveq2d ⊢ ( 𝑘 = 4 → ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) = ( 𝐴 + ( 1 · 𝐵 ) ) )
101 100 fveq2d ⊢ ( 𝑘 = 4 → ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐴 + ( 1 · 𝐵 ) ) ) )
102 101 oveq1d ⊢ ( 𝑘 = 4 → ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 + ( 1 · 𝐵 ) ) ) ↑ 2 ) )
103 98 102 oveq12d ⊢ ( 𝑘 = 4 → ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) ) = ( 1 · ( ( 𝑁 ‘ ( 𝐴 + ( 1 · 𝐵 ) ) ) ↑ 2 ) ) )
104 10 a1i ⊢ ( 𝑘 ∈ ℕ → i ∈ ℂ )
105 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
106 104 105 expcld ⊢ ( 𝑘 ∈ ℕ → ( i ↑ 𝑘 ) ∈ ℂ )
107 106 adantl ⊢ ( ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → ( i ↑ 𝑘 ) ∈ ℂ )
108 12 adantr ⊢ ( ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → 𝑊 ∈ ℂPreHil )
109 17 adantr ⊢ ( ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → 𝑊 ∈ Grp )
110 18 adantr ⊢ ( ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ 𝑋 )
111 35 adantr ⊢ ( ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → 𝑊 ∈ LMod )
112 36 anim1i ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) → ( 𝑊 ∈ ℂMod ∧ i ∈ 𝐾 ) )
113 112 3ad2ant1 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑊 ∈ ℂMod ∧ i ∈ 𝐾 ) )
114 6 7 cmodscexp ⊢ ( ( ( 𝑊 ∈ ℂMod ∧ i ∈ 𝐾 ) ∧ 𝑘 ∈ ℕ ) → ( i ↑ 𝑘 ) ∈ 𝐾 )
115 113 114 sylan ⊢ ( ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → ( i ↑ 𝑘 ) ∈ 𝐾 )
116 41 adantr ⊢ ( ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → 𝐵 ∈ 𝑋 )
117 1 6 3 7 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ ( i ↑ 𝑘 ) ∈ 𝐾 ∧ 𝐵 ∈ 𝑋 ) → ( ( i ↑ 𝑘 ) · 𝐵 ) ∈ 𝑋 )
118 111 115 116 117 syl3anc ⊢ ( ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → ( ( i ↑ 𝑘 ) · 𝐵 ) ∈ 𝑋 )
119 1 2 grpcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( ( i ↑ 𝑘 ) · 𝐵 ) ∈ 𝑋 ) → ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ∈ 𝑋 )
120 109 110 118 119 syl3anc ⊢ ( ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ∈ 𝑋 )
121 1 5 4 nmsq ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) , ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) )
122 108 120 121 syl2anc ⊢ ( ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) , ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) )
123 1 5 reipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ∈ 𝑋 ) → ( ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) , ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ∈ ℝ )
124 108 120 123 syl2anc ⊢ ( ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) , ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ∈ ℝ )
125 124 recnd ⊢ ( ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) , ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ∈ ℂ )
126 122 125 eqeltrd ⊢ ( ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
127 107 126 mulcld ⊢ ( ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ )
128 df-3 ⊢ 3 = ( 2 + 1 )
129 oveq2 ⊢ ( 𝑘 = 3 → ( i ↑ 𝑘 ) = ( i ↑ 3 ) )
130 i3 ⊢ ( i ↑ 3 ) = - i
131 129 130 eqtrdi ⊢ ( 𝑘 = 3 → ( i ↑ 𝑘 ) = - i )
132 131 oveq1d ⊢ ( 𝑘 = 3 → ( ( i ↑ 𝑘 ) · 𝐵 ) = ( - i · 𝐵 ) )
133 132 oveq2d ⊢ ( 𝑘 = 3 → ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) = ( 𝐴 + ( - i · 𝐵 ) ) )
134 133 fveq2d ⊢ ( 𝑘 = 3 → ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐴 + ( - i · 𝐵 ) ) ) )
135 134 oveq1d ⊢ ( 𝑘 = 3 → ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 + ( - i · 𝐵 ) ) ) ↑ 2 ) )
136 131 135 oveq12d ⊢ ( 𝑘 = 3 → ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) ) = ( - i · ( ( 𝑁 ‘ ( 𝐴 + ( - i · 𝐵 ) ) ) ↑ 2 ) ) )
137 10 a1i ⊢ ( ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → i ∈ ℂ )
138 105 adantl ⊢ ( ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ0 )
139 137 138 expcld ⊢ ( ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → ( i ↑ 𝑘 ) ∈ ℂ )
140 123 recnd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ∈ 𝑋 ) → ( ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) , ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ∈ ℂ )
141 108 120 140 syl2anc ⊢ ( ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) , ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ∈ ℂ )
142 122 141 eqeltrd ⊢ ( ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
143 139 142 mulcld ⊢ ( ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ )
144 df-2 ⊢ 2 = ( 1 + 1 )
145 oveq2 ⊢ ( 𝑘 = 2 → ( i ↑ 𝑘 ) = ( i ↑ 2 ) )
146 i2 ⊢ ( i ↑ 2 ) = - 1
147 145 146 eqtrdi ⊢ ( 𝑘 = 2 → ( i ↑ 𝑘 ) = - 1 )
148 147 oveq1d ⊢ ( 𝑘 = 2 → ( ( i ↑ 𝑘 ) · 𝐵 ) = ( - 1 · 𝐵 ) )
149 148 oveq2d ⊢ ( 𝑘 = 2 → ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) = ( 𝐴 + ( - 1 · 𝐵 ) ) )
150 149 fveq2d ⊢ ( 𝑘 = 2 → ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) )
151 150 oveq1d ⊢ ( 𝑘 = 2 → ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) )
152 147 151 oveq12d ⊢ ( 𝑘 = 2 → ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) ) = ( - 1 · ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) ) )
153 139 126 mulcld ⊢ ( ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ )
154 1z ⊢ 1 ∈ ℤ
155 oveq2 ⊢ ( 𝑘 = 1 → ( i ↑ 𝑘 ) = ( i ↑ 1 ) )
156 exp1 ⊢ ( i ∈ ℂ → ( i ↑ 1 ) = i )
157 10 156 ax-mp ⊢ ( i ↑ 1 ) = i
158 155 157 eqtrdi ⊢ ( 𝑘 = 1 → ( i ↑ 𝑘 ) = i )
159 158 oveq1d ⊢ ( 𝑘 = 1 → ( ( i ↑ 𝑘 ) · 𝐵 ) = ( i · 𝐵 ) )
160 159 oveq2d ⊢ ( 𝑘 = 1 → ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) = ( 𝐴 + ( i · 𝐵 ) ) )
161 160 fveq2d ⊢ ( 𝑘 = 1 → ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) )
162 161 oveq1d ⊢ ( 𝑘 = 1 → ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) )
163 158 162 oveq12d ⊢ ( 𝑘 = 1 → ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) ) = ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) )
164 163 fsum1 ⊢ ( ( 1 ∈ ℤ ∧ ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... 1 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) ) = ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) )
165 154 33 164 sylancr ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → Σ 𝑘 ∈ ( 1 ... 1 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) ) = ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) )
166 1nn ⊢ 1 ∈ ℕ
167 165 166 jctil ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 1 ∈ ℕ ∧ Σ 𝑘 ∈ ( 1 ... 1 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) ) = ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) ) )
168 eqidd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) ) ) )
169 94 144 152 153 167 168 fsump1i ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 2 ∈ ℕ ∧ Σ 𝑘 ∈ ( 1 ... 2 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) ) = ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) ) ) ) )
170 eqidd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 + ( - i · 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 + ( - i · 𝐵 ) ) ) ↑ 2 ) ) ) )
171 94 128 136 143 169 170 fsump1i ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 3 ∈ ℕ ∧ Σ 𝑘 ∈ ( 1 ... 3 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) ) = ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 + ( - i · 𝐵 ) ) ) ↑ 2 ) ) ) ) )
172 eqidd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 + ( - i · 𝐵 ) ) ) ↑ 2 ) ) ) + ( 1 · ( ( 𝑁 ‘ ( 𝐴 + ( 1 · 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 + ( - i · 𝐵 ) ) ) ↑ 2 ) ) ) + ( 1 · ( ( 𝑁 ‘ ( 𝐴 + ( 1 · 𝐵 ) ) ) ↑ 2 ) ) ) )
173 94 95 103 127 171 172 fsump1i ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 4 ∈ ℕ ∧ Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) ) = ( ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 + ( - i · 𝐵 ) ) ) ↑ 2 ) ) ) + ( 1 · ( ( 𝑁 ‘ ( 𝐴 + ( 1 · 𝐵 ) ) ) ↑ 2 ) ) ) ) )
174 173 simprd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) ) = ( ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) + ( - 1 · ( ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ↑ 2 ) ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 + ( - i · 𝐵 ) ) ) ↑ 2 ) ) ) + ( 1 · ( ( 𝑁 ‘ ( 𝐴 + ( 1 · 𝐵 ) ) ) ↑ 2 ) ) ) )
175 1 8 grpsubcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ∈ 𝑋 )
176 16 175 syl3an1 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ∈ 𝑋 )
177 1 5 4 nmsq ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) )
178 12 176 177 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) )
179 1 5 reipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ∈ 𝑋 ) → ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ∈ ℝ )
180 12 176 179 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ∈ ℝ )
181 178 180 eqeltrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ∈ ℝ )
182 181 recnd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ∈ ℂ )
183 90 182 subcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) ∈ ℂ )
184 1 8 grpsubcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( i · 𝐵 ) ∈ 𝑋 ) → ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ∈ 𝑋 )
185 17 18 24 184 syl3anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ∈ 𝑋 )
186 1 5 4 nmsq ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) , ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) )
187 12 185 186 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) , ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) )
188 1 5 reipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ∈ 𝑋 ) → ( ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) , ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ∈ ℝ )
189 12 185 188 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) , ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ∈ ℝ )
190 187 189 eqeltrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ∈ ℝ )
191 190 recnd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
192 32 191 subcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ )
193 11 192 mulcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) ∈ ℂ )
194 183 193 addcomd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) ) = ( ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) + ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) ) )
195 193 182 90 subadd23d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) + ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) ) = ( ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) + ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) ) )
196 11 32 191 subdid ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) )
197 196 oveq1d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) = ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) )
198 11 191 mulcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ )
199 33 198 182 sub32d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) = ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) − ( i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) )
200 197 199 eqtrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) = ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) − ( i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) )
201 200 oveq1d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) + ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) ) = ( ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) − ( i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) + ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) ) )
202 194 195 201 3eqtr2d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) ) = ( ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) − ( i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) + ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) ) )
203 33 182 subcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) ∈ ℂ )
204 203 198 negsubd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) + - ( i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) − ( i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) )
205 11 191 mulneg1d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) = - ( i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) )
206 205 eqcomd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → - ( i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) = ( - i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) )
207 206 oveq2d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) + - ( i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) )
208 204 207 eqtr3d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) − ( i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) )
209 208 oveq1d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) − ( i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) + ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) ) = ( ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) + ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) ) )
210 202 209 eqtrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) ) = ( ( ( ( i · ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) + ( - i · ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) + ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) ) )
211 93 174 210 3eqtr4rd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) ) = Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) ) )
212 211 oveq1d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) ( i · 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) = ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) ) / 4 ) )
213 9 212 eqtrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 , 𝐵 ) = ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 + ( ( i ↑ 𝑘 ) · 𝐵 ) ) ) ↑ 2 ) ) / 4 ) )