Theorem sto1i

Description: The state of a subspace plus the state of its orthocomplement. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypothesis	sto1.1	⊢ 𝐴 ∈ Cℋ
Assertion	sto1i	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		sto1.1	⊢ 𝐴 ∈ Cℋ
2	1	chjoi	⊢ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐴 ) ) = ℋ
3	2	fveq2i	⊢ ( 𝑆 ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) = ( 𝑆 ‘ ℋ )
4	1	choccli	⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
5	1 4	pm3.2i	⊢ ( 𝐴 ∈ Cℋ ∧ ( ⊥ ‘ 𝐴 ) ∈ Cℋ )
6	1	chshii	⊢ 𝐴 ∈ Sℋ
7		shococss	⊢ ( 𝐴 ∈ Sℋ → 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
8	6 7	ax-mp	⊢ 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) )
9		stj	⊢ ( 𝑆 ∈ States → ( ( ( 𝐴 ∈ Cℋ ∧ ( ⊥ ‘ 𝐴 ) ∈ Cℋ ) ∧ 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) → ( 𝑆 ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) = ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) ) )
10	5 8 9	mp2ani	⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) = ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) )
11		sthil	⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ ℋ ) = 1 )
12	3 10 11	3eqtr3a	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = 1 )