Definition df-hst

Description: Define the set of complex Hilbert-space-valued states on a Hilbert lattice. Definition of CH-states in Mayet3 p. 9. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	df-hst	⊢ CHStates = { 𝑓 ∈ ( ℋ ↑m Cℋ ) ∣ ( ( normℎ ‘ ( 𝑓 ‘ ℋ ) ) = 1 ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑓 ‘ 𝑥 ) ·ih ( 𝑓 ‘ 𝑦 ) ) = 0 ∧ ( 𝑓 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) +ℎ ( 𝑓 ‘ 𝑦 ) ) ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chst	⊢ CHStates
1		vf	⊢ 𝑓
2		chba	⊢ ℋ
3		cmap	⊢ ↑m
4		cch	⊢ Cℋ
5	2 4 3	co	⊢ ( ℋ ↑m Cℋ )
6		cno	⊢ normℎ
7	1	cv	⊢ 𝑓
8	2 7	cfv	⊢ ( 𝑓 ‘ ℋ )
9	8 6	cfv	⊢ ( normℎ ‘ ( 𝑓 ‘ ℋ ) )
10		c1	⊢ 1
11	9 10	wceq	⊢ ( normℎ ‘ ( 𝑓 ‘ ℋ ) ) = 1
12		vx	⊢ 𝑥
13		vy	⊢ 𝑦
14	12	cv	⊢ 𝑥
15		cort	⊢ ⊥
16	13	cv	⊢ 𝑦
17	16 15	cfv	⊢ ( ⊥ ‘ 𝑦 )
18	14 17	wss	⊢ 𝑥 ⊆ ( ⊥ ‘ 𝑦 )
19	14 7	cfv	⊢ ( 𝑓 ‘ 𝑥 )
20		csp	⊢ ·ih
21	16 7	cfv	⊢ ( 𝑓 ‘ 𝑦 )
22	19 21 20	co	⊢ ( ( 𝑓 ‘ 𝑥 ) ·ih ( 𝑓 ‘ 𝑦 ) )
23		cc0	⊢ 0
24	22 23	wceq	⊢ ( ( 𝑓 ‘ 𝑥 ) ·ih ( 𝑓 ‘ 𝑦 ) ) = 0
25		chj	⊢ ∨ℋ
26	14 16 25	co	⊢ ( 𝑥 ∨ℋ 𝑦 )
27	26 7	cfv	⊢ ( 𝑓 ‘ ( 𝑥 ∨ℋ 𝑦 ) )
28		cva	⊢ +ℎ
29	19 21 28	co	⊢ ( ( 𝑓 ‘ 𝑥 ) +ℎ ( 𝑓 ‘ 𝑦 ) )
30	27 29	wceq	⊢ ( 𝑓 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) +ℎ ( 𝑓 ‘ 𝑦 ) )
31	24 30	wa	⊢ ( ( ( 𝑓 ‘ 𝑥 ) ·ih ( 𝑓 ‘ 𝑦 ) ) = 0 ∧ ( 𝑓 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) +ℎ ( 𝑓 ‘ 𝑦 ) ) )
32	18 31	wi	⊢ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑓 ‘ 𝑥 ) ·ih ( 𝑓 ‘ 𝑦 ) ) = 0 ∧ ( 𝑓 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) +ℎ ( 𝑓 ‘ 𝑦 ) ) ) )
33	32 13 4	wral	⊢ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑓 ‘ 𝑥 ) ·ih ( 𝑓 ‘ 𝑦 ) ) = 0 ∧ ( 𝑓 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) +ℎ ( 𝑓 ‘ 𝑦 ) ) ) )
34	33 12 4	wral	⊢ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑓 ‘ 𝑥 ) ·ih ( 𝑓 ‘ 𝑦 ) ) = 0 ∧ ( 𝑓 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) +ℎ ( 𝑓 ‘ 𝑦 ) ) ) )
35	11 34	wa	⊢ ( ( normℎ ‘ ( 𝑓 ‘ ℋ ) ) = 1 ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑓 ‘ 𝑥 ) ·ih ( 𝑓 ‘ 𝑦 ) ) = 0 ∧ ( 𝑓 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) +ℎ ( 𝑓 ‘ 𝑦 ) ) ) ) )
36	35 1 5	crab	⊢ { 𝑓 ∈ ( ℋ ↑m Cℋ ) ∣ ( ( normℎ ‘ ( 𝑓 ‘ ℋ ) ) = 1 ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑓 ‘ 𝑥 ) ·ih ( 𝑓 ‘ 𝑦 ) ) = 0 ∧ ( 𝑓 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) +ℎ ( 𝑓 ‘ 𝑦 ) ) ) ) ) }
37	0 36	wceq	⊢ CHStates = { 𝑓 ∈ ( ℋ ↑m Cℋ ) ∣ ( ( normℎ ‘ ( 𝑓 ‘ ℋ ) ) = 1 ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑓 ‘ 𝑥 ) ·ih ( 𝑓 ‘ 𝑦 ) ) = 0 ∧ ( 𝑓 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) +ℎ ( 𝑓 ‘ 𝑦 ) ) ) ) ) }