Theorem blocnilem

Description: Lemma for blocni and lnocni . If a linear operator is continuous at any point, it is bounded. (Contributed by NM, 17-Dec-2007) (Revised by Mario Carneiro, 10-Jan-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	blocni.8	⊢ 𝐶 = ( IndMet ‘ 𝑈 )
	blocni.d	⊢ 𝐷 = ( IndMet ‘ 𝑊 )
	blocni.j	⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
	blocni.k	⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
	blocni.4	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
	blocni.5	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
	blocni.u	⊢ 𝑈 ∈ NrmCVec
	blocni.w	⊢ 𝑊 ∈ NrmCVec
	blocni.l	⊢ 𝑇 ∈ 𝐿
	blocnilem.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
Assertion	blocnilem	⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝑇 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		blocni.8	⊢ 𝐶 = ( IndMet ‘ 𝑈 )
2		blocni.d	⊢ 𝐷 = ( IndMet ‘ 𝑊 )
3		blocni.j	⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
4		blocni.k	⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
5		blocni.4	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
6		blocni.5	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
7		blocni.u	⊢ 𝑈 ∈ NrmCVec
8		blocni.w	⊢ 𝑊 ∈ NrmCVec
9		blocni.l	⊢ 𝑇 ∈ 𝐿
10		blocnilem.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
11	10 1	imsxmet	⊢ ( 𝑈 ∈ NrmCVec → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
12	7 11	ax-mp	⊢ 𝐶 ∈ ( ∞Met ‘ 𝑋 )
13		eqid	⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
14	13 2	imsxmet	⊢ ( 𝑊 ∈ NrmCVec → 𝐷 ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑊 ) ) )
15	8 14	ax-mp	⊢ 𝐷 ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑊 ) )
16		1rp	⊢ 1 ∈ ℝ+
17	3 4	metcnpi3	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑊 ) ) ) ∧ ( 𝑇 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 1 ∈ ℝ+ ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐶 𝑃 ) ≤ 𝑦 → ( ( 𝑇 ‘ 𝑥 ) 𝐷 ( 𝑇 ‘ 𝑃 ) ) ≤ 1 ) )
18	16 17	mpanr2	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑊 ) ) ) ∧ 𝑇 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐶 𝑃 ) ≤ 𝑦 → ( ( 𝑇 ‘ 𝑥 ) 𝐷 ( 𝑇 ‘ 𝑃 ) ) ≤ 1 ) )
19	12 15 18	mpanl12	⊢ ( 𝑇 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐶 𝑃 ) ≤ 𝑦 → ( ( 𝑇 ‘ 𝑥 ) 𝐷 ( 𝑇 ‘ 𝑃 ) ) ≤ 1 ) )
20		rpreccl	⊢ ( 𝑦 ∈ ℝ+ → ( 1 / 𝑦 ) ∈ ℝ+ )
21	20	rpred	⊢ ( 𝑦 ∈ ℝ+ → ( 1 / 𝑦 ) ∈ ℝ )
22	21	ad2antlr	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐶 𝑃 ) ≤ 𝑦 → ( ( 𝑇 ‘ 𝑥 ) 𝐷 ( 𝑇 ‘ 𝑃 ) ) ≤ 1 ) ) → ( 1 / 𝑦 ) ∈ ℝ )
23		eqid	⊢ ( −𝑣 ‘ 𝑈 ) = ( −𝑣 ‘ 𝑈 )
24		eqid	⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
25	10 23 24 1	imsdval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑥 𝐶 𝑃 ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) )
26	7 25	mp3an1	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑥 𝐶 𝑃 ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) )
27	26	breq1d	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝑥 𝐶 𝑃 ) ≤ 𝑦 ↔ ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 ) )
28	10 13 5	lnof	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
29	7 8 9 28	mp3an	⊢ 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 )
30	29	ffvelcdmi	⊢ ( 𝑥 ∈ 𝑋 → ( 𝑇 ‘ 𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) )
31	29	ffvelcdmi	⊢ ( 𝑃 ∈ 𝑋 → ( 𝑇 ‘ 𝑃 ) ∈ ( BaseSet ‘ 𝑊 ) )
32		eqid	⊢ ( −𝑣 ‘ 𝑊 ) = ( −𝑣 ‘ 𝑊 )
33		eqid	⊢ ( normCV ‘ 𝑊 ) = ( normCV ‘ 𝑊 )
34	13 32 33 2	imsdval	⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑇 ‘ 𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) ∧ ( 𝑇 ‘ 𝑃 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( ( 𝑇 ‘ 𝑥 ) 𝐷 ( 𝑇 ‘ 𝑃 ) ) = ( ( normCV ‘ 𝑊 ) ‘ ( ( 𝑇 ‘ 𝑥 ) ( −𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝑃 ) ) ) )
35	8 34	mp3an1	⊢ ( ( ( 𝑇 ‘ 𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) ∧ ( 𝑇 ‘ 𝑃 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( ( 𝑇 ‘ 𝑥 ) 𝐷 ( 𝑇 ‘ 𝑃 ) ) = ( ( normCV ‘ 𝑊 ) ‘ ( ( 𝑇 ‘ 𝑥 ) ( −𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝑃 ) ) ) )
36	30 31 35	syl2an	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝑇 ‘ 𝑥 ) 𝐷 ( 𝑇 ‘ 𝑃 ) ) = ( ( normCV ‘ 𝑊 ) ‘ ( ( 𝑇 ‘ 𝑥 ) ( −𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝑃 ) ) ) )
37	7 8 9	3pm3.2i	⊢ ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 )
38	10 23 32 5	lnosub	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( −𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝑃 ) ) )
39	37 38	mpan	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( −𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝑃 ) ) )
40	39	fveq2d	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) = ( ( normCV ‘ 𝑊 ) ‘ ( ( 𝑇 ‘ 𝑥 ) ( −𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝑃 ) ) ) )
41	36 40	eqtr4d	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝑇 ‘ 𝑥 ) 𝐷 ( 𝑇 ‘ 𝑃 ) ) = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) )
42	41	breq1d	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( ( ( 𝑇 ‘ 𝑥 ) 𝐷 ( 𝑇 ‘ 𝑃 ) ) ≤ 1 ↔ ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ) )
43	27 42	imbi12d	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( ( ( 𝑥 𝐶 𝑃 ) ≤ 𝑦 → ( ( 𝑇 ‘ 𝑥 ) 𝐷 ( 𝑇 ‘ 𝑃 ) ) ≤ 1 ) ↔ ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ) ) )
44	43	ancoms	⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑥 𝐶 𝑃 ) ≤ 𝑦 → ( ( 𝑇 ‘ 𝑥 ) 𝐷 ( 𝑇 ‘ 𝑃 ) ) ≤ 1 ) ↔ ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ) ) )
45	44	adantlr	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑥 𝐶 𝑃 ) ≤ 𝑦 → ( ( 𝑇 ‘ 𝑥 ) 𝐷 ( 𝑇 ‘ 𝑃 ) ) ≤ 1 ) ↔ ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ) ) )
46	45	ralbidva	⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) → ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐶 𝑃 ) ≤ 𝑦 → ( ( 𝑇 ‘ 𝑥 ) 𝐷 ( 𝑇 ‘ 𝑃 ) ) ≤ 1 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ) ) )
47		2fveq3	⊢ ( 𝑧 = ( 0vec ‘ 𝑈 ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) )
48		fveq2	⊢ ( 𝑧 = ( 0vec ‘ 𝑈 ) → ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) = ( ( normCV ‘ 𝑈 ) ‘ ( 0vec ‘ 𝑈 ) ) )
49	48	oveq2d	⊢ ( 𝑧 = ( 0vec ‘ 𝑈 ) → ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) = ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ ( 0vec ‘ 𝑈 ) ) ) )
50	47 49	breq12d	⊢ ( 𝑧 = ( 0vec ‘ 𝑈 ) → ( ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ↔ ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) ≤ ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ ( 0vec ‘ 𝑈 ) ) ) ) )
51	7	a1i	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → 𝑈 ∈ NrmCVec )
52		simpll	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → 𝑃 ∈ 𝑋 )
53		simpr	⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ+ )
54	10 24	nvcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ) → ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ∈ ℝ )
55	7 54	mpan	⊢ ( 𝑧 ∈ 𝑋 → ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ∈ ℝ )
56	55	adantr	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) → ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ∈ ℝ )
57		eqid	⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
58	10 57 24	nvgt0	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ≠ ( 0vec ‘ 𝑈 ) ↔ 0 < ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) )
59	7 58	mpan	⊢ ( 𝑧 ∈ 𝑋 → ( 𝑧 ≠ ( 0vec ‘ 𝑈 ) ↔ 0 < ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) )
60	59	biimpa	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) → 0 < ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) )
61	56 60	elrpd	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) → ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ∈ ℝ+ )
62		rpdivcl	⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ∈ ℝ+ ) → ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ∈ ℝ+ )
63	53 61 62	syl2an	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ∈ ℝ+ )
64	63	rpcnd	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ∈ ℂ )
65		simprl	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → 𝑧 ∈ 𝑋 )
66		eqid	⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
67	10 66	nvscl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ∈ ℂ ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ∈ 𝑋 )
68	51 64 65 67	syl3anc	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ∈ 𝑋 )
69		eqid	⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
70	10 69 23	nvpncan2	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ∈ 𝑋 ) → ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) = ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) )
71	51 52 68 70	syl3anc	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) = ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) )
72	71	fveq2d	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ( normCV ‘ 𝑈 ) ‘ ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) = ( ( normCV ‘ 𝑈 ) ‘ ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) )
73	63	rprege0d	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) )
74	10 66 24	nvsge0	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( normCV ‘ 𝑈 ) ‘ ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) = ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) )
75	51 73 65 74	syl3anc	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ( normCV ‘ 𝑈 ) ‘ ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) = ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) )
76		rpcn	⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℂ )
77	76	ad2antlr	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → 𝑦 ∈ ℂ )
78	55	ad2antrl	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ∈ ℝ )
79	78	recnd	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ∈ ℂ )
80	10 57 24	nvz	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) = 0 ↔ 𝑧 = ( 0vec ‘ 𝑈 ) ) )
81	7 80	mpan	⊢ ( 𝑧 ∈ 𝑋 → ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) = 0 ↔ 𝑧 = ( 0vec ‘ 𝑈 ) ) )
82	81	necon3bid	⊢ ( 𝑧 ∈ 𝑋 → ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≠ 0 ↔ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) )
83	82	biimpar	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) → ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≠ 0 )
84	83	adantl	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≠ 0 )
85	77 79 84	divcan1d	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) = 𝑦 )
86	72 75 85	3eqtrd	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ( normCV ‘ 𝑈 ) ‘ ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) = 𝑦 )
87		rpre	⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ )
88	87	leidd	⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ≤ 𝑦 )
89	88	ad2antlr	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → 𝑦 ≤ 𝑦 )
90	86 89	eqbrtrd	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ( normCV ‘ 𝑈 ) ‘ ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 )
91	10 69	nvgcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ∈ 𝑋 ) → ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ∈ 𝑋 )
92	51 52 68 91	syl3anc	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ∈ 𝑋 )
93		fvoveq1	⊢ ( 𝑥 = ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) → ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) = ( ( normCV ‘ 𝑈 ) ‘ ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) )
94	93	breq1d	⊢ ( 𝑥 = ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 ↔ ( ( normCV ‘ 𝑈 ) ‘ ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 ) )
95		fvoveq1	⊢ ( 𝑥 = ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) → ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) = ( 𝑇 ‘ ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) )
96	95	fveq2d	⊢ ( 𝑥 = ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) )
97	96	breq1d	⊢ ( 𝑥 = ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) → ( ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ↔ ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ) )
98	94 97	imbi12d	⊢ ( 𝑥 = ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) → ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ) ↔ ( ( ( normCV ‘ 𝑈 ) ‘ ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ) ) )
99	98	rspcv	⊢ ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ∈ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ) ) )
100	92 99	syl	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ∀ 𝑥 ∈ 𝑋 ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ) ) )
101	90 100	mpid	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ∀ 𝑥 ∈ 𝑋 ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ) )
102	29	ffvelcdmi	⊢ ( 𝑧 ∈ 𝑋 → ( 𝑇 ‘ 𝑧 ) ∈ ( BaseSet ‘ 𝑊 ) )
103	13 33	nvcl	⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑇 ‘ 𝑧 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ∈ ℝ )
104	8 102 103	sylancr	⊢ ( 𝑧 ∈ 𝑋 → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ∈ ℝ )
105	104	ad2antrl	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ∈ ℝ )
106		1red	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → 1 ∈ ℝ )
107	105 106 63	lemuldiv2d	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) · ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) ≤ 1 ↔ ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( 1 / ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) ) )
108	71	fveq2d	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( 𝑇 ‘ ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) = ( 𝑇 ‘ ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) )
109		eqid	⊢ ( ·𝑠OLD ‘ 𝑊 ) = ( ·𝑠OLD ‘ 𝑊 )
110	10 66 109 5	lnomul	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ∈ ℂ ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) = ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝑧 ) ) )
111	37 110	mpan	⊢ ( ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ∈ ℂ ∧ 𝑧 ∈ 𝑋 ) → ( 𝑇 ‘ ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) = ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝑧 ) ) )
112	64 65 111	syl2anc	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( 𝑇 ‘ ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) = ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝑧 ) ) )
113	108 112	eqtrd	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( 𝑇 ‘ ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) = ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝑧 ) ) )
114	113	fveq2d	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) = ( ( normCV ‘ 𝑊 ) ‘ ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝑧 ) ) ) )
115	8	a1i	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → 𝑊 ∈ NrmCVec )
116	102	ad2antrl	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( 𝑇 ‘ 𝑧 ) ∈ ( BaseSet ‘ 𝑊 ) )
117	13 109 33	nvsge0	⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) ∧ ( 𝑇 ‘ 𝑧 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( ( normCV ‘ 𝑊 ) ‘ ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝑧 ) ) ) = ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) · ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) )
118	115 73 116 117	syl3anc	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ( normCV ‘ 𝑊 ) ‘ ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝑧 ) ) ) = ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) · ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) )
119	114 118	eqtrd	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) = ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) · ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) )
120	119	breq1d	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ↔ ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) · ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) ≤ 1 ) )
121		rpcnne0	⊢ ( 𝑦 ∈ ℝ+ → ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
122		rpcnne0	⊢ ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ∈ ℝ+ → ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ∈ ℂ ∧ ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≠ 0 ) )
123		recdiv	⊢ ( ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ∧ ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ∈ ℂ ∧ ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≠ 0 ) ) → ( 1 / ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) = ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) / 𝑦 ) )
124	121 122 123	syl2an	⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ∈ ℝ+ ) → ( 1 / ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) = ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) / 𝑦 ) )
125	53 61 124	syl2an	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( 1 / ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) = ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) / 𝑦 ) )
126		rpne0	⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ≠ 0 )
127	126	ad2antlr	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → 𝑦 ≠ 0 )
128	79 77 127	divrec2d	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) / 𝑦 ) = ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) )
129	125 128	eqtr2d	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) = ( 1 / ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) )
130	129	breq2d	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ↔ ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( 1 / ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) ) )
131	107 120 130	3bitr4d	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( ( 𝑦 / ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ) ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ↔ ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) )
132	101 131	sylibd	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ) → ( ∀ 𝑥 ∈ 𝑋 ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) )
133	132	anassrs	⊢ ( ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) → ( ∀ 𝑥 ∈ 𝑋 ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) )
134	133	imp	⊢ ( ( ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ) ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) )
135	134	an32s	⊢ ( ( ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ) ) ∧ 𝑧 ≠ ( 0vec ‘ 𝑈 ) ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) )
136		eqid	⊢ ( 0vec ‘ 𝑊 ) = ( 0vec ‘ 𝑊 )
137	10 13 57 136 5	lno0	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) = ( 0vec ‘ 𝑊 ) )
138	7 8 9 137	mp3an	⊢ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) = ( 0vec ‘ 𝑊 )
139	138	fveq2i	⊢ ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) = ( ( normCV ‘ 𝑊 ) ‘ ( 0vec ‘ 𝑊 ) )
140	136 33	nvz0	⊢ ( 𝑊 ∈ NrmCVec → ( ( normCV ‘ 𝑊 ) ‘ ( 0vec ‘ 𝑊 ) ) = 0 )
141	8 140	ax-mp	⊢ ( ( normCV ‘ 𝑊 ) ‘ ( 0vec ‘ 𝑊 ) ) = 0
142	139 141	eqtri	⊢ ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) = 0
143		0le0	⊢ 0 ≤ 0
144	142 143	eqbrtri	⊢ ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) ≤ 0
145	20	rpcnd	⊢ ( 𝑦 ∈ ℝ+ → ( 1 / 𝑦 ) ∈ ℂ )
146	57 24	nvz0	⊢ ( 𝑈 ∈ NrmCVec → ( ( normCV ‘ 𝑈 ) ‘ ( 0vec ‘ 𝑈 ) ) = 0 )
147	7 146	ax-mp	⊢ ( ( normCV ‘ 𝑈 ) ‘ ( 0vec ‘ 𝑈 ) ) = 0
148	147	oveq2i	⊢ ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ ( 0vec ‘ 𝑈 ) ) ) = ( ( 1 / 𝑦 ) · 0 )
149		mul01	⊢ ( ( 1 / 𝑦 ) ∈ ℂ → ( ( 1 / 𝑦 ) · 0 ) = 0 )
150	148 149	eqtrid	⊢ ( ( 1 / 𝑦 ) ∈ ℂ → ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ ( 0vec ‘ 𝑈 ) ) ) = 0 )
151	145 150	syl	⊢ ( 𝑦 ∈ ℝ+ → ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ ( 0vec ‘ 𝑈 ) ) ) = 0 )
152	144 151	breqtrrid	⊢ ( 𝑦 ∈ ℝ+ → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) ≤ ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ ( 0vec ‘ 𝑈 ) ) ) )
153	152	ad3antlr	⊢ ( ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ) ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) ≤ ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ ( 0vec ‘ 𝑈 ) ) ) )
154	50 135 153	pm2.61ne	⊢ ( ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ) ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) )
155	154	ex	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) )
156	155	ralrimdva	⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) → ( ∀ 𝑥 ∈ 𝑋 ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ≤ 𝑦 → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑥 ( −𝑣 ‘ 𝑈 ) 𝑃 ) ) ) ≤ 1 ) → ∀ 𝑧 ∈ 𝑋 ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) )
157	46 156	sylbid	⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) → ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐶 𝑃 ) ≤ 𝑦 → ( ( 𝑇 ‘ 𝑥 ) 𝐷 ( 𝑇 ‘ 𝑃 ) ) ≤ 1 ) → ∀ 𝑧 ∈ 𝑋 ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) )
158	157	imp	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐶 𝑃 ) ≤ 𝑦 → ( ( 𝑇 ‘ 𝑥 ) 𝐷 ( 𝑇 ‘ 𝑃 ) ) ≤ 1 ) ) → ∀ 𝑧 ∈ 𝑋 ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) )
159		oveq1	⊢ ( 𝑥 = ( 1 / 𝑦 ) → ( 𝑥 · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) = ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) )
160	159	breq2d	⊢ ( 𝑥 = ( 1 / 𝑦 ) → ( ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( 𝑥 · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ↔ ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) )
161	160	ralbidv	⊢ ( 𝑥 = ( 1 / 𝑦 ) → ( ∀ 𝑧 ∈ 𝑋 ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( 𝑥 · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝑋 ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) )
162	161	rspcev	⊢ ( ( ( 1 / 𝑦 ) ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( ( 1 / 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑋 ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( 𝑥 · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) )
163	22 158 162	syl2anc	⊢ ( ( ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐶 𝑃 ) ≤ 𝑦 → ( ( 𝑇 ‘ 𝑥 ) 𝐷 ( 𝑇 ‘ 𝑃 ) ) ≤ 1 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑋 ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( 𝑥 · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) )
164	163	rexlimdva2	⊢ ( 𝑃 ∈ 𝑋 → ( ∃ 𝑦 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐶 𝑃 ) ≤ 𝑦 → ( ( 𝑇 ‘ 𝑥 ) 𝐷 ( 𝑇 ‘ 𝑃 ) ) ≤ 1 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑋 ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( 𝑥 · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) )
165	19 164	syl5	⊢ ( 𝑃 ∈ 𝑋 → ( 𝑇 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑋 ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( 𝑥 · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) )
166	165	imp	⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑋 ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( 𝑥 · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) )
167	10 24 33 5 6 7 8	isblo3i	⊢ ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ 𝐿 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑋 ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( 𝑥 · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) )
168	9 167	mpbiran	⊢ ( 𝑇 ∈ 𝐵 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑋 ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( 𝑥 · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) )
169	166 168	sylibr	⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝑇 ∈ 𝐵 )