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