srabn

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

	Ref	Expression
Hypotheses	srabn.a	$⊢ A = subringAlg (W) (S)$
	srabn.j	$⊢ J = TopOpen (W)$
Assertion	srabn	$⊢ (W \in NrmRing \land W \in CMetSp \land S \in SubRing (W)) \to (A \in Ban \leftrightarrow (S \in Clsd (J) \land W ↾_{𝑠} S \in DivRing))$

Proof

Step	Hyp	Ref	Expression
1		srabn.a	$⊢ A = subringAlg (W) (S)$
2		srabn.j	$⊢ J = TopOpen (W)$
3		simp2	$⊢ (W \in NrmRing \land W \in CMetSp \land S \in SubRing (W)) \to W \in CMetSp$
4		eqidd	$⊢ (W \in NrmRing \land W \in CMetSp \land S \in SubRing (W)) \to {Base}_{W} = {Base}_{W}$
5	1	a1i	$⊢ (W \in NrmRing \land W \in CMetSp \land S \in SubRing (W)) \to A = subringAlg (W) (S)$
6		eqid	$⊢ {Base}_{W} = {Base}_{W}$
7	6	subrgss	$⊢ S \in SubRing (W) \to S \subseteq {Base}_{W}$
8	7	3ad2ant3	$⊢ (W \in NrmRing \land W \in CMetSp \land S \in SubRing (W)) \to S \subseteq {Base}_{W}$
9	5 8	srabase	$⊢ (W \in NrmRing \land W \in CMetSp \land S \in SubRing (W)) \to {Base}_{W} = {Base}_{A}$
10	5 8	srads	$⊢ (W \in NrmRing \land W \in CMetSp \land S \in SubRing (W)) \to dist (W) = dist (A)$
11	10	reseq1d	$⊢ (W \in NrmRing \land W \in CMetSp \land S \in SubRing (W)) \to {dist (W) ↾}_{({Base}_{W} \times {Base}_{W})} = {dist (A) ↾}_{({Base}_{W} \times {Base}_{W})}$
12	5 8	sratopn	$⊢ (W \in NrmRing \land W \in CMetSp \land S \in SubRing (W)) \to TopOpen (W) = TopOpen (A)$
13	4 9 11 12	cmspropd	$⊢ (W \in NrmRing \land W \in CMetSp \land S \in SubRing (W)) \to (W \in CMetSp \leftrightarrow A \in CMetSp)$
14	3 13	mpbid	$⊢ (W \in NrmRing \land W \in CMetSp \land S \in SubRing (W)) \to A \in CMetSp$
15		eqid	$⊢ Scalar (A) = Scalar (A)$
16	15	isbn	$⊢ A \in Ban \leftrightarrow (A \in NrmVec \land A \in CMetSp \land Scalar (A) \in CMetSp)$
17		3anrot	$⊢ (A \in NrmVec \land A \in CMetSp \land Scalar (A) \in CMetSp) \leftrightarrow (A \in CMetSp \land Scalar (A) \in CMetSp \land A \in NrmVec)$
18		3anass	$⊢ (A \in CMetSp \land Scalar (A) \in CMetSp \land A \in NrmVec) \leftrightarrow (A \in CMetSp \land (Scalar (A) \in CMetSp \land A \in NrmVec))$
19	16 17 18	3bitri	$⊢ A \in Ban \leftrightarrow (A \in CMetSp \land (Scalar (A) \in CMetSp \land A \in NrmVec))$
20	19	baib	$⊢ A \in CMetSp \to (A \in Ban \leftrightarrow (Scalar (A) \in CMetSp \land A \in NrmVec))$
21	14 20	syl	$⊢ (W \in NrmRing \land W \in CMetSp \land S \in SubRing (W)) \to (A \in Ban \leftrightarrow (Scalar (A) \in CMetSp \land A \in NrmVec))$
22	5 8	srasca	$⊢ (W \in NrmRing \land W \in CMetSp \land S \in SubRing (W)) \to W ↾_{𝑠} S = Scalar (A)$
23	22	eleq1d	$⊢ (W \in NrmRing \land W \in CMetSp \land S \in SubRing (W)) \to (W ↾_{𝑠} S \in CMetSp \leftrightarrow Scalar (A) \in CMetSp)$
24		eqid	$⊢ W ↾_{𝑠} S = W ↾_{𝑠} S$
25	24 6 2	cmsss	$⊢ (W \in CMetSp \land S \subseteq {Base}_{W}) \to (W ↾_{𝑠} S \in CMetSp \leftrightarrow S \in Clsd (J))$
26	3 8 25	syl2anc	$⊢ (W \in NrmRing \land W \in CMetSp \land S \in SubRing (W)) \to (W ↾_{𝑠} S \in CMetSp \leftrightarrow S \in Clsd (J))$
27	23 26	bitr3d	$⊢ (W \in NrmRing \land W \in CMetSp \land S \in SubRing (W)) \to (Scalar (A) \in CMetSp \leftrightarrow S \in Clsd (J))$
28	1	sranlm	$⊢ (W \in NrmRing \land S \in SubRing (W)) \to A \in NrmMod$
29	28	3adant2	$⊢ (W \in NrmRing \land W \in CMetSp \land S \in SubRing (W)) \to A \in NrmMod$
30	15	isnvc2	$⊢ A \in NrmVec \leftrightarrow (A \in NrmMod \land Scalar (A) \in DivRing)$
31	30	baib	$⊢ A \in NrmMod \to (A \in NrmVec \leftrightarrow Scalar (A) \in DivRing)$
32	29 31	syl	$⊢ (W \in NrmRing \land W \in CMetSp \land S \in SubRing (W)) \to (A \in NrmVec \leftrightarrow Scalar (A) \in DivRing)$
33	22	eleq1d	$⊢ (W \in NrmRing \land W \in CMetSp \land S \in SubRing (W)) \to (W ↾_{𝑠} S \in DivRing \leftrightarrow Scalar (A) \in DivRing)$
34	32 33	bitr4d	$⊢ (W \in NrmRing \land W \in CMetSp \land S \in SubRing (W)) \to (A \in NrmVec \leftrightarrow W ↾_{𝑠} S \in DivRing)$
35	27 34	anbi12d	$⊢ (W \in NrmRing \land W \in CMetSp \land S \in SubRing (W)) \to ((Scalar (A) \in CMetSp \land A \in NrmVec) \leftrightarrow (S \in Clsd (J) \land W ↾_{𝑠} S \in DivRing))$
36	21 35	bitrd	$⊢ (W \in NrmRing \land W \in CMetSp \land S \in SubRing (W)) \to (A \in Ban \leftrightarrow (S \in Clsd (J) \land W ↾_{𝑠} S \in DivRing))$

Metamath Proof Explorer

Theorem srabn

Proof