Metamath Proof Explorer

Theorem shlej1

Description: Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 22-Jun-2004) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> A C_ B )
2 unss1 
 |-  ( A C_ B -> ( A u. C ) C_ ( B u. C ) )
3 simpl1 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> A e. SH )
4 shss 
 |-  ( A e. SH -> A C_ ~H )
5 3 4 syl 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> A C_ ~H )
6 simpl3 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> C e. SH )
7 shss 
 |-  ( C e. SH -> C C_ ~H )
8 6 7 syl 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> C C_ ~H )
9 5 8 unssd 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> ( A u. C ) C_ ~H )
10 simpl2 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> B e. SH )
11 shss 
 |-  ( B e. SH -> B C_ ~H )
12 10 11 syl 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> B C_ ~H )
13 12 8 unssd 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> ( B u. C ) C_ ~H )
14 occon2 
 |-  ( ( ( A u. C ) C_ ~H /\ ( B u. C ) C_ ~H ) -> ( ( A u. C ) C_ ( B u. C ) -> ( _|_ ` ( _|_ ` ( A u. C ) ) ) C_ ( _|_ ` ( _|_ ` ( B u. C ) ) ) ) )
15 9 13 14 syl2anc 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> ( ( A u. C ) C_ ( B u. C ) -> ( _|_ ` ( _|_ ` ( A u. C ) ) ) C_ ( _|_ ` ( _|_ ` ( B u. C ) ) ) ) )
16 2 15 syl5 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> ( A C_ B -> ( _|_ ` ( _|_ ` ( A u. C ) ) ) C_ ( _|_ ` ( _|_ ` ( B u. C ) ) ) ) )
17 1 16 mpd 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> ( _|_ ` ( _|_ ` ( A u. C ) ) ) C_ ( _|_ ` ( _|_ ` ( B u. C ) ) ) )
18 shjval 
 |-  ( ( A e. SH /\ C e. SH ) -> ( A vH C ) = ( _|_ ` ( _|_ ` ( A u. C ) ) ) )
19 3 6 18 syl2anc 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> ( A vH C ) = ( _|_ ` ( _|_ ` ( A u. C ) ) ) )
20 shjval 
 |-  ( ( B e. SH /\ C e. SH ) -> ( B vH C ) = ( _|_ ` ( _|_ ` ( B u. C ) ) ) )
21 10 6 20 syl2anc 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> ( B vH C ) = ( _|_ ` ( _|_ ` ( B u. C ) ) ) )
22 17 19 21 3sstr4d 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> ( A vH C ) C_ ( B vH C ) )