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 ⊢ H ⊆ ℋ → A ∈ ⊥ ⁡ H ↔ A ∈ ℋ ∧ ∀ x ∈ H A ⋅ ih x = 0

Proof

Step Hyp Ref Expression
1 ocval ⊢ H ⊆ ℋ → ⊥ ⁡ H = y ∈ ℋ | ∀ x ∈ H y ⋅ ih x = 0
2 1 eleq2d ⊢ H ⊆ ℋ → A ∈ ⊥ ⁡ H ↔ A ∈ y ∈ ℋ | ∀ x ∈ H y ⋅ ih x = 0
3 oveq1 ⊢ y = A → y ⋅ ih x = A ⋅ ih x
4 3 eqeq1d ⊢ y = A → y ⋅ ih x = 0 ↔ A ⋅ ih x = 0
5 4 ralbidv ⊢ y = A → ∀ x ∈ H y ⋅ ih x = 0 ↔ ∀ x ∈ H A ⋅ ih x = 0
6 5 elrab ⊢ A ∈ y ∈ ℋ | ∀ x ∈ H y ⋅ ih x = 0 ↔ A ∈ ℋ ∧ ∀ x ∈ H A ⋅ ih x = 0
7 2 6 bitrdi ⊢ H ⊆ ℋ → A ∈ ⊥ ⁡ H ↔ A ∈ ℋ ∧ ∀ x ∈ H A ⋅ ih x = 0