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

Metamath Proof Explorer

Theorem lsatexch1

Description: The atom exch1ange property. ( hlatexch1 analog.) (Contributed by NM, 14-Jan-2015)

Ref Expression
Hypotheses lsatexch1.p 
|- .(+) = ( LSSum ` W )
lsatexch1.a 
|- A = ( LSAtoms ` W )
lsatexch1.w 
|- ( ph -> W e. LVec )
lsatexch1.u 
|- ( ph -> Q e. A )
lsatexch1.q 
|- ( ph -> R e. A )
lsatexch1.r 
|- ( ph -> S e. A )
lsatexch1.l 
|- ( ph -> Q C_ ( S .(+) R ) )
lsatexch1.z 
|- ( ph -> Q =/= S )
Assertion lsatexch1 
|- ( ph -> R C_ ( S .(+) Q ) )

Proof

Step Hyp Ref Expression
1 lsatexch1.p 
 |-  .(+) = ( LSSum ` W )
2 lsatexch1.a 
 |-  A = ( LSAtoms ` W )
3 lsatexch1.w 
 |-  ( ph -> W e. LVec )
4 lsatexch1.u 
 |-  ( ph -> Q e. A )
5 lsatexch1.q 
 |-  ( ph -> R e. A )
6 lsatexch1.r 
 |-  ( ph -> S e. A )
7 lsatexch1.l 
 |-  ( ph -> Q C_ ( S .(+) R ) )
8 lsatexch1.z 
 |-  ( ph -> Q =/= S )
9 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
10 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
11 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
12 3 11 syl 
 |-  ( ph -> W e. LMod )
13 9 2 12 6 lsatlssel 
 |-  ( ph -> S e. ( LSubSp ` W ) )
14 8 necomd 
 |-  ( ph -> S =/= Q )
15 10 2 3 6 4 lsatnem0 
 |-  ( ph -> ( S =/= Q <-> ( S i^i Q ) = { ( 0g ` W ) } ) )
16 14 15 mpbid 
 |-  ( ph -> ( S i^i Q ) = { ( 0g ` W ) } )
17 9 1 10 2 3 13 4 5 7 16 lsatexch 
 |-  ( ph -> R C_ ( S .(+) Q ) )