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