Theorem hstoc

Description: Sum of a Hilbert-space-valued state of a lattice element and its orthocomplement. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hstoc	⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( 𝑆 ‘ 𝐴 ) +ℎ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = ( 𝑆 ‘ ℋ ) )

Proof

Step	Hyp	Ref	Expression
1		choccl	⊢ ( 𝐴 ∈ Cℋ → ( ⊥ ‘ 𝐴 ) ∈ Cℋ )
2	1	adantl	⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ⊥ ‘ 𝐴 ) ∈ Cℋ )
3		chsh	⊢ ( 𝐴 ∈ Cℋ → 𝐴 ∈ Sℋ )
4		shococss	⊢ ( 𝐴 ∈ Sℋ → 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
5	3 4	syl	⊢ ( 𝐴 ∈ Cℋ → 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
6	5	adantl	⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
7	2 6	jca	⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( ⊥ ‘ 𝐴 ) ∈ Cℋ ∧ 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) )
8		hstosum	⊢ ( ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ ( ( ⊥ ‘ 𝐴 ) ∈ Cℋ ∧ 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) ) → ( 𝑆 ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) = ( ( 𝑆 ‘ 𝐴 ) +ℎ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) )
9	7 8	mpdan	⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( 𝑆 ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) = ( ( 𝑆 ‘ 𝐴 ) +ℎ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) )
10		chjo	⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐴 ) ) = ℋ )
11	10	fveq2d	⊢ ( 𝐴 ∈ Cℋ → ( 𝑆 ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) = ( 𝑆 ‘ ℋ ) )
12	11	adantl	⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( 𝑆 ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) = ( 𝑆 ‘ ℋ ) )
13	9 12	eqtr3d	⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ( ( 𝑆 ‘ 𝐴 ) +ℎ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = ( 𝑆 ‘ ℋ ) )