Theorem dihat

Description: There exists at least one atom in the subspaces of vector space H. (Contributed by NM, 12-Aug-2014)

	Ref	Expression
Hypotheses	dihat.h	|- H = ( LHyp ` K )
	dihat.p	|- P = ( ( oc ` K ) ` W )
	dihat.i	|- I = ( ( DIsoH ` K ) ` W )
	dihat.u	|- U = ( ( DVecH ` K ) ` W )
	dihat.a	|- A = ( LSAtoms ` U )
	dihat.k	|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion	dihat	|- ( ph -> ( I ` P ) e. A )

Proof

Step	Hyp	Ref	Expression
1		dihat.h	|- H = ( LHyp ` K )
2		dihat.p	|- P = ( ( oc ` K ) ` W )
3		dihat.i	|- I = ( ( DIsoH ` K ) ` W )
4		dihat.u	|- U = ( ( DVecH ` K ) ` W )
5		dihat.a	|- A = ( LSAtoms ` U )
6		dihat.k	|- ( ph -> ( K e. HL /\ W e. H ) )
7		eqid	|- ( oc ` K ) = ( oc ` K )
8		eqid	|- ( Atoms ` K ) = ( Atoms ` K )
9	7 8 1	lhpocat	|- ( ( K e. HL /\ W e. H ) -> ( ( oc ` K ) ` W ) e. ( Atoms ` K ) )
10	6 9	syl	|- ( ph -> ( ( oc ` K ) ` W ) e. ( Atoms ` K ) )
11	2 10	eqeltrid	|- ( ph -> P e. ( Atoms ` K ) )
12	8 1 4 3 5	dihatlat	|- ( ( ( K e. HL /\ W e. H ) /\ P e. ( Atoms ` K ) ) -> ( I ` P ) e. A )
13	6 11 12	syl2anc	|- ( ph -> ( I ` P ) e. A )