rlmbn

Description: The ring module over a complete normed division ring is a Banach space. (Contributed by Mario Carneiro, 15-Oct-2015)

		Ref	Expression
	Assertion	rlmbn	$⊢ (R \in NrmRing \land R \in DivRing \land R \in CMetSp) \to ringLMod (R) \in Ban$

Proof

Step	Hyp	Ref	Expression
1		simp3	$⊢ (R \in NrmRing \land R \in DivRing \land R \in CMetSp) \to R \in CMetSp$
2		cmsms	$⊢ R \in CMetSp \to R \in MetSp$
3		mstps	$⊢ R \in MetSp \to R \in TopSp$
4	1 2 3	3syl	$⊢ (R \in NrmRing \land R \in DivRing \land R \in CMetSp) \to R \in TopSp$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6		eqid	$⊢ TopOpen (R) = TopOpen (R)$
7	5 6	tpsuni	$⊢ R \in TopSp \to {Base}_{R} = ⋃ TopOpen (R)$
8	4 7	syl	$⊢ (R \in NrmRing \land R \in DivRing \land R \in CMetSp) \to {Base}_{R} = ⋃ TopOpen (R)$
9	6	tpstop	$⊢ R \in TopSp \to TopOpen (R) \in Top$
10		eqid	$⊢ ⋃ TopOpen (R) = ⋃ TopOpen (R)$
11	10	topcld	$⊢ TopOpen (R) \in Top \to ⋃ TopOpen (R) \in Clsd (TopOpen (R))$
12	4 9 11	3syl	$⊢ (R \in NrmRing \land R \in DivRing \land R \in CMetSp) \to ⋃ TopOpen (R) \in Clsd (TopOpen (R))$
13	8 12	eqeltrd	$⊢ (R \in NrmRing \land R \in DivRing \land R \in CMetSp) \to {Base}_{R} \in Clsd (TopOpen (R))$
14	5	ressid	$⊢ R \in NrmRing \to R ↾_{𝑠} {Base}_{R} = R$
15	14	3ad2ant1	$⊢ (R \in NrmRing \land R \in DivRing \land R \in CMetSp) \to R ↾_{𝑠} {Base}_{R} = R$
16		simp2	$⊢ (R \in NrmRing \land R \in DivRing \land R \in CMetSp) \to R \in DivRing$
17	15 16	eqeltrd	$⊢ (R \in NrmRing \land R \in DivRing \land R \in CMetSp) \to R ↾_{𝑠} {Base}_{R} \in DivRing$
18		simp1	$⊢ (R \in NrmRing \land R \in DivRing \land R \in CMetSp) \to R \in NrmRing$
19		nrgring	$⊢ R \in NrmRing \to R \in Ring$
20	19	3ad2ant1	$⊢ (R \in NrmRing \land R \in DivRing \land R \in CMetSp) \to R \in Ring$
21	5	subrgid	$⊢ R \in Ring \to {Base}_{R} \in SubRing (R)$
22	20 21	syl	$⊢ (R \in NrmRing \land R \in DivRing \land R \in CMetSp) \to {Base}_{R} \in SubRing (R)$
23		rlmval	$⊢ ringLMod (R) = subringAlg (R) ({Base}_{R})$
24	23 6	srabn	$⊢ (R \in NrmRing \land R \in CMetSp \land {Base}_{R} \in SubRing (R)) \to (ringLMod (R) \in Ban \leftrightarrow ({Base}_{R} \in Clsd (TopOpen (R)) \land R ↾_{𝑠} {Base}_{R} \in DivRing))$
25	18 1 22 24	syl3anc	$⊢ (R \in NrmRing \land R \in DivRing \land R \in CMetSp) \to (ringLMod (R) \in Ban \leftrightarrow ({Base}_{R} \in Clsd (TopOpen (R)) \land R ↾_{𝑠} {Base}_{R} \in DivRing))$
26	13 17 25	mpbir2and	$⊢ (R \in NrmRing \land R \in DivRing \land R \in CMetSp) \to ringLMod (R) \in Ban$

Metamath Proof Explorer

Theorem rlmbn

Proof