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 ` W )
lsatnem0.a 
|- A = ( LSAtoms ` W )
lsatnem0.w 
|- ( ph -> W e. LVec )
lsatnem0.q 
|- ( ph -> Q e. A )
lsatnem0.r 
|- ( ph -> R e. A )
Assertion lsatnem0 
|- ( ph -> ( Q =/= R <-> ( Q i^i R ) = { .0. } ) )

Proof

Step Hyp Ref Expression
1 lsatnem0.o 
 |-  .0. = ( 0g ` W )
2 lsatnem0.a 
 |-  A = ( LSAtoms ` W )
3 lsatnem0.w 
 |-  ( ph -> W e. LVec )
4 lsatnem0.q 
 |-  ( ph -> Q e. A )
5 lsatnem0.r 
 |-  ( ph -> R e. A )
6 2 3 5 4 lsatcmp 
 |-  ( ph -> ( R C_ Q <-> R = Q ) )
7 eqcom 
 |-  ( R = Q <-> Q = R )
8 6 7 bitrdi 
 |-  ( ph -> ( R C_ Q <-> Q = R ) )
9 8 necon3bbid 
 |-  ( ph -> ( -. R C_ Q <-> Q =/= R ) )
10 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
11 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
12 3 11 syl 
 |-  ( ph -> W e. LMod )
13 10 2 12 4 lsatlssel 
 |-  ( ph -> Q e. ( LSubSp ` W ) )
14 1 10 2 3 13 5 lsatnle 
 |-  ( ph -> ( -. R C_ Q <-> ( Q i^i R ) = { .0. } ) )
15 9 14 bitr3d 
 |-  ( ph -> ( Q =/= R <-> ( Q i^i R ) = { .0. } ) )