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 )