Metamath Proof Explorer


Theorem lsatel

Description: A nonzero vector in an atom determines the atom. (Contributed by NM, 25-Aug-2014)

Ref Expression
Hypotheses lsatel.o 0 = ( 0g𝑊 )
lsatel.n 𝑁 = ( LSpan ‘ 𝑊 )
lsatel.a 𝐴 = ( LSAtoms ‘ 𝑊 )
lsatel.w ( 𝜑𝑊 ∈ LVec )
lsatel.u ( 𝜑𝑈𝐴 )
lsatel.x ( 𝜑𝑋𝑈 )
lsatel.e ( 𝜑𝑋0 )
Assertion lsatel ( 𝜑𝑈 = ( 𝑁 ‘ { 𝑋 } ) )

Proof

Step Hyp Ref Expression
1 lsatel.o 0 = ( 0g𝑊 )
2 lsatel.n 𝑁 = ( LSpan ‘ 𝑊 )
3 lsatel.a 𝐴 = ( LSAtoms ‘ 𝑊 )
4 lsatel.w ( 𝜑𝑊 ∈ LVec )
5 lsatel.u ( 𝜑𝑈𝐴 )
6 lsatel.x ( 𝜑𝑋𝑈 )
7 lsatel.e ( 𝜑𝑋0 )
8 eqid ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
9 lveclmod ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
10 4 9 syl ( 𝜑𝑊 ∈ LMod )
11 8 3 10 5 lsatlssel ( 𝜑𝑈 ∈ ( LSubSp ‘ 𝑊 ) )
12 8 2 10 11 6 lspsnel5a ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
13 eqid ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
14 13 8 lssel ( ( 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑋𝑈 ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
15 11 6 14 syl2anc ( 𝜑𝑋 ∈ ( Base ‘ 𝑊 ) )
16 13 2 1 3 lsatlspsn2 ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ∧ 𝑋0 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 )
17 10 15 7 16 syl3anc ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 )
18 3 4 17 5 lsatcmp ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ↔ ( 𝑁 ‘ { 𝑋 } ) = 𝑈 ) )
19 12 18 mpbid ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) = 𝑈 )
20 19 eqcomd ( 𝜑𝑈 = ( 𝑁 ‘ { 𝑋 } ) )