Metamath Proof Explorer


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 = ( BaseSet ` U )
elimnv.5
|- Z = ( 0vec ` U )
elimnv.9
|- U e. NrmCVec
Assertion elimnv
|- if ( A e. X , A , Z ) e. X

Proof

Step Hyp Ref Expression
1 elimnv.1
 |-  X = ( BaseSet ` U )
2 elimnv.5
 |-  Z = ( 0vec ` U )
3 elimnv.9
 |-  U e. NrmCVec
4 1 2 nvzcl
 |-  ( U e. NrmCVec -> Z e. X )
5 3 4 ax-mp
 |-  Z e. X
6 5 elimel
 |-  if ( A e. X , A , Z ) e. X