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

Metamath Proof Explorer

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