Metamath Proof Explorer

Theorem sshhococi

Description: The join of two Hilbert space subsets (not necessarily closed subspaces) equals the join of their closures (double orthocomplements). (Contributed by NM, 1-Jun-2004) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses sshjococ.1 ⊢ 𝐴 ⊆ ℋ
sshjococ.2 ⊢ 𝐵 ⊆ ℋ
Assertion sshhococi ( 𝐴 ∨ℋ 𝐵 ) = ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∨ℋ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 sshjococ.1 ⊢ 𝐴 ⊆ ℋ
2 sshjococ.2 ⊢ 𝐵 ⊆ ℋ
3 ococss ⊢ ( 𝐴 ⊆ ℋ → 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
4 1 3 ax-mp ⊢ 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) )
5 ococss ⊢ ( 𝐵 ⊆ ℋ → 𝐵 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) )
6 2 5 ax-mp ⊢ 𝐵 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) )
7 unss12 ⊢ ( ( 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∧ 𝐵 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) → ( 𝐴 ∪ 𝐵 ) ⊆ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∪ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) )
8 4 6 7 mp2an ⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∪ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) )
9 1 2 unssi ⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ℋ
10 occl ⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) ∈ Cℋ )
11 1 10 ax-mp ⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
12 11 choccli ⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∈ Cℋ
13 12 chssii ⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ⊆ ℋ
14 occl ⊢ ( 𝐵 ⊆ ℋ → ( ⊥ ‘ 𝐵 ) ∈ Cℋ )
15 2 14 ax-mp ⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
16 15 choccli ⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ∈ Cℋ
17 16 chssii ⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ⊆ ℋ
18 13 17 unssi ⊢ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∪ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) ⊆ ℋ
19 9 18 occon2i ⊢ ( ( 𝐴 ∪ 𝐵 ) ⊆ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∪ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∪ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) ) ) )
20 8 19 ax-mp ⊢ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∪ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) ) )
21 sshjval ⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐴 ∨ℋ 𝐵 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ) )
22 1 2 21 mp2an ⊢ ( 𝐴 ∨ℋ 𝐵 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) )
23 12 16 chjvali ⊢ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∨ℋ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) = ( ⊥ ‘ ( ⊥ ‘ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∪ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) ) )
24 20 22 23 3sstr4i ⊢ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∨ℋ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) )
25 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
26 ococss ⊢ ( ( 𝐴 ∪ 𝐵 ) ⊆ ℋ → ( 𝐴 ∪ 𝐵 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ) )
27 9 26 ax-mp ⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) )
28 25 27 sstri ⊢ 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) )
29 28 22 sseqtrri ⊢ 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 )
30 sshjcl ⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ )
31 1 2 30 mp2an ⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ
32 31 chssii ⊢ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ℋ
33 1 32 occon2i ⊢ ( 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
34 29 33 ax-mp ⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) )
35 ssun2 ⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
36 35 27 sstri ⊢ 𝐵 ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) )
37 36 22 sseqtrri ⊢ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 )
38 2 32 occon2i ⊢ ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
39 37 38 ax-mp ⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) )
40 31 choccli ⊢ ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) ∈ Cℋ
41 40 choccli ⊢ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∈ Cℋ
42 12 16 41 chlubii ⊢ ( ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∨ℋ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
43 34 39 42 mp2an ⊢ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∨ℋ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) )
44 31 ococi ⊢ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) ) = ( 𝐴 ∨ℋ 𝐵 )
45 43 44 sseqtri ⊢ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∨ℋ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 )
46 24 45 eqssi ⊢ ( 𝐴 ∨ℋ 𝐵 ) = ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∨ℋ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) )