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⋅ihx=0→A⋅ihx=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∈⊥⁡BA⋅ihx=0
7 5 6 ax-mp ⊢A∈⊥⁡⊥⁡B↔A∈ℋ∧∀x∈⊥⁡BA⋅ihx=0
8 1 h1deoi ⊢x∈⊥⁡B↔x∈ℋ∧x⋅ihB=0
9 orthcom ⊢x∈ℋ∧B∈ℋ→x⋅ihB=0↔B⋅ihx=0
10 1 9 mpan2 ⊢x∈ℋ→x⋅ihB=0↔B⋅ihx=0
11 10 pm5.32i ⊢x∈ℋ∧x⋅ihB=0↔x∈ℋ∧B⋅ihx=0
12 8 11 bitri ⊢x∈⊥⁡B↔x∈ℋ∧B⋅ihx=0
13 12 imbi1i ⊢x∈⊥⁡B→A⋅ihx=0↔x∈ℋ∧B⋅ihx=0→A⋅ihx=0
14 impexp ⊢x∈ℋ∧B⋅ihx=0→A⋅ihx=0↔x∈ℋ→B⋅ihx=0→A⋅ihx=0
15 13 14 bitri ⊢x∈⊥⁡B→A⋅ihx=0↔x∈ℋ→B⋅ihx=0→A⋅ihx=0
16 15 ralbii2 ⊢∀x∈⊥⁡BA⋅ihx=0↔∀x∈ℋB⋅ihx=0→A⋅ihx=0
17 16 anbi2i ⊢A∈ℋ∧∀x∈⊥⁡BA⋅ihx=0↔A∈ℋ∧∀x∈ℋB⋅ihx=0→A⋅ihx=0
18 7 17 bitri ⊢A∈⊥⁡⊥⁡B↔A∈ℋ∧∀x∈ℋB⋅ihx=0→A⋅ihx=0