Theorem elimnv

Description: Hypothesis elimination lemma for normed complex vector spaces to assist weak deduction theorem. (Contributed by NM, 16-May-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	elimnv.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
	elimnv.5	$$⊢Z=0_{\mathrm{vec}}\left(U\right)$$
	elimnv.9	$$⊢U\in \mathrm{NrmCVec}$$
Assertion	elimnv	$$⊢if\left(A\in X,A,Z\right)\in X$$

Proof

Step	Hyp	Ref	Expression
1		elimnv.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		elimnv.5	$$⊢Z=0_{\mathrm{vec}}\left(U\right)$$
3		elimnv.9	$$⊢U\in \mathrm{NrmCVec}$$
4	1 2	nvzcl	$$⊢U\in \mathrm{NrmCVec}\to Z\in X$$
5	3 4	ax-mp	$$⊢Z\in X$$
6	5	elimel	$$⊢if\left(A\in X,A,Z\right)\in X$$