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ℋ ) → ( 𝐶 ∈ 𝐴 → 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ) )