Metamath Proof Explorer


Theorem ssjo

Description: The lattice join of a subset with its orthocomplement is the whole space. (Contributed by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Assertion ssjo ( 𝐴 ⊆ ℋ → ( 𝐴 ( ⊥ ‘ 𝐴 ) ) = ℋ )

Proof

Step Hyp Ref Expression
1 ocss ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) ⊆ ℋ )
2 sshjval ( ( 𝐴 ⊆ ℋ ∧ ( ⊥ ‘ 𝐴 ) ⊆ ℋ ) → ( 𝐴 ( ⊥ ‘ 𝐴 ) ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) ) ) )
3 1 2 mpdan ( 𝐴 ⊆ ℋ → ( 𝐴 ( ⊥ ‘ 𝐴 ) ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) ) ) )
4 ssun1 𝐴 ⊆ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) )
5 1 ancli ( 𝐴 ⊆ ℋ → ( 𝐴 ⊆ ℋ ∧ ( ⊥ ‘ 𝐴 ) ⊆ ℋ ) )
6 unss ( ( 𝐴 ⊆ ℋ ∧ ( ⊥ ‘ 𝐴 ) ⊆ ℋ ) ↔ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) ⊆ ℋ )
7 5 6 sylib ( 𝐴 ⊆ ℋ → ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) ⊆ ℋ )
8 occon ( ( 𝐴 ⊆ ℋ ∧ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) ⊆ ℋ ) → ( 𝐴 ⊆ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) → ( ⊥ ‘ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) ) ⊆ ( ⊥ ‘ 𝐴 ) ) )
9 7 8 mpdan ( 𝐴 ⊆ ℋ → ( 𝐴 ⊆ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) → ( ⊥ ‘ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) ) ⊆ ( ⊥ ‘ 𝐴 ) ) )
10 4 9 mpi ( 𝐴 ⊆ ℋ → ( ⊥ ‘ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) ) ⊆ ( ⊥ ‘ 𝐴 ) )
11 ssun2 ( ⊥ ‘ 𝐴 ) ⊆ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) )
12 occon ( ( ( ⊥ ‘ 𝐴 ) ⊆ ℋ ∧ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) ⊆ ℋ ) → ( ( ⊥ ‘ 𝐴 ) ⊆ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) → ( ⊥ ‘ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) )
13 1 7 12 syl2anc ( 𝐴 ⊆ ℋ → ( ( ⊥ ‘ 𝐴 ) ⊆ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) → ( ⊥ ‘ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) )
14 11 13 mpi ( 𝐴 ⊆ ℋ → ( ⊥ ‘ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
15 10 14 ssind ( 𝐴 ⊆ ℋ → ( ⊥ ‘ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) ) ⊆ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) )
16 ocsh ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) ∈ S )
17 ocin ( ( ⊥ ‘ 𝐴 ) ∈ S → ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) = 0 )
18 16 17 syl ( 𝐴 ⊆ ℋ → ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) = 0 )
19 15 18 sseqtrd ( 𝐴 ⊆ ℋ → ( ⊥ ‘ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) ) ⊆ 0 )
20 ocsh ( ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) ⊆ ℋ → ( ⊥ ‘ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) ) ∈ S )
21 sh0le ( ( ⊥ ‘ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) ) ∈ S → 0 ⊆ ( ⊥ ‘ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) ) )
22 7 20 21 3syl ( 𝐴 ⊆ ℋ → 0 ⊆ ( ⊥ ‘ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) ) )
23 19 22 eqssd ( 𝐴 ⊆ ℋ → ( ⊥ ‘ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) ) = 0 )
24 23 fveq2d ( 𝐴 ⊆ ℋ → ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) ) ) = ( ⊥ ‘ 0 ) )
25 choc0 ( ⊥ ‘ 0 ) = ℋ
26 24 25 eqtrdi ( 𝐴 ⊆ ℋ → ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ ( ⊥ ‘ 𝐴 ) ) ) ) = ℋ )
27 3 26 eqtrd ( 𝐴 ⊆ ℋ → ( 𝐴 ( ⊥ ‘ 𝐴 ) ) = ℋ )