Step |
Hyp |
Ref |
Expression |
1 |
|
shel |
⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ ℋ ) |
2 |
|
elspansn |
⊢ ( 𝐵 ∈ ℋ → ( 𝑥 ∈ ( span ‘ { 𝐵 } ) ↔ ∃ 𝑦 ∈ ℂ 𝑥 = ( 𝑦 ·ℎ 𝐵 ) ) ) |
3 |
1 2
|
syl |
⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴 ) → ( 𝑥 ∈ ( span ‘ { 𝐵 } ) ↔ ∃ 𝑦 ∈ ℂ 𝑥 = ( 𝑦 ·ℎ 𝐵 ) ) ) |
4 |
|
shmulcl |
⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝑦 ∈ ℂ ∧ 𝐵 ∈ 𝐴 ) → ( 𝑦 ·ℎ 𝐵 ) ∈ 𝐴 ) |
5 |
|
eleq1a |
⊢ ( ( 𝑦 ·ℎ 𝐵 ) ∈ 𝐴 → ( 𝑥 = ( 𝑦 ·ℎ 𝐵 ) → 𝑥 ∈ 𝐴 ) ) |
6 |
4 5
|
syl |
⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝑦 ∈ ℂ ∧ 𝐵 ∈ 𝐴 ) → ( 𝑥 = ( 𝑦 ·ℎ 𝐵 ) → 𝑥 ∈ 𝐴 ) ) |
7 |
6
|
3exp |
⊢ ( 𝐴 ∈ Sℋ → ( 𝑦 ∈ ℂ → ( 𝐵 ∈ 𝐴 → ( 𝑥 = ( 𝑦 ·ℎ 𝐵 ) → 𝑥 ∈ 𝐴 ) ) ) ) |
8 |
7
|
com23 |
⊢ ( 𝐴 ∈ Sℋ → ( 𝐵 ∈ 𝐴 → ( 𝑦 ∈ ℂ → ( 𝑥 = ( 𝑦 ·ℎ 𝐵 ) → 𝑥 ∈ 𝐴 ) ) ) ) |
9 |
8
|
imp |
⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴 ) → ( 𝑦 ∈ ℂ → ( 𝑥 = ( 𝑦 ·ℎ 𝐵 ) → 𝑥 ∈ 𝐴 ) ) ) |
10 |
9
|
rexlimdv |
⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ ℂ 𝑥 = ( 𝑦 ·ℎ 𝐵 ) → 𝑥 ∈ 𝐴 ) ) |
11 |
3 10
|
sylbid |
⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴 ) → ( 𝑥 ∈ ( span ‘ { 𝐵 } ) → 𝑥 ∈ 𝐴 ) ) |
12 |
11
|
ssrdv |
⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴 ) → ( span ‘ { 𝐵 } ) ⊆ 𝐴 ) |