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
|- A e. CH
chjcl.2
|- B e. CH
Assertion chseli
|- ( C e. ( A +H B ) <-> E. x e. A E. y e. B C = ( x +h y ) )

Proof

Step Hyp Ref Expression
1 ch0le.1
 |-  A e. CH
2 chjcl.2
 |-  B e. CH
3 1 chshii
 |-  A e. SH
4 2 chshii
 |-  B e. SH
5 3 4 shseli
 |-  ( C e. ( A +H B ) <-> E. x e. A E. y e. B C = ( x +h y ) )