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

Metamath Proof Explorer

Theorem shjshsi

Description: Hilbert lattice join equals the double orthocomplement of subspace sum. (Contributed by NM, 27-Nov-2004) (New usage is discouraged.)

Ref Expression
Hypotheses shjshs.1 
|- A e. SH
shjshs.2 
|- B e. SH
Assertion shjshsi 
|- ( A vH B ) = ( _|_ ` ( _|_ ` ( A +H B ) ) )

Proof

Step Hyp Ref Expression
1 shjshs.1 
 |-  A e. SH
2 shjshs.2 
 |-  B e. SH
3 shjval 
 |-  ( ( A e. SH /\ B e. SH ) -> ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) )
4 1 2 3 mp2an 
 |-  ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) )
5 1 2 shunssi 
 |-  ( A u. B ) C_ ( A +H B )
6 1 shssii 
 |-  A C_ ~H
7 2 shssii 
 |-  B C_ ~H
8 6 7 unssi 
 |-  ( A u. B ) C_ ~H
9 1 2 shscli 
 |-  ( A +H B ) e. SH
10 9 shssii 
 |-  ( A +H B ) C_ ~H
11 8 10 occon2i 
 |-  ( ( A u. B ) C_ ( A +H B ) -> ( _|_ ` ( _|_ ` ( A u. B ) ) ) C_ ( _|_ ` ( _|_ ` ( A +H B ) ) ) )
12 5 11 ax-mp 
 |-  ( _|_ ` ( _|_ ` ( A u. B ) ) ) C_ ( _|_ ` ( _|_ ` ( A +H B ) ) )
13 4 12 eqsstri 
 |-  ( A vH B ) C_ ( _|_ ` ( _|_ ` ( A +H B ) ) )
14 1 2 shsleji 
 |-  ( A +H B ) C_ ( A vH B )
15 1 2 shjcli 
 |-  ( A vH B ) e. CH
16 15 chssii 
 |-  ( A vH B ) C_ ~H
17 occon 
 |-  ( ( ( A +H B ) C_ ~H /\ ( A vH B ) C_ ~H ) -> ( ( A +H B ) C_ ( A vH B ) -> ( _|_ ` ( A vH B ) ) C_ ( _|_ ` ( A +H B ) ) ) )
18 10 16 17 mp2an 
 |-  ( ( A +H B ) C_ ( A vH B ) -> ( _|_ ` ( A vH B ) ) C_ ( _|_ ` ( A +H B ) ) )
19 14 18 ax-mp 
 |-  ( _|_ ` ( A vH B ) ) C_ ( _|_ ` ( A +H B ) )
20 occl 
 |-  ( ( A +H B ) C_ ~H -> ( _|_ ` ( A +H B ) ) e. CH )
21 10 20 ax-mp 
 |-  ( _|_ ` ( A +H B ) ) e. CH
22 15 21 chsscon1i 
 |-  ( ( _|_ ` ( A vH B ) ) C_ ( _|_ ` ( A +H B ) ) <-> ( _|_ ` ( _|_ ` ( A +H B ) ) ) C_ ( A vH B ) )
23 19 22 mpbi 
 |-  ( _|_ ` ( _|_ ` ( A +H B ) ) ) C_ ( A vH B )
24 13 23 eqssi 
 |-  ( A vH B ) = ( _|_ ` ( _|_ ` ( A +H B ) ) )