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

Metamath Proof Explorer

Theorem ocel

Description: Membership in orthogonal complement of H subset. (Contributed by NM, 7-Aug-2000) (New usage is discouraged.)

Ref Expression
Assertion ocel ( 𝐻 ⊆ ℋ → ( 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ↔ ( 𝐴 ∈ ℋ ∧ ∀ 𝑥 ∈ 𝐻 ( 𝐴 ·ih 𝑥 ) = 0 ) ) )

Proof

Step Hyp Ref Expression
1 ocval ⊢ ( 𝐻 ⊆ ℋ → ( ⊥ ‘ 𝐻 ) = { 𝑦 ∈ ℋ ∣ ∀ 𝑥 ∈ 𝐻 ( 𝑦 ·ih 𝑥 ) = 0 } )
2 1 eleq2d ⊢ ( 𝐻 ⊆ ℋ → ( 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ↔ 𝐴 ∈ { 𝑦 ∈ ℋ ∣ ∀ 𝑥 ∈ 𝐻 ( 𝑦 ·ih 𝑥 ) = 0 } ) )
3 oveq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ·ih 𝑥 ) = ( 𝐴 ·ih 𝑥 ) )
4 3 eqeq1d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ·ih 𝑥 ) = 0 ↔ ( 𝐴 ·ih 𝑥 ) = 0 ) )
5 4 ralbidv ⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ∈ 𝐻 ( 𝑦 ·ih 𝑥 ) = 0 ↔ ∀ 𝑥 ∈ 𝐻 ( 𝐴 ·ih 𝑥 ) = 0 ) )
6 5 elrab ⊢ ( 𝐴 ∈ { 𝑦 ∈ ℋ ∣ ∀ 𝑥 ∈ 𝐻 ( 𝑦 ·ih 𝑥 ) = 0 } ↔ ( 𝐴 ∈ ℋ ∧ ∀ 𝑥 ∈ 𝐻 ( 𝐴 ·ih 𝑥 ) = 0 ) )
7 2 6 bitrdi ⊢ ( 𝐻 ⊆ ℋ → ( 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ↔ ( 𝐴 ∈ ℋ ∧ ∀ 𝑥 ∈ 𝐻 ( 𝐴 ·ih 𝑥 ) = 0 ) ) )