Theorem blocnilem 30836

Description: Lemma for blocni 30837 and lnocni 30838. 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 30724	. . . . . 6 ⊢ (𝑈 ∈ NrmCVec → 𝐶 ∈ (∞Met‘𝑋))
5	1, 4	ax-mp 5	. . . . 5 ⊢ 𝐶 ∈ (∞Met‘𝑋)
6		blocni.w	. . . . . 6 ⊢ 𝑊 ∈ NrmCVec
7		eqid 2740	. . . . . . 7 ⊢ (BaseSet‘𝑊) = (BaseSet‘𝑊)
8		blocni.d	. . . . . . 7 ⊢ 𝐷 = (IndMet‘𝑊)
9	7, 8	imsxmet 30724	. . . . . 6 ⊢ (𝑊 ∈ NrmCVec → 𝐷 ∈ (∞Met‘(BaseSet‘𝑊)))
10	6, 9	ax-mp 5	. . . . 5 ⊢ 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))
11		1rp 13061	. . . . . 6 ⊢ 1 ∈ ℝ+
12		blocni.j	. . . . . . 7 ⊢ 𝐽 = (MetOpen‘𝐶)
13		blocni.k	. . . . . . 7 ⊢ 𝐾 = (MetOpen‘𝐷)
14	12, 13	metcnpi3 24580	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))) ∧ (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 1 ∈ ℝ+)) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1))
15	11, 14	mpanr2 703	. . . . 5 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))) ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1))
16	5, 10, 15	mpanl12 701	. . . 4 ⊢ (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1))
17		rpreccl 13083	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℝ+)
18	17	rpred 13099	. . . . . . 7 ⊢ (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℝ)
19	18	ad2antlr 726	. . . . . 6 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → (1 / 𝑦) ∈ ℝ)
20		eqid 2740	. . . . . . . . . . . . . . 15 ⊢ ( −𝑣 ‘𝑈) = ( −𝑣 ‘𝑈)
21		eqid 2740	. . . . . . . . . . . . . . 15 ⊢ (normCV‘𝑈) = (normCV‘𝑈)
22	2, 20, 21, 3	imsdval 30718	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑥𝐶𝑃) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)))
23	1, 22	mp3an1 1448	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑥𝐶𝑃) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)))
24	23	breq1d 5176	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑥𝐶𝑃) ≤ 𝑦 ↔ ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦))
25		blocni.l	. . . . . . . . . . . . . . . . 17 ⊢ 𝑇 ∈ 𝐿
26		blocni.4	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐿 = (𝑈 LnOp 𝑊)
27	2, 7, 26	lnof 30787	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶(BaseSet‘𝑊))
28	1, 6, 25, 27	mp3an 1461	. . . . . . . . . . . . . . . 16 ⊢ 𝑇:𝑋⟶(BaseSet‘𝑊)
29	28	ffvelcdmi 7117	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝑋 → (𝑇‘𝑥) ∈ (BaseSet‘𝑊))
30	28	ffvelcdmi 7117	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ 𝑋 → (𝑇‘𝑃) ∈ (BaseSet‘𝑊))
31		eqid 2740	. . . . . . . . . . . . . . . . 17 ⊢ ( −𝑣 ‘𝑊) = ( −𝑣 ‘𝑊)
32		eqid 2740	. . . . . . . . . . . . . . . . 17 ⊢ (normCV‘𝑊) = (normCV‘𝑊)
33	7, 31, 32, 8	imsdval 30718	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇‘𝑃) ∈ (BaseSet‘𝑊)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))))
34	6, 33	mp3an1 1448	. . . . . . . . . . . . . . 15 ⊢ (((𝑇‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇‘𝑃) ∈ (BaseSet‘𝑊)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))))
35	29, 30, 34	syl2an 595	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))))
36	1, 6, 25	3pm3.2i 1339	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿)
37	2, 20, 31, 26	lnosub 30791	. . . . . . . . . . . . . . . 16 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋)) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))
38	36, 37	mpan 689	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))
39	38	fveq2d 6924	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))))
40	35, 39	eqtr4d 2783	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))))
41	40	breq1d 5176	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1 ↔ ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1))
42	24, 41	imbi12d 344	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔ (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)))
43	42	ancoms 458	. . . . . . . . . 10 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔ (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)))
44	43	adantlr 714	. . . . . . . . 9 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔ (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)))
45	44	ralbidva 3182	. . . . . . . 8 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) → (∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)))
46		2fveq3 6925	. . . . . . . . . . . 12 ⊢ (𝑧 = (0vec‘𝑈) → ((normCV‘𝑊)‘(𝑇‘𝑧)) = ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))))
47		fveq2 6920	. . . . . . . . . . . . 13 ⊢ (𝑧 = (0vec‘𝑈) → ((normCV‘𝑈)‘𝑧) = ((normCV‘𝑈)‘(0vec‘𝑈)))
48	47	oveq2d 7464	. . . . . . . . . . . 12 ⊢ (𝑧 = (0vec‘𝑈) → ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) = ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))))
49	46, 48	breq12d 5179	. . . . . . . . . . 11 ⊢ (𝑧 = (0vec‘𝑈) → (((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈)))))
50	1	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑈 ∈ NrmCVec)
51		simpll 766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑃 ∈ 𝑋)
52		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ+)
53	2, 21	nvcl 30693	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → ((normCV‘𝑈)‘𝑧) ∈ ℝ)
54	1, 53	mpan 689	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ 𝑋 → ((normCV‘𝑈)‘𝑧) ∈ ℝ)
55	54	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) → ((normCV‘𝑈)‘𝑧) ∈ ℝ)
56		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0vec‘𝑈) = (0vec‘𝑈)
57	2, 56, 21	nvgt0 30706	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → (𝑧 ≠ (0vec‘𝑈) ↔ 0 < ((normCV‘𝑈)‘𝑧)))
58	1, 57	mpan 689	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ 𝑋 → (𝑧 ≠ (0vec‘𝑈) ↔ 0 < ((normCV‘𝑈)‘𝑧)))
59	58	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) → 0 < ((normCV‘𝑈)‘𝑧))
60	55, 59	elrpd 13096	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) → ((normCV‘𝑈)‘𝑧) ∈ ℝ+)
61		rpdivcl 13082	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ ℝ+ ∧ ((normCV‘𝑈)‘𝑧) ∈ ℝ+) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ+)
62	52, 60, 61	syl2an 595	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ+)
63	62	rpcnd 13101	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ)
64		simprl 770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑧 ∈ 𝑋)
65		eqid 2740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( ·𝑠OLD ‘𝑈) = ( ·𝑠OLD ‘𝑈)
66	2, 65	nvscl 30658	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋) → ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧) ∈ 𝑋)
67	50, 63, 64, 66	syl3anc 1371	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧) ∈ 𝑋)
68		eqid 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ( +𝑣 ‘𝑈) = ( +𝑣 ‘𝑈)
69	2, 68, 20	nvpncan2 30685	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧) ∈ 𝑋) → ((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))
70	50, 51, 67, 69	syl3anc 1371	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))
71	70	fveq2d 6924	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = ((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)))
72	62	rprege0d 13106	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 / ((normCV‘𝑈)‘𝑧))))
73	2, 65, 21	nvsge0 30696	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 ∈ NrmCVec ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 / ((normCV‘𝑈)‘𝑧))) ∧ 𝑧 ∈ 𝑋) → ((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧)))
74	50, 72, 64, 73	syl3anc 1371	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧)))
75		rpcn 13067	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℂ)
76	75	ad2antlr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ∈ ℂ)
77	54	ad2antrl 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘𝑧) ∈ ℝ)
78	77	recnd 11318	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘𝑧) ∈ ℂ)
79	2, 56, 21	nvz 30701	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → (((normCV‘𝑈)‘𝑧) = 0 ↔ 𝑧 = (0vec‘𝑈)))
80	1, 79	mpan 689	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ 𝑋 → (((normCV‘𝑈)‘𝑧) = 0 ↔ 𝑧 = (0vec‘𝑈)))
81	80	necon3bid 2991	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ 𝑋 → (((normCV‘𝑈)‘𝑧) ≠ 0 ↔ 𝑧 ≠ (0vec‘𝑈)))
82	81	biimpar 477	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) → ((normCV‘𝑈)‘𝑧) ≠ 0)
83	82	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘𝑧) ≠ 0)
84	76, 78, 83	divcan1d 12071	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧)) = 𝑦)
85	71, 74, 84	3eqtrd 2784	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = 𝑦)
86		rpre 13065	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
87	86	leidd 11856	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ≤ 𝑦)
88	87	ad2antlr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ≤ 𝑦)
89	85, 88	eqbrtrd 5188	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦)
90	2, 68	nvgcl 30652	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧) ∈ 𝑋) → (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) ∈ 𝑋)
91	50, 51, 67, 90	syl3anc 1371	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) ∈ 𝑋)
92		fvoveq1 7471	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)))
93	92	breq1d 5176	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 ↔ ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦))
94		fvoveq1 7471	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)))
95	94	fveq2d 6924	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))))
96	95	breq1d 5176	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → (((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1 ↔ ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1))
97	93, 96	imbi12d 344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → ((((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) ↔ (((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1)))
98	97	rspcv 3631	. . . . . . . . . . . . . . . . 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	ffvelcdmi 7117	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑋 → (𝑇‘𝑧) ∈ (BaseSet‘𝑊))
102	7, 32	nvcl 30693	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ)
103	6, 101, 102	sylancr 586	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑋 → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ)
104	103	ad2antrl 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ)
105		1red 11291	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 1 ∈ ℝ)
106	104, 105, 62	lemuldiv2d 13149	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))) ≤ 1 ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (1 / (𝑦 / ((normCV‘𝑈)‘𝑧)))))
107	70	fveq2d 6924	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)))
108		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ( ·𝑠OLD ‘𝑊) = ( ·𝑠OLD ‘𝑊)
109	2, 65, 108, 26	lnomul 30792	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋)) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧)))
110	36, 109	mpan 689	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧)))
111	63, 64, 110	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧)))
112	107, 111	eqtrd 2780	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧)))
113	112	fveq2d 6924	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧))))
114	6	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑊 ∈ NrmCVec)
115	101	ad2antrl 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘𝑧) ∈ (BaseSet‘𝑊))
116	7, 108, 32	nvsge0 30696	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ NrmCVec ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 / ((normCV‘𝑈)‘𝑧))) ∧ (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))))
117	114, 72, 115, 116	syl3anc 1371	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑊)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))))
118	113, 117	eqtrd 2780	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))))
119	118	breq1d 5176	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1 ↔ ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))) ≤ 1))
120		rpcnne0 13075	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℝ+ → (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0))
121		rpcnne0 13075	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((normCV‘𝑈)‘𝑧) ∈ ℝ+ → (((normCV‘𝑈)‘𝑧) ∈ ℂ ∧ ((normCV‘𝑈)‘𝑧) ≠ 0))
122		recdiv 12000	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) ∧ (((normCV‘𝑈)‘𝑧) ∈ ℂ ∧ ((normCV‘𝑈)‘𝑧) ≠ 0)) → (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))) = (((normCV‘𝑈)‘𝑧) / 𝑦))
123	120, 121, 122	syl2an 595	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ℝ+ ∧ ((normCV‘𝑈)‘𝑧) ∈ ℝ+) → (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))) = (((normCV‘𝑈)‘𝑧) / 𝑦))
124	52, 60, 123	syl2an 595	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))) = (((normCV‘𝑈)‘𝑧) / 𝑦))
125		rpne0 13073	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ≠ 0)
126	125	ad2antlr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ≠ 0)
127	78, 76, 126	divrec2d 12074	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((normCV‘𝑈)‘𝑧) / 𝑦) = ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
128	124, 127	eqtr2d 2781	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) = (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))))
129	128	breq2d 5178	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (1 / (𝑦 / ((normCV‘𝑈)‘𝑧)))))
130	106, 119, 129	3bitr4d 311	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1 ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
131	100, 130	sylibd 239	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
132	131	anassrs 467	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 ≠ (0vec‘𝑈)) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
133	132	imp 406	. . . . . . . . . . . 12 ⊢ (((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 ≠ (0vec‘𝑈)) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
134	133	an32s 651	. . . . . . . . . . 11 ⊢ (((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) ∧ 𝑧 ≠ (0vec‘𝑈)) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
135		eqid 2740	. . . . . . . . . . . . . . . . . 18 ⊢ (0vec‘𝑊) = (0vec‘𝑊)
136	2, 7, 56, 135, 26	lno0 30788	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇‘(0vec‘𝑈)) = (0vec‘𝑊))
137	1, 6, 25, 136	mp3an 1461	. . . . . . . . . . . . . . . 16 ⊢ (𝑇‘(0vec‘𝑈)) = (0vec‘𝑊)
138	137	fveq2i 6923	. . . . . . . . . . . . . . 15 ⊢ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) = ((normCV‘𝑊)‘(0vec‘𝑊))
139	135, 32	nvz0 30700	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 ∈ NrmCVec → ((normCV‘𝑊)‘(0vec‘𝑊)) = 0)
140	6, 139	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((normCV‘𝑊)‘(0vec‘𝑊)) = 0
141	138, 140	eqtri 2768	. . . . . . . . . . . . . 14 ⊢ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) = 0
142		0le0 12394	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 0
143	141, 142	eqbrtri 5187	. . . . . . . . . . . . 13 ⊢ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ 0
144	17	rpcnd 13101	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℂ)
145	56, 21	nvz0 30700	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ NrmCVec → ((normCV‘𝑈)‘(0vec‘𝑈)) = 0)
146	1, 145	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((normCV‘𝑈)‘(0vec‘𝑈)) = 0
147	146	oveq2i 7459	. . . . . . . . . . . . . . 15 ⊢ ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))) = ((1 / 𝑦) · 0)
148		mul01 11469	. . . . . . . . . . . . . . 15 ⊢ ((1 / 𝑦) ∈ ℂ → ((1 / 𝑦) · 0) = 0)
149	147, 148	eqtrid 2792	. . . . . . . . . . . . . 14 ⊢ ((1 / 𝑦) ∈ ℂ → ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))) = 0)
150	144, 149	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ+ → ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))) = 0)
151	143, 150	breqtrrid 5204	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ+ → ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))))
152	151	ad3antlr 730	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) → ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))))
153	49, 134, 152	pm2.61ne 3033	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
154	153	ex 412	. . . . . . . . 9 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
155	154	ralrimdva 3160	. . . . . . . 8 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
156	45, 155	sylbid 240	. . . . . . 7 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) → (∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
157	156	imp 406	. . . . . 6 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
158		oveq1 7455	. . . . . . . . 9 ⊢ (𝑥 = (1 / 𝑦) → (𝑥 · ((normCV‘𝑈)‘𝑧)) = ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
159	158	breq2d 5178	. . . . . . . 8 ⊢ (𝑥 = (1 / 𝑦) → (((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
160	159	ralbidv 3184	. . . . . . 7 ⊢ (𝑥 = (1 / 𝑦) → (∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)) ↔ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
161	160	rspcev 3635	. . . . . 6 ⊢ (((1 / 𝑦) ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))
162	19, 157, 161	syl2anc 583	. . . . 5 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))
163	162	rexlimdva2 3163	. . . 4 ⊢ (𝑃 ∈ 𝑋 → (∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))))
164	16, 163	syl5 34	. . 3 ⊢ (𝑃 ∈ 𝑋 → (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))))
165	164	imp 406	. 2 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))
166		blocni.5	. . . 4 ⊢ 𝐵 = (𝑈 BLnOp 𝑊)
167	2, 21, 32, 26, 166, 1, 6	isblo3i 30833	. . 3 ⊢ (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))))
168	25, 167	mpbiran 708	. 2 ⊢ (𝑇 ∈ 𝐵 ↔ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))
169	165, 168	sylibr 234	1 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑇 ∈ 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108   ≠ wne 2946  ∀wral 3067  ∃wrex 3076   class class class wbr 5166  ⟶wf 6569  ‘cfv 6573  (class class class)co 7448  ℂcc 11182  ℝcr 11183  0cc0 11184  1c1 11185   · cmul 11189   < clt 11324   ≤ cle 11325   / cdiv 11947  ℝ⁺crp 13057  ∞Metcxmet 21372  MetOpencmopn 21377   CnP ccnp 23254  NrmCVeccnv 30616   +_𝑣 cpv 30617  BaseSetcba 30618   ·_𝑠OLD cns 30619  0_veccn0v 30620   −_𝑣 cnsb 30621  norm_CVcnmcv 30622  IndMetcims 30623   LnOp clno 30772   BLnOp cblo 30774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-pre-sup 11262  ax-addf 11263  ax-mulf 11264

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-er 8763  df-map 8886  df-en 9004  df-dom 9005  df-sdom 9006  df-sup 9511  df-inf 9512  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-2 12356  df-3 12357  df-n0 12554  df-z 12640  df-uz 12904  df-q 13014  df-rp 13058  df-xneg 13175  df-xadd 13176  df-xmul 13177  df-seq 14053  df-exp 14113  df-cj 15148  df-re 15149  df-im 15150  df-sqrt 15284  df-abs 15285  df-topgen 17503  df-psmet 21379  df-xmet 21380  df-met 21381  df-bl 21382  df-mopn 21383  df-top 22921  df-topon 22938  df-bases 22974  df-cnp 23257  df-grpo 30525  df-gid 30526  df-ginv 30527  df-gdiv 30528  df-ablo 30577  df-vc 30591  df-nv 30624  df-va 30627  df-ba 30628  df-sm 30629  df-0v 30630  df-vs 30631  df-nmcv 30632  df-ims 30633  df-lno 30776  df-nmoo 30777  df-blo 30778  df-0o 30779

This theorem is referenced by:  blocni  30837  lnocni  30838