Metamath Proof Explorer

Theorem lsatn0

Description: A 1-dim subspace (atom) of a left module or left vector space is nonzero. ( atne0 analog.) (Contributed by NM, 25-Aug-2014)

Ref Expression
Hypotheses lsatn0.o ⊢ 0 = ( 0g ‘ 𝑊 )
lsatn0.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
lsatn0.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lsatn0.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
Assertion lsatn0 ( 𝜑 → 𝑈 ≠ { 0 } )

Proof

Step Hyp Ref Expression
1 lsatn0.o ⊢ 0 = ( 0g ‘ 𝑊 )
2 lsatn0.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
3 lsatn0.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
4 lsatn0.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 eldifsn ⊢ ( 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ↔ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ≠ 0 ) )
11 5 1 6 lspsneq0 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) = { 0 } ↔ 𝑣 = 0 ) )
12 3 11 sylan ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) = { 0 } ↔ 𝑣 = 0 ) )
13 12 biimpd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) = { 0 } → 𝑣 = 0 ) )
14 13 necon3d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑣 ≠ 0 → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ≠ { 0 } ) )
15 14 expimpd ⊢ ( 𝜑 → ( ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ≠ 0 ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ≠ { 0 } ) )
16 10 15 syl5bi ⊢ ( 𝜑 → ( 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ≠ { 0 } ) )
17 neeq1 ⊢ ( 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( 𝑈 ≠ { 0 } ↔ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ≠ { 0 } ) )
18 17 biimprcd ⊢ ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ≠ { 0 } → ( 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → 𝑈 ≠ { 0 } ) )
19 16 18 syl6 ⊢ ( 𝜑 → ( 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) → ( 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → 𝑈 ≠ { 0 } ) ) )
20 19 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → 𝑈 ≠ { 0 } ) )
21 9 20 mpd ⊢ ( 𝜑 → 𝑈 ≠ { 0 } )