Metamath Proof Explorer

Theorem sto2i

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

Ref Expression
Hypothesis sto1.1 ⊢ A ∈ C ℋ
Assertion sto2i ⊢ S ∈ States → S ⁡ ⊥ ⁡ A = 1 − S ⁡ A

Proof

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