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

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 ⊢ ( 𝐴 ⊆ ℋ → ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐴 ) ) = ℋ )