Metamath Proof Explorer

Theorem lsateln0

Description: A 1-dim subspace (atom) (of a left module or left vector space) contains a nonzero vector. (Contributed by NM, 2-Jan-2015)

Ref Expression
Hypotheses lsateln0.z ⊢ 0 = ( 0g ‘ 𝑊 )
lsateln0.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
lsateln0.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lsateln0.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
Assertion lsateln0 ( 𝜑 → ∃ 𝑣 ∈ 𝑈 𝑣 ≠ 0 )

Proof

Step Hyp Ref Expression
1 lsateln0.z ⊢ 0 = ( 0g ‘ 𝑊 )
2 lsateln0.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
3 lsateln0.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
4 lsateln0.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
5 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
6 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
7 5 6 1 2 islsat ⊢ ( 𝑊 ∈ LMod → ( 𝑈 ∈ 𝐴 ↔ ∃ 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
8 3 7 syl ⊢ ( 𝜑 → ( 𝑈 ∈ 𝐴 ↔ ∃ 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
9 4 8 mpbid ⊢ ( 𝜑 → ∃ 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) )
10 eldifi ⊢ ( 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) → 𝑣 ∈ ( Base ‘ 𝑊 ) )
11 5 6 lspsnid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → 𝑣 ∈ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) )
12 3 10 11 syl2an ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) → 𝑣 ∈ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) )
13 eleq2 ⊢ ( 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( 𝑣 ∈ 𝑈 ↔ 𝑣 ∈ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
14 12 13 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) → ( 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → 𝑣 ∈ 𝑈 ) )
15 14 reximdva ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ∃ 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑣 ∈ 𝑈 ) )
16 9 15 mpd ⊢ ( 𝜑 → ∃ 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑣 ∈ 𝑈 )
17 eldifsn ⊢ ( 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ↔ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ≠ 0 ) )
18 17 anbi1i ⊢ ( ( 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑣 ∈ 𝑈 ) ↔ ( ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ≠ 0 ) ∧ 𝑣 ∈ 𝑈 ) )
19 anass ⊢ ( ( ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ≠ 0 ) ∧ 𝑣 ∈ 𝑈 ) ↔ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑣 ≠ 0 ∧ 𝑣 ∈ 𝑈 ) ) )
20 18 19 bitri ⊢ ( ( 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑣 ∈ 𝑈 ) ↔ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑣 ≠ 0 ∧ 𝑣 ∈ 𝑈 ) ) )
21 20 simprbi ⊢ ( ( 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑣 ∈ 𝑈 ) → ( 𝑣 ≠ 0 ∧ 𝑣 ∈ 𝑈 ) )
22 21 ancomd ⊢ ( ( 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑣 ∈ 𝑈 ) → ( 𝑣 ∈ 𝑈 ∧ 𝑣 ≠ 0 ) )
23 22 reximi2 ⊢ ( ∃ 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑣 ∈ 𝑈 → ∃ 𝑣 ∈ 𝑈 𝑣 ≠ 0 )
24 16 23 syl ⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝑈 𝑣 ≠ 0 )