Step |
Hyp |
Ref |
Expression |
1 |
|
csslss.c |
⊢ 𝐶 = ( ClSubSp ‘ 𝑊 ) |
2 |
|
csslss.l |
⊢ 𝐿 = ( LSubSp ‘ 𝑊 ) |
3 |
|
eqid |
⊢ ( ocv ‘ 𝑊 ) = ( ocv ‘ 𝑊 ) |
4 |
3 1
|
cssi |
⊢ ( 𝑆 ∈ 𝐶 → 𝑆 = ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ) ) |
5 |
4
|
adantl |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐶 ) → 𝑆 = ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ) ) |
6 |
|
eqid |
⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) |
7 |
6 3
|
ocvss |
⊢ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ⊆ ( Base ‘ 𝑊 ) |
8 |
7
|
a1i |
⊢ ( 𝑆 ∈ 𝐶 → ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ⊆ ( Base ‘ 𝑊 ) ) |
9 |
6 3 2
|
ocvlss |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ⊆ ( Base ‘ 𝑊 ) ) → ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ) ∈ 𝐿 ) |
10 |
8 9
|
sylan2 |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐶 ) → ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ) ∈ 𝐿 ) |
11 |
5 10
|
eqeltrd |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐶 ) → 𝑆 ∈ 𝐿 ) |