Theorem sto2i

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

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

Proof

Step	Hyp	Ref	Expression
1		sto1.1	⊢ 𝐴 ∈ Cℋ
2	1	sto1i	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = 1 )
3		stcl	⊢ ( 𝑆 ∈ States → ( 𝐴 ∈ Cℋ → ( 𝑆 ‘ 𝐴 ) ∈ ℝ ) )
4	1 3	mpi	⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 𝐴 ) ∈ ℝ )
5	4	recnd	⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 𝐴 ) ∈ ℂ )
6	1	choccli	⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
7		stcl	⊢ ( 𝑆 ∈ States → ( ( ⊥ ‘ 𝐴 ) ∈ Cℋ → ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ∈ ℝ ) )
8	6 7	mpi	⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ∈ ℝ )
9	8	recnd	⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ∈ ℂ )
10		ax-1cn	⊢ 1 ∈ ℂ
11		subadd	⊢ ( ( 1 ∈ ℂ ∧ ( 𝑆 ‘ 𝐴 ) ∈ ℂ ∧ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ∈ ℂ ) → ( ( 1 − ( 𝑆 ‘ 𝐴 ) ) = ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ↔ ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = 1 ) )
12	10 11	mp3an1	⊢ ( ( ( 𝑆 ‘ 𝐴 ) ∈ ℂ ∧ ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ∈ ℂ ) → ( ( 1 − ( 𝑆 ‘ 𝐴 ) ) = ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ↔ ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = 1 ) )
13	5 9 12	syl2anc	⊢ ( 𝑆 ∈ States → ( ( 1 − ( 𝑆 ‘ 𝐴 ) ) = ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ↔ ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = 1 ) )
14	2 13	mpbird	⊢ ( 𝑆 ∈ States → ( 1 − ( 𝑆 ‘ 𝐴 ) ) = ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) )
15	14	eqcomd	⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) = ( 1 − ( 𝑆 ‘ 𝐴 ) ) )