Theorem blocnilem 30890

Description: Lemma for blocni 30891 and lnocni 30892. 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 30778	. . . . . 6 ⊢ (𝑈 ∈ NrmCVec → 𝐶 ∈ (∞Met‘𝑋))
5	1, 4	ax-mp 5	. . . . 5 ⊢ 𝐶 ∈ (∞Met‘𝑋)
6		blocni.w	. . . . . 6 ⊢ 𝑊 ∈ NrmCVec
7		eqid 2737	. . . . . . 7 ⊢ (BaseSet‘𝑊) = (BaseSet‘𝑊)
8		blocni.d	. . . . . . 7 ⊢ 𝐷 = (IndMet‘𝑊)
9	7, 8	imsxmet 30778	. . . . . 6 ⊢ (𝑊 ∈ NrmCVec → 𝐷 ∈ (∞Met‘(BaseSet‘𝑊)))
10	6, 9	ax-mp 5	. . . . 5 ⊢ 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))
11		1rp 12937	. . . . . 6 ⊢ 1 ∈ ℝ+
12		blocni.j	. . . . . . 7 ⊢ 𝐽 = (MetOpen‘𝐶)
13		blocni.k	. . . . . . 7 ⊢ 𝐾 = (MetOpen‘𝐷)
14	12, 13	metcnpi3 24521	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))) ∧ (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 1 ∈ ℝ+)) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1))
15	11, 14	mpanr2 705	. . . . 5 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))) ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1))
16	5, 10, 15	mpanl12 703	. . . 4 ⊢ (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1))
17		rpreccl 12961	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℝ+)
18	17	rpred 12977	. . . . . . 7 ⊢ (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℝ)
19	18	ad2antlr 728	. . . . . 6 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → (1 / 𝑦) ∈ ℝ)
20		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ ( −𝑣 ‘𝑈) = ( −𝑣 ‘𝑈)
21		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (normCV‘𝑈) = (normCV‘𝑈)
22	2, 20, 21, 3	imsdval 30772	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑥𝐶𝑃) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)))
23	1, 22	mp3an1 1451	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑥𝐶𝑃) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)))
24	23	breq1d 5096	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑥𝐶𝑃) ≤ 𝑦 ↔ ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦))
25		blocni.l	. . . . . . . . . . . . . . . . 17 ⊢ 𝑇 ∈ 𝐿
26		blocni.4	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐿 = (𝑈 LnOp 𝑊)
27	2, 7, 26	lnof 30841	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶(BaseSet‘𝑊))
28	1, 6, 25, 27	mp3an 1464	. . . . . . . . . . . . . . . 16 ⊢ 𝑇:𝑋⟶(BaseSet‘𝑊)
29	28	ffvelcdmi 7029	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝑋 → (𝑇‘𝑥) ∈ (BaseSet‘𝑊))
30	28	ffvelcdmi 7029	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ 𝑋 → (𝑇‘𝑃) ∈ (BaseSet‘𝑊))
31		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ ( −𝑣 ‘𝑊) = ( −𝑣 ‘𝑊)
32		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (normCV‘𝑊) = (normCV‘𝑊)
33	7, 31, 32, 8	imsdval 30772	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇‘𝑃) ∈ (BaseSet‘𝑊)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))))
34	6, 33	mp3an1 1451	. . . . . . . . . . . . . . 15 ⊢ (((𝑇‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇‘𝑃) ∈ (BaseSet‘𝑊)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))))
35	29, 30, 34	syl2an 597	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))))
36	1, 6, 25	3pm3.2i 1341	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿)
37	2, 20, 31, 26	lnosub 30845	. . . . . . . . . . . . . . . 16 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋)) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))
38	36, 37	mpan 691	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))
39	38	fveq2d 6838	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))))
40	35, 39	eqtr4d 2775	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))))
41	40	breq1d 5096	. . . . . . . . . . . 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 716	. . . . . . . . 9 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔ (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)))
45	44	ralbidva 3159	. . . . . . . 8 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) → (∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)))
46		2fveq3 6839	. . . . . . . . . . . 12 ⊢ (𝑧 = (0vec‘𝑈) → ((normCV‘𝑊)‘(𝑇‘𝑧)) = ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))))
47		fveq2 6834	. . . . . . . . . . . . 13 ⊢ (𝑧 = (0vec‘𝑈) → ((normCV‘𝑈)‘𝑧) = ((normCV‘𝑈)‘(0vec‘𝑈)))
48	47	oveq2d 7376	. . . . . . . . . . . 12 ⊢ (𝑧 = (0vec‘𝑈) → ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) = ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))))
49	46, 48	breq12d 5099	. . . . . . . . . . 11 ⊢ (𝑧 = (0vec‘𝑈) → (((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈)))))
50	1	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑈 ∈ NrmCVec)
51		simpll 767	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑃 ∈ 𝑋)
52		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ+)
53	2, 21	nvcl 30747	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → ((normCV‘𝑈)‘𝑧) ∈ ℝ)
54	1, 53	mpan 691	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ 𝑋 → ((normCV‘𝑈)‘𝑧) ∈ ℝ)
55	54	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) → ((normCV‘𝑈)‘𝑧) ∈ ℝ)
56		eqid 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0vec‘𝑈) = (0vec‘𝑈)
57	2, 56, 21	nvgt0 30760	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → (𝑧 ≠ (0vec‘𝑈) ↔ 0 < ((normCV‘𝑈)‘𝑧)))
58	1, 57	mpan 691	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ 𝑋 → (𝑧 ≠ (0vec‘𝑈) ↔ 0 < ((normCV‘𝑈)‘𝑧)))
59	58	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) → 0 < ((normCV‘𝑈)‘𝑧))
60	55, 59	elrpd 12974	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) → ((normCV‘𝑈)‘𝑧) ∈ ℝ+)
61		rpdivcl 12960	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ ℝ+ ∧ ((normCV‘𝑈)‘𝑧) ∈ ℝ+) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ+)
62	52, 60, 61	syl2an 597	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ+)
63	62	rpcnd 12979	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ)
64		simprl 771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑧 ∈ 𝑋)
65		eqid 2737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( ·𝑠OLD ‘𝑈) = ( ·𝑠OLD ‘𝑈)
66	2, 65	nvscl 30712	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋) → ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧) ∈ 𝑋)
67	50, 63, 64, 66	syl3anc 1374	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧) ∈ 𝑋)
68		eqid 2737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ( +𝑣 ‘𝑈) = ( +𝑣 ‘𝑈)
69	2, 68, 20	nvpncan2 30739	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧) ∈ 𝑋) → ((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))
70	50, 51, 67, 69	syl3anc 1374	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))
71	70	fveq2d 6838	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = ((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)))
72	62	rprege0d 12984	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 / ((normCV‘𝑈)‘𝑧))))
73	2, 65, 21	nvsge0 30750	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 ∈ NrmCVec ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 / ((normCV‘𝑈)‘𝑧))) ∧ 𝑧 ∈ 𝑋) → ((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧)))
74	50, 72, 64, 73	syl3anc 1374	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧)))
75		rpcn 12944	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℂ)
76	75	ad2antlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ∈ ℂ)
77	54	ad2antrl 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘𝑧) ∈ ℝ)
78	77	recnd 11164	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘𝑧) ∈ ℂ)
79	2, 56, 21	nvz 30755	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → (((normCV‘𝑈)‘𝑧) = 0 ↔ 𝑧 = (0vec‘𝑈)))
80	1, 79	mpan 691	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ 𝑋 → (((normCV‘𝑈)‘𝑧) = 0 ↔ 𝑧 = (0vec‘𝑈)))
81	80	necon3bid 2977	. . . . . . . . . . . . . . . . . . . . 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 11923	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧)) = 𝑦)
85	71, 74, 84	3eqtrd 2776	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = 𝑦)
86		rpre 12942	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
87	86	leidd 11707	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ≤ 𝑦)
88	87	ad2antlr 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ≤ 𝑦)
89	85, 88	eqbrtrd 5108	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦)
90	2, 68	nvgcl 30706	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧) ∈ 𝑋) → (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) ∈ 𝑋)
91	50, 51, 67, 90	syl3anc 1374	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) ∈ 𝑋)
92		fvoveq1 7383	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)))
93	92	breq1d 5096	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 ↔ ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦))
94		fvoveq1 7383	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)))
95	94	fveq2d 6838	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))))
96	95	breq1d 5096	. . . . . . . . . . . . . . . . . . 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 3561	. . . . . . . . . . . . . . . . 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 7029	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑋 → (𝑇‘𝑧) ∈ (BaseSet‘𝑊))
102	7, 32	nvcl 30747	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ)
103	6, 101, 102	sylancr 588	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑋 → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ)
104	103	ad2antrl 729	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ)
105		1red 11136	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 1 ∈ ℝ)
106	104, 105, 62	lemuldiv2d 13027	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))) ≤ 1 ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (1 / (𝑦 / ((normCV‘𝑈)‘𝑧)))))
107	70	fveq2d 6838	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)))
108		eqid 2737	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ( ·𝑠OLD ‘𝑊) = ( ·𝑠OLD ‘𝑊)
109	2, 65, 108, 26	lnomul 30846	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋)) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧)))
110	36, 109	mpan 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧)))
111	63, 64, 110	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧)))
112	107, 111	eqtrd 2772	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧)))
113	112	fveq2d 6838	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧))))
114	6	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑊 ∈ NrmCVec)
115	101	ad2antrl 729	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘𝑧) ∈ (BaseSet‘𝑊))
116	7, 108, 32	nvsge0 30750	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ NrmCVec ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 / ((normCV‘𝑈)‘𝑧))) ∧ (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))))
117	114, 72, 115, 116	syl3anc 1374	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑊)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))))
118	113, 117	eqtrd 2772	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))))
119	118	breq1d 5096	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1 ↔ ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))) ≤ 1))
120		rpcnne0 12952	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℝ+ → (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0))
121		rpcnne0 12952	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((normCV‘𝑈)‘𝑧) ∈ ℝ+ → (((normCV‘𝑈)‘𝑧) ∈ ℂ ∧ ((normCV‘𝑈)‘𝑧) ≠ 0))
122		recdiv 11852	. . . . . . . . . . . . . . . . . . . 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 12950	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ≠ 0)
126	125	ad2antlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ≠ 0)
127	78, 76, 126	divrec2d 11926	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((normCV‘𝑈)‘𝑧) / 𝑦) = ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
128	124, 127	eqtr2d 2773	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) = (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))))
129	128	breq2d 5098	. . . . . . . . . . . . . . . 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 653	. . . . . . . . . . 11 ⊢ (((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) ∧ 𝑧 ≠ (0vec‘𝑈)) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
135		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (0vec‘𝑊) = (0vec‘𝑊)
136	2, 7, 56, 135, 26	lno0 30842	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇‘(0vec‘𝑈)) = (0vec‘𝑊))
137	1, 6, 25, 136	mp3an 1464	. . . . . . . . . . . . . . . 16 ⊢ (𝑇‘(0vec‘𝑈)) = (0vec‘𝑊)
138	137	fveq2i 6837	. . . . . . . . . . . . . . 15 ⊢ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) = ((normCV‘𝑊)‘(0vec‘𝑊))
139	135, 32	nvz0 30754	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 ∈ NrmCVec → ((normCV‘𝑊)‘(0vec‘𝑊)) = 0)
140	6, 139	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((normCV‘𝑊)‘(0vec‘𝑊)) = 0
141	138, 140	eqtri 2760	. . . . . . . . . . . . . 14 ⊢ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) = 0
142		0le0 12273	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 0
143	141, 142	eqbrtri 5107	. . . . . . . . . . . . 13 ⊢ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ 0
144	17	rpcnd 12979	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℂ)
145	56, 21	nvz0 30754	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ NrmCVec → ((normCV‘𝑈)‘(0vec‘𝑈)) = 0)
146	1, 145	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((normCV‘𝑈)‘(0vec‘𝑈)) = 0
147	146	oveq2i 7371	. . . . . . . . . . . . . . 15 ⊢ ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))) = ((1 / 𝑦) · 0)
148		mul01 11316	. . . . . . . . . . . . . . 15 ⊢ ((1 / 𝑦) ∈ ℂ → ((1 / 𝑦) · 0) = 0)
149	147, 148	eqtrid 2784	. . . . . . . . . . . . . 14 ⊢ ((1 / 𝑦) ∈ ℂ → ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))) = 0)
150	144, 149	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ+ → ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))) = 0)
151	143, 150	breqtrrid 5124	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ+ → ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))))
152	151	ad3antlr 732	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) → ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))))
153	49, 134, 152	pm2.61ne 3018	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
154	153	ex 412	. . . . . . . . 9 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
155	154	ralrimdva 3138	. . . . . . . 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 7367	. . . . . . . . 9 ⊢ (𝑥 = (1 / 𝑦) → (𝑥 · ((normCV‘𝑈)‘𝑧)) = ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
159	158	breq2d 5098	. . . . . . . 8 ⊢ (𝑥 = (1 / 𝑦) → (((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
160	159	ralbidv 3161	. . . . . . 7 ⊢ (𝑥 = (1 / 𝑦) → (∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)) ↔ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
161	160	rspcev 3565	. . . . . 6 ⊢ (((1 / 𝑦) ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))
162	19, 157, 161	syl2anc 585	. . . . 5 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))
163	162	rexlimdva2 3141	. . . 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 30887	. . 3 ⊢ (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))))
168	25, 167	mpbiran 710	. 2 ⊢ (𝑇 ∈ 𝐵 ↔ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))
169	165, 168	sylibr 234	1 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑇 ∈ 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3062   class class class wbr 5086  ⟶wf 6488  ‘cfv 6492  (class class class)co 7360  ℂcc 11027  ℝcr 11028  0cc0 11029  1c1 11030   · cmul 11034   < clt 11170   ≤ cle 11171   / cdiv 11798  ℝ⁺crp 12933  ∞Metcxmet 21329  MetOpencmopn 21334   CnP ccnp 23200  NrmCVeccnv 30670   +_𝑣 cpv 30671  BaseSetcba 30672   ·_𝑠OLD cns 30673  0_veccn0v 30674   −_𝑣 cnsb 30675  norm_CVcnmcv 30676  IndMetcims 30677   LnOp clno 30826   BLnOp cblo 30828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106  ax-pre-sup 11107  ax-addf 11108  ax-mulf 11109

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-1st 7935  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-er 8636  df-map 8768  df-en 8887  df-dom 8888  df-sdom 8889  df-sup 9348  df-inf 9349  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799  df-nn 12166  df-2 12235  df-3 12236  df-n0 12429  df-z 12516  df-uz 12780  df-q 12890  df-rp 12934  df-xneg 13054  df-xadd 13055  df-xmul 13056  df-seq 13955  df-exp 14015  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-topgen 17397  df-psmet 21336  df-xmet 21337  df-met 21338  df-bl 21339  df-mopn 21340  df-top 22869  df-topon 22886  df-bases 22921  df-cnp 23203  df-grpo 30579  df-gid 30580  df-ginv 30581  df-gdiv 30582  df-ablo 30631  df-vc 30645  df-nv 30678  df-va 30681  df-ba 30682  df-sm 30683  df-0v 30684  df-vs 30685  df-nmcv 30686  df-ims 30687  df-lno 30830  df-nmoo 30831  df-blo 30832  df-0o 30833

This theorem is referenced by:  blocni  30891  lnocni  30892