This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ocv1

Description: The orthocomplement of the base set. (Contributed by Mario Carneiro, 23-Oct-2015)

Ref Expression
Hypotheses ocvz.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
ocvz.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
ocvz.z ⊢ 0 = ( 0g ‘ 𝑊 )
Assertion ocv1 ( 𝑊 ∈ PreHil → ( ⊥ ‘ 𝑉 ) = { 0 } )

Proof

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 } )