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