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=\mathrm{LHyp}\left(K\right)$$
	dihat.p	$$⊢P=\mathrm{oc}\left(K\right)\left(W\right)$$
	dihat.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	dihat.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dihat.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
	dihat.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	dihat	$$⊢\phi \to I\left(P\right)\in A$$

Proof

Step	Hyp	Ref	Expression
1		dihat.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dihat.p	$$⊢P=\mathrm{oc}\left(K\right)\left(W\right)$$
3		dihat.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
4		dihat.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		dihat.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
6		dihat.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
7		eqid	$$⊢\mathrm{oc}\left(K\right)=\mathrm{oc}\left(K\right)$$
8		eqid	$$⊢\mathrm{Atoms}\left(K\right)=\mathrm{Atoms}\left(K\right)$$
9	7 8 1	lhpocat	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \mathrm{oc}\left(K\right)\left(W\right)\in \mathrm{Atoms}\left(K\right)$$
10	6 9	syl	$$⊢\phi \to \mathrm{oc}\left(K\right)\left(W\right)\in \mathrm{Atoms}\left(K\right)$$
11	2 10	eqeltrid	$$⊢\phi \to P\in \mathrm{Atoms}\left(K\right)$$
12	8 1 4 3 5	dihatlat	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge P\in \mathrm{Atoms}\left(K\right)\right)\to I\left(P\right)\in A$$
13	6 11 12	syl2anc	$$⊢\phi \to I\left(P\right)\in A$$