Metamath Proof Explorer

Theorem cphipval2

Description: Value of the inner product expressed by the norm defined by it. (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 ⊒ , = ( ·𝑖 β€˜ π‘Š )
cphipval2.m ⊒ βˆ’ = ( -g β€˜ π‘Š )
cphipval2.f ⊒ 𝐹 = ( Scalar β€˜ π‘Š )
cphipval2.k ⊒ 𝐾 = ( Base β€˜ 𝐹 )
Assertion cphipval2 ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( 𝐴 , 𝐡 ) = ( ( ( ( ( 𝑁 β€˜ ( 𝐴 + 𝐡 ) ) ↑ 2 ) βˆ’ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐡 ) ) ↑ 2 ) ) + ( i Β· ( ( ( 𝑁 β€˜ ( 𝐴 + ( i Β· 𝐡 ) ) ) ↑ 2 ) βˆ’ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( 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 cphipval2.m ⊒ βˆ’ = ( -g β€˜ π‘Š )
7 cphipval2.f ⊒ 𝐹 = ( Scalar β€˜ π‘Š )
8 cphipval2.k ⊒ 𝐾 = ( Base β€˜ 𝐹 )
9 simpl ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) β†’ π‘Š ∈ β„‚PreHil )
10 9 3ad2ant1 ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ π‘Š ∈ β„‚PreHil )
11 cphngp ⊒ ( π‘Š ∈ β„‚PreHil β†’ π‘Š ∈ NrmGrp )
12 11 adantr ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) β†’ π‘Š ∈ NrmGrp )
13 ngpgrp ⊒ ( π‘Š ∈ NrmGrp β†’ π‘Š ∈ Grp )
14 12 13 syl ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) β†’ π‘Š ∈ Grp )
15 1 2 grpcl ⊒ ( ( π‘Š ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( 𝐴 + 𝐡 ) ∈ 𝑋 )
16 14 15 syl3an1 ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( 𝐴 + 𝐡 ) ∈ 𝑋 )
17 1 5 4 nmsq ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ ( 𝐴 + 𝐡 ) ∈ 𝑋 ) β†’ ( ( 𝑁 β€˜ ( 𝐴 + 𝐡 ) ) ↑ 2 ) = ( ( 𝐴 + 𝐡 ) , ( 𝐴 + 𝐡 ) ) )
18 10 16 17 syl2anc ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝑁 β€˜ ( 𝐴 + 𝐡 ) ) ↑ 2 ) = ( ( 𝐴 + 𝐡 ) , ( 𝐴 + 𝐡 ) ) )
19 simp2 ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ 𝐴 ∈ 𝑋 )
20 simp3 ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ 𝐡 ∈ 𝑋 )
21 5 1 2 10 19 20 19 20 cph2di ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝐴 + 𝐡 ) , ( 𝐴 + 𝐡 ) ) = ( ( ( 𝐴 , 𝐴 ) + ( 𝐡 , 𝐡 ) ) + ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) ) )
22 18 21 eqtrd ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝑁 β€˜ ( 𝐴 + 𝐡 ) ) ↑ 2 ) = ( ( ( 𝐴 , 𝐴 ) + ( 𝐡 , 𝐡 ) ) + ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) ) )
23 1 6 grpsubcl ⊒ ( ( π‘Š ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( 𝐴 βˆ’ 𝐡 ) ∈ 𝑋 )
24 14 23 syl3an1 ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( 𝐴 βˆ’ 𝐡 ) ∈ 𝑋 )
25 1 5 4 nmsq ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ ( 𝐴 βˆ’ 𝐡 ) ∈ 𝑋 ) β†’ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐡 ) ) ↑ 2 ) = ( ( 𝐴 βˆ’ 𝐡 ) , ( 𝐴 βˆ’ 𝐡 ) ) )
26 10 24 25 syl2anc ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐡 ) ) ↑ 2 ) = ( ( 𝐴 βˆ’ 𝐡 ) , ( 𝐴 βˆ’ 𝐡 ) ) )
27 5 1 6 10 19 20 19 20 cph2subdi ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝐴 βˆ’ 𝐡 ) , ( 𝐴 βˆ’ 𝐡 ) ) = ( ( ( 𝐴 , 𝐴 ) + ( 𝐡 , 𝐡 ) ) βˆ’ ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) ) )
28 26 27 eqtrd ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐡 ) ) ↑ 2 ) = ( ( ( 𝐴 , 𝐴 ) + ( 𝐡 , 𝐡 ) ) βˆ’ ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) ) )
29 22 28 oveq12d ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( ( 𝑁 β€˜ ( 𝐴 + 𝐡 ) ) ↑ 2 ) βˆ’ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐡 ) ) ↑ 2 ) ) = ( ( ( ( 𝐴 , 𝐴 ) + ( 𝐡 , 𝐡 ) ) + ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) ) βˆ’ ( ( ( 𝐴 , 𝐴 ) + ( 𝐡 , 𝐡 ) ) βˆ’ ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) ) ) )
30 1 5 reipcl ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ 𝐴 ∈ 𝑋 ) β†’ ( 𝐴 , 𝐴 ) ∈ ℝ )
31 30 adantlr ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) β†’ ( 𝐴 , 𝐴 ) ∈ ℝ )
32 31 recnd ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) β†’ ( 𝐴 , 𝐴 ) ∈ β„‚ )
33 32 3adant3 ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( 𝐴 , 𝐴 ) ∈ β„‚ )
34 1 5 reipcl ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ 𝐡 ∈ 𝑋 ) β†’ ( 𝐡 , 𝐡 ) ∈ ℝ )
35 34 adantlr ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐡 ∈ 𝑋 ) β†’ ( 𝐡 , 𝐡 ) ∈ ℝ )
36 35 recnd ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐡 ∈ 𝑋 ) β†’ ( 𝐡 , 𝐡 ) ∈ β„‚ )
37 36 3adant2 ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( 𝐡 , 𝐡 ) ∈ β„‚ )
38 33 37 addcld ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝐴 , 𝐴 ) + ( 𝐡 , 𝐡 ) ) ∈ β„‚ )
39 1 5 cphipcl ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( 𝐴 , 𝐡 ) ∈ β„‚ )
40 9 39 syl3an1 ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( 𝐴 , 𝐡 ) ∈ β„‚ )
41 1 5 cphipcl ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ 𝐡 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) β†’ ( 𝐡 , 𝐴 ) ∈ β„‚ )
42 9 41 syl3an1 ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐡 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) β†’ ( 𝐡 , 𝐴 ) ∈ β„‚ )
43 42 3com23 ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( 𝐡 , 𝐴 ) ∈ β„‚ )
44 40 43 addcld ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) ∈ β„‚ )
45 38 44 44 pnncand ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( ( ( 𝐴 , 𝐴 ) + ( 𝐡 , 𝐡 ) ) + ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) ) βˆ’ ( ( ( 𝐴 , 𝐴 ) + ( 𝐡 , 𝐡 ) ) βˆ’ ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) ) ) = ( ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) + ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) ) )
46 29 45 eqtrd ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( ( 𝑁 β€˜ ( 𝐴 + 𝐡 ) ) ↑ 2 ) βˆ’ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐡 ) ) ↑ 2 ) ) = ( ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) + ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) ) )
47 14 3ad2ant1 ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ π‘Š ∈ Grp )
48 cphlmod ⊒ ( π‘Š ∈ β„‚PreHil β†’ π‘Š ∈ LMod )
49 48 adantr ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) β†’ π‘Š ∈ LMod )
50 49 adantr ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐡 ∈ 𝑋 ) β†’ π‘Š ∈ LMod )
51 simplr ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐡 ∈ 𝑋 ) β†’ i ∈ 𝐾 )
52 simpr ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐡 ∈ 𝑋 ) β†’ 𝐡 ∈ 𝑋 )
53 1 7 3 8 lmodvscl ⊒ ( ( π‘Š ∈ LMod ∧ i ∈ 𝐾 ∧ 𝐡 ∈ 𝑋 ) β†’ ( i Β· 𝐡 ) ∈ 𝑋 )
54 50 51 52 53 syl3anc ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐡 ∈ 𝑋 ) β†’ ( i Β· 𝐡 ) ∈ 𝑋 )
55 54 3adant2 ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( i Β· 𝐡 ) ∈ 𝑋 )
56 1 2 grpcl ⊒ ( ( π‘Š ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( i Β· 𝐡 ) ∈ 𝑋 ) β†’ ( 𝐴 + ( i Β· 𝐡 ) ) ∈ 𝑋 )
57 47 19 55 56 syl3anc ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( 𝐴 + ( i Β· 𝐡 ) ) ∈ 𝑋 )
58 1 5 4 nmsq ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ ( 𝐴 + ( i Β· 𝐡 ) ) ∈ 𝑋 ) β†’ ( ( 𝑁 β€˜ ( 𝐴 + ( i Β· 𝐡 ) ) ) ↑ 2 ) = ( ( 𝐴 + ( i Β· 𝐡 ) ) , ( 𝐴 + ( i Β· 𝐡 ) ) ) )
59 10 57 58 syl2anc ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝑁 β€˜ ( 𝐴 + ( i Β· 𝐡 ) ) ) ↑ 2 ) = ( ( 𝐴 + ( i Β· 𝐡 ) ) , ( 𝐴 + ( i Β· 𝐡 ) ) ) )
60 5 1 2 10 19 55 19 55 cph2di ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝐴 + ( i Β· 𝐡 ) ) , ( 𝐴 + ( i Β· 𝐡 ) ) ) = ( ( ( 𝐴 , 𝐴 ) + ( ( i Β· 𝐡 ) , ( i Β· 𝐡 ) ) ) + ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) ) )
61 59 60 eqtrd ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝑁 β€˜ ( 𝐴 + ( i Β· 𝐡 ) ) ) ↑ 2 ) = ( ( ( 𝐴 , 𝐴 ) + ( ( i Β· 𝐡 ) , ( i Β· 𝐡 ) ) ) + ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) ) )
62 1 6 grpsubcl ⊒ ( ( π‘Š ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( i Β· 𝐡 ) ∈ 𝑋 ) β†’ ( 𝐴 βˆ’ ( i Β· 𝐡 ) ) ∈ 𝑋 )
63 47 19 55 62 syl3anc ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( 𝐴 βˆ’ ( i Β· 𝐡 ) ) ∈ 𝑋 )
64 1 5 4 nmsq ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ ( 𝐴 βˆ’ ( i Β· 𝐡 ) ) ∈ 𝑋 ) β†’ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( i Β· 𝐡 ) ) ) ↑ 2 ) = ( ( 𝐴 βˆ’ ( i Β· 𝐡 ) ) , ( 𝐴 βˆ’ ( i Β· 𝐡 ) ) ) )
65 10 63 64 syl2anc ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( i Β· 𝐡 ) ) ) ↑ 2 ) = ( ( 𝐴 βˆ’ ( i Β· 𝐡 ) ) , ( 𝐴 βˆ’ ( i Β· 𝐡 ) ) ) )
66 5 1 6 10 19 55 19 55 cph2subdi ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝐴 βˆ’ ( i Β· 𝐡 ) ) , ( 𝐴 βˆ’ ( i Β· 𝐡 ) ) ) = ( ( ( 𝐴 , 𝐴 ) + ( ( i Β· 𝐡 ) , ( i Β· 𝐡 ) ) ) βˆ’ ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) ) )
67 65 66 eqtrd ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( i Β· 𝐡 ) ) ) ↑ 2 ) = ( ( ( 𝐴 , 𝐴 ) + ( ( i Β· 𝐡 ) , ( i Β· 𝐡 ) ) ) βˆ’ ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) ) )
68 61 67 oveq12d ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( ( 𝑁 β€˜ ( 𝐴 + ( i Β· 𝐡 ) ) ) ↑ 2 ) βˆ’ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( i Β· 𝐡 ) ) ) ↑ 2 ) ) = ( ( ( ( 𝐴 , 𝐴 ) + ( ( i Β· 𝐡 ) , ( i Β· 𝐡 ) ) ) + ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) ) βˆ’ ( ( ( 𝐴 , 𝐴 ) + ( ( i Β· 𝐡 ) , ( i Β· 𝐡 ) ) ) βˆ’ ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) ) ) )
69 68 oveq2d ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( i Β· ( ( ( 𝑁 β€˜ ( 𝐴 + ( i Β· 𝐡 ) ) ) ↑ 2 ) βˆ’ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( i Β· 𝐡 ) ) ) ↑ 2 ) ) ) = ( i Β· ( ( ( ( 𝐴 , 𝐴 ) + ( ( i Β· 𝐡 ) , ( i Β· 𝐡 ) ) ) + ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) ) βˆ’ ( ( ( 𝐴 , 𝐴 ) + ( ( i Β· 𝐡 ) , ( i Β· 𝐡 ) ) ) βˆ’ ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) ) ) ) )
70 1 5 cphipcl ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ ( i Β· 𝐡 ) ∈ 𝑋 ∧ ( i Β· 𝐡 ) ∈ 𝑋 ) β†’ ( ( i Β· 𝐡 ) , ( i Β· 𝐡 ) ) ∈ β„‚ )
71 10 55 55 70 syl3anc ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( i Β· 𝐡 ) , ( i Β· 𝐡 ) ) ∈ β„‚ )
72 33 71 addcld ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝐴 , 𝐴 ) + ( ( i Β· 𝐡 ) , ( i Β· 𝐡 ) ) ) ∈ β„‚ )
73 1 5 cphipcl ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ 𝐴 ∈ 𝑋 ∧ ( i Β· 𝐡 ) ∈ 𝑋 ) β†’ ( 𝐴 , ( i Β· 𝐡 ) ) ∈ β„‚ )
74 10 19 55 73 syl3anc ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( 𝐴 , ( i Β· 𝐡 ) ) ∈ β„‚ )
75 1 5 cphipcl ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ ( i Β· 𝐡 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) β†’ ( ( i Β· 𝐡 ) , 𝐴 ) ∈ β„‚ )
76 10 55 19 75 syl3anc ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( i Β· 𝐡 ) , 𝐴 ) ∈ β„‚ )
77 74 76 addcld ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) ∈ β„‚ )
78 72 77 77 pnncand ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( ( ( 𝐴 , 𝐴 ) + ( ( i Β· 𝐡 ) , ( i Β· 𝐡 ) ) ) + ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) ) βˆ’ ( ( ( 𝐴 , 𝐴 ) + ( ( i Β· 𝐡 ) , ( i Β· 𝐡 ) ) ) βˆ’ ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) ) ) = ( ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) + ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) ) )
79 78 oveq2d ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( i Β· ( ( ( ( 𝐴 , 𝐴 ) + ( ( i Β· 𝐡 ) , ( i Β· 𝐡 ) ) ) + ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) ) βˆ’ ( ( ( 𝐴 , 𝐴 ) + ( ( i Β· 𝐡 ) , ( i Β· 𝐡 ) ) ) βˆ’ ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) ) ) ) = ( i Β· ( ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) + ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) ) ) )
80 1 3 5 7 8 cphassir ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( 𝐴 , ( i Β· 𝐡 ) ) = ( - i Β· ( 𝐴 , 𝐡 ) ) )
81 1 3 5 7 8 cphassi ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( i Β· 𝐡 ) , 𝐴 ) = ( i Β· ( 𝐡 , 𝐴 ) ) )
82 80 81 oveq12d ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) = ( ( - i Β· ( 𝐴 , 𝐡 ) ) + ( i Β· ( 𝐡 , 𝐴 ) ) ) )
83 82 82 oveq12d ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) + ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) ) = ( ( ( - i Β· ( 𝐴 , 𝐡 ) ) + ( i Β· ( 𝐡 , 𝐴 ) ) ) + ( ( - i Β· ( 𝐴 , 𝐡 ) ) + ( i Β· ( 𝐡 , 𝐴 ) ) ) ) )
84 83 oveq2d ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( i Β· ( ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) + ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) ) ) = ( i Β· ( ( ( - i Β· ( 𝐴 , 𝐡 ) ) + ( i Β· ( 𝐡 , 𝐴 ) ) ) + ( ( - i Β· ( 𝐴 , 𝐡 ) ) + ( i Β· ( 𝐡 , 𝐴 ) ) ) ) ) )
85 ax-icn ⊒ i ∈ β„‚
86 85 a1i ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ i ∈ β„‚ )
87 negicn ⊒ - i ∈ β„‚
88 87 a1i ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ - i ∈ β„‚ )
89 88 40 mulcld ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( - i Β· ( 𝐴 , 𝐡 ) ) ∈ β„‚ )
90 86 43 mulcld ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( i Β· ( 𝐡 , 𝐴 ) ) ∈ β„‚ )
91 89 90 addcld ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( - i Β· ( 𝐴 , 𝐡 ) ) + ( i Β· ( 𝐡 , 𝐴 ) ) ) ∈ β„‚ )
92 86 91 91 adddid ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( i Β· ( ( ( - i Β· ( 𝐴 , 𝐡 ) ) + ( i Β· ( 𝐡 , 𝐴 ) ) ) + ( ( - i Β· ( 𝐴 , 𝐡 ) ) + ( i Β· ( 𝐡 , 𝐴 ) ) ) ) ) = ( ( i Β· ( ( - i Β· ( 𝐴 , 𝐡 ) ) + ( i Β· ( 𝐡 , 𝐴 ) ) ) ) + ( i Β· ( ( - i Β· ( 𝐴 , 𝐡 ) ) + ( i Β· ( 𝐡 , 𝐴 ) ) ) ) ) )
93 86 89 90 adddid ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( i Β· ( ( - i Β· ( 𝐴 , 𝐡 ) ) + ( i Β· ( 𝐡 , 𝐴 ) ) ) ) = ( ( i Β· ( - i Β· ( 𝐴 , 𝐡 ) ) ) + ( i Β· ( i Β· ( 𝐡 , 𝐴 ) ) ) ) )
94 86 88 40 mulassd ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( i Β· - i ) Β· ( 𝐴 , 𝐡 ) ) = ( i Β· ( - i Β· ( 𝐴 , 𝐡 ) ) ) )
95 85 85 mulneg2i ⊒ ( i · - i ) = - ( i · i )
96 ixi ⊒ ( i · i ) = - 1
97 96 negeqi ⊒ - ( i · i ) = - - 1
98 negneg1e1 ⊒ - - 1 = 1
99 95 97 98 3eqtri ⊒ ( i · - i ) = 1
100 99 oveq1i ⊒ ( ( i · - i ) · ( 𝐴 , 𝐡 ) ) = ( 1 · ( 𝐴 , 𝐡 ) )
101 94 100 eqtr3di ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( i Β· ( - i Β· ( 𝐴 , 𝐡 ) ) ) = ( 1 Β· ( 𝐴 , 𝐡 ) ) )
102 86 86 43 mulassd ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( i Β· i ) Β· ( 𝐡 , 𝐴 ) ) = ( i Β· ( i Β· ( 𝐡 , 𝐴 ) ) ) )
103 96 oveq1i ⊒ ( ( i · i ) · ( 𝐡 , 𝐴 ) ) = ( - 1 · ( 𝐡 , 𝐴 ) )
104 102 103 eqtr3di ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( i Β· ( i Β· ( 𝐡 , 𝐴 ) ) ) = ( - 1 Β· ( 𝐡 , 𝐴 ) ) )
105 101 104 oveq12d ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( i Β· ( - i Β· ( 𝐴 , 𝐡 ) ) ) + ( i Β· ( i Β· ( 𝐡 , 𝐴 ) ) ) ) = ( ( 1 Β· ( 𝐴 , 𝐡 ) ) + ( - 1 Β· ( 𝐡 , 𝐴 ) ) ) )
106 93 105 eqtrd ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( i Β· ( ( - i Β· ( 𝐴 , 𝐡 ) ) + ( i Β· ( 𝐡 , 𝐴 ) ) ) ) = ( ( 1 Β· ( 𝐴 , 𝐡 ) ) + ( - 1 Β· ( 𝐡 , 𝐴 ) ) ) )
107 106 106 oveq12d ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( i Β· ( ( - i Β· ( 𝐴 , 𝐡 ) ) + ( i Β· ( 𝐡 , 𝐴 ) ) ) ) + ( i Β· ( ( - i Β· ( 𝐴 , 𝐡 ) ) + ( i Β· ( 𝐡 , 𝐴 ) ) ) ) ) = ( ( ( 1 Β· ( 𝐴 , 𝐡 ) ) + ( - 1 Β· ( 𝐡 , 𝐴 ) ) ) + ( ( 1 Β· ( 𝐴 , 𝐡 ) ) + ( - 1 Β· ( 𝐡 , 𝐴 ) ) ) ) )
108 40 mullidd ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( 1 Β· ( 𝐴 , 𝐡 ) ) = ( 𝐴 , 𝐡 ) )
109 108 oveq1d ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 1 Β· ( 𝐴 , 𝐡 ) ) + ( - 1 Β· ( 𝐡 , 𝐴 ) ) ) = ( ( 𝐴 , 𝐡 ) + ( - 1 Β· ( 𝐡 , 𝐴 ) ) ) )
110 addneg1mul ⊒ ( ( ( 𝐴 , 𝐡 ) ∈ β„‚ ∧ ( 𝐡 , 𝐴 ) ∈ β„‚ ) β†’ ( ( 𝐴 , 𝐡 ) + ( - 1 Β· ( 𝐡 , 𝐴 ) ) ) = ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) )
111 40 43 110 syl2anc ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝐴 , 𝐡 ) + ( - 1 Β· ( 𝐡 , 𝐴 ) ) ) = ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) )
112 109 111 eqtrd ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 1 Β· ( 𝐴 , 𝐡 ) ) + ( - 1 Β· ( 𝐡 , 𝐴 ) ) ) = ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) )
113 112 112 oveq12d ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( ( 1 Β· ( 𝐴 , 𝐡 ) ) + ( - 1 Β· ( 𝐡 , 𝐴 ) ) ) + ( ( 1 Β· ( 𝐴 , 𝐡 ) ) + ( - 1 Β· ( 𝐡 , 𝐴 ) ) ) ) = ( ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) + ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) ) )
114 107 113 eqtrd ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( i Β· ( ( - i Β· ( 𝐴 , 𝐡 ) ) + ( i Β· ( 𝐡 , 𝐴 ) ) ) ) + ( i Β· ( ( - i Β· ( 𝐴 , 𝐡 ) ) + ( i Β· ( 𝐡 , 𝐴 ) ) ) ) ) = ( ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) + ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) ) )
115 84 92 114 3eqtrd ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( i Β· ( ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) + ( ( 𝐴 , ( i Β· 𝐡 ) ) + ( ( i Β· 𝐡 ) , 𝐴 ) ) ) ) = ( ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) + ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) ) )
116 69 79 115 3eqtrd ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( i Β· ( ( ( 𝑁 β€˜ ( 𝐴 + ( i Β· 𝐡 ) ) ) ↑ 2 ) βˆ’ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( i Β· 𝐡 ) ) ) ↑ 2 ) ) ) = ( ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) + ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) ) )
117 46 116 oveq12d ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( ( ( 𝑁 β€˜ ( 𝐴 + 𝐡 ) ) ↑ 2 ) βˆ’ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐡 ) ) ↑ 2 ) ) + ( i Β· ( ( ( 𝑁 β€˜ ( 𝐴 + ( i Β· 𝐡 ) ) ) ↑ 2 ) βˆ’ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( i Β· 𝐡 ) ) ) ↑ 2 ) ) ) ) = ( ( ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) + ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) ) + ( ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) + ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) ) ) )
118 117 oveq1d ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( ( ( ( 𝑁 β€˜ ( 𝐴 + 𝐡 ) ) ↑ 2 ) βˆ’ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐡 ) ) ↑ 2 ) ) + ( i Β· ( ( ( 𝑁 β€˜ ( 𝐴 + ( i Β· 𝐡 ) ) ) ↑ 2 ) βˆ’ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( i Β· 𝐡 ) ) ) ↑ 2 ) ) ) ) / 4 ) = ( ( ( ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) + ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) ) + ( ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) + ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) ) ) / 4 ) )
119 40 43 subcld ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) ∈ β„‚ )
120 44 44 119 119 add4d ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) + ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) ) + ( ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) + ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) ) ) = ( ( ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) + ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) ) + ( ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) + ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) ) ) )
121 40 43 40 ppncand ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) + ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) ) = ( ( 𝐴 , 𝐡 ) + ( 𝐴 , 𝐡 ) ) )
122 121 121 oveq12d ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) + ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) ) + ( ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) + ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) ) ) = ( ( ( 𝐴 , 𝐡 ) + ( 𝐴 , 𝐡 ) ) + ( ( 𝐴 , 𝐡 ) + ( 𝐴 , 𝐡 ) ) ) )
123 120 122 eqtrd ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) + ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) ) + ( ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) + ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) ) ) = ( ( ( 𝐴 , 𝐡 ) + ( 𝐴 , 𝐡 ) ) + ( ( 𝐴 , 𝐡 ) + ( 𝐴 , 𝐡 ) ) ) )
124 123 oveq1d ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( ( ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) + ( ( 𝐴 , 𝐡 ) + ( 𝐡 , 𝐴 ) ) ) + ( ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) + ( ( 𝐴 , 𝐡 ) βˆ’ ( 𝐡 , 𝐴 ) ) ) ) / 4 ) = ( ( ( ( 𝐴 , 𝐡 ) + ( 𝐴 , 𝐡 ) ) + ( ( 𝐴 , 𝐡 ) + ( 𝐴 , 𝐡 ) ) ) / 4 ) )
125 40 2timesd ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( 2 Β· ( 𝐴 , 𝐡 ) ) = ( ( 𝐴 , 𝐡 ) + ( 𝐴 , 𝐡 ) ) )
126 125 eqcomd ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝐴 , 𝐡 ) + ( 𝐴 , 𝐡 ) ) = ( 2 Β· ( 𝐴 , 𝐡 ) ) )
127 126 126 oveq12d ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( ( 𝐴 , 𝐡 ) + ( 𝐴 , 𝐡 ) ) + ( ( 𝐴 , 𝐡 ) + ( 𝐴 , 𝐡 ) ) ) = ( ( 2 Β· ( 𝐴 , 𝐡 ) ) + ( 2 Β· ( 𝐴 , 𝐡 ) ) ) )
128 2cnd ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ 2 ∈ β„‚ )
129 128 128 40 adddird ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 2 + 2 ) Β· ( 𝐴 , 𝐡 ) ) = ( ( 2 Β· ( 𝐴 , 𝐡 ) ) + ( 2 Β· ( 𝐴 , 𝐡 ) ) ) )
130 2p2e4 ⊒ ( 2 + 2 ) = 4
131 130 a1i ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( 2 + 2 ) = 4 )
132 131 oveq1d ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 2 + 2 ) Β· ( 𝐴 , 𝐡 ) ) = ( 4 Β· ( 𝐴 , 𝐡 ) ) )
133 127 129 132 3eqtr2d ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( ( 𝐴 , 𝐡 ) + ( 𝐴 , 𝐡 ) ) + ( ( 𝐴 , 𝐡 ) + ( 𝐴 , 𝐡 ) ) ) = ( 4 Β· ( 𝐴 , 𝐡 ) ) )
134 133 oveq1d ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( ( ( 𝐴 , 𝐡 ) + ( 𝐴 , 𝐡 ) ) + ( ( 𝐴 , 𝐡 ) + ( 𝐴 , 𝐡 ) ) ) / 4 ) = ( ( 4 Β· ( 𝐴 , 𝐡 ) ) / 4 ) )
135 4cn ⊒ 4 ∈ β„‚
136 135 a1i ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ 4 ∈ β„‚ )
137 4ne0 ⊒ 4 β‰  0
138 137 a1i ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ 4 β‰  0 )
139 40 136 138 divcan3d ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 4 Β· ( 𝐴 , 𝐡 ) ) / 4 ) = ( 𝐴 , 𝐡 ) )
140 134 139 eqtrd ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( ( ( 𝐴 , 𝐡 ) + ( 𝐴 , 𝐡 ) ) + ( ( 𝐴 , 𝐡 ) + ( 𝐴 , 𝐡 ) ) ) / 4 ) = ( 𝐴 , 𝐡 ) )
141 118 124 140 3eqtrrd ⊒ ( ( ( π‘Š ∈ β„‚PreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( 𝐴 , 𝐡 ) = ( ( ( ( ( 𝑁 β€˜ ( 𝐴 + 𝐡 ) ) ↑ 2 ) βˆ’ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐡 ) ) ↑ 2 ) ) + ( i Β· ( ( ( 𝑁 β€˜ ( 𝐴 + ( i Β· 𝐡 ) ) ) ↑ 2 ) βˆ’ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( i Β· 𝐡 ) ) ) ↑ 2 ) ) ) ) / 4 ) )