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

Metamath Proof Explorer

Theorem lsatlssel

Description: An atom is a subspace. (Contributed by NM, 25-Aug-2014)

Ref Expression
Hypotheses lsatlss.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lsatlss.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
lssatssel.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lssatssel.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
Assertion lsatlssel ( 𝜑 → 𝑈 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 lsatlss.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2 lsatlss.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
3 lssatssel.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
4 lssatssel.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
5 1 2 lsatlss ⊢ ( 𝑊 ∈ LMod → 𝐴 ⊆ 𝑆 )
6 3 5 syl ⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
7 6 4 sseldd ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )