Description: The orthocomplement of a subset is a subset of the base. (Contributed by Mario Carneiro, 13-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ocvss.v | ⊢ 𝑉 = ( Base ‘ 𝑊 ) | |
ocvss.o | ⊢ ⊥ = ( ocv ‘ 𝑊 ) | ||
Assertion | ocvss | ⊢ ( ⊥ ‘ 𝑆 ) ⊆ 𝑉 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ocvss.v | ⊢ 𝑉 = ( Base ‘ 𝑊 ) | |
2 | ocvss.o | ⊢ ⊥ = ( ocv ‘ 𝑊 ) | |
3 | eqid | ⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 ) | |
4 | eqid | ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 ) | |
5 | eqid | ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) | |
6 | 1 3 4 5 2 | elocv | ⊢ ( 𝑥 ∈ ( ⊥ ‘ 𝑆 ) ↔ ( 𝑆 ⊆ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) |
7 | 6 | simp2bi | ⊢ ( 𝑥 ∈ ( ⊥ ‘ 𝑆 ) → 𝑥 ∈ 𝑉 ) |
8 | 7 | ssriv | ⊢ ( ⊥ ‘ 𝑆 ) ⊆ 𝑉 |