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 } )