This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iscbn

Description: A complex Banach space is a normed complex vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006) Use isbn instead. (New usage is discouraged.)

		Ref	Expression
	Hypotheses	iscbn.x	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
		iscbn.8	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
	Assertion	iscbn	⊢ ( 𝑈 ∈ CBan ↔ ( 𝑈 ∈ NrmCVec ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscbn.x	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		iscbn.8	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
3		fveq2	⊢ ( 𝑢 = 𝑈 → ( IndMet ‘ 𝑢 ) = ( IndMet ‘ 𝑈 ) )
4	3 2	eqtr4di	⊢ ( 𝑢 = 𝑈 → ( IndMet ‘ 𝑢 ) = 𝐷 )
5		fveq2	⊢ ( 𝑢 = 𝑈 → ( BaseSet ‘ 𝑢 ) = ( BaseSet ‘ 𝑈 ) )
6	5 1	eqtr4di	⊢ ( 𝑢 = 𝑈 → ( BaseSet ‘ 𝑢 ) = 𝑋 )
7	6	fveq2d	⊢ ( 𝑢 = 𝑈 → ( CMet ‘ ( BaseSet ‘ 𝑢 ) ) = ( CMet ‘ 𝑋 ) )
8	4 7	eleq12d	⊢ ( 𝑢 = 𝑈 → ( ( IndMet ‘ 𝑢 ) ∈ ( CMet ‘ ( BaseSet ‘ 𝑢 ) ) ↔ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) )
9		df-cbn	⊢ CBan = { 𝑢 ∈ NrmCVec ∣ ( IndMet ‘ 𝑢 ) ∈ ( CMet ‘ ( BaseSet ‘ 𝑢 ) ) }
10	8 9	elrab2	⊢ ( 𝑈 ∈ CBan ↔ ( 𝑈 ∈ NrmCVec ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) )