Metamath Proof Explorer

Theorem lspdisjb

Description: A nonzero vector is not in a subspace iff its span is disjoint with the subspace. (Contributed by NM, 23-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 lspdisjb.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspdisjb.o ⊢ 0 = ( 0g ‘ 𝑊 )
3 lspdisjb.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 lspdisjb.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
5 lspdisjb.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
6 lspdisjb.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
7 lspdisjb.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
8 5 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) → 𝑊 ∈ LVec )
9 6 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) → 𝑈 ∈ 𝑆 )
10 7 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
11 10 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑉 )
12 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) → ¬ 𝑋 ∈ 𝑈 )
13 1 2 3 4 8 9 11 12 lspdisj ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) → ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) = { 0 } )
14 eldifsni ⊢ ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) → 𝑋 ≠ 0 )
15 7 14 syl ⊢ ( 𝜑 → 𝑋 ≠ 0 )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) = { 0 } ) → 𝑋 ≠ 0 )
17 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
18 5 17 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
19 1 3 lspsnid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
20 18 10 19 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
21 elin ⊢ ( 𝑋 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) ↔ ( 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑋 ∈ 𝑈 ) )
22 eleq2 ⊢ ( ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) = { 0 } → ( 𝑋 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) ↔ 𝑋 ∈ { 0 } ) )
23 elsni ⊢ ( 𝑋 ∈ { 0 } → 𝑋 = 0 )
24 22 23 biimtrdi ⊢ ( ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) = { 0 } → ( 𝑋 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) → 𝑋 = 0 ) )
25 21 24 biimtrrid ⊢ ( ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) = { 0 } → ( ( 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑋 ∈ 𝑈 ) → 𝑋 = 0 ) )
26 25 expd ⊢ ( ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) = { 0 } → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) → ( 𝑋 ∈ 𝑈 → 𝑋 = 0 ) ) )
27 20 26 mpan9 ⊢ ( ( 𝜑 ∧ ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) = { 0 } ) → ( 𝑋 ∈ 𝑈 → 𝑋 = 0 ) )
28 27 necon3ad ⊢ ( ( 𝜑 ∧ ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) = { 0 } ) → ( 𝑋 ≠ 0 → ¬ 𝑋 ∈ 𝑈 ) )
29 16 28 mpd ⊢ ( ( 𝜑 ∧ ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) = { 0 } ) → ¬ 𝑋 ∈ 𝑈 )
30 13 29 impbida ⊢ ( 𝜑 → ( ¬ 𝑋 ∈ 𝑈 ↔ ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) = { 0 } ) )