This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-lnfn

Description: Define the set of linear functionals on Hilbert space. (Contributed by NM, 11-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion df-lnfn LinFn = { 𝑡 ∈ ( ℂ ↑m ℋ ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( 𝑡 ‘ 𝑦 ) ) + ( 𝑡 ‘ 𝑧 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 clf ⊢ LinFn
1 vt ⊢ 𝑡
2 cc ⊢ ℂ
3 cmap ⊢ ↑m
4 chba ⊢ ℋ
5 2 4 3 co ⊢ ( ℂ ↑m ℋ )
6 vx ⊢ 𝑥
7 vy ⊢ 𝑦
8 vz ⊢ 𝑧
9 1 cv ⊢ 𝑡
10 6 cv ⊢ 𝑥
11 csm ⊢ ·ℎ
12 7 cv ⊢ 𝑦
13 10 12 11 co ⊢ ( 𝑥 ·ℎ 𝑦 )
14 cva ⊢ +ℎ
15 8 cv ⊢ 𝑧
16 13 15 14 co ⊢ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 )
17 16 9 cfv ⊢ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) )
18 cmul ⊢ ·
19 12 9 cfv ⊢ ( 𝑡 ‘ 𝑦 )
20 10 19 18 co ⊢ ( 𝑥 · ( 𝑡 ‘ 𝑦 ) )
21 caddc ⊢ +
22 15 9 cfv ⊢ ( 𝑡 ‘ 𝑧 )
23 20 22 21 co ⊢ ( ( 𝑥 · ( 𝑡 ‘ 𝑦 ) ) + ( 𝑡 ‘ 𝑧 ) )
24 17 23 wceq ⊢ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( 𝑡 ‘ 𝑦 ) ) + ( 𝑡 ‘ 𝑧 ) )
25 24 8 4 wral ⊢ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( 𝑡 ‘ 𝑦 ) ) + ( 𝑡 ‘ 𝑧 ) )
26 25 7 4 wral ⊢ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( 𝑡 ‘ 𝑦 ) ) + ( 𝑡 ‘ 𝑧 ) )
27 26 6 2 wral ⊢ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( 𝑡 ‘ 𝑦 ) ) + ( 𝑡 ‘ 𝑧 ) )
28 27 1 5 crab ⊢ { 𝑡 ∈ ( ℂ ↑m ℋ ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( 𝑡 ‘ 𝑦 ) ) + ( 𝑡 ‘ 𝑧 ) ) }
29 0 28 wceq ⊢ LinFn = { 𝑡 ∈ ( ℂ ↑m ℋ ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( 𝑡 ‘ 𝑦 ) ) + ( 𝑡 ‘ 𝑧 ) ) }