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