Metamath Proof Explorer


Theorem shlub

Description: Hilbert lattice join is the least upper bound (among Hilbert lattice elements) of two subspaces. (Contributed by NM, 15-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion shlub
|- ( ( A e. SH /\ B e. SH /\ C e. CH ) -> ( ( A C_ C /\ B C_ C ) <-> ( A vH B ) C_ C ) )

Proof

Step Hyp Ref Expression
1 unss
 |-  ( ( A C_ C /\ B C_ C ) <-> ( A u. B ) C_ C )
2 simp1
 |-  ( ( A e. SH /\ B e. SH /\ C e. CH ) -> A e. SH )
3 shss
 |-  ( A e. SH -> A C_ ~H )
4 2 3 syl
 |-  ( ( A e. SH /\ B e. SH /\ C e. CH ) -> A C_ ~H )
5 simp2
 |-  ( ( A e. SH /\ B e. SH /\ C e. CH ) -> B e. SH )
6 shss
 |-  ( B e. SH -> B C_ ~H )
7 5 6 syl
 |-  ( ( A e. SH /\ B e. SH /\ C e. CH ) -> B C_ ~H )
8 4 7 unssd
 |-  ( ( A e. SH /\ B e. SH /\ C e. CH ) -> ( A u. B ) C_ ~H )
9 chss
 |-  ( C e. CH -> C C_ ~H )
10 9 3ad2ant3
 |-  ( ( A e. SH /\ B e. SH /\ C e. CH ) -> C C_ ~H )
11 occon2
 |-  ( ( ( A u. B ) C_ ~H /\ C C_ ~H ) -> ( ( A u. B ) C_ C -> ( _|_ ` ( _|_ ` ( A u. B ) ) ) C_ ( _|_ ` ( _|_ ` C ) ) ) )
12 8 10 11 syl2anc
 |-  ( ( A e. SH /\ B e. SH /\ C e. CH ) -> ( ( A u. B ) C_ C -> ( _|_ ` ( _|_ ` ( A u. B ) ) ) C_ ( _|_ ` ( _|_ ` C ) ) ) )
13 1 12 syl5bi
 |-  ( ( A e. SH /\ B e. SH /\ C e. CH ) -> ( ( A C_ C /\ B C_ C ) -> ( _|_ ` ( _|_ ` ( A u. B ) ) ) C_ ( _|_ ` ( _|_ ` C ) ) ) )
14 shjval
 |-  ( ( A e. SH /\ B e. SH ) -> ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) )
15 2 5 14 syl2anc
 |-  ( ( A e. SH /\ B e. SH /\ C e. CH ) -> ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) )
16 ococ
 |-  ( C e. CH -> ( _|_ ` ( _|_ ` C ) ) = C )
17 16 3ad2ant3
 |-  ( ( A e. SH /\ B e. SH /\ C e. CH ) -> ( _|_ ` ( _|_ ` C ) ) = C )
18 17 eqcomd
 |-  ( ( A e. SH /\ B e. SH /\ C e. CH ) -> C = ( _|_ ` ( _|_ ` C ) ) )
19 15 18 sseq12d
 |-  ( ( A e. SH /\ B e. SH /\ C e. CH ) -> ( ( A vH B ) C_ C <-> ( _|_ ` ( _|_ ` ( A u. B ) ) ) C_ ( _|_ ` ( _|_ ` C ) ) ) )
20 13 19 sylibrd
 |-  ( ( A e. SH /\ B e. SH /\ C e. CH ) -> ( ( A C_ C /\ B C_ C ) -> ( A vH B ) C_ C ) )
21 shub1
 |-  ( ( A e. SH /\ B e. SH ) -> A C_ ( A vH B ) )
22 2 5 21 syl2anc
 |-  ( ( A e. SH /\ B e. SH /\ C e. CH ) -> A C_ ( A vH B ) )
23 sstr
 |-  ( ( A C_ ( A vH B ) /\ ( A vH B ) C_ C ) -> A C_ C )
24 22 23 sylan
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. CH ) /\ ( A vH B ) C_ C ) -> A C_ C )
25 shub2
 |-  ( ( B e. SH /\ A e. SH ) -> B C_ ( A vH B ) )
26 5 2 25 syl2anc
 |-  ( ( A e. SH /\ B e. SH /\ C e. CH ) -> B C_ ( A vH B ) )
27 sstr
 |-  ( ( B C_ ( A vH B ) /\ ( A vH B ) C_ C ) -> B C_ C )
28 26 27 sylan
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. CH ) /\ ( A vH B ) C_ C ) -> B C_ C )
29 24 28 jca
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. CH ) /\ ( A vH B ) C_ C ) -> ( A C_ C /\ B C_ C ) )
30 29 ex
 |-  ( ( A e. SH /\ B e. SH /\ C e. CH ) -> ( ( A vH B ) C_ C -> ( A C_ C /\ B C_ C ) ) )
31 20 30 impbid
 |-  ( ( A e. SH /\ B e. SH /\ C e. CH ) -> ( ( A C_ C /\ B C_ C ) <-> ( A vH B ) C_ C ) )