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

Metamath Proof Explorer

Theorem shseli

Description: Membership in subspace sum. (Contributed by NM, 4-May-2000) (New usage is discouraged.)

Ref Expression
Hypotheses shscl.1 ⊢ 𝐴 ∈ Sℋ
shscl.2 ⊢ 𝐵 ∈ Sℋ
Assertion shseli ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) )

Proof

Step Hyp Ref Expression
1 shscl.1 ⊢ 𝐴 ∈ Sℋ
2 shscl.2 ⊢ 𝐵 ∈ Sℋ
3 shsel ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ) )
4 1 2 3 mp2an ⊢ ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) )