Definition df-st

Description: Define the set of states on a Hilbert lattice. Definition of Kalmbach p. 266. (Contributed by NM, 23-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	df-st	⊢ States = { 𝑓 ∈ ( ( 0 [,] 1 ) ↑m Cℋ ) ∣ ( ( 𝑓 ‘ ℋ ) = 1 ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( 𝑓 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) }

Detailed syntax breakdown

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