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\in {\mathbf{S}}_{\mathscr{H}}$$
	shincl.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
Assertion	shunssi	$$⊢A\cup B\subseteq A{+}_{\mathscr{H}}B$$

Proof

Step	Hyp	Ref	Expression
1		shincl.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
2		shincl.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
3	1	sheli	$$⊢x\in A\to x\in \mathscr{H}$$
4		ax-hvaddid	$$⊢x\in \mathscr{H}\to x{+}_{ℎ}{0}_{ℎ}=x$$
5	4	eqcomd	$$⊢x\in \mathscr{H}\to x=x{+}_{ℎ}{0}_{ℎ}$$
6	3 5	syl	$$⊢x\in A\to x=x{+}_{ℎ}{0}_{ℎ}$$
7		sh0	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}\to 0_{ℎ}\in B$$
8	2 7	ax-mp	$$⊢0_{ℎ}\in B$$
9		rspceov	$$⊢\left(x\in A\wedge 0_{ℎ}\in B\wedge x=x{+}_{ℎ}{0}_{ℎ}\right)\to \exists y\in A\exists z\in Bx=y{+}_{ℎ}z$$
10	8 9	mp3an2	$$⊢\left(x\in A\wedge x=x{+}_{ℎ}{0}_{ℎ}\right)\to \exists y\in A\exists z\in Bx=y{+}_{ℎ}z$$
11	6 10	mpdan	$$⊢x\in A\to \exists y\in A\exists z\in Bx=y{+}_{ℎ}z$$
12	2	sheli	$$⊢x\in B\to x\in \mathscr{H}$$
13		hvaddid2	$$⊢x\in \mathscr{H}\to 0_{ℎ}{+}_{ℎ}x=x$$
14	13	eqcomd	$$⊢x\in \mathscr{H}\to x=0_{ℎ}{+}_{ℎ}x$$
15	12 14	syl	$$⊢x\in B\to x=0_{ℎ}{+}_{ℎ}x$$
16		sh0	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}\to 0_{ℎ}\in A$$
17	1 16	ax-mp	$$⊢0_{ℎ}\in A$$
18		rspceov	$$⊢\left(0_{ℎ}\in A\wedge x\in B\wedge x=0_{ℎ}{+}_{ℎ}x\right)\to \exists y\in A\exists z\in Bx=y{+}_{ℎ}z$$
19	17 18	mp3an1	$$⊢\left(x\in B\wedge x=0_{ℎ}{+}_{ℎ}x\right)\to \exists y\in A\exists z\in Bx=y{+}_{ℎ}z$$
20	15 19	mpdan	$$⊢x\in B\to \exists y\in A\exists z\in Bx=y{+}_{ℎ}z$$
21	11 20	jaoi	$$⊢\left(x\in A\vee x\in B\right)\to \exists y\in A\exists z\in Bx=y{+}_{ℎ}z$$
22		elun	$$⊢x\in \left(A\cup B\right)\leftrightarrow \left(x\in A\vee x\in B\right)$$
23	1 2	shseli	$$⊢x\in \left(A{+}_{\mathscr{H}}B\right)\leftrightarrow \exists y\in A\exists z\in Bx=y{+}_{ℎ}z$$
24	21 22 23	3imtr4i	$$⊢x\in \left(A\cup B\right)\to x\in \left(A{+}_{\mathscr{H}}B\right)$$
25	24	ssriv	$$⊢A\cup B\subseteq A{+}_{\mathscr{H}}B$$