Theorem ipval 8437

Description: Value of the inner product. The definition is meaningful for normed complex vector spaces that are also inner product spaces, i.e. satisfy the parallelogram law, although for convenience we define it for any normed complex vector space. The vector (group) addition operation is G, the scalar product is S, the norm is N, and the set of vectors is X. Equation 6.45 of [Ponnusamy] p. 361.

Hypotheses

Ref	Expression
ipfval.1	|- X = (Base` U)
ipfval.2	|- G = (+v` U)
ipfval.4	|- S = (.s` U)
ipfval.6	|- N = (norm` U)
ipfval.7	|- P = (.i` U)

Assertion

Ref	Expression
ipval	|- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (APB) = (sum_k e. (1...4)((i^k) x. ((N` (AG((i^k)SB)))^2)) / 4))

Distinct variable groups:   k,G   k,N   S,k   U,k   A,k   B,k

Proof of Theorem ipval

Step	Hyp	Ref	Expression
1		ipfval.1	. . . . 5 |- X = (Base` U)
2		ipfval.2	. . . . 5 |- G = (+v` U)
3		ipfval.4	. . . . 5 |- S = (.s` U)
4		ipfval.6	. . . . 5 |- N = (norm` U)
5		ipfval.7	. . . . 5 |- P = (.i` U)
6	1, 2, 3, 4, 5	ipfval 8436	. . . 4 |- (U e. NrmCVec -> P = {<.<.x, y>., z>. | ((x e. X /\ y e. X) /\ z = (sum_k e. (1...4)((i^k) x. ((N` (xG((i^k)Sy)))^2)) / 4))})
7	6	opreqd 4035	. . 3 |- (U e. NrmCVec -> (APB) = (A{<.<.x, y>., z>. | ((x e. X /\ y e. X) /\ z = (sum_k e. (1...4)((i^k) x. ((N` (xG((i^k)Sy)))^2)) / 4))}B))
8	7	3ad2ant1 812	. 2 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (APB) = (A{<.<.x, y>., z>. | ((x e. X /\ y e. X) /\ z = (sum_k e. (1...4)((i^k) x. ((N` (xG((i^k)Sy)))^2)) / 4))}B))
9		oprex 4041	. . . 4 |- (sum_k e. (1...4)((i^k) x. ((N` (AG((i^k)SB)))^2)) / 4) e. V
10		opreq1 4026	. . . . . . . . 9 |- (x = A -> (xG((i^k)Sy)) = (AG((i^k)Sy)))
11	10	fveq2d 3785	. . . . . . . 8 |- (x = A -> (N` (xG((i^k)Sy))) = (N` (AG((i^k)Sy))))
12	11	opreq1d 4033	. . . . . . 7 |- (x = A -> ((N` (xG((i^k)Sy)))^2) = ((N` (AG((i^k)Sy)))^2))
13	12	opreq2d 4034	. . . . . 6 |- (x = A -> ((i^k) x. ((N` (xG((i^k)Sy)))^2)) = ((i^k) x. ((N` (AG((i^k)Sy)))^2)))
14	13	sumeq2sdv 7083	. . . . 5 |- (x = A -> sum_k e. (1...4)((i^k) x. ((N` (xG((i^k)Sy)))^2)) = sum_k e. (1...4)((i^k) x. ((N` (AG((i^k)Sy)))^2)))
15	14	opreq1d 4033	. . . 4 |- (x = A -> (sum_k e. (1...4)((i^k) x. ((N` (xG((i^k)Sy)))^2)) / 4) = (sum_k e. (1...4)((i^k) x. ((N` (AG((i^k)Sy)))^2)) / 4))
16		opreq2 4027	. . . . . . . . . 10 |- (y = B -> ((i^k)Sy) = ((i^k)SB))
17	16	opreq2d 4034	. . . . . . . . 9 |- (y = B -> (AG((i^k)Sy)) = (AG((i^k)SB)))
18	17	fveq2d 3785	. . . . . . . 8 |- (y = B -> (N` (AG((i^k)Sy))) = (N` (AG((i^k)SB))))
19	18	opreq1d 4033	. . . . . . 7 |- (y = B -> ((N` (AG((i^k)Sy)))^2) = ((N` (AG((i^k)SB)))^2))
20	19	opreq2d 4034	. . . . . 6 |- (y = B -> ((i^k) x. ((N` (AG((i^k)Sy)))^2)) = ((i^k) x. ((N` (AG((i^k)SB)))^2)))
21	20	sumeq2sdv 7083	. . . . 5 |- (y = B -> sum_k e. (1...4)((i^k) x. ((N` (AG((i^k)Sy)))^2)) = sum_k e. (1...4)((i^k) x. ((N` (AG((i^k)SB)))^2)))
22	21	opreq1d 4033	. . . 4 |- (y = B -> (sum_k e. (1...4)((i^k) x. ((N` (AG((i^k)Sy)))^2)) / 4) = (sum_k e. (1...4)((i^k) x. ((N` (AG((i^k)SB)))^2)) / 4))
23		eqid 1522	. . . 4 |- {<.<.x, y>., z>. | ((x e. X /\ y e. X) /\ z = (sum_k e. (1...4)((i^k) x. ((N` (xG((i^k)Sy)))^2)) / 4))} = {<.<.x, y>., z>. | ((x e. X /\ y e. X) /\ z = (sum_k e. (1...4)((i^k) x. ((N` (xG((i^k)Sy)))^2)) / 4))}
24	9, 15, 22, 23	oprabval2 4086	. . 3 |- ((A e. X /\ B e. X) -> (A{<.<.x, y>., z>. | ((x e. X /\ y e. X) /\ z = (sum_k e. (1...4)((i^k) x. ((N` (xG((i^k)Sy)))^2)) / 4))}B) = (sum_k e. (1...4)((i^k) x. ((N` (AG((i^k)SB)))^2)) / 4))
25	24	3adant1 809	. 2 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (A{<.<.x, y>., z>. | ((x e. X /\ y e. X) /\ z = (sum_k e. (1...4)((i^k) x. ((N` (xG((i^k)Sy)))^2)) / 4))}B) = (sum_k e. (1...4)((i^k) x. ((N` (AG((i^k)SB)))^2)) / 4))
26	8, 25	eqtrd 1554	1 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (APB) = (sum_k e. (1...4)((i^k) x. ((N` (AG((i^k)SB)))^2)) / 4))

Syntax hints:   -> wi 3   /\ wa 230   /\ w3a 787   = wceq 997   e. wcel 999  ` cfv 3239  (class class class)co 4021  {copab2 4022  1c1 5300  ici 5301   x. cmul 5304   / cdiv 5359  2c2 6022  4c4 6024  ...cfz 6493  ^cexp 6657  sum_csu 7069  NrmCVeccnv 8287  +vcpv 8288  Basecba 8289  .scns 8290  normcnm 8293  .icip 8433

This theorem is referenced by:  ipval2 8441  ipcl 8449  ipf 8450  ip1cnilem6 8462  sspival 8481

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-9 1006  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-rep 2748  ax-sep 2758  ax-nul 2765  ax-pow 2798  ax-pr 2835  ax-un 2922  ax-inf2 4687

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3or 788  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-nel 1635  df-ral 1696  df-rex 1697  df-reu 1698  df-rab 1699  df-v 1859  df-sbc 1989  df-csb 2052  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-pss 2106  df-nul 2332  df-if 2414  df-pw 2454  df-sn 2464  df-pr 2465  df-tp 2467  df-op 2468  df-uni 2558  df-int 2588  df-iun 2622  df-br 2675  df-opab 2722  df-tr 2736  df-eprel 2888  df-id 2891  df-po 2896  df-so 2906  df-fr 2974  df-we 2991  df-ord 3008  df-on 3009  df-lim 3010  df-suc 3011  df-om 3189  df-xp 3241  df-rel 3242  df-cnv 3243  df-co 3244  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fun 3249  df-fn 3250  df-f 3251  df-f1 3252  df-fo 3253  df-f1o 3254  df-fv 3255  df-rdg 3990  df-opr 4023  df-oprab 4024  df-1st 4137  df-2nd 4138  df-1o 4191  df-oadd 4193  df-omul 4194  df-er 4319  df-ec 4321  df-qs 4324  df-en 4429  df-dom 4430  df-sdom 4431  df-ni 5065  df-pli 5066  df-mi 5067  df-lti 5068  df-plpq 5100  df-mpq 5101  df-enq 5102  df-nq 5103  df-plq 5104  df-mq 5105  df-rq 5106  df-ltq 5107  df-1q 5108  df-np 5151  df-1p 5152  df-plp 5153  df-mp 5154  df-ltp 5155  df-plpr 5229  df-mpr 5230  df-enr 5231  df-nr 5232  df-plr 5233  df-mr 5234  df-ltr 5235  df-0r 5236  df-1r 5237  df-m1r 5238  df-c 5305  df-0 5306  df-1 5307  df-i 5308  df-r 5309  df-plus 5310  df-mul 5311  df-lt 5312  df-sub 5421  df-neg 5423  df-pnf 5552  df-mnf 5553  df-xr 5554  df-ltxr 5555  df-le 5556  df-n 5985  df-n0 6182  df-z 6218  df-uz 6444  df-fz 6494  df-seq1 6567  df-shft 6600  df-seqz 6622  df-sum 7070  df-grp 8122  df-gid 8123  df-nv 8295  df-va 8298  df-ba 8299  df-sm 8300  df-0v 8301  df-nm 8303  df-ip 8434

Copyright terms: Public domain