This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ellspsn5 ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
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 ⊢ ( 𝜑 → 𝑈 = ( 𝑁 ‘ { 𝑋 } ) )