Theorem blocnilem 28575

Description: Lemma for blocni 28576 and lnocni 28577. 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.)

Hypotheses

Ref	Expression
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

Ref	Expression
blocnilem	⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑇 ∈ 𝐵)

Proof of Theorem blocnilem

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		blocni.u	. . . . . 6 ⊢ 𝑈 ∈ NrmCVec
2		blocnilem.1	. . . . . . 7 ⊢ 𝑋 = (BaseSet‘𝑈)
3		blocni.8	. . . . . . 7 ⊢ 𝐶 = (IndMet‘𝑈)
4	2, 3	imsxmet 28463	. . . . . 6 ⊢ (𝑈 ∈ NrmCVec → 𝐶 ∈ (∞Met‘𝑋))
5	1, 4	ax-mp 5	. . . . 5 ⊢ 𝐶 ∈ (∞Met‘𝑋)
6		blocni.w	. . . . . 6 ⊢ 𝑊 ∈ NrmCVec
7		eqid 2821	. . . . . . 7 ⊢ (BaseSet‘𝑊) = (BaseSet‘𝑊)
8		blocni.d	. . . . . . 7 ⊢ 𝐷 = (IndMet‘𝑊)
9	7, 8	imsxmet 28463	. . . . . 6 ⊢ (𝑊 ∈ NrmCVec → 𝐷 ∈ (∞Met‘(BaseSet‘𝑊)))
10	6, 9	ax-mp 5	. . . . 5 ⊢ 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))
11		1rp 12387	. . . . . 6 ⊢ 1 ∈ ℝ+
12		blocni.j	. . . . . . 7 ⊢ 𝐽 = (MetOpen‘𝐶)
13		blocni.k	. . . . . . 7 ⊢ 𝐾 = (MetOpen‘𝐷)
14	12, 13	metcnpi3 23150	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))) ∧ (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 1 ∈ ℝ+)) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1))
15	11, 14	mpanr2 702	. . . . 5 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))) ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1))
16	5, 10, 15	mpanl12 700	. . . 4 ⊢ (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1))
17		rpreccl 12409	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℝ+)
18	17	rpred 12425	. . . . . . 7 ⊢ (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℝ)
19	18	ad2antlr 725	. . . . . 6 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → (1 / 𝑦) ∈ ℝ)
20		eqid 2821	. . . . . . . . . . . . . . 15 ⊢ ( −𝑣 ‘𝑈) = ( −𝑣 ‘𝑈)
21		eqid 2821	. . . . . . . . . . . . . . 15 ⊢ (normCV‘𝑈) = (normCV‘𝑈)
22	2, 20, 21, 3	imsdval 28457	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑥𝐶𝑃) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)))
23	1, 22	mp3an1 1444	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑥𝐶𝑃) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)))
24	23	breq1d 5068	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑥𝐶𝑃) ≤ 𝑦 ↔ ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦))
25		blocni.l	. . . . . . . . . . . . . . . . 17 ⊢ 𝑇 ∈ 𝐿
26		blocni.4	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐿 = (𝑈 LnOp 𝑊)
27	2, 7, 26	lnof 28526	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶(BaseSet‘𝑊))
28	1, 6, 25, 27	mp3an 1457	. . . . . . . . . . . . . . . 16 ⊢ 𝑇:𝑋⟶(BaseSet‘𝑊)
29	28	ffvelrni 6844	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝑋 → (𝑇‘𝑥) ∈ (BaseSet‘𝑊))
30	28	ffvelrni 6844	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ 𝑋 → (𝑇‘𝑃) ∈ (BaseSet‘𝑊))
31		eqid 2821	. . . . . . . . . . . . . . . . 17 ⊢ ( −𝑣 ‘𝑊) = ( −𝑣 ‘𝑊)
32		eqid 2821	. . . . . . . . . . . . . . . . 17 ⊢ (normCV‘𝑊) = (normCV‘𝑊)
33	7, 31, 32, 8	imsdval 28457	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇‘𝑃) ∈ (BaseSet‘𝑊)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))))
34	6, 33	mp3an1 1444	. . . . . . . . . . . . . . 15 ⊢ (((𝑇‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇‘𝑃) ∈ (BaseSet‘𝑊)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))))
35	29, 30, 34	syl2an 597	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))))
36	1, 6, 25	3pm3.2i 1335	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿)
37	2, 20, 31, 26	lnosub 28530	. . . . . . . . . . . . . . . 16 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋)) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))
38	36, 37	mpan 688	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))
39	38	fveq2d 6668	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))))
40	35, 39	eqtr4d 2859	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))))
41	40	breq1d 5068	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1 ↔ ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1))
42	24, 41	imbi12d 347	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔ (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)))
43	42	ancoms 461	. . . . . . . . . 10 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔ (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)))
44	43	adantlr 713	. . . . . . . . 9 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔ (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)))
45	44	ralbidva 3196	. . . . . . . 8 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) → (∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)))
46		2fveq3 6669	. . . . . . . . . . . 12 ⊢ (𝑧 = (0vec‘𝑈) → ((normCV‘𝑊)‘(𝑇‘𝑧)) = ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))))
47		fveq2 6664	. . . . . . . . . . . . 13 ⊢ (𝑧 = (0vec‘𝑈) → ((normCV‘𝑈)‘𝑧) = ((normCV‘𝑈)‘(0vec‘𝑈)))
48	47	oveq2d 7166	. . . . . . . . . . . 12 ⊢ (𝑧 = (0vec‘𝑈) → ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) = ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))))
49	46, 48	breq12d 5071	. . . . . . . . . . 11 ⊢ (𝑧 = (0vec‘𝑈) → (((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈)))))
50	1	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑈 ∈ NrmCVec)
51		simpll 765	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑃 ∈ 𝑋)
52		simpr 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ+)
53	2, 21	nvcl 28432	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → ((normCV‘𝑈)‘𝑧) ∈ ℝ)
54	1, 53	mpan 688	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ 𝑋 → ((normCV‘𝑈)‘𝑧) ∈ ℝ)
55	54	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) → ((normCV‘𝑈)‘𝑧) ∈ ℝ)
56		eqid 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0vec‘𝑈) = (0vec‘𝑈)
57	2, 56, 21	nvgt0 28445	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → (𝑧 ≠ (0vec‘𝑈) ↔ 0 < ((normCV‘𝑈)‘𝑧)))
58	1, 57	mpan 688	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ 𝑋 → (𝑧 ≠ (0vec‘𝑈) ↔ 0 < ((normCV‘𝑈)‘𝑧)))
59	58	biimpa 479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) → 0 < ((normCV‘𝑈)‘𝑧))
60	55, 59	elrpd 12422	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) → ((normCV‘𝑈)‘𝑧) ∈ ℝ+)
61		rpdivcl 12408	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ ℝ+ ∧ ((normCV‘𝑈)‘𝑧) ∈ ℝ+) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ+)
62	52, 60, 61	syl2an 597	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ+)
63	62	rpcnd 12427	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ)
64		simprl 769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑧 ∈ 𝑋)
65		eqid 2821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( ·𝑠OLD ‘𝑈) = ( ·𝑠OLD ‘𝑈)
66	2, 65	nvscl 28397	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋) → ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧) ∈ 𝑋)
67	50, 63, 64, 66	syl3anc 1367	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧) ∈ 𝑋)
68		eqid 2821	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ( +𝑣 ‘𝑈) = ( +𝑣 ‘𝑈)
69	2, 68, 20	nvpncan2 28424	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧) ∈ 𝑋) → ((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))
70	50, 51, 67, 69	syl3anc 1367	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))
71	70	fveq2d 6668	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = ((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)))
72	62	rprege0d 12432	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 / ((normCV‘𝑈)‘𝑧))))
73	2, 65, 21	nvsge0 28435	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 ∈ NrmCVec ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 / ((normCV‘𝑈)‘𝑧))) ∧ 𝑧 ∈ 𝑋) → ((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧)))
74	50, 72, 64, 73	syl3anc 1367	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧)))
75		rpcn 12393	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℂ)
76	75	ad2antlr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ∈ ℂ)
77	54	ad2antrl 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘𝑧) ∈ ℝ)
78	77	recnd 10663	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘𝑧) ∈ ℂ)
79	2, 56, 21	nvz 28440	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → (((normCV‘𝑈)‘𝑧) = 0 ↔ 𝑧 = (0vec‘𝑈)))
80	1, 79	mpan 688	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ 𝑋 → (((normCV‘𝑈)‘𝑧) = 0 ↔ 𝑧 = (0vec‘𝑈)))
81	80	necon3bid 3060	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ 𝑋 → (((normCV‘𝑈)‘𝑧) ≠ 0 ↔ 𝑧 ≠ (0vec‘𝑈)))
82	81	biimpar 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) → ((normCV‘𝑈)‘𝑧) ≠ 0)
83	82	adantl 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘𝑧) ≠ 0)
84	76, 78, 83	divcan1d 11411	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧)) = 𝑦)
85	71, 74, 84	3eqtrd 2860	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = 𝑦)
86		rpre 12391	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
87	86	leidd 11200	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ≤ 𝑦)
88	87	ad2antlr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ≤ 𝑦)
89	85, 88	eqbrtrd 5080	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦)
90	2, 68	nvgcl 28391	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧) ∈ 𝑋) → (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) ∈ 𝑋)
91	50, 51, 67, 90	syl3anc 1367	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) ∈ 𝑋)
92		fvoveq1 7173	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)))
93	92	breq1d 5068	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 ↔ ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦))
94		fvoveq1 7173	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)))
95	94	fveq2d 6668	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))))
96	95	breq1d 5068	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → (((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1 ↔ ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1))
97	93, 96	imbi12d 347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → ((((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) ↔ (((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1)))
98	97	rspcv 3617	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) → (((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1)))
99	91, 98	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) → (((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1)))
100	89, 99	mpid 44	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1))
101	28	ffvelrni 6844	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑋 → (𝑇‘𝑧) ∈ (BaseSet‘𝑊))
102	7, 32	nvcl 28432	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ)
103	6, 101, 102	sylancr 589	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑋 → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ)
104	103	ad2antrl 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ)
105		1red 10636	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 1 ∈ ℝ)
106	104, 105, 62	lemuldiv2d 12475	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))) ≤ 1 ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (1 / (𝑦 / ((normCV‘𝑈)‘𝑧)))))
107	70	fveq2d 6668	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)))
108		eqid 2821	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ( ·𝑠OLD ‘𝑊) = ( ·𝑠OLD ‘𝑊)
109	2, 65, 108, 26	lnomul 28531	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋)) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧)))
110	36, 109	mpan 688	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧)))
111	63, 64, 110	syl2anc 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧)))
112	107, 111	eqtrd 2856	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧)))
113	112	fveq2d 6668	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧))))
114	6	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑊 ∈ NrmCVec)
115	101	ad2antrl 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘𝑧) ∈ (BaseSet‘𝑊))
116	7, 108, 32	nvsge0 28435	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ NrmCVec ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 / ((normCV‘𝑈)‘𝑧))) ∧ (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))))
117	114, 72, 115, 116	syl3anc 1367	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑊)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))))
118	113, 117	eqtrd 2856	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))))
119	118	breq1d 5068	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1 ↔ ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))) ≤ 1))
120		rpcnne0 12401	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℝ+ → (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0))
121		rpcnne0 12401	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((normCV‘𝑈)‘𝑧) ∈ ℝ+ → (((normCV‘𝑈)‘𝑧) ∈ ℂ ∧ ((normCV‘𝑈)‘𝑧) ≠ 0))
122		recdiv 11340	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) ∧ (((normCV‘𝑈)‘𝑧) ∈ ℂ ∧ ((normCV‘𝑈)‘𝑧) ≠ 0)) → (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))) = (((normCV‘𝑈)‘𝑧) / 𝑦))
123	120, 121, 122	syl2an 597	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ℝ+ ∧ ((normCV‘𝑈)‘𝑧) ∈ ℝ+) → (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))) = (((normCV‘𝑈)‘𝑧) / 𝑦))
124	52, 60, 123	syl2an 597	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))) = (((normCV‘𝑈)‘𝑧) / 𝑦))
125		rpne0 12399	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ≠ 0)
126	125	ad2antlr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ≠ 0)
127	78, 76, 126	divrec2d 11414	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((normCV‘𝑈)‘𝑧) / 𝑦) = ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
128	124, 127	eqtr2d 2857	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) = (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))))
129	128	breq2d 5070	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (1 / (𝑦 / ((normCV‘𝑈)‘𝑧)))))
130	106, 119, 129	3bitr4d 313	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1 ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
131	100, 130	sylibd 241	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
132	131	anassrs 470	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 ≠ (0vec‘𝑈)) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
133	132	imp 409	. . . . . . . . . . . 12 ⊢ (((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 ≠ (0vec‘𝑈)) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
134	133	an32s 650	. . . . . . . . . . 11 ⊢ (((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) ∧ 𝑧 ≠ (0vec‘𝑈)) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
135		eqid 2821	. . . . . . . . . . . . . . . . . 18 ⊢ (0vec‘𝑊) = (0vec‘𝑊)
136	2, 7, 56, 135, 26	lno0 28527	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇‘(0vec‘𝑈)) = (0vec‘𝑊))
137	1, 6, 25, 136	mp3an 1457	. . . . . . . . . . . . . . . 16 ⊢ (𝑇‘(0vec‘𝑈)) = (0vec‘𝑊)
138	137	fveq2i 6667	. . . . . . . . . . . . . . 15 ⊢ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) = ((normCV‘𝑊)‘(0vec‘𝑊))
139	135, 32	nvz0 28439	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 ∈ NrmCVec → ((normCV‘𝑊)‘(0vec‘𝑊)) = 0)
140	6, 139	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((normCV‘𝑊)‘(0vec‘𝑊)) = 0
141	138, 140	eqtri 2844	. . . . . . . . . . . . . 14 ⊢ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) = 0
142		0le0 11732	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 0
143	141, 142	eqbrtri 5079	. . . . . . . . . . . . 13 ⊢ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ 0
144	17	rpcnd 12427	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℂ)
145	56, 21	nvz0 28439	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ NrmCVec → ((normCV‘𝑈)‘(0vec‘𝑈)) = 0)
146	1, 145	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((normCV‘𝑈)‘(0vec‘𝑈)) = 0
147	146	oveq2i 7161	. . . . . . . . . . . . . . 15 ⊢ ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))) = ((1 / 𝑦) · 0)
148		mul01 10813	. . . . . . . . . . . . . . 15 ⊢ ((1 / 𝑦) ∈ ℂ → ((1 / 𝑦) · 0) = 0)
149	147, 148	syl5eq 2868	. . . . . . . . . . . . . 14 ⊢ ((1 / 𝑦) ∈ ℂ → ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))) = 0)
150	144, 149	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ+ → ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))) = 0)
151	143, 150	breqtrrid 5096	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ+ → ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))))
152	151	ad3antlr 729	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) → ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))))
153	49, 134, 152	pm2.61ne 3102	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
154	153	ex 415	. . . . . . . . 9 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
155	154	ralrimdva 3189	. . . . . . . 8 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
156	45, 155	sylbid 242	. . . . . . 7 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) → (∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
157	156	imp 409	. . . . . 6 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
158		oveq1 7157	. . . . . . . . 9 ⊢ (𝑥 = (1 / 𝑦) → (𝑥 · ((normCV‘𝑈)‘𝑧)) = ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
159	158	breq2d 5070	. . . . . . . 8 ⊢ (𝑥 = (1 / 𝑦) → (((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
160	159	ralbidv 3197	. . . . . . 7 ⊢ (𝑥 = (1 / 𝑦) → (∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)) ↔ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
161	160	rspcev 3622	. . . . . 6 ⊢ (((1 / 𝑦) ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))
162	19, 157, 161	syl2anc 586	. . . . 5 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))
163	162	rexlimdva2 3287	. . . 4 ⊢ (𝑃 ∈ 𝑋 → (∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))))
164	16, 163	syl5 34	. . 3 ⊢ (𝑃 ∈ 𝑋 → (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))))
165	164	imp 409	. 2 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))
166		blocni.5	. . . 4 ⊢ 𝐵 = (𝑈 BLnOp 𝑊)
167	2, 21, 32, 26, 166, 1, 6	isblo3i 28572	. . 3 ⊢ (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))))
168	25, 167	mpbiran 707	. 2 ⊢ (𝑇 ∈ 𝐵 ↔ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))
169	165, 168	sylibr 236	1 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑇 ∈ 𝐵)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110   ≠ wne 3016  ∀wral 3138  ∃wrex 3139   class class class wbr 5058  ⟶wf 6345  ‘cfv 6349  (class class class)co 7150  ℂcc 10529  ℝcr 10530  0cc0 10531  1c1 10532   · cmul 10536   < clt 10669   ≤ cle 10670   / cdiv 11291  ℝ⁺crp 12383  ∞Metcxmet 20524  MetOpencmopn 20529   CnP ccnp 21827  NrmCVeccnv 28355   +_𝑣 cpv 28356  BaseSetcba 28357   ·_𝑠OLD cns 28358  0_veccn0v 28359   −_𝑣 cnsb 28360  norm_CVcnmcv 28361  IndMetcims 28362   LnOp clno 28511   BLnOp cblo 28513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609  ax-addf 10610  ax-mulf 10611

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-er 8283  df-map 8402  df-en 8504  df-dom 8505  df-sdom 8506  df-sup 8900  df-inf 8901  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-3 11695  df-n0 11892  df-z 11976  df-uz 12238  df-q 12343  df-rp 12384  df-xneg 12501  df-xadd 12502  df-xmul 12503  df-seq 13364  df-exp 13424  df-cj 14452  df-re 14453  df-im 14454  df-sqrt 14588  df-abs 14589  df-topgen 16711  df-psmet 20531  df-xmet 20532  df-met 20533  df-bl 20534  df-mopn 20535  df-top 21496  df-topon 21513  df-bases 21548  df-cnp 21830  df-grpo 28264  df-gid 28265  df-ginv 28266  df-gdiv 28267  df-ablo 28316  df-vc 28330  df-nv 28363  df-va 28366  df-ba 28367  df-sm 28368  df-0v 28369  df-vs 28370  df-nmcv 28371  df-ims 28372  df-lno 28515  df-nmoo 28516  df-blo 28517  df-0o 28518

This theorem is referenced by:  blocni  28576  lnocni  28577