Definition df-homul 9447

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

Assertion

Ref	Expression
df-homul	⊢ ·op = {⟨⟨f, g⟩, h⟩∣((f ∈ ℂ ⋀ g: ℋ –→ ℋ ) ⋀ h = {⟨x, y⟩∣(x ∈ ℋ ⋀ y = (f ·h (g ‘x)))})}

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

Detailed syntax breakdown of Definition df-homul

Step	Hyp	Ref	Expression
1		chot 8747	. 2 class ·op
2		vf	. . . . . . 7 set f
3	2	cv 953	. . . . . 6 class f
4		cc 5212	. . . . . 6 class ℂ
5	3, 4	wcel 956	. . . . 5 wff f ∈ ℂ
6		chil 8727	. . . . . 6 class ℋ
7		vg	. . . . . . 7 set g
8	7	cv 953	. . . . . 6 class g
9	6, 6, 8	wf 3173	. . . . 5 wff g: ℋ –→ ℋ
10	5, 9	wa 223	. . . 4 wff (f ∈ ℂ ⋀ g: ℋ –→ ℋ )
11		vh	. . . . . 6 set h
12	11	cv 953	. . . . 5 class h
13		vx	. . . . . . . . 9 set x
14	13	cv 953	. . . . . . . 8 class x
15	14, 6	wcel 956	. . . . . . 7 wff x ∈ ℋ
16		vy	. . . . . . . . 9 set y
17	16	cv 953	. . . . . . . 8 class y
18	14, 8	cfv 3177	. . . . . . . . 9 class (g ‘x)
19		csm 8729	. . . . . . . . 9 class ·h
20	3, 18, 19	co 3954	. . . . . . . 8 class (f ·h (g ‘x))
21	17, 20	wceq 954	. . . . . . 7 wff y = (f ·h (g ‘x))
22	15, 21	wa 223	. . . . . 6 wff (x ∈ ℋ ⋀ y = (f ·h (g ‘x)))
23	22, 13, 16	copab 2661	. . . . 5 class {⟨x, y⟩∣(x ∈ ℋ ⋀ y = (f ·h (g ‘x)))}
24	12, 23	wceq 954	. . . 4 wff h = {⟨x, y⟩∣(x ∈ ℋ ⋀ y = (f ·h (g ‘x)))}
25	10, 24	wa 223	. . 3 wff ((f ∈ ℂ ⋀ g: ℋ –→ ℋ ) ⋀ h = {⟨x, y⟩∣(x ∈ ℋ ⋀ y = (f ·h (g ‘x)))})
26	25, 2, 7, 11	copab2 3955	. 2 class {⟨⟨f, g⟩, h⟩∣((f ∈ ℂ ⋀ g: ℋ –→ ℋ ) ⋀ h = {⟨x, y⟩∣(x ∈ ℋ ⋀ y = (f ·h (g ‘x)))})}
27	1, 26	wceq 954	1 wff ·op = {⟨⟨f, g⟩, h⟩∣((f ∈ ℂ ⋀ g: ℋ –→ ℋ ) ⋀ h = {⟨x, y⟩∣(x ∈ ℋ ⋀ y = (f ·h (g ‘x)))})}

This definition is referenced by:  hommvalt 9452

Copyright terms: Public domain