cnbn

Description: The set of complex numbers is a complex Banach space. (Contributed by Steve Rodriguez, 4-Jan-2007) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	cnbn.6	$⊢ U = ⟨⟨+ \times⟩, abs⟩$
	Assertion	cnbn	$⊢ U \in CBan$

Step	Hyp	Ref	Expression
1		cnbn.6	$⊢ U = ⟨⟨+ \times⟩, abs⟩$
2	1	cnnv	$⊢ U \in NrmCVec$
3		eqid	$⊢ ⟨⟨+ \times⟩, abs⟩ = ⟨⟨+ \times⟩, abs⟩$
4		eqid	$⊢ abs \circ - = abs \circ -$
5	3 4	cnims	$⊢ abs \circ - = IndMet (⟨⟨+ \times⟩, abs⟩)$
6	5	eqcomi	$⊢ IndMet (⟨⟨+ \times⟩, abs⟩) = abs \circ -$
7	6	cncmet	$⊢ IndMet (⟨⟨+ \times⟩, abs⟩) \in CMet (ℂ)$
8	1	cnnvba	$⊢ ℂ = BaseSet (U)$
9	1	fveq2i	$⊢ IndMet (U) = IndMet (⟨⟨+ \times⟩, abs⟩)$
10	9	eqcomi	$⊢ IndMet (⟨⟨+ \times⟩, abs⟩) = IndMet (U)$
11	8 10	iscbn	$⊢ U \in CBan \leftrightarrow (U \in NrmCVec \land IndMet (⟨⟨+ \times⟩, abs⟩) \in CMet (ℂ))$
12	2 7 11	mpbir2an	$⊢ U \in CBan$

Metamath Proof Explorer