Theorem lsatnle

Description: The meet of a subspace and an incomparable atom is the zero subspace. ( atnssm0 analog.) (Contributed by NM, 10-Jan-2015)

	Ref	Expression
Hypotheses	lsatnle.o	⊢ 0 = ( 0g ‘ 𝑊 )
	lsatnle.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lsatnle.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
	lsatnle.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lsatnle.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	lsatnle.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
Assertion	lsatnle	⊢ ( 𝜑 → ( ¬ 𝑄 ⊆ 𝑈 ↔ ( 𝑈 ∩ 𝑄 ) = { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		lsatnle.o	⊢ 0 = ( 0g ‘ 𝑊 )
2		lsatnle.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3		lsatnle.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
4		lsatnle.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
5		lsatnle.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
6		lsatnle.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
7		eqid	⊢ ( LSSum ‘ 𝑊 ) = ( LSSum ‘ 𝑊 )
8		eqid	⊢ ( ⋖L ‘ 𝑊 ) = ( ⋖L ‘ 𝑊 )
9	2 7 3 8 4 5 6	lcv1	⊢ ( 𝜑 → ( ¬ 𝑄 ⊆ 𝑈 ↔ 𝑈 ( ⋖L ‘ 𝑊 ) ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑄 ) ) )
10	2 7 1 3 8 4 5 6	lcvp	⊢ ( 𝜑 → ( ( 𝑈 ∩ 𝑄 ) = { 0 } ↔ 𝑈 ( ⋖L ‘ 𝑊 ) ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑄 ) ) )
11	9 10	bitr4d	⊢ ( 𝜑 → ( ¬ 𝑄 ⊆ 𝑈 ↔ ( 𝑈 ∩ 𝑄 ) = { 0 } ) )