Metamath Proof Explorer
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 |
⊢ ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ) |