Theorem dvh3dimatN

Description: There is an atom that is outside the subspace sum of 2 others. (Contributed by NM, 25-Apr-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dvh4dimat.h	|- H = ( LHyp ` K )
	dvh4dimat.u	|- U = ( ( DVecH ` K ) ` W )
	dvh3dimat.s	|- .(+) = ( LSSum ` U )
	dvh3dimat.a	|- A = ( LSAtoms ` U )
	dvh3dimat.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	dvh3dimat.p	|- ( ph -> P e. A )
	dvh3dimat.q	|- ( ph -> Q e. A )
Assertion	dvh3dimatN	|- ( ph -> E. s e. A -. s C_ ( P .(+) Q ) )

Proof

Step	Hyp	Ref	Expression
1		dvh4dimat.h	|- H = ( LHyp ` K )
2		dvh4dimat.u	|- U = ( ( DVecH ` K ) ` W )
3		dvh3dimat.s	|- .(+) = ( LSSum ` U )
4		dvh3dimat.a	|- A = ( LSAtoms ` U )
5		dvh3dimat.k	|- ( ph -> ( K e. HL /\ W e. H ) )
6		dvh3dimat.p	|- ( ph -> P e. A )
7		dvh3dimat.q	|- ( ph -> Q e. A )
8	1 2 3 4 5 6 6 7	dvh4dimat	|- ( ph -> E. s e. A -. s C_ ( ( P .(+) P ) .(+) Q ) )
9	1 2 5	dvhlmod	|- ( ph -> U e. LMod )
10		eqid	|- ( LSubSp ` U ) = ( LSubSp ` U )
11	10 4 9 6	lsatlssel	|- ( ph -> P e. ( LSubSp ` U ) )
12	10	lsssubg	|- ( ( U e. LMod /\ P e. ( LSubSp ` U ) ) -> P e. ( SubGrp ` U ) )
13	9 11 12	syl2anc	|- ( ph -> P e. ( SubGrp ` U ) )
14	3	lsmidm	|- ( P e. ( SubGrp ` U ) -> ( P .(+) P ) = P )
15	13 14	syl	|- ( ph -> ( P .(+) P ) = P )
16	15	oveq1d	|- ( ph -> ( ( P .(+) P ) .(+) Q ) = ( P .(+) Q ) )
17	16	sseq2d	|- ( ph -> ( s C_ ( ( P .(+) P ) .(+) Q ) <-> s C_ ( P .(+) Q ) ) )
18	17	notbid	|- ( ph -> ( -. s C_ ( ( P .(+) P ) .(+) Q ) <-> -. s C_ ( P .(+) Q ) ) )
19	18	rexbidv	|- ( ph -> ( E. s e. A -. s C_ ( ( P .(+) P ) .(+) Q ) <-> E. s e. A -. s C_ ( P .(+) Q ) ) )
20	8 19	mpbid	|- ( ph -> E. s e. A -. s C_ ( P .(+) Q ) )