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

Metamath Proof Explorer

Theorem lsatelbN

Description: A nonzero vector in an atom determines the atom. (Contributed by NM, 3-Feb-2015) (New usage is discouraged.)

Ref Expression
Hypotheses lsatelb.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lsatelb.o ⊢ 0 = ( 0g ‘ 𝑊 )
lsatelb.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lsatelb.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
lsatelb.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lsatelb.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
lsatelb.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
Assertion lsatelbN ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ 𝑈 = ( 𝑁 ‘ { 𝑋 } ) ) )

Proof

Step Hyp Ref Expression
1 lsatelb.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lsatelb.o ⊢ 0 = ( 0g ‘ 𝑊 )
3 lsatelb.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 lsatelb.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
5 lsatelb.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
6 lsatelb.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
7 lsatelb.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
8 5 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑊 ∈ LVec )
9 7 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑈 ∈ 𝐴 )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑈 )
11 eldifsn ⊢ ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) ↔ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) )
12 6 11 sylib ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) )
13 12 simprd ⊢ ( 𝜑 → 𝑋 ≠ 0 )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ≠ 0 )
15 2 3 4 8 9 10 14 lsatel ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑈 = ( 𝑁 ‘ { 𝑋 } ) )
16 eqimss2 ⊢ ( 𝑈 = ( 𝑁 ‘ { 𝑋 } ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑈 = ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
18 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
19 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
20 5 19 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
21 18 4 20 7 lsatlssel ⊢ ( 𝜑 → 𝑈 ∈ ( LSubSp ‘ 𝑊 ) )
22 6 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
23 1 18 3 20 21 22 ellspsn5b ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑈 = ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑋 ∈ 𝑈 ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) )
25 17 24 mpbird ⊢ ( ( 𝜑 ∧ 𝑈 = ( 𝑁 ‘ { 𝑋 } ) ) → 𝑋 ∈ 𝑈 )
26 15 25 impbida ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ 𝑈 = ( 𝑁 ‘ { 𝑋 } ) ) )