Metamath Proof Explorer

Theorem h1dei

Description: Membership in 1-dimensional subspace. (Contributed by NM, 7-Jul-2001) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Hypothesis h1deot.1 ⊢ B ∈ ℋ
Assertion h1dei ⊢ A ∈ ⊥ ⁡ ⊥ ⁡ B ↔ A ∈ ℋ ∧ ∀ x ∈ ℋ B ⋅ ih x = 0 → A ⋅ ih x = 0

Proof

Step Hyp Ref Expression
1 h1deot.1 ⊢ B ∈ ℋ
2 snssi ⊢ B ∈ ℋ → B ⊆ ℋ
3 occl ⊢ B ⊆ ℋ → ⊥ ⁡ B ∈ C ℋ
4 1 2 3 mp2b ⊢ ⊥ ⁡ B ∈ C ℋ
5 4 chssii ⊢ ⊥ ⁡ B ⊆ ℋ
6 ocel ⊢ ⊥ ⁡ B ⊆ ℋ → A ∈ ⊥ ⁡ ⊥ ⁡ B ↔ A ∈ ℋ ∧ ∀ x ∈ ⊥ ⁡ B A ⋅ ih x = 0
7 5 6 ax-mp ⊢ A ∈ ⊥ ⁡ ⊥ ⁡ B ↔ A ∈ ℋ ∧ ∀ x ∈ ⊥ ⁡ B A ⋅ ih x = 0
8 1 h1deoi ⊢ x ∈ ⊥ ⁡ B ↔ x ∈ ℋ ∧ x ⋅ ih B = 0
9 orthcom ⊢ x ∈ ℋ ∧ B ∈ ℋ → x ⋅ ih B = 0 ↔ B ⋅ ih x = 0
10 1 9 mpan2 ⊢ x ∈ ℋ → x ⋅ ih B = 0 ↔ B ⋅ ih x = 0
11 10 pm5.32i ⊢ x ∈ ℋ ∧ x ⋅ ih B = 0 ↔ x ∈ ℋ ∧ B ⋅ ih x = 0
12 8 11 bitri ⊢ x ∈ ⊥ ⁡ B ↔ x ∈ ℋ ∧ B ⋅ ih x = 0
13 12 imbi1i ⊢ x ∈ ⊥ ⁡ B → A ⋅ ih x = 0 ↔ x ∈ ℋ ∧ B ⋅ ih x = 0 → A ⋅ ih x = 0
14 impexp ⊢ x ∈ ℋ ∧ B ⋅ ih x = 0 → A ⋅ ih x = 0 ↔ x ∈ ℋ → B ⋅ ih x = 0 → A ⋅ ih x = 0
15 13 14 bitri ⊢ x ∈ ⊥ ⁡ B → A ⋅ ih x = 0 ↔ x ∈ ℋ → B ⋅ ih x = 0 → A ⋅ ih x = 0
16 15 ralbii2 ⊢ ∀ x ∈ ⊥ ⁡ B A ⋅ ih x = 0 ↔ ∀ x ∈ ℋ B ⋅ ih x = 0 → A ⋅ ih x = 0
17 16 anbi2i ⊢ A ∈ ℋ ∧ ∀ x ∈ ⊥ ⁡ B A ⋅ ih x = 0 ↔ A ∈ ℋ ∧ ∀ x ∈ ℋ B ⋅ ih x = 0 → A ⋅ ih x = 0
18 7 17 bitri ⊢ A ∈ ⊥ ⁡ ⊥ ⁡ B ↔ A ∈ ℋ ∧ ∀ x ∈ ℋ B ⋅ ih x = 0 → A ⋅ ih x = 0