Theorem blocnilem 29067

Description: Lemma for blocni 29068 and lnocni 29069. 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 28955	. . . . . 6 ⊢ (𝑈 ∈ NrmCVec → 𝐶 ∈ (∞Met‘𝑋))
5	1, 4	ax-mp 5	. . . . 5 ⊢ 𝐶 ∈ (∞Met‘𝑋)
6		blocni.w	. . . . . 6 ⊢ 𝑊 ∈ NrmCVec
7		eqid 2738	. . . . . . 7 ⊢ (BaseSet‘𝑊) = (BaseSet‘𝑊)
8		blocni.d	. . . . . . 7 ⊢ 𝐷 = (IndMet‘𝑊)
9	7, 8	imsxmet 28955	. . . . . 6 ⊢ (𝑊 ∈ NrmCVec → 𝐷 ∈ (∞Met‘(BaseSet‘𝑊)))
10	6, 9	ax-mp 5	. . . . 5 ⊢ 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))
11		1rp 12663	. . . . . 6 ⊢ 1 ∈ ℝ+
12		blocni.j	. . . . . . 7 ⊢ 𝐽 = (MetOpen‘𝐶)
13		blocni.k	. . . . . . 7 ⊢ 𝐾 = (MetOpen‘𝐷)
14	12, 13	metcnpi3 23608	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))) ∧ (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 1 ∈ ℝ+)) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1))
15	11, 14	mpanr2 700	. . . . 5 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))) ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1))
16	5, 10, 15	mpanl12 698	. . . 4 ⊢ (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1))
17		rpreccl 12685	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℝ+)
18	17	rpred 12701	. . . . . . 7 ⊢ (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℝ)
19	18	ad2antlr 723	. . . . . 6 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → (1 / 𝑦) ∈ ℝ)
20		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ ( −𝑣 ‘𝑈) = ( −𝑣 ‘𝑈)
21		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ (normCV‘𝑈) = (normCV‘𝑈)
22	2, 20, 21, 3	imsdval 28949	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑥𝐶𝑃) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)))
23	1, 22	mp3an1 1446	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑥𝐶𝑃) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)))
24	23	breq1d 5080	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑥𝐶𝑃) ≤ 𝑦 ↔ ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦))
25		blocni.l	. . . . . . . . . . . . . . . . 17 ⊢ 𝑇 ∈ 𝐿
26		blocni.4	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐿 = (𝑈 LnOp 𝑊)
27	2, 7, 26	lnof 29018	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶(BaseSet‘𝑊))
28	1, 6, 25, 27	mp3an 1459	. . . . . . . . . . . . . . . 16 ⊢ 𝑇:𝑋⟶(BaseSet‘𝑊)
29	28	ffvelrni 6942	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝑋 → (𝑇‘𝑥) ∈ (BaseSet‘𝑊))
30	28	ffvelrni 6942	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ 𝑋 → (𝑇‘𝑃) ∈ (BaseSet‘𝑊))
31		eqid 2738	. . . . . . . . . . . . . . . . 17 ⊢ ( −𝑣 ‘𝑊) = ( −𝑣 ‘𝑊)
32		eqid 2738	. . . . . . . . . . . . . . . . 17 ⊢ (normCV‘𝑊) = (normCV‘𝑊)
33	7, 31, 32, 8	imsdval 28949	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇‘𝑃) ∈ (BaseSet‘𝑊)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))))
34	6, 33	mp3an1 1446	. . . . . . . . . . . . . . 15 ⊢ (((𝑇‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇‘𝑃) ∈ (BaseSet‘𝑊)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))))
35	29, 30, 34	syl2an 595	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))))
36	1, 6, 25	3pm3.2i 1337	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿)
37	2, 20, 31, 26	lnosub 29022	. . . . . . . . . . . . . . . 16 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋)) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))
38	36, 37	mpan 686	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))
39	38	fveq2d 6760	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))))
40	35, 39	eqtr4d 2781	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))))
41	40	breq1d 5080	. . . . . . . . . . . 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 711	. . . . . . . . 9 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔ (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)))
45	44	ralbidva 3119	. . . . . . . 8 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) → (∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)))
46		2fveq3 6761	. . . . . . . . . . . 12 ⊢ (𝑧 = (0vec‘𝑈) → ((normCV‘𝑊)‘(𝑇‘𝑧)) = ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))))
47		fveq2 6756	. . . . . . . . . . . . 13 ⊢ (𝑧 = (0vec‘𝑈) → ((normCV‘𝑈)‘𝑧) = ((normCV‘𝑈)‘(0vec‘𝑈)))
48	47	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (𝑧 = (0vec‘𝑈) → ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) = ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))))
49	46, 48	breq12d 5083	. . . . . . . . . . 11 ⊢ (𝑧 = (0vec‘𝑈) → (((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈)))))
50	1	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑈 ∈ NrmCVec)
51		simpll 763	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑃 ∈ 𝑋)
52		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ+)
53	2, 21	nvcl 28924	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → ((normCV‘𝑈)‘𝑧) ∈ ℝ)
54	1, 53	mpan 686	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ 𝑋 → ((normCV‘𝑈)‘𝑧) ∈ ℝ)
55	54	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) → ((normCV‘𝑈)‘𝑧) ∈ ℝ)
56		eqid 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0vec‘𝑈) = (0vec‘𝑈)
57	2, 56, 21	nvgt0 28937	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → (𝑧 ≠ (0vec‘𝑈) ↔ 0 < ((normCV‘𝑈)‘𝑧)))
58	1, 57	mpan 686	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ 𝑋 → (𝑧 ≠ (0vec‘𝑈) ↔ 0 < ((normCV‘𝑈)‘𝑧)))
59	58	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) → 0 < ((normCV‘𝑈)‘𝑧))
60	55, 59	elrpd 12698	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) → ((normCV‘𝑈)‘𝑧) ∈ ℝ+)
61		rpdivcl 12684	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ ℝ+ ∧ ((normCV‘𝑈)‘𝑧) ∈ ℝ+) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ+)
62	52, 60, 61	syl2an 595	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ+)
63	62	rpcnd 12703	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ)
64		simprl 767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑧 ∈ 𝑋)
65		eqid 2738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( ·𝑠OLD ‘𝑈) = ( ·𝑠OLD ‘𝑈)
66	2, 65	nvscl 28889	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋) → ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧) ∈ 𝑋)
67	50, 63, 64, 66	syl3anc 1369	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧) ∈ 𝑋)
68		eqid 2738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ( +𝑣 ‘𝑈) = ( +𝑣 ‘𝑈)
69	2, 68, 20	nvpncan2 28916	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧) ∈ 𝑋) → ((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))
70	50, 51, 67, 69	syl3anc 1369	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))
71	70	fveq2d 6760	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = ((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)))
72	62	rprege0d 12708	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 / ((normCV‘𝑈)‘𝑧))))
73	2, 65, 21	nvsge0 28927	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 ∈ NrmCVec ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 / ((normCV‘𝑈)‘𝑧))) ∧ 𝑧 ∈ 𝑋) → ((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧)))
74	50, 72, 64, 73	syl3anc 1369	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧)))
75		rpcn 12669	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℂ)
76	75	ad2antlr 723	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ∈ ℂ)
77	54	ad2antrl 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘𝑧) ∈ ℝ)
78	77	recnd 10934	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘𝑧) ∈ ℂ)
79	2, 56, 21	nvz 28932	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → (((normCV‘𝑈)‘𝑧) = 0 ↔ 𝑧 = (0vec‘𝑈)))
80	1, 79	mpan 686	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ 𝑋 → (((normCV‘𝑈)‘𝑧) = 0 ↔ 𝑧 = (0vec‘𝑈)))
81	80	necon3bid 2987	. . . . . . . . . . . . . . . . . . . . 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 11682	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧)) = 𝑦)
85	71, 74, 84	3eqtrd 2782	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = 𝑦)
86		rpre 12667	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
87	86	leidd 11471	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ≤ 𝑦)
88	87	ad2antlr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ≤ 𝑦)
89	85, 88	eqbrtrd 5092	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦)
90	2, 68	nvgcl 28883	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧) ∈ 𝑋) → (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) ∈ 𝑋)
91	50, 51, 67, 90	syl3anc 1369	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) ∈ 𝑋)
92		fvoveq1 7278	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)))
93	92	breq1d 5080	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 ↔ ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦))
94		fvoveq1 7278	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)))
95	94	fveq2d 6760	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))))
96	95	breq1d 5080	. . . . . . . . . . . . . . . . . . 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 3547	. . . . . . . . . . . . . . . . 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 6942	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑋 → (𝑇‘𝑧) ∈ (BaseSet‘𝑊))
102	7, 32	nvcl 28924	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ)
103	6, 101, 102	sylancr 586	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑋 → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ)
104	103	ad2antrl 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ)
105		1red 10907	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 1 ∈ ℝ)
106	104, 105, 62	lemuldiv2d 12751	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))) ≤ 1 ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (1 / (𝑦 / ((normCV‘𝑈)‘𝑧)))))
107	70	fveq2d 6760	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)))
108		eqid 2738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ( ·𝑠OLD ‘𝑊) = ( ·𝑠OLD ‘𝑊)
109	2, 65, 108, 26	lnomul 29023	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋)) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧)))
110	36, 109	mpan 686	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧)))
111	63, 64, 110	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧)))
112	107, 111	eqtrd 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧)))
113	112	fveq2d 6760	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧))))
114	6	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑊 ∈ NrmCVec)
115	101	ad2antrl 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘𝑧) ∈ (BaseSet‘𝑊))
116	7, 108, 32	nvsge0 28927	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ NrmCVec ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 / ((normCV‘𝑈)‘𝑧))) ∧ (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))))
117	114, 72, 115, 116	syl3anc 1369	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑊)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))))
118	113, 117	eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))))
119	118	breq1d 5080	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1 ↔ ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))) ≤ 1))
120		rpcnne0 12677	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℝ+ → (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0))
121		rpcnne0 12677	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((normCV‘𝑈)‘𝑧) ∈ ℝ+ → (((normCV‘𝑈)‘𝑧) ∈ ℂ ∧ ((normCV‘𝑈)‘𝑧) ≠ 0))
122		recdiv 11611	. . . . . . . . . . . . . . . . . . . 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 12675	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ≠ 0)
126	125	ad2antlr 723	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ≠ 0)
127	78, 76, 126	divrec2d 11685	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((normCV‘𝑈)‘𝑧) / 𝑦) = ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
128	124, 127	eqtr2d 2779	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) = (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))))
129	128	breq2d 5082	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (1 / (𝑦 / ((normCV‘𝑈)‘𝑧)))))
130	106, 119, 129	3bitr4d 310	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1 ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
131	100, 130	sylibd 238	. . . . . . . . . . . . . 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 648	. . . . . . . . . . 11 ⊢ (((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) ∧ 𝑧 ≠ (0vec‘𝑈)) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
135		eqid 2738	. . . . . . . . . . . . . . . . . 18 ⊢ (0vec‘𝑊) = (0vec‘𝑊)
136	2, 7, 56, 135, 26	lno0 29019	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇‘(0vec‘𝑈)) = (0vec‘𝑊))
137	1, 6, 25, 136	mp3an 1459	. . . . . . . . . . . . . . . 16 ⊢ (𝑇‘(0vec‘𝑈)) = (0vec‘𝑊)
138	137	fveq2i 6759	. . . . . . . . . . . . . . 15 ⊢ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) = ((normCV‘𝑊)‘(0vec‘𝑊))
139	135, 32	nvz0 28931	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 ∈ NrmCVec → ((normCV‘𝑊)‘(0vec‘𝑊)) = 0)
140	6, 139	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((normCV‘𝑊)‘(0vec‘𝑊)) = 0
141	138, 140	eqtri 2766	. . . . . . . . . . . . . 14 ⊢ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) = 0
142		0le0 12004	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 0
143	141, 142	eqbrtri 5091	. . . . . . . . . . . . 13 ⊢ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ 0
144	17	rpcnd 12703	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℂ)
145	56, 21	nvz0 28931	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ NrmCVec → ((normCV‘𝑈)‘(0vec‘𝑈)) = 0)
146	1, 145	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((normCV‘𝑈)‘(0vec‘𝑈)) = 0
147	146	oveq2i 7266	. . . . . . . . . . . . . . 15 ⊢ ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))) = ((1 / 𝑦) · 0)
148		mul01 11084	. . . . . . . . . . . . . . 15 ⊢ ((1 / 𝑦) ∈ ℂ → ((1 / 𝑦) · 0) = 0)
149	147, 148	syl5eq 2791	. . . . . . . . . . . . . 14 ⊢ ((1 / 𝑦) ∈ ℂ → ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))) = 0)
150	144, 149	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ+ → ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))) = 0)
151	143, 150	breqtrrid 5108	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ+ → ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))))
152	151	ad3antlr 727	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) → ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))))
153	49, 134, 152	pm2.61ne 3029	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
154	153	ex 412	. . . . . . . . 9 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
155	154	ralrimdva 3112	. . . . . . . 8 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
156	45, 155	sylbid 239	. . . . . . 7 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) → (∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
157	156	imp 406	. . . . . 6 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
158		oveq1 7262	. . . . . . . . 9 ⊢ (𝑥 = (1 / 𝑦) → (𝑥 · ((normCV‘𝑈)‘𝑧)) = ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
159	158	breq2d 5082	. . . . . . . 8 ⊢ (𝑥 = (1 / 𝑦) → (((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
160	159	ralbidv 3120	. . . . . . 7 ⊢ (𝑥 = (1 / 𝑦) → (∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)) ↔ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
161	160	rspcev 3552	. . . . . 6 ⊢ (((1 / 𝑦) ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))
162	19, 157, 161	syl2anc 583	. . . . 5 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))
163	162	rexlimdva2 3215	. . . 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 29064	. . 3 ⊢ (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))))
168	25, 167	mpbiran 705	. 2 ⊢ (𝑇 ∈ 𝐵 ↔ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))
169	165, 168	sylibr 233	1 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑇 ∈ 𝐵)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108   ≠ wne 2942  ∀wral 3063  ∃wrex 3064   class class class wbr 5070  ⟶wf 6414  ‘cfv 6418  (class class class)co 7255  ℂcc 10800  ℝcr 10801  0cc0 10802  1c1 10803   · cmul 10807   < clt 10940   ≤ cle 10941   / cdiv 11562  ℝ⁺crp 12659  ∞Metcxmet 20495  MetOpencmopn 20500   CnP ccnp 22284  NrmCVeccnv 28847   +_𝑣 cpv 28848  BaseSetcba 28849   ·_𝑠OLD cns 28850  0_veccn0v 28851   −_𝑣 cnsb 28852  norm_CVcnmcv 28853  IndMetcims 28854   LnOp clno 29003   BLnOp cblo 29005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879  ax-pre-sup 10880  ax-addf 10881  ax-mulf 10882

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-1st 7804  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-er 8456  df-map 8575  df-en 8692  df-dom 8693  df-sdom 8694  df-sup 9131  df-inf 9132  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-div 11563  df-nn 11904  df-2 11966  df-3 11967  df-n0 12164  df-z 12250  df-uz 12512  df-q 12618  df-rp 12660  df-xneg 12777  df-xadd 12778  df-xmul 12779  df-seq 13650  df-exp 13711  df-cj 14738  df-re 14739  df-im 14740  df-sqrt 14874  df-abs 14875  df-topgen 17071  df-psmet 20502  df-xmet 20503  df-met 20504  df-bl 20505  df-mopn 20506  df-top 21951  df-topon 21968  df-bases 22004  df-cnp 22287  df-grpo 28756  df-gid 28757  df-ginv 28758  df-gdiv 28759  df-ablo 28808  df-vc 28822  df-nv 28855  df-va 28858  df-ba 28859  df-sm 28860  df-0v 28861  df-vs 28862  df-nmcv 28863  df-ims 28864  df-lno 29007  df-nmoo 29008  df-blo 29009  df-0o 29010

This theorem is referenced by:  blocni  29068  lnocni  29069