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

Metamath Proof Explorer

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