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
|- ( A C_ ~H -> ( A vH ( _|_ ` A ) ) = ~H )

Proof

Step Hyp Ref Expression
1 ocss
 |-  ( A C_ ~H -> ( _|_ ` A ) C_ ~H )
2 sshjval
 |-  ( ( A C_ ~H /\ ( _|_ ` A ) C_ ~H ) -> ( A vH ( _|_ ` A ) ) = ( _|_ ` ( _|_ ` ( A u. ( _|_ ` A ) ) ) ) )
3 1 2 mpdan
 |-  ( A C_ ~H -> ( A vH ( _|_ ` A ) ) = ( _|_ ` ( _|_ ` ( A u. ( _|_ ` A ) ) ) ) )
4 ssun1
 |-  A C_ ( A u. ( _|_ ` A ) )
5 1 ancli
 |-  ( A C_ ~H -> ( A C_ ~H /\ ( _|_ ` A ) C_ ~H ) )
6 unss
 |-  ( ( A C_ ~H /\ ( _|_ ` A ) C_ ~H ) <-> ( A u. ( _|_ ` A ) ) C_ ~H )
7 5 6 sylib
 |-  ( A C_ ~H -> ( A u. ( _|_ ` A ) ) C_ ~H )
8 occon
 |-  ( ( A C_ ~H /\ ( A u. ( _|_ ` A ) ) C_ ~H ) -> ( A C_ ( A u. ( _|_ ` A ) ) -> ( _|_ ` ( A u. ( _|_ ` A ) ) ) C_ ( _|_ ` A ) ) )
9 7 8 mpdan
 |-  ( A C_ ~H -> ( A C_ ( A u. ( _|_ ` A ) ) -> ( _|_ ` ( A u. ( _|_ ` A ) ) ) C_ ( _|_ ` A ) ) )
10 4 9 mpi
 |-  ( A C_ ~H -> ( _|_ ` ( A u. ( _|_ ` A ) ) ) C_ ( _|_ ` A ) )
11 ssun2
 |-  ( _|_ ` A ) C_ ( A u. ( _|_ ` A ) )
12 occon
 |-  ( ( ( _|_ ` A ) C_ ~H /\ ( A u. ( _|_ ` A ) ) C_ ~H ) -> ( ( _|_ ` A ) C_ ( A u. ( _|_ ` A ) ) -> ( _|_ ` ( A u. ( _|_ ` A ) ) ) C_ ( _|_ ` ( _|_ ` A ) ) ) )
13 1 7 12 syl2anc
 |-  ( A C_ ~H -> ( ( _|_ ` A ) C_ ( A u. ( _|_ ` A ) ) -> ( _|_ ` ( A u. ( _|_ ` A ) ) ) C_ ( _|_ ` ( _|_ ` A ) ) ) )
14 11 13 mpi
 |-  ( A C_ ~H -> ( _|_ ` ( A u. ( _|_ ` A ) ) ) C_ ( _|_ ` ( _|_ ` A ) ) )
15 10 14 ssind
 |-  ( A C_ ~H -> ( _|_ ` ( A u. ( _|_ ` A ) ) ) C_ ( ( _|_ ` A ) i^i ( _|_ ` ( _|_ ` A ) ) ) )
16 ocsh
 |-  ( A C_ ~H -> ( _|_ ` A ) e. SH )
17 ocin
 |-  ( ( _|_ ` A ) e. SH -> ( ( _|_ ` A ) i^i ( _|_ ` ( _|_ ` A ) ) ) = 0H )
18 16 17 syl
 |-  ( A C_ ~H -> ( ( _|_ ` A ) i^i ( _|_ ` ( _|_ ` A ) ) ) = 0H )
19 15 18 sseqtrd
 |-  ( A C_ ~H -> ( _|_ ` ( A u. ( _|_ ` A ) ) ) C_ 0H )
20 ocsh
 |-  ( ( A u. ( _|_ ` A ) ) C_ ~H -> ( _|_ ` ( A u. ( _|_ ` A ) ) ) e. SH )
21 sh0le
 |-  ( ( _|_ ` ( A u. ( _|_ ` A ) ) ) e. SH -> 0H C_ ( _|_ ` ( A u. ( _|_ ` A ) ) ) )
22 7 20 21 3syl
 |-  ( A C_ ~H -> 0H C_ ( _|_ ` ( A u. ( _|_ ` A ) ) ) )
23 19 22 eqssd
 |-  ( A C_ ~H -> ( _|_ ` ( A u. ( _|_ ` A ) ) ) = 0H )
24 23 fveq2d
 |-  ( A C_ ~H -> ( _|_ ` ( _|_ ` ( A u. ( _|_ ` A ) ) ) ) = ( _|_ ` 0H ) )
25 choc0
 |-  ( _|_ ` 0H ) = ~H
26 24 25 eqtrdi
 |-  ( A C_ ~H -> ( _|_ ` ( _|_ ` ( A u. ( _|_ ` A ) ) ) ) = ~H )
27 3 26 eqtrd
 |-  ( A C_ ~H -> ( A vH ( _|_ ` A ) ) = ~H )