Theorem lsatcvat2

Description: A subspace covered by the sum of two distinct atoms is an atom. ( atcvat2i analog.) (Contributed by NM, 10-Jan-2015)

	Ref	Expression
Hypotheses	lsatcvat2.s	|- S = ( LSubSp ` W )
	lsatcvat2.p	|- .(+) = ( LSSum ` W )
	lsatcvat2.a	|- A = ( LSAtoms ` W )
	lsatcvat2.c	|- C = (
	lsatcvat2.w	|- ( ph -> W e. LVec )
	lsatcvat2.u	|- ( ph -> U e. S )
	lsatcvat2.q	|- ( ph -> Q e. A )
	lsatcvat2.r	|- ( ph -> R e. A )
	lsatcvat2.n	|- ( ph -> Q =/= R )
	lsatcvat2.l	|- ( ph -> U C ( Q .(+) R ) )
Assertion	lsatcvat2	|- ( ph -> U e. A )

Proof

Step	Hyp	Ref	Expression
1		lsatcvat2.s	|- S = ( LSubSp ` W )
2		lsatcvat2.p	|- .(+) = ( LSSum ` W )
3		lsatcvat2.a	|- A = ( LSAtoms ` W )
4		lsatcvat2.c	|- C = (
5		lsatcvat2.w	|- ( ph -> W e. LVec )
6		lsatcvat2.u	|- ( ph -> U e. S )
7		lsatcvat2.q	|- ( ph -> Q e. A )
8		lsatcvat2.r	|- ( ph -> R e. A )
9		lsatcvat2.n	|- ( ph -> Q =/= R )
10		lsatcvat2.l	|- ( ph -> U C ( Q .(+) R ) )
11		eqid	|- ( 0g ` W ) = ( 0g ` W )
12	11 2 1 3 4 5 6 7 8 10	lsatcv1	|- ( ph -> ( U = { ( 0g ` W ) } <-> Q = R ) )
13	12	necon3bid	|- ( ph -> ( U =/= { ( 0g ` W ) } <-> Q =/= R ) )
14	9 13	mpbird	|- ( ph -> U =/= { ( 0g ` W ) } )
15		lveclmod	|- ( W e. LVec -> W e. LMod )
16	5 15	syl	|- ( ph -> W e. LMod )
17	1 3 16 7	lsatlssel	|- ( ph -> Q e. S )
18	1 3 16 8	lsatlssel	|- ( ph -> R e. S )
19	1 2	lsmcl	|- ( ( W e. LMod /\ Q e. S /\ R e. S ) -> ( Q .(+) R ) e. S )
20	16 17 18 19	syl3anc	|- ( ph -> ( Q .(+) R ) e. S )
21	1 4 5 6 20 10	lcvpss	|- ( ph -> U C. ( Q .(+) R ) )
22	11 1 2 3 5 6 7 8 14 21	lsatcvat	|- ( ph -> U e. A )