Metamath Proof Explorer


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 A C
Assertion sto1i S States S A + S A = 1

Proof

Step Hyp Ref Expression
1 sto1.1 A C
2 1 chjoi A A =
3 2 fveq2i S A A = S
4 1 choccli A C
5 1 4 pm3.2i A C A C
6 1 chshii A S
7 shococss A S A A
8 6 7 ax-mp A A
9 stj S States A C A C A A S A A = S A + S A
10 5 8 9 mp2ani S States S A A = S A + S A
11 sthil S States S = 1
12 3 10 11 3eqtr3a S States S A + S A = 1