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 ∈ S ℋ
shincl.2 ⊢ B ∈ S ℋ
Assertion shunssi ⊢ A ∪ B ⊆ A + ℋ B

Proof

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