Theorem dvh1dimat

Description: There exists an atom. (Contributed by NM, 25-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		dvh4dimat.h	|- H = ( LHyp ` K )
2		dvh4dimat.u	|- U = ( ( DVecH ` K ) ` W )
3		dvh1dimat.a	|- A = ( LSAtoms ` U )
4		dvh1dimat.k	|- ( ph -> ( K e. HL /\ W e. H ) )
5		eqid	|- ( ( oc ` K ) ` W ) = ( ( oc ` K ) ` W )
6		eqid	|- ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
7	1 5 6 2 3 4	dihat	|- ( ph -> ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` W ) ) e. A )
8		elex2	|- ( ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` W ) ) e. A -> E. s s e. A )
9	7 8	syl	|- ( ph -> E. s s e. A )