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 ⊢ 𝐴 ∈ 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 hvaddlid ⊢ ( 𝑥 ∈ ℋ → ( 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 ⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 )