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 ) ) )