This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sshjval3

Description: Value of join for subsets of Hilbert space in terms of supremum: the join is the supremum of its two arguments. Based on the definition of join in Beran p. 3. For later convenience we prove a general version that works for any subset of Hilbert space, not just the elements of the lattice CH . (Contributed by NM, 2-Mar-2004) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion sshjval3 
|- ( ( A C_ ~H /\ B C_ ~H ) -> ( A vH B ) = ( \/H ` { A , B } ) )

Proof

Step Hyp Ref Expression
1 ax-hilex 
 |-  ~H e. _V
2 1 elpw2 
 |-  ( A e. ~P ~H <-> A C_ ~H )
3 1 elpw2 
 |-  ( B e. ~P ~H <-> B C_ ~H )
4 uniprg 
 |-  ( ( A e. ~P ~H /\ B e. ~P ~H ) -> U. { A , B } = ( A u. B ) )
5 2 3 4 syl2anbr 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> U. { A , B } = ( A u. B ) )
6 5 fveq2d 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( _|_ ` U. { A , B } ) = ( _|_ ` ( A u. B ) ) )
7 6 fveq2d 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( _|_ ` ( _|_ ` U. { A , B } ) ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) )
8 prssi 
 |-  ( ( A e. ~P ~H /\ B e. ~P ~H ) -> { A , B } C_ ~P ~H )
9 2 3 8 syl2anbr 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> { A , B } C_ ~P ~H )
10 hsupval 
 |-  ( { A , B } C_ ~P ~H -> ( \/H ` { A , B } ) = ( _|_ ` ( _|_ ` U. { A , B } ) ) )
11 9 10 syl 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( \/H ` { A , B } ) = ( _|_ ` ( _|_ ` U. { A , B } ) ) )
12 sshjval 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) )
13 7 11 12 3eqtr4rd 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( A vH B ) = ( \/H ` { A , B } ) )