Metamath Proof Explorer

Theorem stj

Description: The value of a state on a join. (Contributed by NM, 23-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion stj 
|- ( S e. States -> ( ( ( A e. CH /\ B e. CH ) /\ A C_ ( _|_ ` B ) ) -> ( S ` ( A vH B ) ) = ( ( S ` A ) + ( S ` B ) ) ) )

Proof

Step Hyp Ref Expression
1 isst 
 |-  ( S e. States <-> ( S : CH --> ( 0 [,] 1 ) /\ ( S ` ~H ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( S ` ( x vH y ) ) = ( ( S ` x ) + ( S ` y ) ) ) ) )
2 1 simp3bi 
 |-  ( S e. States -> A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( S ` ( x vH y ) ) = ( ( S ` x ) + ( S ` y ) ) ) )
3 sseq1 
 |-  ( x = A -> ( x C_ ( _|_ ` y ) <-> A C_ ( _|_ ` y ) ) )
4 fvoveq1 
 |-  ( x = A -> ( S ` ( x vH y ) ) = ( S ` ( A vH y ) ) )
5 fveq2 
 |-  ( x = A -> ( S ` x ) = ( S ` A ) )
6 5 oveq1d 
 |-  ( x = A -> ( ( S ` x ) + ( S ` y ) ) = ( ( S ` A ) + ( S ` y ) ) )
7 4 6 eqeq12d 
 |-  ( x = A -> ( ( S ` ( x vH y ) ) = ( ( S ` x ) + ( S ` y ) ) <-> ( S ` ( A vH y ) ) = ( ( S ` A ) + ( S ` y ) ) ) )
8 3 7 imbi12d 
 |-  ( x = A -> ( ( x C_ ( _|_ ` y ) -> ( S ` ( x vH y ) ) = ( ( S ` x ) + ( S ` y ) ) ) <-> ( A C_ ( _|_ ` y ) -> ( S ` ( A vH y ) ) = ( ( S ` A ) + ( S ` y ) ) ) ) )
9 fveq2 
 |-  ( y = B -> ( _|_ ` y ) = ( _|_ ` B ) )
10 9 sseq2d 
 |-  ( y = B -> ( A C_ ( _|_ ` y ) <-> A C_ ( _|_ ` B ) ) )
11 oveq2 
 |-  ( y = B -> ( A vH y ) = ( A vH B ) )
12 11 fveq2d 
 |-  ( y = B -> ( S ` ( A vH y ) ) = ( S ` ( A vH B ) ) )
13 fveq2 
 |-  ( y = B -> ( S ` y ) = ( S ` B ) )
14 13 oveq2d 
 |-  ( y = B -> ( ( S ` A ) + ( S ` y ) ) = ( ( S ` A ) + ( S ` B ) ) )
15 12 14 eqeq12d 
 |-  ( y = B -> ( ( S ` ( A vH y ) ) = ( ( S ` A ) + ( S ` y ) ) <-> ( S ` ( A vH B ) ) = ( ( S ` A ) + ( S ` B ) ) ) )
16 10 15 imbi12d 
 |-  ( y = B -> ( ( A C_ ( _|_ ` y ) -> ( S ` ( A vH y ) ) = ( ( S ` A ) + ( S ` y ) ) ) <-> ( A C_ ( _|_ ` B ) -> ( S ` ( A vH B ) ) = ( ( S ` A ) + ( S ` B ) ) ) ) )
17 8 16 rspc2v 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( S ` ( x vH y ) ) = ( ( S ` x ) + ( S ` y ) ) ) -> ( A C_ ( _|_ ` B ) -> ( S ` ( A vH B ) ) = ( ( S ` A ) + ( S ` B ) ) ) ) )
18 2 17 syl5com 
 |-  ( S e. States -> ( ( A e. CH /\ B e. CH ) -> ( A C_ ( _|_ ` B ) -> ( S ` ( A vH B ) ) = ( ( S ` A ) + ( S ` B ) ) ) ) )
19 18 impd 
 |-  ( S e. States -> ( ( ( A e. CH /\ B e. CH ) /\ A C_ ( _|_ ` B ) ) -> ( S ` ( A vH B ) ) = ( ( S ` A ) + ( S ` B ) ) ) )