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⊆ℋ∧B⊆ℋ→A∨ℋB=⋁ℋ⁡AB

Proof

Step Hyp Ref Expression
1 ax-hilex ⊢ℋ∈V
2 1 elpw2 ⊢A∈𝒫ℋ↔A⊆ℋ
3 1 elpw2 ⊢B∈𝒫ℋ↔B⊆ℋ
4 uniprg ⊢A∈𝒫ℋ∧B∈𝒫ℋ→⋃AB=A∪B
5 2 3 4 syl2anbr ⊢A⊆ℋ∧B⊆ℋ→⋃AB=A∪B
6 5 fveq2d ⊢A⊆ℋ∧B⊆ℋ→⊥⁡⋃AB=⊥⁡A∪B
7 6 fveq2d ⊢A⊆ℋ∧B⊆ℋ→⊥⁡⊥⁡⋃AB=⊥⁡⊥⁡A∪B
8 prssi ⊢A∈𝒫ℋ∧B∈𝒫ℋ→AB⊆𝒫ℋ
9 2 3 8 syl2anbr ⊢A⊆ℋ∧B⊆ℋ→AB⊆𝒫ℋ
10 hsupval ⊢AB⊆𝒫ℋ→⋁ℋ⁡AB=⊥⁡⊥⁡⋃AB
11 9 10 syl ⊢A⊆ℋ∧B⊆ℋ→⋁ℋ⁡AB=⊥⁡⊥⁡⋃AB
12 sshjval ⊢A⊆ℋ∧B⊆ℋ→A∨ℋB=⊥⁡⊥⁡A∪B
13 7 11 12 3eqtr4rd ⊢A⊆ℋ∧B⊆ℋ→A∨ℋB=⋁ℋ⁡AB