Metamath Proof Explorer


Theorem chseli

Description: Membership in subspace sum. (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses ch0le.1 𝐴C
chjcl.2 𝐵C
Assertion chseli ( 𝐶 ∈ ( 𝐴 + 𝐵 ) ↔ ∃ 𝑥𝐴𝑦𝐵 𝐶 = ( 𝑥 + 𝑦 ) )

Proof

Step Hyp Ref Expression
1 ch0le.1 𝐴C
2 chjcl.2 𝐵C
3 1 chshii 𝐴S
4 2 chshii 𝐵S
5 3 4 shseli ( 𝐶 ∈ ( 𝐴 + 𝐵 ) ↔ ∃ 𝑥𝐴𝑦𝐵 𝐶 = ( 𝑥 + 𝑦 ) )