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

Metamath Proof Explorer

Theorem spansnm0i

Description: The meet of different one-dimensional subspaces is the zero subspace. (Contributed by NM, 1-Nov-2005) (New usage is discouraged.)

Ref Expression
Hypotheses spansnm0.1 ⊢ 𝐴 ∈ ℋ
spansnm0.2 ⊢ 𝐵 ∈ ℋ
Assertion spansnm0i ( ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) → ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) = 0ℋ )

Proof

Step Hyp Ref Expression
1 spansnm0.1 ⊢ 𝐴 ∈ ℋ
2 spansnm0.2 ⊢ 𝐵 ∈ ℋ
3 2 spansnchi ⊢ ( span ‘ { 𝐵 } ) ∈ Cℋ
4 3 chshii ⊢ ( span ‘ { 𝐵 } ) ∈ Sℋ
5 elspansn5 ⊢ ( ( span ‘ { 𝐵 } ) ∈ Sℋ → ( ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) ) ∧ ( 𝑥 ∈ ( span ‘ { 𝐴 } ) ∧ 𝑥 ∈ ( span ‘ { 𝐵 } ) ) ) → 𝑥 = 0ℎ ) )
6 4 5 ax-mp ⊢ ( ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) ) ∧ ( 𝑥 ∈ ( span ‘ { 𝐴 } ) ∧ 𝑥 ∈ ( span ‘ { 𝐵 } ) ) ) → 𝑥 = 0ℎ )
7 1 6 mpanl1 ⊢ ( ( ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) ∧ ( 𝑥 ∈ ( span ‘ { 𝐴 } ) ∧ 𝑥 ∈ ( span ‘ { 𝐵 } ) ) ) → 𝑥 = 0ℎ )
8 7 ex ⊢ ( ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) → ( ( 𝑥 ∈ ( span ‘ { 𝐴 } ) ∧ 𝑥 ∈ ( span ‘ { 𝐵 } ) ) → 𝑥 = 0ℎ ) )
9 elin ⊢ ( 𝑥 ∈ ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) ↔ ( 𝑥 ∈ ( span ‘ { 𝐴 } ) ∧ 𝑥 ∈ ( span ‘ { 𝐵 } ) ) )
10 elch0 ⊢ ( 𝑥 ∈ 0ℋ ↔ 𝑥 = 0ℎ )
11 8 9 10 3imtr4g ⊢ ( ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) → ( 𝑥 ∈ ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) → 𝑥 ∈ 0ℋ ) )
12 11 ssrdv ⊢ ( ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) → ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) ⊆ 0ℋ )
13 1 spansnchi ⊢ ( span ‘ { 𝐴 } ) ∈ Cℋ
14 13 3 chincli ⊢ ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) ∈ Cℋ
15 14 chle0i ⊢ ( ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) ⊆ 0ℋ ↔ ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) = 0ℋ )
16 12 15 sylib ⊢ ( ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) → ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) = 0ℋ )