Metamath Proof Explorer


Theorem isbn

Description: A Banach space is a normed vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006) (Revised by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypothesis isbn.1 F = Scalar W
Assertion isbn W Ban W NrmVec W CMetSp F CMetSp

Proof

Step Hyp Ref Expression
1 isbn.1 F = Scalar W
2 elin W NrmVec CMetSp W NrmVec W CMetSp
3 2 anbi1i W NrmVec CMetSp F CMetSp W NrmVec W CMetSp F CMetSp
4 fveq2 w = W Scalar w = Scalar W
5 4 1 eqtr4di w = W Scalar w = F
6 5 eleq1d w = W Scalar w CMetSp F CMetSp
7 df-bn Ban = w NrmVec CMetSp | Scalar w CMetSp
8 6 7 elrab2 W Ban W NrmVec CMetSp F CMetSp
9 df-3an W NrmVec W CMetSp F CMetSp W NrmVec W CMetSp F CMetSp
10 3 8 9 3bitr4i W Ban W NrmVec W CMetSp F CMetSp