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

Metamath Proof Explorer

Theorem ocvi

Description: Property of a member of the orthocomplement of a subset. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses ocvfval.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
ocvfval.i ⊢ , = ( ·𝑖 ‘ 𝑊 )
ocvfval.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
ocvfval.z ⊢ 0 = ( 0g ‘ 𝐹 )
ocvfval.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
Assertion ocvi ( ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 , 𝐵 ) = 0 )

Proof

Step Hyp Ref Expression
1 ocvfval.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 ocvfval.i ⊢ , = ( ·𝑖 ‘ 𝑊 )
3 ocvfval.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4 ocvfval.z ⊢ 0 = ( 0g ‘ 𝐹 )
5 ocvfval.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
6 1 2 3 4 5 elocv ⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) ↔ ( 𝑆 ⊆ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐴 , 𝑥 ) = 0 ) )
7 6 simp3bi ⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) → ∀ 𝑥 ∈ 𝑆 ( 𝐴 , 𝑥 ) = 0 )
8 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐴 , 𝑥 ) = ( 𝐴 , 𝐵 ) )
9 8 eqeq1d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 , 𝑥 ) = 0 ↔ ( 𝐴 , 𝐵 ) = 0 ) )
10 9 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑆 ( 𝐴 , 𝑥 ) = 0 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 , 𝐵 ) = 0 )
11 7 10 sylan ⊢ ( ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 , 𝐵 ) = 0 )