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

Metamath Proof Explorer

Theorem h1deoi

Description: Membership in orthocomplement of 1-dimensional subspace. (Contributed by NM, 7-Jul-2001) (New usage is discouraged.)

Ref Expression
Hypothesis h1deot.1 ⊢ 𝐵 ∈ ℋ
Assertion h1deoi ( 𝐴 ∈ ( ⊥ ‘ { 𝐵 } ) ↔ ( 𝐴 ∈ ℋ ∧ ( 𝐴 ·ih 𝐵 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 h1deot.1 ⊢ 𝐵 ∈ ℋ
2 snssi ⊢ ( 𝐵 ∈ ℋ → { 𝐵 } ⊆ ℋ )
3 ocel ⊢ ( { 𝐵 } ⊆ ℋ → ( 𝐴 ∈ ( ⊥ ‘ { 𝐵 } ) ↔ ( 𝐴 ∈ ℋ ∧ ∀ 𝑥 ∈ { 𝐵 } ( 𝐴 ·ih 𝑥 ) = 0 ) ) )
4 1 2 3 mp2b ⊢ ( 𝐴 ∈ ( ⊥ ‘ { 𝐵 } ) ↔ ( 𝐴 ∈ ℋ ∧ ∀ 𝑥 ∈ { 𝐵 } ( 𝐴 ·ih 𝑥 ) = 0 ) )
5 1 elexi ⊢ 𝐵 ∈ V
6 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐴 ·ih 𝑥 ) = ( 𝐴 ·ih 𝐵 ) )
7 6 eqeq1d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ·ih 𝑥 ) = 0 ↔ ( 𝐴 ·ih 𝐵 ) = 0 ) )
8 5 7 ralsn ⊢ ( ∀ 𝑥 ∈ { 𝐵 } ( 𝐴 ·ih 𝑥 ) = 0 ↔ ( 𝐴 ·ih 𝐵 ) = 0 )
9 8 anbi2i ⊢ ( ( 𝐴 ∈ ℋ ∧ ∀ 𝑥 ∈ { 𝐵 } ( 𝐴 ·ih 𝑥 ) = 0 ) ↔ ( 𝐴 ∈ ℋ ∧ ( 𝐴 ·ih 𝐵 ) = 0 ) )
10 4 9 bitri ⊢ ( 𝐴 ∈ ( ⊥ ‘ { 𝐵 } ) ↔ ( 𝐴 ∈ ℋ ∧ ( 𝐴 ·ih 𝐵 ) = 0 ) )