Theorem dvh2dimatN

Description: Given an atom, there exists another. (Contributed by NM, 25-Apr-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dvh4dimat.h	|- H = ( LHyp ` K )
	dvh4dimat.u	|- U = ( ( DVecH ` K ) ` W )
	dvh2dimat.a	|- A = ( LSAtoms ` U )
	dvh2dimat.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	dvh2dimat.p	|- ( ph -> P e. A )
Assertion	dvh2dimatN	|- ( ph -> E. s e. A s =/= P )

Proof

Step	Hyp	Ref	Expression
1		dvh4dimat.h	|- H = ( LHyp ` K )
2		dvh4dimat.u	|- U = ( ( DVecH ` K ) ` W )
3		dvh2dimat.a	|- A = ( LSAtoms ` U )
4		dvh2dimat.k	|- ( ph -> ( K e. HL /\ W e. H ) )
5		dvh2dimat.p	|- ( ph -> P e. A )
6		eqid	|- ( LSSum ` U ) = ( LSSum ` U )
7	1 2 6 3 4 5 5	dvh3dimatN	|- ( ph -> E. s e. A -. s C_ ( P ( LSSum ` U ) P ) )
8	1 2 4	dvhlmod	|- ( ph -> U e. LMod )
9		eqid	|- ( LSubSp ` U ) = ( LSubSp ` U )
10	9 3 8 5	lsatlssel	|- ( ph -> P e. ( LSubSp ` U ) )
11	9	lsssubg	|- ( ( U e. LMod /\ P e. ( LSubSp ` U ) ) -> P e. ( SubGrp ` U ) )
12	8 10 11	syl2anc	|- ( ph -> P e. ( SubGrp ` U ) )
13	6	lsmidm	|- ( P e. ( SubGrp ` U ) -> ( P ( LSSum ` U ) P ) = P )
14	12 13	syl	|- ( ph -> ( P ( LSSum ` U ) P ) = P )
15	14	sseq2d	|- ( ph -> ( s C_ ( P ( LSSum ` U ) P ) <-> s C_ P ) )
16	15	adantr	|- ( ( ph /\ s e. A ) -> ( s C_ ( P ( LSSum ` U ) P ) <-> s C_ P ) )
17	1 2 4	dvhlvec	|- ( ph -> U e. LVec )
18	17	adantr	|- ( ( ph /\ s e. A ) -> U e. LVec )
19		simpr	|- ( ( ph /\ s e. A ) -> s e. A )
20	5	adantr	|- ( ( ph /\ s e. A ) -> P e. A )
21	3 18 19 20	lsatcmp	|- ( ( ph /\ s e. A ) -> ( s C_ P <-> s = P ) )
22	16 21	bitrd	|- ( ( ph /\ s e. A ) -> ( s C_ ( P ( LSSum ` U ) P ) <-> s = P ) )
23	22	necon3bbid	|- ( ( ph /\ s e. A ) -> ( -. s C_ ( P ( LSSum ` U ) P ) <-> s =/= P ) )
24	23	rexbidva	|- ( ph -> ( E. s e. A -. s C_ ( P ( LSSum ` U ) P ) <-> E. s e. A s =/= P ) )
25	7 24	mpbid	|- ( ph -> E. s e. A s =/= P )