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 )