Definition df-hosum

Description: Define the sum of two Hilbert space operators. Definition of Beran p. 111. (Contributed by NM, 9-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Assertion	df-hosum	⊢ +op = ( 𝑓 ∈ ( ℋ ↑m ℋ ) , 𝑔 ∈ ( ℋ ↑m ℋ ) ↦ ( 𝑥 ∈ ℋ ↦ ( ( 𝑓 ‘ 𝑥 ) +ℎ ( 𝑔 ‘ 𝑥 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chos	⊢ +op
1		vf	⊢ 𝑓
2		chba	⊢ ℋ
3		cmap	⊢ ↑m
4	2 2 3	co	⊢ ( ℋ ↑m ℋ )
5		vg	⊢ 𝑔
6		vx	⊢ 𝑥
7	1	cv	⊢ 𝑓
8	6	cv	⊢ 𝑥
9	8 7	cfv	⊢ ( 𝑓 ‘ 𝑥 )
10		cva	⊢ +ℎ
11	5	cv	⊢ 𝑔
12	8 11	cfv	⊢ ( 𝑔 ‘ 𝑥 )
13	9 12 10	co	⊢ ( ( 𝑓 ‘ 𝑥 ) +ℎ ( 𝑔 ‘ 𝑥 ) )
14	6 2 13	cmpt	⊢ ( 𝑥 ∈ ℋ ↦ ( ( 𝑓 ‘ 𝑥 ) +ℎ ( 𝑔 ‘ 𝑥 ) ) )
15	1 5 4 4 14	cmpo	⊢ ( 𝑓 ∈ ( ℋ ↑m ℋ ) , 𝑔 ∈ ( ℋ ↑m ℋ ) ↦ ( 𝑥 ∈ ℋ ↦ ( ( 𝑓 ‘ 𝑥 ) +ℎ ( 𝑔 ‘ 𝑥 ) ) ) )
16	0 15	wceq	⊢ +op = ( 𝑓 ∈ ( ℋ ↑m ℋ ) , 𝑔 ∈ ( ℋ ↑m ℋ ) ↦ ( 𝑥 ∈ ℋ ↦ ( ( 𝑓 ‘ 𝑥 ) +ℎ ( 𝑔 ‘ 𝑥 ) ) ) )