Step |
Hyp |
Ref |
Expression |
1 |
|
ocvz.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
2 |
|
ocvz.o |
⊢ ⊥ = ( ocv ‘ 𝑊 ) |
3 |
|
ocvz.z |
⊢ 0 = ( 0g ‘ 𝑊 ) |
4 |
1 2
|
ocvss |
⊢ ( ⊥ ‘ 𝑉 ) ⊆ 𝑉 |
5 |
|
sseqin2 |
⊢ ( ( ⊥ ‘ 𝑉 ) ⊆ 𝑉 ↔ ( 𝑉 ∩ ( ⊥ ‘ 𝑉 ) ) = ( ⊥ ‘ 𝑉 ) ) |
6 |
4 5
|
mpbi |
⊢ ( 𝑉 ∩ ( ⊥ ‘ 𝑉 ) ) = ( ⊥ ‘ 𝑉 ) |
7 |
|
phllmod |
⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod ) |
8 |
|
eqid |
⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 ) |
9 |
1 8
|
lss1 |
⊢ ( 𝑊 ∈ LMod → 𝑉 ∈ ( LSubSp ‘ 𝑊 ) ) |
10 |
7 9
|
syl |
⊢ ( 𝑊 ∈ PreHil → 𝑉 ∈ ( LSubSp ‘ 𝑊 ) ) |
11 |
2 8 3
|
ocvin |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑉 ∈ ( LSubSp ‘ 𝑊 ) ) → ( 𝑉 ∩ ( ⊥ ‘ 𝑉 ) ) = { 0 } ) |
12 |
10 11
|
mpdan |
⊢ ( 𝑊 ∈ PreHil → ( 𝑉 ∩ ( ⊥ ‘ 𝑉 ) ) = { 0 } ) |
13 |
6 12
|
eqtr3id |
⊢ ( 𝑊 ∈ PreHil → ( ⊥ ‘ 𝑉 ) = { 0 } ) |