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 ⊢ B ∈ ℋ
Assertion h1deoi ⊢ A ∈ ⊥ ⁡ B ↔ A ∈ ℋ ∧ A ⋅ ih B = 0

Proof

Step Hyp Ref Expression
1 h1deot.1 ⊢ B ∈ ℋ
2 snssi ⊢ B ∈ ℋ → B ⊆ ℋ
3 ocel ⊢ B ⊆ ℋ → A ∈ ⊥ ⁡ B ↔ A ∈ ℋ ∧ ∀ x ∈ B A ⋅ ih x = 0
4 1 2 3 mp2b ⊢ A ∈ ⊥ ⁡ B ↔ A ∈ ℋ ∧ ∀ x ∈ B A ⋅ ih x = 0
5 1 elexi ⊢ B ∈ V
6 oveq2 ⊢ x = B → A ⋅ ih x = A ⋅ ih B
7 6 eqeq1d ⊢ x = B → A ⋅ ih x = 0 ↔ A ⋅ ih B = 0
8 5 7 ralsn ⊢ ∀ x ∈ B A ⋅ ih x = 0 ↔ A ⋅ ih B = 0
9 8 anbi2i ⊢ A ∈ ℋ ∧ ∀ x ∈ B A ⋅ ih x = 0 ↔ A ∈ ℋ ∧ A ⋅ ih B = 0
10 4 9 bitri ⊢ A ∈ ⊥ ⁡ B ↔ A ∈ ℋ ∧ A ⋅ ih B = 0