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 )