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 e. CH
Assertion sto2i 
|- ( S e. States -> ( S ` ( _|_ ` A ) ) = ( 1 - ( S ` A ) ) )

Proof

Step Hyp Ref Expression
1 sto1.1 
 |-  A e. CH
2 1 sto1i 
 |-  ( S e. States -> ( ( S ` A ) + ( S ` ( _|_ ` A ) ) ) = 1 )
3 stcl 
 |-  ( S e. States -> ( A e. CH -> ( S ` A ) e. RR ) )
4 1 3 mpi 
 |-  ( S e. States -> ( S ` A ) e. RR )
5 4 recnd 
 |-  ( S e. States -> ( S ` A ) e. CC )
6 1 choccli 
 |-  ( _|_ ` A ) e. CH
7 stcl 
 |-  ( S e. States -> ( ( _|_ ` A ) e. CH -> ( S ` ( _|_ ` A ) ) e. RR ) )
8 6 7 mpi 
 |-  ( S e. States -> ( S ` ( _|_ ` A ) ) e. RR )
9 8 recnd 
 |-  ( S e. States -> ( S ` ( _|_ ` A ) ) e. CC )
10 ax-1cn 
 |-  1 e. CC
11 subadd 
 |-  ( ( 1 e. CC /\ ( S ` A ) e. CC /\ ( S ` ( _|_ ` A ) ) e. CC ) -> ( ( 1 - ( S ` A ) ) = ( S ` ( _|_ ` A ) ) <-> ( ( S ` A ) + ( S ` ( _|_ ` A ) ) ) = 1 ) )
12 10 11 mp3an1 
 |-  ( ( ( S ` A ) e. CC /\ ( S ` ( _|_ ` A ) ) e. CC ) -> ( ( 1 - ( S ` A ) ) = ( S ` ( _|_ ` A ) ) <-> ( ( S ` A ) + ( S ` ( _|_ ` A ) ) ) = 1 ) )
13 5 9 12 syl2anc 
 |-  ( S e. States -> ( ( 1 - ( S ` A ) ) = ( S ` ( _|_ ` A ) ) <-> ( ( S ` A ) + ( S ` ( _|_ ` A ) ) ) = 1 ) )
14 2 13 mpbird 
 |-  ( S e. States -> ( 1 - ( S ` A ) ) = ( S ` ( _|_ ` A ) ) )
15 14 eqcomd 
 |-  ( S e. States -> ( S ` ( _|_ ` A ) ) = ( 1 - ( S ` A ) ) )