Description: The double orthocomplement (closure) of an orthonormal basis is the whole space. (Contributed by Mario Carneiro, 23-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | obs2ocv.o | ⊢ ⊥ = ( ocv ‘ 𝑊 ) | |
obs2ocv.v | ⊢ 𝑉 = ( Base ‘ 𝑊 ) | ||
Assertion | obs2ocv | ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) = 𝑉 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | obs2ocv.o | ⊢ ⊥ = ( ocv ‘ 𝑊 ) | |
2 | obs2ocv.v | ⊢ 𝑉 = ( Base ‘ 𝑊 ) | |
3 | eqid | ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 ) | |
4 | 3 1 | obsocv | ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → ( ⊥ ‘ 𝐵 ) = { ( 0g ‘ 𝑊 ) } ) |
5 | 4 | fveq2d | ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) = ( ⊥ ‘ { ( 0g ‘ 𝑊 ) } ) ) |
6 | obsrcl | ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → 𝑊 ∈ PreHil ) | |
7 | 2 1 3 | ocvz | ⊢ ( 𝑊 ∈ PreHil → ( ⊥ ‘ { ( 0g ‘ 𝑊 ) } ) = 𝑉 ) |
8 | 6 7 | syl | ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → ( ⊥ ‘ { ( 0g ‘ 𝑊 ) } ) = 𝑉 ) |
9 | 5 8 | eqtrd | ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) = 𝑉 ) |