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

Metamath Proof Explorer

Theorem lspdisj2

Description: Unequal spans are disjoint (share only the zero vector). (Contributed by NM, 22-Mar-2015)

Ref Expression
Hypotheses lspdisj2.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspdisj2.o ⊢ 0 = ( 0g ‘ 𝑊 )
lspdisj2.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lspdisj2.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lspdisj2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lspdisj2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lspdisj2.q ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
Assertion lspdisj2 ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ∩ ( 𝑁 ‘ { 𝑌 } ) ) = { 0 } )

Proof

Step Hyp Ref Expression
1 lspdisj2.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspdisj2.o ⊢ 0 = ( 0g ‘ 𝑊 )
3 lspdisj2.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 lspdisj2.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
5 lspdisj2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
6 lspdisj2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
7 lspdisj2.q ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
8 sneq ⊢ ( 𝑋 = 0 → { 𝑋 } = { 0 } )
9 8 fveq2d ⊢ ( 𝑋 = 0 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 0 } ) )
10 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
11 4 10 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
12 2 3 lspsn0 ⊢ ( 𝑊 ∈ LMod → ( 𝑁 ‘ { 0 } ) = { 0 } )
13 11 12 syl ⊢ ( 𝜑 → ( 𝑁 ‘ { 0 } ) = { 0 } )
14 9 13 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( 𝑁 ‘ { 𝑋 } ) = { 0 } )
15 14 ineq1d ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( ( 𝑁 ‘ { 𝑋 } ) ∩ ( 𝑁 ‘ { 𝑌 } ) ) = ( { 0 } ∩ ( 𝑁 ‘ { 𝑌 } ) ) )
16 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
17 1 16 3 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
18 11 6 17 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
19 2 16 lss0ss ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) ) → { 0 } ⊆ ( 𝑁 ‘ { 𝑌 } ) )
20 11 18 19 syl2anc ⊢ ( 𝜑 → { 0 } ⊆ ( 𝑁 ‘ { 𝑌 } ) )
21 dfss2 ⊢ ( { 0 } ⊆ ( 𝑁 ‘ { 𝑌 } ) ↔ ( { 0 } ∩ ( 𝑁 ‘ { 𝑌 } ) ) = { 0 } )
22 20 21 sylib ⊢ ( 𝜑 → ( { 0 } ∩ ( 𝑁 ‘ { 𝑌 } ) ) = { 0 } )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( { 0 } ∩ ( 𝑁 ‘ { 𝑌 } ) ) = { 0 } )
24 15 23 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( ( 𝑁 ‘ { 𝑋 } ) ∩ ( 𝑁 ‘ { 𝑌 } ) ) = { 0 } )
25 4 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → 𝑊 ∈ LVec )
26 18 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
27 5 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ 𝑉 )
28 7 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
29 25 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ 0 ) ∧ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑊 ∈ LVec )
30 6 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → 𝑌 ∈ 𝑉 )
31 30 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ 0 ) ∧ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑌 ∈ 𝑉 )
32 simpr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ 0 ) ∧ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )
33 simplr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ 0 ) ∧ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑋 ≠ 0 )
34 1 2 3 29 31 32 33 lspsneleq ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ 0 ) ∧ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) )
35 34 ex ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) )
36 35 necon3ad ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → ( ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ) )
37 28 36 mpd ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )
38 1 2 3 16 25 26 27 37 lspdisj ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → ( ( 𝑁 ‘ { 𝑋 } ) ∩ ( 𝑁 ‘ { 𝑌 } ) ) = { 0 } )
39 24 38 pm2.61dane ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ∩ ( 𝑁 ‘ { 𝑌 } ) ) = { 0 } )