Theorem shunssi

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

	Ref	Expression
Hypotheses	shincl.1	⊢ 𝐴 ∈ Sℋ
	shincl.2	⊢ 𝐵 ∈ Sℋ
Assertion	shunssi	⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		shincl.1	⊢ 𝐴 ∈ Sℋ
2		shincl.2	⊢ 𝐵 ∈ Sℋ
3	1	sheli	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℋ )
4		ax-hvaddid	⊢ ( 𝑥 ∈ ℋ → ( 𝑥 +ℎ 0ℎ ) = 𝑥 )
5	4	eqcomd	⊢ ( 𝑥 ∈ ℋ → 𝑥 = ( 𝑥 +ℎ 0ℎ ) )
6	3 5	syl	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 = ( 𝑥 +ℎ 0ℎ ) )
7		sh0	⊢ ( 𝐵 ∈ Sℋ → 0ℎ ∈ 𝐵 )
8	2 7	ax-mp	⊢ 0ℎ ∈ 𝐵
9		rspceov	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 0ℎ ∈ 𝐵 ∧ 𝑥 = ( 𝑥 +ℎ 0ℎ ) ) → ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 +ℎ 𝑧 ) )
10	8 9	mp3an2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 = ( 𝑥 +ℎ 0ℎ ) ) → ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 +ℎ 𝑧 ) )
11	6 10	mpdan	⊢ ( 𝑥 ∈ 𝐴 → ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 +ℎ 𝑧 ) )
12	2	sheli	⊢ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ℋ )
13		hvaddid2	⊢ ( 𝑥 ∈ ℋ → ( 0ℎ +ℎ 𝑥 ) = 𝑥 )
14	13	eqcomd	⊢ ( 𝑥 ∈ ℋ → 𝑥 = ( 0ℎ +ℎ 𝑥 ) )
15	12 14	syl	⊢ ( 𝑥 ∈ 𝐵 → 𝑥 = ( 0ℎ +ℎ 𝑥 ) )
16		sh0	⊢ ( 𝐴 ∈ Sℋ → 0ℎ ∈ 𝐴 )
17	1 16	ax-mp	⊢ 0ℎ ∈ 𝐴
18		rspceov	⊢ ( ( 0ℎ ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 = ( 0ℎ +ℎ 𝑥 ) ) → ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 +ℎ 𝑧 ) )
19	17 18	mp3an1	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = ( 0ℎ +ℎ 𝑥 ) ) → ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 +ℎ 𝑧 ) )
20	15 19	mpdan	⊢ ( 𝑥 ∈ 𝐵 → ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 +ℎ 𝑧 ) )
21	11 20	jaoi	⊢ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 +ℎ 𝑧 ) )
22		elun	⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
23	1 2	shseli	⊢ ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 +ℎ 𝑧 ) )
24	21 22 23	3imtr4i	⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) → 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) )
25	24	ssriv	⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 )