Theorem dvh1dimat

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

	Ref	Expression
Hypotheses	dvh4dimat.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dvh4dimat.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dvh1dimat.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
	dvh1dimat.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	dvh1dimat	$$⊢\phi \to \exists ss\in A$$

Proof

Step	Hyp	Ref	Expression
1		dvh4dimat.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dvh4dimat.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		dvh1dimat.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
4		dvh1dimat.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
5		eqid	$$⊢\mathrm{oc}\left(K\right)\left(W\right)=\mathrm{oc}\left(K\right)\left(W\right)$$
6		eqid	$$⊢\mathrm{DIsoH}\left(K\right)\left(W\right)=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
7	1 5 6 2 3 4	dihat	$$⊢\phi \to \mathrm{DIsoH}\left(K\right)\left(W\right)\left(\mathrm{oc}\left(K\right)\left(W\right)\right)\in A$$
8		elex2	$$⊢\mathrm{DIsoH}\left(K\right)\left(W\right)\left(\mathrm{oc}\left(K\right)\left(W\right)\right)\in A\to \exists ss\in A$$
9	7 8	syl	$$⊢\phi \to \exists ss\in A$$