nmhmcn

Description: A linear operator over a normed subcomplex module is bounded iff it is continuous. (Contributed by Mario Carneiro, 22-Oct-2015)

	Ref	Expression
Hypotheses	nmhmcn.j	$⊢ J = TopOpen (S)$
	nmhmcn.k	$⊢ K = TopOpen (T)$
	nmhmcn.g	$⊢ G = Scalar (S)$
	nmhmcn.b	$⊢ B = {Base}_{G}$
Assertion	nmhmcn	$⊢ (S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \to (F \in (S NMHom T) \leftrightarrow (F \in (S LMHom T) \land F \in (J Cn K)))$

Proof

Step	Hyp	Ref	Expression
1		nmhmcn.j	$⊢ J = TopOpen (S)$
2		nmhmcn.k	$⊢ K = TopOpen (T)$
3		nmhmcn.g	$⊢ G = Scalar (S)$
4		nmhmcn.b	$⊢ B = {Base}_{G}$
5		elinel1	$⊢ S \in (NrmMod \cap CMod) \to S \in NrmMod$
6		elinel1	$⊢ T \in (NrmMod \cap CMod) \to T \in NrmMod$
7		isnmhm	$⊢ F \in (S NMHom T) \leftrightarrow ((S \in NrmMod \land T \in NrmMod) \land (F \in (S LMHom T) \land F \in (S NGHom T)))$
8	7	baib	$⊢ (S \in NrmMod \land T \in NrmMod) \to (F \in (S NMHom T) \leftrightarrow (F \in (S LMHom T) \land F \in (S NGHom T)))$
9	5 6 8	syl2an	$⊢ (S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod)) \to (F \in (S NMHom T) \leftrightarrow (F \in (S LMHom T) \land F \in (S NGHom T)))$
10	9	3adant3	$⊢ (S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \to (F \in (S NMHom T) \leftrightarrow (F \in (S LMHom T) \land F \in (S NGHom T)))$
11	1 2	nghmcn	$⊢ F \in (S NGHom T) \to F \in (J Cn K)$
12		simpll1	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to S \in (NrmMod \cap CMod)$
13	12	elin1d	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to S \in NrmMod$
14		nlmngp	$⊢ S \in NrmMod \to S \in NrmGrp$
15		ngpms	$⊢ S \in NrmGrp \to S \in MetSp$
16	13 14 15	3syl	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to S \in MetSp$
17		msxms	$⊢ S \in MetSp \to S \in ∞MetSp$
18		eqid	$⊢ {Base}_{S} = {Base}_{S}$
19		eqid	$⊢ {dist (S) ↾}_{({Base}_{S} \times {Base}_{S})} = {dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}$
20	18 19	xmsxmet	$⊢ S \in ∞MetSp \to {dist (S) ↾}_{({Base}_{S} \times {Base}_{S})} \in ∞Met ({Base}_{S})$
21	16 17 20	3syl	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to {dist (S) ↾}_{({Base}_{S} \times {Base}_{S})} \in ∞Met ({Base}_{S})$
22		simpr	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to F \in (J Cn K)$
23		simpll2	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to T \in (NrmMod \cap CMod)$
24	23	elin1d	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to T \in NrmMod$
25		nlmngp	$⊢ T \in NrmMod \to T \in NrmGrp$
26		ngpms	$⊢ T \in NrmGrp \to T \in MetSp$
27	24 25 26	3syl	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to T \in MetSp$
28		msxms	$⊢ T \in MetSp \to T \in ∞MetSp$
29		eqid	$⊢ {Base}_{T} = {Base}_{T}$
30		eqid	$⊢ {dist (T) ↾}_{({Base}_{T} \times {Base}_{T})} = {dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}$
31	29 30	xmsxmet	$⊢ T \in ∞MetSp \to {dist (T) ↾}_{({Base}_{T} \times {Base}_{T})} \in ∞Met ({Base}_{T})$
32	27 28 31	3syl	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to {dist (T) ↾}_{({Base}_{T} \times {Base}_{T})} \in ∞Met ({Base}_{T})$
33		nlmlmod	$⊢ T \in NrmMod \to T \in LMod$
34		eqid	$⊢ 0_{T} = 0_{T}$
35	29 34	lmod0vcl	$⊢ T \in LMod \to 0_{T} \in {Base}_{T}$
36	24 33 35	3syl	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to 0_{T} \in {Base}_{T}$
37		1rp	$⊢ 1 \in ℝ^{+}$
38		rpxr	$⊢ 1 \in ℝ^{+} \to 1 \in ℝ^{*}$
39	37 38	mp1i	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to 1 \in ℝ^{*}$
40		eqid	$⊢ MetOpen ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) = MetOpen ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})})$
41	40	blopn	$⊢ ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})} \in ∞Met ({Base}_{T}) \land 0_{T} \in {Base}_{T} \land 1 \in ℝ^{*}) \to 0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1 \in MetOpen ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})})$
42	32 36 39 41	syl3anc	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to 0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1 \in MetOpen ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})})$
43	2 29 30	mstopn	$⊢ T \in MetSp \to K = MetOpen ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})})$
44	24 25 26 43	4syl	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to K = MetOpen ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})})$
45	42 44	eleqtrrd	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to 0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1 \in K$
46		cnima	$⊢ (F \in (J Cn K) \land 0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1 \in K) \to F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1] \in J$
47	22 45 46	syl2anc	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1] \in J$
48	1 18 19	mstopn	$⊢ S \in MetSp \to J = MetOpen ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})})$
49	13 14 15 48	4syl	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to J = MetOpen ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})})$
50	47 49	eleqtrd	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1] \in MetOpen ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})})$
51		nlmlmod	$⊢ S \in NrmMod \to S \in LMod$
52		eqid	$⊢ 0_{S} = 0_{S}$
53	18 52	lmod0vcl	$⊢ S \in LMod \to 0_{S} \in {Base}_{S}$
54	13 51 53	3syl	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to 0_{S} \in {Base}_{S}$
55		lmghm	$⊢ F \in (S LMHom T) \to F \in (S GrpHom T)$
56	55	ad2antlr	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to F \in (S GrpHom T)$
57	52 34	ghmid	$⊢ F \in (S GrpHom T) \to F (0_{S}) = 0_{T}$
58	56 57	syl	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to F (0_{S}) = 0_{T}$
59	37	a1i	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to 1 \in ℝ^{+}$
60		blcntr	$⊢ ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})} \in ∞Met ({Base}_{T}) \land 0_{T} \in {Base}_{T} \land 1 \in ℝ^{+}) \to 0_{T} \in (0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1)$
61	32 36 59 60	syl3anc	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to 0_{T} \in (0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1)$
62	58 61	eqeltrd	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to F (0_{S}) \in (0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1)$
63	18 29	lmhmf	$⊢ F \in (S LMHom T) \to F : {Base}_{S} ⟶ {Base}_{T}$
64	63	ad2antlr	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to F : {Base}_{S} ⟶ {Base}_{T}$
65		ffn	$⊢ F : {Base}_{S} ⟶ {Base}_{T} \to F Fn {Base}_{S}$
66		elpreima	$⊢ F Fn {Base}_{S} \to (0_{S} \in F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1] \leftrightarrow (0_{S} \in {Base}_{S} \land F (0_{S}) \in (0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1)))$
67	64 65 66	3syl	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to (0_{S} \in F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1] \leftrightarrow (0_{S} \in {Base}_{S} \land F (0_{S}) \in (0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1)))$
68	54 62 67	mpbir2and	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to 0_{S} \in F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1]$
69		eqid	$⊢ MetOpen ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) = MetOpen ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})})$
70	69	mopni2	$⊢ ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})} \in ∞Met ({Base}_{S}) \land F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1] \in MetOpen ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) \land 0_{S} \in F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1]) \to \exists x \in ℝ^{+} 0_{S} ball ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) x \subseteq F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1]$
71	21 50 68 70	syl3anc	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to \exists x \in ℝ^{+} 0_{S} ball ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) x \subseteq F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1]$
72		simpl1	$⊢ ((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \to S \in (NrmMod \cap CMod)$
73	72	elin1d	$⊢ ((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \to S \in NrmMod$
74	73 14	syl	$⊢ ((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \to S \in NrmGrp$
75	74	adantr	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to S \in NrmGrp$
76	75	ad2antrr	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to S \in NrmGrp$
77		ngpgrp	$⊢ S \in NrmGrp \to S \in Grp$
78	76 77	syl	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to S \in Grp$
79		simpr	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to y \in {Base}_{S}$
80		eqid	$⊢ norm (S) = norm (S)$
81		eqid	$⊢ dist (S) = dist (S)$
82	80 18 52 81 19	nmval2	$⊢ (S \in Grp \land y \in {Base}_{S}) \to norm (S) (y) = y ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) 0_{S}$
83	78 79 82	syl2anc	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to norm (S) (y) = y ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) 0_{S}$
84	21	ad2antrr	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to {dist (S) ↾}_{({Base}_{S} \times {Base}_{S})} \in ∞Met ({Base}_{S})$
85	54	ad2antrr	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to 0_{S} \in {Base}_{S}$
86		xmetsym	$⊢ ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})} \in ∞Met ({Base}_{S}) \land y \in {Base}_{S} \land 0_{S} \in {Base}_{S}) \to y ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) 0_{S} = 0_{S} ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y$
87	84 79 85 86	syl3anc	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to y ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) 0_{S} = 0_{S} ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y$
88	83 87	eqtrd	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to norm (S) (y) = 0_{S} ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y$
89	88	breq1d	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to (norm (S) (y) < x \leftrightarrow 0_{S} ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y < x)$
90	89	biimpd	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to (norm (S) (y) < x \to 0_{S} ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y < x)$
91	64	ad2antrr	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to F : {Base}_{S} ⟶ {Base}_{T}$
92		elpreima	$⊢ F Fn {Base}_{S} \to (y \in F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1] \leftrightarrow (y \in {Base}_{S} \land F (y) \in (0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1)))$
93	91 65 92	3syl	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to (y \in F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1] \leftrightarrow (y \in {Base}_{S} \land F (y) \in (0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1)))$
94	32	ad2antrr	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to {dist (T) ↾}_{({Base}_{T} \times {Base}_{T})} \in ∞Met ({Base}_{T})$
95	36	ad2antrr	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to 0_{T} \in {Base}_{T}$
96	37 38	mp1i	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to 1 \in ℝ^{*}$
97		elbl	$⊢ ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})} \in ∞Met ({Base}_{T}) \land 0_{T} \in {Base}_{T} \land 1 \in ℝ^{*}) \to (F (y) \in (0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1) \leftrightarrow (F (y) \in {Base}_{T} \land 0_{T} ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) F (y) < 1))$
98	94 95 96 97	syl3anc	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to (F (y) \in (0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1) \leftrightarrow (F (y) \in {Base}_{T} \land 0_{T} ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) F (y) < 1))$
99		simpl2	$⊢ ((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \to T \in (NrmMod \cap CMod)$
100	99	elin1d	$⊢ ((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \to T \in NrmMod$
101	100 25	syl	$⊢ ((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \to T \in NrmGrp$
102	101	adantr	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to T \in NrmGrp$
103	102	ad2antrr	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to T \in NrmGrp$
104		simplr	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to F \in (S LMHom T)$
105	104	adantr	$⊢ ((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \to F \in (S LMHom T)$
106	105 63	syl	$⊢ ((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \to F : {Base}_{S} ⟶ {Base}_{T}$
107	106	ffvelcdmda	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to F (y) \in {Base}_{T}$
108		eqid	$⊢ norm (T) = norm (T)$
109	29 108	nmcl	$⊢ (T \in NrmGrp \land F (y) \in {Base}_{T}) \to norm (T) (F (y)) \in ℝ$
110	103 107 109	syl2anc	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to norm (T) (F (y)) \in ℝ$
111		1re	$⊢ 1 \in ℝ$
112		ltle	$⊢ (norm (T) (F (y)) \in ℝ \land 1 \in ℝ) \to (norm (T) (F (y)) < 1 \to norm (T) (F (y)) \leq 1)$
113	110 111 112	sylancl	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to (norm (T) (F (y)) < 1 \to norm (T) (F (y)) \leq 1)$
114		ngpgrp	$⊢ T \in NrmGrp \to T \in Grp$
115	103 114	syl	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to T \in Grp$
116		eqid	$⊢ dist (T) = dist (T)$
117	108 29 34 116 30	nmval2	$⊢ (T \in Grp \land F (y) \in {Base}_{T}) \to norm (T) (F (y)) = F (y) ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 0_{T}$
118	115 107 117	syl2anc	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to norm (T) (F (y)) = F (y) ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 0_{T}$
119		xmetsym	$⊢ ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})} \in ∞Met ({Base}_{T}) \land F (y) \in {Base}_{T} \land 0_{T} \in {Base}_{T}) \to F (y) ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 0_{T} = 0_{T} ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) F (y)$
120	94 107 95 119	syl3anc	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to F (y) ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 0_{T} = 0_{T} ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) F (y)$
121	118 120	eqtrd	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to norm (T) (F (y)) = 0_{T} ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) F (y)$
122	121	breq1d	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to (norm (T) (F (y)) < 1 \leftrightarrow 0_{T} ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) F (y) < 1)$
123		1red	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to 1 \in ℝ$
124		simplr	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to x \in ℝ^{+}$
125	110 123 124	lediv1d	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to (norm (T) (F (y)) \leq 1 \leftrightarrow \frac{norm (T) (F (y))}{x} \leq \frac{1}{x})$
126	113 122 125	3imtr3d	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to (0_{T} ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) F (y) < 1 \to \frac{norm (T) (F (y))}{x} \leq \frac{1}{x})$
127	126	adantld	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to ((F (y) \in {Base}_{T} \land 0_{T} ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) F (y) < 1) \to \frac{norm (T) (F (y))}{x} \leq \frac{1}{x})$
128	98 127	sylbid	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to (F (y) \in (0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1) \to \frac{norm (T) (F (y))}{x} \leq \frac{1}{x})$
129	128	adantld	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to ((y \in {Base}_{S} \land F (y) \in (0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1)) \to \frac{norm (T) (F (y))}{x} \leq \frac{1}{x})$
130	93 129	sylbid	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to (y \in F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1] \to \frac{norm (T) (F (y))}{x} \leq \frac{1}{x})$
131	90 130	imim12d	$⊢ (((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \land y \in {Base}_{S}) \to ((0_{S} ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y < x \to y \in F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1]) \to (norm (S) (y) < x \to \frac{norm (T) (F (y))}{x} \leq \frac{1}{x}))$
132	131	ralimdva	$⊢ ((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \to (\forall y \in {Base}_{S} (0_{S} ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y < x \to y \in F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1]) \to \forall y \in {Base}_{S} (norm (S) (y) < x \to \frac{norm (T) (F (y))}{x} \leq \frac{1}{x}))$
133		rpxr	$⊢ x \in ℝ^{+} \to x \in ℝ^{*}$
134		blval	$⊢ ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})} \in ∞Met ({Base}_{S}) \land 0_{S} \in {Base}_{S} \land x \in ℝ^{*}) \to 0_{S} ball ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) x = \{y \in {Base}_{S} \| 0_{S} ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y < x\}$
135	21 54 133 134	syl2an3an	$⊢ ((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \to 0_{S} ball ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) x = \{y \in {Base}_{S} \| 0_{S} ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y < x\}$
136	135	sseq1d	$⊢ ((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \to (0_{S} ball ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) x \subseteq F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1] \leftrightarrow \{y \in {Base}_{S} \| 0_{S} ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y < x\} \subseteq F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1])$
137		rabss	$⊢ \{y \in {Base}_{S} \| 0_{S} ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y < x\} \subseteq F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1] \leftrightarrow \forall y \in {Base}_{S} (0_{S} ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y < x \to y \in F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1])$
138	136 137	bitrdi	$⊢ ((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \to (0_{S} ball ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) x \subseteq F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1] \leftrightarrow \forall y \in {Base}_{S} (0_{S} ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y < x \to y \in F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1]))$
139		eqid	$⊢ S normOp T = S normOp T$
140	12	adantr	$⊢ ((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \to S \in (NrmMod \cap CMod)$
141	23	adantr	$⊢ ((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \to T \in (NrmMod \cap CMod)$
142		rpreccl	$⊢ x \in ℝ^{+} \to \frac{1}{x} \in ℝ^{+}$
143	142	adantl	$⊢ ((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \to \frac{1}{x} \in ℝ^{+}$
144	143	rpxrd	$⊢ ((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \to \frac{1}{x} \in ℝ^{*}$
145		simpr	$⊢ ((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \to x \in ℝ^{+}$
146		simpl3	$⊢ ((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \to ℚ \subseteq B$
147	146	ad2antrr	$⊢ ((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \to ℚ \subseteq B$
148	139 18 80 108 3 4 140 141 105 144 145 147	nmoleub2b	$⊢ ((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \to ((S normOp T) (F) \leq \frac{1}{x} \leftrightarrow \forall y \in {Base}_{S} (norm (S) (y) < x \to \frac{norm (T) (F (y))}{x} \leq \frac{1}{x}))$
149	132 138 148	3imtr4d	$⊢ ((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \to (0_{S} ball ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) x \subseteq F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1] \to (S normOp T) (F) \leq \frac{1}{x})$
150	75 102 56	3jca	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T))$
151	142	rpred	$⊢ x \in ℝ^{+} \to \frac{1}{x} \in ℝ$
152	139	bddnghm	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (\frac{1}{x} \in ℝ \land (S normOp T) (F) \leq \frac{1}{x})) \to F \in (S NGHom T)$
153	152	expr	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land \frac{1}{x} \in ℝ) \to ((S normOp T) (F) \leq \frac{1}{x} \to F \in (S NGHom T))$
154	150 151 153	syl2an	$⊢ ((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \to ((S normOp T) (F) \leq \frac{1}{x} \to F \in (S NGHom T))$
155	149 154	syld	$⊢ ((((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \land x \in ℝ^{+}) \to (0_{S} ball ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) x \subseteq F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1] \to F \in (S NGHom T))$
156	155	rexlimdva	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to (\exists x \in ℝ^{+} 0_{S} ball ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) x \subseteq F^{-1} [0_{T} ball ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) 1] \to F \in (S NGHom T))$
157	71 156	mpd	$⊢ (((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \land F \in (J Cn K)) \to F \in (S NGHom T)$
158	157	ex	$⊢ ((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \to (F \in (J Cn K) \to F \in (S NGHom T))$
159	11 158	impbid2	$⊢ ((S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \land F \in (S LMHom T)) \to (F \in (S NGHom T) \leftrightarrow F \in (J Cn K))$
160	159	pm5.32da	$⊢ (S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \to ((F \in (S LMHom T) \land F \in (S NGHom T)) \leftrightarrow (F \in (S LMHom T) \land F \in (J Cn K)))$
161	10 160	bitrd	$⊢ (S \in (NrmMod \cap CMod) \land T \in (NrmMod \cap CMod) \land ℚ \subseteq B) \to (F \in (S NMHom T) \leftrightarrow (F \in (S LMHom T) \land F \in (J Cn K)))$

Metamath Proof Explorer

Theorem nmhmcn

Proof