Theorem lsatnem0

Description: The meet of distinct atoms is the zero subspace. ( atnemeq0 analog.) (Contributed by NM, 10-Jan-2015)

	Ref	Expression
Hypotheses	lsatnem0.o	⊢ 0 = ( 0g ‘ 𝑊 )
	lsatnem0.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
	lsatnem0.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lsatnem0.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
	lsatnem0.r	⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
Assertion	lsatnem0	⊢ ( 𝜑 → ( 𝑄 ≠ 𝑅 ↔ ( 𝑄 ∩ 𝑅 ) = { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		lsatnem0.o	⊢ 0 = ( 0g ‘ 𝑊 )
2		lsatnem0.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
3		lsatnem0.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
4		lsatnem0.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
5		lsatnem0.r	⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
6	2 3 5 4	lsatcmp	⊢ ( 𝜑 → ( 𝑅 ⊆ 𝑄 ↔ 𝑅 = 𝑄 ) )
7		eqcom	⊢ ( 𝑅 = 𝑄 ↔ 𝑄 = 𝑅 )
8	6 7	bitrdi	⊢ ( 𝜑 → ( 𝑅 ⊆ 𝑄 ↔ 𝑄 = 𝑅 ) )
9	8	necon3bbid	⊢ ( 𝜑 → ( ¬ 𝑅 ⊆ 𝑄 ↔ 𝑄 ≠ 𝑅 ) )
10		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
11		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
12	3 11	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
13	10 2 12 4	lsatlssel	⊢ ( 𝜑 → 𝑄 ∈ ( LSubSp ‘ 𝑊 ) )
14	1 10 2 3 13 5	lsatnle	⊢ ( 𝜑 → ( ¬ 𝑅 ⊆ 𝑄 ↔ ( 𝑄 ∩ 𝑅 ) = { 0 } ) )
15	9 14	bitr3d	⊢ ( 𝜑 → ( 𝑄 ≠ 𝑅 ↔ ( 𝑄 ∩ 𝑅 ) = { 0 } ) )