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

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 ⊢ 𝐵 ∈ ℋ
Assertion h1dei ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ( 𝐴 ∈ ℋ ∧ ∀ 𝑥 ∈ ℋ ( ( 𝐵 ·ih 𝑥 ) = 0 → ( 𝐴 ·ih 𝑥 ) = 0 ) ) )

Proof

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