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

Metamath Proof Explorer

Theorem shunssi

Description: Union is smaller than subspace sum. (Contributed by NM, 18-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses shincl.1 
|- A e. SH
shincl.2 
|- B e. SH
Assertion shunssi 
|- ( A u. B ) C_ ( A +H B )

Proof

Step Hyp Ref Expression
1 shincl.1 
 |-  A e. SH
2 shincl.2 
 |-  B e. SH
3 1 sheli 
 |-  ( x e. A -> x e. ~H )
4 ax-hvaddid 
 |-  ( x e. ~H -> ( x +h 0h ) = x )
5 4 eqcomd 
 |-  ( x e. ~H -> x = ( x +h 0h ) )
6 3 5 syl 
 |-  ( x e. A -> x = ( x +h 0h ) )
7 sh0 
 |-  ( B e. SH -> 0h e. B )
8 2 7 ax-mp 
 |-  0h e. B
9 rspceov 
 |-  ( ( x e. A /\ 0h e. B /\ x = ( x +h 0h ) ) -> E. y e. A E. z e. B x = ( y +h z ) )
10 8 9 mp3an2 
 |-  ( ( x e. A /\ x = ( x +h 0h ) ) -> E. y e. A E. z e. B x = ( y +h z ) )
11 6 10 mpdan 
 |-  ( x e. A -> E. y e. A E. z e. B x = ( y +h z ) )
12 2 sheli 
 |-  ( x e. B -> x e. ~H )
13 hvaddlid 
 |-  ( x e. ~H -> ( 0h +h x ) = x )
14 13 eqcomd 
 |-  ( x e. ~H -> x = ( 0h +h x ) )
15 12 14 syl 
 |-  ( x e. B -> x = ( 0h +h x ) )
16 sh0 
 |-  ( A e. SH -> 0h e. A )
17 1 16 ax-mp 
 |-  0h e. A
18 rspceov 
 |-  ( ( 0h e. A /\ x e. B /\ x = ( 0h +h x ) ) -> E. y e. A E. z e. B x = ( y +h z ) )
19 17 18 mp3an1 
 |-  ( ( x e. B /\ x = ( 0h +h x ) ) -> E. y e. A E. z e. B x = ( y +h z ) )
20 15 19 mpdan 
 |-  ( x e. B -> E. y e. A E. z e. B x = ( y +h z ) )
21 11 20 jaoi 
 |-  ( ( x e. A \/ x e. B ) -> E. y e. A E. z e. B x = ( y +h z ) )
22 elun 
 |-  ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
23 1 2 shseli 
 |-  ( x e. ( A +H B ) <-> E. y e. A E. z e. B x = ( y +h z ) )
24 21 22 23 3imtr4i 
 |-  ( x e. ( A u. B ) -> x e. ( A +H B ) )
25 24 ssriv 
 |-  ( A u. B ) C_ ( A +H B )