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 
|- X = ( Base ` W )
cphipfval.p 
|- .+ = ( +g ` W )
cphipfval.s 
|- .x. = ( .s ` W )
cphipfval.n 
|- N = ( norm ` W )
cphipfval.i 
|- ., = ( .i ` W )
cphipval2.m 
|- .- = ( -g ` W )
cphipval2.f 
|- F = ( Scalar ` W )
cphipval2.k 
|- K = ( Base ` F )
Assertion cphipval2 
|- ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( A ., B ) = ( ( ( ( ( N ` ( A .+ B ) ) ^ 2 ) - ( ( N ` ( A .- B ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A .+ ( _i .x. B ) ) ) ^ 2 ) - ( ( N ` ( A .- ( _i .x. B ) ) ) ^ 2 ) ) ) ) / 4 ) )

Proof

Step Hyp Ref Expression
1 cphipfval.x 
 |-  X = ( Base ` W )
2 cphipfval.p 
 |-  .+ = ( +g ` W )
3 cphipfval.s 
 |-  .x. = ( .s ` W )
4 cphipfval.n 
 |-  N = ( norm ` W )
5 cphipfval.i 
 |-  ., = ( .i ` W )
6 cphipval2.m 
 |-  .- = ( -g ` W )
7 cphipval2.f 
 |-  F = ( Scalar ` W )
8 cphipval2.k 
 |-  K = ( Base ` F )
9 simpl 
 |-  ( ( W e. CPreHil /\ _i e. K ) -> W e. CPreHil )
10 9 3ad2ant1 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> W e. CPreHil )
11 cphngp 
 |-  ( W e. CPreHil -> W e. NrmGrp )
12 11 adantr 
 |-  ( ( W e. CPreHil /\ _i e. K ) -> W e. NrmGrp )
13 ngpgrp 
 |-  ( W e. NrmGrp -> W e. Grp )
14 12 13 syl 
 |-  ( ( W e. CPreHil /\ _i e. K ) -> W e. Grp )
15 1 2 grpcl 
 |-  ( ( W e. Grp /\ A e. X /\ B e. X ) -> ( A .+ B ) e. X )
16 14 15 syl3an1 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( A .+ B ) e. X )
17 1 5 4 nmsq 
 |-  ( ( W e. CPreHil /\ ( A .+ B ) e. X ) -> ( ( N ` ( A .+ B ) ) ^ 2 ) = ( ( A .+ B ) ., ( A .+ B ) ) )
18 10 16 17 syl2anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( N ` ( A .+ B ) ) ^ 2 ) = ( ( A .+ B ) ., ( A .+ B ) ) )
19 simp2 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> A e. X )
20 simp3 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> B e. X )
21 5 1 2 10 19 20 19 20 cph2di 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( A .+ B ) ., ( A .+ B ) ) = ( ( ( A ., A ) + ( B ., B ) ) + ( ( A ., B ) + ( B ., A ) ) ) )
22 18 21 eqtrd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( N ` ( A .+ B ) ) ^ 2 ) = ( ( ( A ., A ) + ( B ., B ) ) + ( ( A ., B ) + ( B ., A ) ) ) )
23 1 6 grpsubcl 
 |-  ( ( W e. Grp /\ A e. X /\ B e. X ) -> ( A .- B ) e. X )
24 14 23 syl3an1 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( A .- B ) e. X )
25 1 5 4 nmsq 
 |-  ( ( W e. CPreHil /\ ( A .- B ) e. X ) -> ( ( N ` ( A .- B ) ) ^ 2 ) = ( ( A .- B ) ., ( A .- B ) ) )
26 10 24 25 syl2anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( N ` ( A .- B ) ) ^ 2 ) = ( ( A .- B ) ., ( A .- B ) ) )
27 5 1 6 10 19 20 19 20 cph2subdi 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( A .- B ) ., ( A .- B ) ) = ( ( ( A ., A ) + ( B ., B ) ) - ( ( A ., B ) + ( B ., A ) ) ) )
28 26 27 eqtrd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( N ` ( A .- B ) ) ^ 2 ) = ( ( ( A ., A ) + ( B ., B ) ) - ( ( A ., B ) + ( B ., A ) ) ) )
29 22 28 oveq12d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( ( N ` ( A .+ B ) ) ^ 2 ) - ( ( N ` ( A .- B ) ) ^ 2 ) ) = ( ( ( ( A ., A ) + ( B ., B ) ) + ( ( A ., B ) + ( B ., A ) ) ) - ( ( ( A ., A ) + ( B ., B ) ) - ( ( A ., B ) + ( B ., A ) ) ) ) )
30 1 5 reipcl 
 |-  ( ( W e. CPreHil /\ A e. X ) -> ( A ., A ) e. RR )
31 30 adantlr 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X ) -> ( A ., A ) e. RR )
32 31 recnd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X ) -> ( A ., A ) e. CC )
33 32 3adant3 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( A ., A ) e. CC )
34 1 5 reipcl 
 |-  ( ( W e. CPreHil /\ B e. X ) -> ( B ., B ) e. RR )
35 34 adantlr 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ B e. X ) -> ( B ., B ) e. RR )
36 35 recnd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ B e. X ) -> ( B ., B ) e. CC )
37 36 3adant2 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( B ., B ) e. CC )
38 33 37 addcld 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( A ., A ) + ( B ., B ) ) e. CC )
39 1 5 cphipcl 
 |-  ( ( W e. CPreHil /\ A e. X /\ B e. X ) -> ( A ., B ) e. CC )
40 9 39 syl3an1 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( A ., B ) e. CC )
41 1 5 cphipcl 
 |-  ( ( W e. CPreHil /\ B e. X /\ A e. X ) -> ( B ., A ) e. CC )
42 9 41 syl3an1 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ B e. X /\ A e. X ) -> ( B ., A ) e. CC )
43 42 3com23 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( B ., A ) e. CC )
44 40 43 addcld 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( A ., B ) + ( B ., A ) ) e. CC )
45 38 44 44 pnncand 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( ( ( A ., A ) + ( B ., B ) ) + ( ( A ., B ) + ( B ., A ) ) ) - ( ( ( A ., A ) + ( B ., B ) ) - ( ( A ., B ) + ( B ., A ) ) ) ) = ( ( ( A ., B ) + ( B ., A ) ) + ( ( A ., B ) + ( B ., A ) ) ) )
46 29 45 eqtrd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( ( N ` ( A .+ B ) ) ^ 2 ) - ( ( N ` ( A .- B ) ) ^ 2 ) ) = ( ( ( A ., B ) + ( B ., A ) ) + ( ( A ., B ) + ( B ., A ) ) ) )
47 14 3ad2ant1 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> W e. Grp )
48 cphlmod 
 |-  ( W e. CPreHil -> W e. LMod )
49 48 adantr 
 |-  ( ( W e. CPreHil /\ _i e. K ) -> W e. LMod )
50 49 adantr 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ B e. X ) -> W e. LMod )
51 simplr 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ B e. X ) -> _i e. K )
52 simpr 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ B e. X ) -> B e. X )
53 1 7 3 8 lmodvscl 
 |-  ( ( W e. LMod /\ _i e. K /\ B e. X ) -> ( _i .x. B ) e. X )
54 50 51 52 53 syl3anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ B e. X ) -> ( _i .x. B ) e. X )
55 54 3adant2 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( _i .x. B ) e. X )
56 1 2 grpcl 
 |-  ( ( W e. Grp /\ A e. X /\ ( _i .x. B ) e. X ) -> ( A .+ ( _i .x. B ) ) e. X )
57 47 19 55 56 syl3anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( A .+ ( _i .x. B ) ) e. X )
58 1 5 4 nmsq 
 |-  ( ( W e. CPreHil /\ ( A .+ ( _i .x. B ) ) e. X ) -> ( ( N ` ( A .+ ( _i .x. B ) ) ) ^ 2 ) = ( ( A .+ ( _i .x. B ) ) ., ( A .+ ( _i .x. B ) ) ) )
59 10 57 58 syl2anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( N ` ( A .+ ( _i .x. B ) ) ) ^ 2 ) = ( ( A .+ ( _i .x. B ) ) ., ( A .+ ( _i .x. B ) ) ) )
60 5 1 2 10 19 55 19 55 cph2di 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( A .+ ( _i .x. B ) ) ., ( A .+ ( _i .x. B ) ) ) = ( ( ( A ., A ) + ( ( _i .x. B ) ., ( _i .x. B ) ) ) + ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) ) )
61 59 60 eqtrd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( N ` ( A .+ ( _i .x. B ) ) ) ^ 2 ) = ( ( ( A ., A ) + ( ( _i .x. B ) ., ( _i .x. B ) ) ) + ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) ) )
62 1 6 grpsubcl 
 |-  ( ( W e. Grp /\ A e. X /\ ( _i .x. B ) e. X ) -> ( A .- ( _i .x. B ) ) e. X )
63 47 19 55 62 syl3anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( A .- ( _i .x. B ) ) e. X )
64 1 5 4 nmsq 
 |-  ( ( W e. CPreHil /\ ( A .- ( _i .x. B ) ) e. X ) -> ( ( N ` ( A .- ( _i .x. B ) ) ) ^ 2 ) = ( ( A .- ( _i .x. B ) ) ., ( A .- ( _i .x. B ) ) ) )
65 10 63 64 syl2anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( N ` ( A .- ( _i .x. B ) ) ) ^ 2 ) = ( ( A .- ( _i .x. B ) ) ., ( A .- ( _i .x. B ) ) ) )
66 5 1 6 10 19 55 19 55 cph2subdi 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( A .- ( _i .x. B ) ) ., ( A .- ( _i .x. B ) ) ) = ( ( ( A ., A ) + ( ( _i .x. B ) ., ( _i .x. B ) ) ) - ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) ) )
67 65 66 eqtrd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( N ` ( A .- ( _i .x. B ) ) ) ^ 2 ) = ( ( ( A ., A ) + ( ( _i .x. B ) ., ( _i .x. B ) ) ) - ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) ) )
68 61 67 oveq12d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( ( N ` ( A .+ ( _i .x. B ) ) ) ^ 2 ) - ( ( N ` ( A .- ( _i .x. B ) ) ) ^ 2 ) ) = ( ( ( ( A ., A ) + ( ( _i .x. B ) ., ( _i .x. B ) ) ) + ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) ) - ( ( ( A ., A ) + ( ( _i .x. B ) ., ( _i .x. B ) ) ) - ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) ) ) )
69 68 oveq2d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( _i x. ( ( ( N ` ( A .+ ( _i .x. B ) ) ) ^ 2 ) - ( ( N ` ( A .- ( _i .x. B ) ) ) ^ 2 ) ) ) = ( _i x. ( ( ( ( A ., A ) + ( ( _i .x. B ) ., ( _i .x. B ) ) ) + ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) ) - ( ( ( A ., A ) + ( ( _i .x. B ) ., ( _i .x. B ) ) ) - ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) ) ) ) )
70 1 5 cphipcl 
 |-  ( ( W e. CPreHil /\ ( _i .x. B ) e. X /\ ( _i .x. B ) e. X ) -> ( ( _i .x. B ) ., ( _i .x. B ) ) e. CC )
71 10 55 55 70 syl3anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( _i .x. B ) ., ( _i .x. B ) ) e. CC )
72 33 71 addcld 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( A ., A ) + ( ( _i .x. B ) ., ( _i .x. B ) ) ) e. CC )
73 1 5 cphipcl 
 |-  ( ( W e. CPreHil /\ A e. X /\ ( _i .x. B ) e. X ) -> ( A ., ( _i .x. B ) ) e. CC )
74 10 19 55 73 syl3anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( A ., ( _i .x. B ) ) e. CC )
75 1 5 cphipcl 
 |-  ( ( W e. CPreHil /\ ( _i .x. B ) e. X /\ A e. X ) -> ( ( _i .x. B ) ., A ) e. CC )
76 10 55 19 75 syl3anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( _i .x. B ) ., A ) e. CC )
77 74 76 addcld 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) e. CC )
78 72 77 77 pnncand 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( ( ( A ., A ) + ( ( _i .x. B ) ., ( _i .x. B ) ) ) + ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) ) - ( ( ( A ., A ) + ( ( _i .x. B ) ., ( _i .x. B ) ) ) - ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) ) ) = ( ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) + ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) ) )
79 78 oveq2d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( _i x. ( ( ( ( A ., A ) + ( ( _i .x. B ) ., ( _i .x. B ) ) ) + ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) ) - ( ( ( A ., A ) + ( ( _i .x. B ) ., ( _i .x. B ) ) ) - ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) ) ) ) = ( _i x. ( ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) + ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) ) ) )
80 1 3 5 7 8 cphassir 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( A ., ( _i .x. B ) ) = ( -u _i x. ( A ., B ) ) )
81 1 3 5 7 8 cphassi 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( _i .x. B ) ., A ) = ( _i x. ( B ., A ) ) )
82 80 81 oveq12d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) = ( ( -u _i x. ( A ., B ) ) + ( _i x. ( B ., A ) ) ) )
83 82 82 oveq12d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) + ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) ) = ( ( ( -u _i x. ( A ., B ) ) + ( _i x. ( B ., A ) ) ) + ( ( -u _i x. ( A ., B ) ) + ( _i x. ( B ., A ) ) ) ) )
84 83 oveq2d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( _i x. ( ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) + ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) ) ) = ( _i x. ( ( ( -u _i x. ( A ., B ) ) + ( _i x. ( B ., A ) ) ) + ( ( -u _i x. ( A ., B ) ) + ( _i x. ( B ., A ) ) ) ) ) )
85 ax-icn 
 |-  _i e. CC
86 85 a1i 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> _i e. CC )
87 negicn 
 |-  -u _i e. CC
88 87 a1i 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> -u _i e. CC )
89 88 40 mulcld 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( -u _i x. ( A ., B ) ) e. CC )
90 86 43 mulcld 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( _i x. ( B ., A ) ) e. CC )
91 89 90 addcld 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( -u _i x. ( A ., B ) ) + ( _i x. ( B ., A ) ) ) e. CC )
92 86 91 91 adddid 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( _i x. ( ( ( -u _i x. ( A ., B ) ) + ( _i x. ( B ., A ) ) ) + ( ( -u _i x. ( A ., B ) ) + ( _i x. ( B ., A ) ) ) ) ) = ( ( _i x. ( ( -u _i x. ( A ., B ) ) + ( _i x. ( B ., A ) ) ) ) + ( _i x. ( ( -u _i x. ( A ., B ) ) + ( _i x. ( B ., A ) ) ) ) ) )
93 86 89 90 adddid 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( _i x. ( ( -u _i x. ( A ., B ) ) + ( _i x. ( B ., A ) ) ) ) = ( ( _i x. ( -u _i x. ( A ., B ) ) ) + ( _i x. ( _i x. ( B ., A ) ) ) ) )
94 86 88 40 mulassd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( _i x. -u _i ) x. ( A ., B ) ) = ( _i x. ( -u _i x. ( A ., B ) ) ) )
95 85 85 mulneg2i 
 |-  ( _i x. -u _i ) = -u ( _i x. _i )
96 ixi 
 |-  ( _i x. _i ) = -u 1
97 96 negeqi 
 |-  -u ( _i x. _i ) = -u -u 1
98 negneg1e1 
 |-  -u -u 1 = 1
99 95 97 98 3eqtri 
 |-  ( _i x. -u _i ) = 1
100 99 oveq1i 
 |-  ( ( _i x. -u _i ) x. ( A ., B ) ) = ( 1 x. ( A ., B ) )
101 94 100 eqtr3di 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( _i x. ( -u _i x. ( A ., B ) ) ) = ( 1 x. ( A ., B ) ) )
102 86 86 43 mulassd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( _i x. _i ) x. ( B ., A ) ) = ( _i x. ( _i x. ( B ., A ) ) ) )
103 96 oveq1i 
 |-  ( ( _i x. _i ) x. ( B ., A ) ) = ( -u 1 x. ( B ., A ) )
104 102 103 eqtr3di 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( _i x. ( _i x. ( B ., A ) ) ) = ( -u 1 x. ( B ., A ) ) )
105 101 104 oveq12d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( _i x. ( -u _i x. ( A ., B ) ) ) + ( _i x. ( _i x. ( B ., A ) ) ) ) = ( ( 1 x. ( A ., B ) ) + ( -u 1 x. ( B ., A ) ) ) )
106 93 105 eqtrd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( _i x. ( ( -u _i x. ( A ., B ) ) + ( _i x. ( B ., A ) ) ) ) = ( ( 1 x. ( A ., B ) ) + ( -u 1 x. ( B ., A ) ) ) )
107 106 106 oveq12d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( _i x. ( ( -u _i x. ( A ., B ) ) + ( _i x. ( B ., A ) ) ) ) + ( _i x. ( ( -u _i x. ( A ., B ) ) + ( _i x. ( B ., A ) ) ) ) ) = ( ( ( 1 x. ( A ., B ) ) + ( -u 1 x. ( B ., A ) ) ) + ( ( 1 x. ( A ., B ) ) + ( -u 1 x. ( B ., A ) ) ) ) )
108 40 mulid2d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( 1 x. ( A ., B ) ) = ( A ., B ) )
109 108 oveq1d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( 1 x. ( A ., B ) ) + ( -u 1 x. ( B ., A ) ) ) = ( ( A ., B ) + ( -u 1 x. ( B ., A ) ) ) )
110 addneg1mul 
 |-  ( ( ( A ., B ) e. CC /\ ( B ., A ) e. CC ) -> ( ( A ., B ) + ( -u 1 x. ( B ., A ) ) ) = ( ( A ., B ) - ( B ., A ) ) )
111 40 43 110 syl2anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( A ., B ) + ( -u 1 x. ( B ., A ) ) ) = ( ( A ., B ) - ( B ., A ) ) )
112 109 111 eqtrd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( 1 x. ( A ., B ) ) + ( -u 1 x. ( B ., A ) ) ) = ( ( A ., B ) - ( B ., A ) ) )
113 112 112 oveq12d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( ( 1 x. ( A ., B ) ) + ( -u 1 x. ( B ., A ) ) ) + ( ( 1 x. ( A ., B ) ) + ( -u 1 x. ( B ., A ) ) ) ) = ( ( ( A ., B ) - ( B ., A ) ) + ( ( A ., B ) - ( B ., A ) ) ) )
114 107 113 eqtrd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( _i x. ( ( -u _i x. ( A ., B ) ) + ( _i x. ( B ., A ) ) ) ) + ( _i x. ( ( -u _i x. ( A ., B ) ) + ( _i x. ( B ., A ) ) ) ) ) = ( ( ( A ., B ) - ( B ., A ) ) + ( ( A ., B ) - ( B ., A ) ) ) )
115 84 92 114 3eqtrd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( _i x. ( ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) + ( ( A ., ( _i .x. B ) ) + ( ( _i .x. B ) ., A ) ) ) ) = ( ( ( A ., B ) - ( B ., A ) ) + ( ( A ., B ) - ( B ., A ) ) ) )
116 69 79 115 3eqtrd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( _i x. ( ( ( N ` ( A .+ ( _i .x. B ) ) ) ^ 2 ) - ( ( N ` ( A .- ( _i .x. B ) ) ) ^ 2 ) ) ) = ( ( ( A ., B ) - ( B ., A ) ) + ( ( A ., B ) - ( B ., A ) ) ) )
117 46 116 oveq12d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( ( ( N ` ( A .+ B ) ) ^ 2 ) - ( ( N ` ( A .- B ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A .+ ( _i .x. B ) ) ) ^ 2 ) - ( ( N ` ( A .- ( _i .x. B ) ) ) ^ 2 ) ) ) ) = ( ( ( ( A ., B ) + ( B ., A ) ) + ( ( A ., B ) + ( B ., A ) ) ) + ( ( ( A ., B ) - ( B ., A ) ) + ( ( A ., B ) - ( B ., A ) ) ) ) )
118 117 oveq1d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( ( ( ( N ` ( A .+ B ) ) ^ 2 ) - ( ( N ` ( A .- B ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A .+ ( _i .x. B ) ) ) ^ 2 ) - ( ( N ` ( A .- ( _i .x. B ) ) ) ^ 2 ) ) ) ) / 4 ) = ( ( ( ( ( A ., B ) + ( B ., A ) ) + ( ( A ., B ) + ( B ., A ) ) ) + ( ( ( A ., B ) - ( B ., A ) ) + ( ( A ., B ) - ( B ., A ) ) ) ) / 4 ) )
119 40 43 subcld 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( A ., B ) - ( B ., A ) ) e. CC )
120 44 44 119 119 add4d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( ( ( A ., B ) + ( B ., A ) ) + ( ( A ., B ) + ( B ., A ) ) ) + ( ( ( A ., B ) - ( B ., A ) ) + ( ( A ., B ) - ( B ., A ) ) ) ) = ( ( ( ( A ., B ) + ( B ., A ) ) + ( ( A ., B ) - ( B ., A ) ) ) + ( ( ( A ., B ) + ( B ., A ) ) + ( ( A ., B ) - ( B ., A ) ) ) ) )
121 40 43 40 ppncand 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( ( A ., B ) + ( B ., A ) ) + ( ( A ., B ) - ( B ., A ) ) ) = ( ( A ., B ) + ( A ., B ) ) )
122 121 121 oveq12d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( ( ( A ., B ) + ( B ., A ) ) + ( ( A ., B ) - ( B ., A ) ) ) + ( ( ( A ., B ) + ( B ., A ) ) + ( ( A ., B ) - ( B ., A ) ) ) ) = ( ( ( A ., B ) + ( A ., B ) ) + ( ( A ., B ) + ( A ., B ) ) ) )
123 120 122 eqtrd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( ( ( A ., B ) + ( B ., A ) ) + ( ( A ., B ) + ( B ., A ) ) ) + ( ( ( A ., B ) - ( B ., A ) ) + ( ( A ., B ) - ( B ., A ) ) ) ) = ( ( ( A ., B ) + ( A ., B ) ) + ( ( A ., B ) + ( A ., B ) ) ) )
124 123 oveq1d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( ( ( ( A ., B ) + ( B ., A ) ) + ( ( A ., B ) + ( B ., A ) ) ) + ( ( ( A ., B ) - ( B ., A ) ) + ( ( A ., B ) - ( B ., A ) ) ) ) / 4 ) = ( ( ( ( A ., B ) + ( A ., B ) ) + ( ( A ., B ) + ( A ., B ) ) ) / 4 ) )
125 40 2timesd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( 2 x. ( A ., B ) ) = ( ( A ., B ) + ( A ., B ) ) )
126 125 eqcomd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( A ., B ) + ( A ., B ) ) = ( 2 x. ( A ., B ) ) )
127 126 126 oveq12d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( ( A ., B ) + ( A ., B ) ) + ( ( A ., B ) + ( A ., B ) ) ) = ( ( 2 x. ( A ., B ) ) + ( 2 x. ( A ., B ) ) ) )
128 2cnd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> 2 e. CC )
129 128 128 40 adddird 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( 2 + 2 ) x. ( A ., B ) ) = ( ( 2 x. ( A ., B ) ) + ( 2 x. ( A ., B ) ) ) )
130 2p2e4 
 |-  ( 2 + 2 ) = 4
131 130 a1i 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( 2 + 2 ) = 4 )
132 131 oveq1d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( 2 + 2 ) x. ( A ., B ) ) = ( 4 x. ( A ., B ) ) )
133 127 129 132 3eqtr2d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( ( A ., B ) + ( A ., B ) ) + ( ( A ., B ) + ( A ., B ) ) ) = ( 4 x. ( A ., B ) ) )
134 133 oveq1d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( ( ( A ., B ) + ( A ., B ) ) + ( ( A ., B ) + ( A ., B ) ) ) / 4 ) = ( ( 4 x. ( A ., B ) ) / 4 ) )
135 4cn 
 |-  4 e. CC
136 135 a1i 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> 4 e. CC )
137 4ne0 
 |-  4 =/= 0
138 137 a1i 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> 4 =/= 0 )
139 40 136 138 divcan3d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( 4 x. ( A ., B ) ) / 4 ) = ( A ., B ) )
140 134 139 eqtrd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( ( ( A ., B ) + ( A ., B ) ) + ( ( A ., B ) + ( A ., B ) ) ) / 4 ) = ( A ., B ) )
141 118 124 140 3eqtrrd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( A ., B ) = ( ( ( ( ( N ` ( A .+ B ) ) ^ 2 ) - ( ( N ` ( A .- B ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A .+ ( _i .x. B ) ) ) ^ 2 ) - ( ( N ` ( A .- ( _i .x. B ) ) ) ^ 2 ) ) ) ) / 4 ) )