Definition df-hfmul 9427

Description: Define the scalar product with a Hilbert space functional. Definition of [Beran] p. 111.

Assertion

Ref	Expression
df-hfmul	|- .fn = {<.<.f, g>., h>. | ((f e. CC /\ g:H~-->CC) /\ h = {<.x, y>. | (x e. H~ /\ y = (f x. (g` x)))})}

Distinct variable group:   f,g,h,x,y

Detailed syntax breakdown of Definition df-hfmul

Step	Hyp	Ref	Expression
1		chft 8750	. 2 class .fn
2		vf	. . . . . . 7 set f
3	2	cv 952	. . . . . 6 class f
4		cc 5204	. . . . . 6 class CC
5	3, 4	wcel 955	. . . . 5 wff f e. CC
6		chil 8727	. . . . . 6 class H~
7		vg	. . . . . . 7 set g
8	7	cv 952	. . . . . 6 class g
9	6, 4, 8	wf 3168	. . . . 5 wff g:H~-->CC
10	5, 9	wa 223	. . . 4 wff (f e. CC /\ g:H~-->CC)
11		vh	. . . . . 6 set h
12	11	cv 952	. . . . 5 class h
13		vx	. . . . . . . . 9 set x
14	13	cv 952	. . . . . . . 8 class x
15	14, 6	wcel 955	. . . . . . 7 wff x e. H~
16		vy	. . . . . . . . 9 set y
17	16	cv 952	. . . . . . . 8 class y
18	14, 8	cfv 3172	. . . . . . . . 9 class (g` x)
19		cmul 5211	. . . . . . . . 9 class x.
20	3, 18, 19	co 3948	. . . . . . . 8 class (f x. (g` x))
21	17, 20	wceq 953	. . . . . . 7 wff y = (f x. (g` x))
22	15, 21	wa 223	. . . . . 6 wff (x e. H~ /\ y = (f x. (g` x)))
23	22, 13, 16	copab 2656	. . . . 5 class {<.x, y>. | (x e. H~ /\ y = (f x. (g` x)))}
24	12, 23	wceq 953	. . . 4 wff h = {<.x, y>. | (x e. H~ /\ y = (f x. (g` x)))}
25	10, 24	wa 223	. . 3 wff ((f e. CC /\ g:H~-->CC) /\ h = {<.x, y>. | (x e. H~ /\ y = (f x. (g` x)))})
26	25, 2, 7, 11	copab2 3949	. 2 class {<.<.f, g>., h>. | ((f e. CC /\ g:H~-->CC) /\ h = {<.x, y>. | (x e. H~ /\ y = (f x. (g` x)))})}
27	1, 26	wceq 953	1 wff .fn = {<.<.f, g>., h>. | ((f e. CC /\ g:H~-->CC) /\ h = {<.x, y>. | (x e. H~ /\ y = (f x. (g` x)))})}

This definition is referenced by:  hfmmvalt 9432

Copyright terms: Public domain