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