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

Metamath Proof Explorer

Theorem h1de2ci

Description: Membership in 1-dimensional subspace. All members are collinear with the generating vector. (Contributed by NM, 21-Jul-2001) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Hypothesis h1de2ct.1 ⊢ 𝐵 ∈ ℋ
Assertion h1de2ci ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ∃ 𝑥 ∈ ℂ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 h1de2ct.1 ⊢ 𝐵 ∈ ℋ
2 snssi ⊢ ( 𝐵 ∈ ℋ → { 𝐵 } ⊆ ℋ )
3 occl ⊢ ( { 𝐵 } ⊆ ℋ → ( ⊥ ‘ { 𝐵 } ) ∈ Cℋ )
4 1 2 3 mp2b ⊢ ( ⊥ ‘ { 𝐵 } ) ∈ Cℋ
5 4 choccli ⊢ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ∈ Cℋ
6 5 cheli ⊢ ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → 𝐴 ∈ ℋ )
7 hvmulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝑥 ·ℎ 𝐵 ) ∈ ℋ )
8 1 7 mpan2 ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ·ℎ 𝐵 ) ∈ ℋ )
9 eleq1 ⊢ ( 𝐴 = ( 𝑥 ·ℎ 𝐵 ) → ( 𝐴 ∈ ℋ ↔ ( 𝑥 ·ℎ 𝐵 ) ∈ ℋ ) )
10 8 9 syl5ibrcom ⊢ ( 𝑥 ∈ ℂ → ( 𝐴 = ( 𝑥 ·ℎ 𝐵 ) → 𝐴 ∈ ℋ ) )
11 10 rexlimiv ⊢ ( ∃ 𝑥 ∈ ℂ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) → 𝐴 ∈ ℋ )
12 eleq1 ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ) )
13 eqeq1 ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ↔ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) = ( 𝑥 ·ℎ 𝐵 ) ) )
14 13 rexbidv ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ∃ 𝑥 ∈ ℂ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ↔ ∃ 𝑥 ∈ ℂ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) = ( 𝑥 ·ℎ 𝐵 ) ) )
15 12 14 bibi12d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ∃ 𝑥 ∈ ℂ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ∃ 𝑥 ∈ ℂ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) = ( 𝑥 ·ℎ 𝐵 ) ) ) )
16 ifhvhv0 ⊢ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ∈ ℋ
17 16 1 h1de2ctlem ⊢ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ∃ 𝑥 ∈ ℂ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) = ( 𝑥 ·ℎ 𝐵 ) )
18 15 17 dedth ⊢ ( 𝐴 ∈ ℋ → ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ∃ 𝑥 ∈ ℂ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) )
19 6 11 18 pm5.21nii ⊢ ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ∃ 𝑥 ∈ ℂ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) )