This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem shsel1

Description: A subspace sum contains a member of one of its subspaces. (Contributed by NM, 15-Dec-2004) (New usage is discouraged.)

Ref Expression
Assertion shsel1 ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐶 ∈ 𝐴 → 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 shel ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐶 ∈ 𝐴 ) → 𝐶 ∈ ℋ )
2 ax-hvaddid ⊢ ( 𝐶 ∈ ℋ → ( 𝐶 +ℎ 0ℎ ) = 𝐶 )
3 1 2 syl ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐶 ∈ 𝐴 ) → ( 𝐶 +ℎ 0ℎ ) = 𝐶 )
4 3 adantlr ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ 𝐶 ∈ 𝐴 ) → ( 𝐶 +ℎ 0ℎ ) = 𝐶 )
5 sh0 ⊢ ( 𝐵 ∈ Sℋ → 0ℎ ∈ 𝐵 )
6 5 adantl ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → 0ℎ ∈ 𝐵 )
7 shsva ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( ( 𝐶 ∈ 𝐴 ∧ 0ℎ ∈ 𝐵 ) → ( 𝐶 +ℎ 0ℎ ) ∈ ( 𝐴 +ℋ 𝐵 ) ) )
8 6 7 mpan2d ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐶 ∈ 𝐴 → ( 𝐶 +ℎ 0ℎ ) ∈ ( 𝐴 +ℋ 𝐵 ) ) )
9 8 imp ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ 𝐶 ∈ 𝐴 ) → ( 𝐶 +ℎ 0ℎ ) ∈ ( 𝐴 +ℋ 𝐵 ) )
10 4 9 eqeltrrd ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ 𝐶 ∈ 𝐴 ) → 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) )
11 10 ex ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐶 ∈ 𝐴 → 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ) )