Metamath Proof Explorer

Theorem lspdisj

Description: The span of a vector not in a subspace is disjoint with the subspace. (Contributed by NM, 6-Apr-2015)

Ref Expression
Hypotheses lspdisj.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspdisj.o ⊢ 0 = ( 0g ‘ 𝑊 )
lspdisj.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lspdisj.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lspdisj.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lspdisj.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
lspdisj.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lspdisj.e ⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )
Assertion lspdisj ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) = { 0 } )

Proof

Step Hyp Ref Expression
1 lspdisj.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspdisj.o ⊢ 0 = ( 0g ‘ 𝑊 )
3 lspdisj.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 lspdisj.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
5 lspdisj.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
6 lspdisj.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
7 lspdisj.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
8 lspdisj.e ⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )
9 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
10 5 9 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
11 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
12 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
13 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
14 11 12 1 13 3 lspsnel ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) )
15 10 7 14 syl2anc ⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) )
16 15 biimpa ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ) → ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) )
17 16 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑣 ∈ 𝑈 ) ) → ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) )
18 simprr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) )
19 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → ¬ 𝑋 ∈ 𝑈 )
20 simplr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → 𝑣 ∈ 𝑈 )
21 18 20 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ 𝑈 )
22 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
23 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → 𝑊 ∈ LVec )
24 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → 𝑈 ∈ 𝑆 )
25 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → 𝑋 ∈ 𝑉 )
26 simprl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
27 1 13 11 12 22 4 23 24 25 26 lssvs0or ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ 𝑈 ↔ ( 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∨ 𝑋 ∈ 𝑈 ) ) )
28 21 27 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → ( 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∨ 𝑋 ∈ 𝑈 ) )
29 28 orcomd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → ( 𝑋 ∈ 𝑈 ∨ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
30 29 ord ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → ( ¬ 𝑋 ∈ 𝑈 → 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
31 19 30 mpd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
32 31 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) )
33 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → 𝑊 ∈ LMod )
34 1 11 13 22 2 lmod0vs ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = 0 )
35 33 25 34 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = 0 )
36 18 32 35 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → 𝑣 = 0 )
37 36 exp32 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) → ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) → ( 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) → 𝑣 = 0 ) ) )
38 37 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑣 ∈ 𝑈 ) ) → ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) → ( 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) → 𝑣 = 0 ) ) )
39 38 rexlimdv ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑣 ∈ 𝑈 ) ) → ( ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) → 𝑣 = 0 ) )
40 17 39 mpd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑣 ∈ 𝑈 ) ) → 𝑣 = 0 )
41 40 ex ⊢ ( 𝜑 → ( ( 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑣 ∈ 𝑈 ) → 𝑣 = 0 ) )
42 elin ⊢ ( 𝑣 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) ↔ ( 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑣 ∈ 𝑈 ) )
43 velsn ⊢ ( 𝑣 ∈ { 0 } ↔ 𝑣 = 0 )
44 41 42 43 3imtr4g ⊢ ( 𝜑 → ( 𝑣 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) → 𝑣 ∈ { 0 } ) )
45 44 ssrdv ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) ⊆ { 0 } )
46 1 4 3 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝑆 )
47 10 7 46 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝑆 )
48 2 4 lss0ss ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ 𝑆 ) → { 0 } ⊆ ( 𝑁 ‘ { 𝑋 } ) )
49 10 47 48 syl2anc ⊢ ( 𝜑 → { 0 } ⊆ ( 𝑁 ‘ { 𝑋 } ) )
50 2 4 lss0ss ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → { 0 } ⊆ 𝑈 )
51 10 6 50 syl2anc ⊢ ( 𝜑 → { 0 } ⊆ 𝑈 )
52 49 51 ssind ⊢ ( 𝜑 → { 0 } ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) )
53 45 52 eqssd ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) = { 0 } )