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

Metamath Proof Explorer

Theorem lsatssn0

Description: A subspace (or any class) including an atom is nonzero. (Contributed by NM, 3-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 lsatssn0.o ⊢ 0 = ( 0g ‘ 𝑊 )
2 lsatssn0.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
3 lsatssn0.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
4 lsatssn0.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
5 lsatssn0.u ⊢ ( 𝜑 → 𝑄 ⊆ 𝑈 )
6 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
7 6 2 3 4 lsatlssel ⊢ ( 𝜑 → 𝑄 ∈ ( LSubSp ‘ 𝑊 ) )
8 1 6 lss0ss ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑄 ∈ ( LSubSp ‘ 𝑊 ) ) → { 0 } ⊆ 𝑄 )
9 3 7 8 syl2anc ⊢ ( 𝜑 → { 0 } ⊆ 𝑄 )
10 1 2 3 4 lsatn0 ⊢ ( 𝜑 → 𝑄 ≠ { 0 } )
11 10 necomd ⊢ ( 𝜑 → { 0 } ≠ 𝑄 )
12 df-pss ⊢ ( { 0 } ⊊ 𝑄 ↔ ( { 0 } ⊆ 𝑄 ∧ { 0 } ≠ 𝑄 ) )
13 9 11 12 sylanbrc ⊢ ( 𝜑 → { 0 } ⊊ 𝑄 )
14 13 5 psssstrd ⊢ ( 𝜑 → { 0 } ⊊ 𝑈 )
15 14 pssned ⊢ ( 𝜑 → { 0 } ≠ 𝑈 )
16 15 necomd ⊢ ( 𝜑 → 𝑈 ≠ { 0 } )