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