Theorem blocnilem 29809

Description: Lemma for blocni 29810 and lnocni 29811. 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 29697	. . . . . 6 ⊢ (𝑈 ∈ NrmCVec → 𝐶 ∈ (∞Met‘𝑋))
5	1, 4	ax-mp 5	. . . . 5 ⊢ 𝐶 ∈ (∞Met‘𝑋)
6		blocni.w	. . . . . 6 ⊢ 𝑊 ∈ NrmCVec
7		eqid 2731	. . . . . . 7 ⊢ (BaseSet‘𝑊) = (BaseSet‘𝑊)
8		blocni.d	. . . . . . 7 ⊢ 𝐷 = (IndMet‘𝑊)
9	7, 8	imsxmet 29697	. . . . . 6 ⊢ (𝑊 ∈ NrmCVec → 𝐷 ∈ (∞Met‘(BaseSet‘𝑊)))
10	6, 9	ax-mp 5	. . . . 5 ⊢ 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))
11		1rp 12928	. . . . . 6 ⊢ 1 ∈ ℝ+
12		blocni.j	. . . . . . 7 ⊢ 𝐽 = (MetOpen‘𝐶)
13		blocni.k	. . . . . . 7 ⊢ 𝐾 = (MetOpen‘𝐷)
14	12, 13	metcnpi3 23939	. . . . . 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 12950	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℝ+)
18	17	rpred 12966	. . . . . . 7 ⊢ (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℝ)
19	18	ad2antlr 725	. . . . . 6 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → (1 / 𝑦) ∈ ℝ)
20		eqid 2731	. . . . . . . . . . . . . . 15 ⊢ ( −𝑣 ‘𝑈) = ( −𝑣 ‘𝑈)
21		eqid 2731	. . . . . . . . . . . . . . 15 ⊢ (normCV‘𝑈) = (normCV‘𝑈)
22	2, 20, 21, 3	imsdval 29691	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑥𝐶𝑃) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)))
23	1, 22	mp3an1 1448	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑥𝐶𝑃) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)))
24	23	breq1d 5120	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑥𝐶𝑃) ≤ 𝑦 ↔ ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦))
25		blocni.l	. . . . . . . . . . . . . . . . 17 ⊢ 𝑇 ∈ 𝐿
26		blocni.4	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐿 = (𝑈 LnOp 𝑊)
27	2, 7, 26	lnof 29760	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶(BaseSet‘𝑊))
28	1, 6, 25, 27	mp3an 1461	. . . . . . . . . . . . . . . 16 ⊢ 𝑇:𝑋⟶(BaseSet‘𝑊)
29	28	ffvelcdmi 7039	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝑋 → (𝑇‘𝑥) ∈ (BaseSet‘𝑊))
30	28	ffvelcdmi 7039	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ 𝑋 → (𝑇‘𝑃) ∈ (BaseSet‘𝑊))
31		eqid 2731	. . . . . . . . . . . . . . . . 17 ⊢ ( −𝑣 ‘𝑊) = ( −𝑣 ‘𝑊)
32		eqid 2731	. . . . . . . . . . . . . . . . 17 ⊢ (normCV‘𝑊) = (normCV‘𝑊)
33	7, 31, 32, 8	imsdval 29691	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇‘𝑃) ∈ (BaseSet‘𝑊)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))))
34	6, 33	mp3an1 1448	. . . . . . . . . . . . . . 15 ⊢ (((𝑇‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇‘𝑃) ∈ (BaseSet‘𝑊)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))))
35	29, 30, 34	syl2an 596	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))))
36	1, 6, 25	3pm3.2i 1339	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿)
37	2, 20, 31, 26	lnosub 29764	. . . . . . . . . . . . . . . 16 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋)) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))
38	36, 37	mpan 688	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))
39	38	fveq2d 6851	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))))
40	35, 39	eqtr4d 2774	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))))
41	40	breq1d 5120	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1 ↔ ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1))
42	24, 41	imbi12d 344	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔ (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)))
43	42	ancoms 459	. . . . . . . . . 10 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔ (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)))
44	43	adantlr 713	. . . . . . . . 9 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔ (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)))
45	44	ralbidva 3168	. . . . . . . 8 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) → (∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)))
46		2fveq3 6852	. . . . . . . . . . . 12 ⊢ (𝑧 = (0vec‘𝑈) → ((normCV‘𝑊)‘(𝑇‘𝑧)) = ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))))
47		fveq2 6847	. . . . . . . . . . . . 13 ⊢ (𝑧 = (0vec‘𝑈) → ((normCV‘𝑈)‘𝑧) = ((normCV‘𝑈)‘(0vec‘𝑈)))
48	47	oveq2d 7378	. . . . . . . . . . . 12 ⊢ (𝑧 = (0vec‘𝑈) → ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) = ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))))
49	46, 48	breq12d 5123	. . . . . . . . . . 11 ⊢ (𝑧 = (0vec‘𝑈) → (((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈)))))
50	1	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑈 ∈ NrmCVec)
51		simpll 765	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑃 ∈ 𝑋)
52		simpr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ+)
53	2, 21	nvcl 29666	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → ((normCV‘𝑈)‘𝑧) ∈ ℝ)
54	1, 53	mpan 688	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ 𝑋 → ((normCV‘𝑈)‘𝑧) ∈ ℝ)
55	54	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) → ((normCV‘𝑈)‘𝑧) ∈ ℝ)
56		eqid 2731	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0vec‘𝑈) = (0vec‘𝑈)
57	2, 56, 21	nvgt0 29679	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → (𝑧 ≠ (0vec‘𝑈) ↔ 0 < ((normCV‘𝑈)‘𝑧)))
58	1, 57	mpan 688	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ 𝑋 → (𝑧 ≠ (0vec‘𝑈) ↔ 0 < ((normCV‘𝑈)‘𝑧)))
59	58	biimpa 477	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) → 0 < ((normCV‘𝑈)‘𝑧))
60	55, 59	elrpd 12963	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) → ((normCV‘𝑈)‘𝑧) ∈ ℝ+)
61		rpdivcl 12949	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ ℝ+ ∧ ((normCV‘𝑈)‘𝑧) ∈ ℝ+) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ+)
62	52, 60, 61	syl2an 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ+)
63	62	rpcnd 12968	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ)
64		simprl 769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑧 ∈ 𝑋)
65		eqid 2731	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( ·𝑠OLD ‘𝑈) = ( ·𝑠OLD ‘𝑈)
66	2, 65	nvscl 29631	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋) → ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧) ∈ 𝑋)
67	50, 63, 64, 66	syl3anc 1371	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧) ∈ 𝑋)
68		eqid 2731	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ( +𝑣 ‘𝑈) = ( +𝑣 ‘𝑈)
69	2, 68, 20	nvpncan2 29658	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧) ∈ 𝑋) → ((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))
70	50, 51, 67, 69	syl3anc 1371	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))
71	70	fveq2d 6851	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = ((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)))
72	62	rprege0d 12973	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 / ((normCV‘𝑈)‘𝑧))))
73	2, 65, 21	nvsge0 29669	. . . . . . . . . . . . . . . . . . 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 12934	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℂ)
76	75	ad2antlr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ∈ ℂ)
77	54	ad2antrl 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘𝑧) ∈ ℝ)
78	77	recnd 11192	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘𝑧) ∈ ℂ)
79	2, 56, 21	nvz 29674	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → (((normCV‘𝑈)‘𝑧) = 0 ↔ 𝑧 = (0vec‘𝑈)))
80	1, 79	mpan 688	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ 𝑋 → (((normCV‘𝑈)‘𝑧) = 0 ↔ 𝑧 = (0vec‘𝑈)))
81	80	necon3bid 2984	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ 𝑋 → (((normCV‘𝑈)‘𝑧) ≠ 0 ↔ 𝑧 ≠ (0vec‘𝑈)))
82	81	biimpar 478	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) → ((normCV‘𝑈)‘𝑧) ≠ 0)
83	82	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘𝑧) ≠ 0)
84	76, 78, 83	divcan1d 11941	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧)) = 𝑦)
85	71, 74, 84	3eqtrd 2775	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = 𝑦)
86		rpre 12932	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
87	86	leidd 11730	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ≤ 𝑦)
88	87	ad2antlr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ≤ 𝑦)
89	85, 88	eqbrtrd 5132	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦)
90	2, 68	nvgcl 29625	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧) ∈ 𝑋) → (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) ∈ 𝑋)
91	50, 51, 67, 90	syl3anc 1371	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) ∈ 𝑋)
92		fvoveq1 7385	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)))
93	92	breq1d 5120	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 ↔ ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦))
94		fvoveq1 7385	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)))
95	94	fveq2d 6851	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))))
96	95	breq1d 5120	. . . . . . . . . . . . . . . . . . 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 3578	. . . . . . . . . . . . . . . . 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 7039	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑋 → (𝑇‘𝑧) ∈ (BaseSet‘𝑊))
102	7, 32	nvcl 29666	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ)
103	6, 101, 102	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑋 → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ)
104	103	ad2antrl 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ)
105		1red 11165	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 1 ∈ ℝ)
106	104, 105, 62	lemuldiv2d 13016	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))) ≤ 1 ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (1 / (𝑦 / ((normCV‘𝑈)‘𝑧)))))
107	70	fveq2d 6851	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)))
108		eqid 2731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ( ·𝑠OLD ‘𝑊) = ( ·𝑠OLD ‘𝑊)
109	2, 65, 108, 26	lnomul 29765	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋)) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧)))
110	36, 109	mpan 688	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧)))
111	63, 64, 110	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧)))
112	107, 111	eqtrd 2771	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑊)(𝑇‘𝑧)))
113	112	fveq2d 6851	. . . . . . . . . . . . . . . . . 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 29669	. . . . . . . . . . . . . . . . . . 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 2771	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))))
119	118	breq1d 5120	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD ‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1 ↔ ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))) ≤ 1))
120		rpcnne0 12942	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℝ+ → (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0))
121		rpcnne0 12942	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((normCV‘𝑈)‘𝑧) ∈ ℝ+ → (((normCV‘𝑈)‘𝑧) ∈ ℂ ∧ ((normCV‘𝑈)‘𝑧) ≠ 0))
122		recdiv 11870	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) ∧ (((normCV‘𝑈)‘𝑧) ∈ ℂ ∧ ((normCV‘𝑈)‘𝑧) ≠ 0)) → (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))) = (((normCV‘𝑈)‘𝑧) / 𝑦))
123	120, 121, 122	syl2an 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ℝ+ ∧ ((normCV‘𝑈)‘𝑧) ∈ ℝ+) → (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))) = (((normCV‘𝑈)‘𝑧) / 𝑦))
124	52, 60, 123	syl2an 596	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))) = (((normCV‘𝑈)‘𝑧) / 𝑦))
125		rpne0 12940	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ≠ 0)
126	125	ad2antlr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ≠ 0)
127	78, 76, 126	divrec2d 11944	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((normCV‘𝑈)‘𝑧) / 𝑦) = ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
128	124, 127	eqtr2d 2772	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) = (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))))
129	128	breq2d 5122	. . . . . . . . . . . . . . . 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 468	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 ≠ (0vec‘𝑈)) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
133	132	imp 407	. . . . . . . . . . . 12 ⊢ (((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 ≠ (0vec‘𝑈)) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
134	133	an32s 650	. . . . . . . . . . 11 ⊢ (((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) ∧ 𝑧 ≠ (0vec‘𝑈)) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
135		eqid 2731	. . . . . . . . . . . . . . . . . 18 ⊢ (0vec‘𝑊) = (0vec‘𝑊)
136	2, 7, 56, 135, 26	lno0 29761	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇‘(0vec‘𝑈)) = (0vec‘𝑊))
137	1, 6, 25, 136	mp3an 1461	. . . . . . . . . . . . . . . 16 ⊢ (𝑇‘(0vec‘𝑈)) = (0vec‘𝑊)
138	137	fveq2i 6850	. . . . . . . . . . . . . . 15 ⊢ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) = ((normCV‘𝑊)‘(0vec‘𝑊))
139	135, 32	nvz0 29673	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 ∈ NrmCVec → ((normCV‘𝑊)‘(0vec‘𝑊)) = 0)
140	6, 139	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((normCV‘𝑊)‘(0vec‘𝑊)) = 0
141	138, 140	eqtri 2759	. . . . . . . . . . . . . 14 ⊢ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) = 0
142		0le0 12263	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 0
143	141, 142	eqbrtri 5131	. . . . . . . . . . . . 13 ⊢ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ 0
144	17	rpcnd 12968	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℂ)
145	56, 21	nvz0 29673	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ NrmCVec → ((normCV‘𝑈)‘(0vec‘𝑈)) = 0)
146	1, 145	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((normCV‘𝑈)‘(0vec‘𝑈)) = 0
147	146	oveq2i 7373	. . . . . . . . . . . . . . 15 ⊢ ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))) = ((1 / 𝑦) · 0)
148		mul01 11343	. . . . . . . . . . . . . . 15 ⊢ ((1 / 𝑦) ∈ ℂ → ((1 / 𝑦) · 0) = 0)
149	147, 148	eqtrid 2783	. . . . . . . . . . . . . 14 ⊢ ((1 / 𝑦) ∈ ℂ → ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))) = 0)
150	144, 149	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ+ → ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈))) = 0)
151	143, 150	breqtrrid 5148	. . . . . . . . . . . 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 3026	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
154	153	ex 413	. . . . . . . . 9 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
155	154	ralrimdva 3147	. . . . . . . 8 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
156	45, 155	sylbid 239	. . . . . . 7 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) → (∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
157	156	imp 407	. . . . . 6 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
158		oveq1 7369	. . . . . . . . 9 ⊢ (𝑥 = (1 / 𝑦) → (𝑥 · ((normCV‘𝑈)‘𝑧)) = ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))
159	158	breq2d 5122	. . . . . . . 8 ⊢ (𝑥 = (1 / 𝑦) → (((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
160	159	ralbidv 3170	. . . . . . 7 ⊢ (𝑥 = (1 / 𝑦) → (∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)) ↔ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))))
161	160	rspcev 3582	. . . . . 6 ⊢ (((1 / 𝑦) ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))
162	19, 157, 161	syl2anc 584	. . . . 5 ⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))
163	162	rexlimdva2 3150	. . . 4 ⊢ (𝑃 ∈ 𝑋 → (∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))))
164	16, 163	syl5 34	. . 3 ⊢ (𝑃 ∈ 𝑋 → (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))))
165	164	imp 407	. 2 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))
166		blocni.5	. . . 4 ⊢ 𝐵 = (𝑈 BLnOp 𝑊)
167	2, 21, 32, 26, 166, 1, 6	isblo3i 29806	. . 3 ⊢ (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))))
168	25, 167	mpbiran 707	. 2 ⊢ (𝑇 ∈ 𝐵 ↔ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))
169	165, 168	sylibr 233	1 ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑇 ∈ 𝐵)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2939  ∀wral 3060  ∃wrex 3069   class class class wbr 5110  ⟶wf 6497  ‘cfv 6501  (class class class)co 7362  ℂcc 11058  ℝcr 11059  0cc0 11060  1c1 11061   · cmul 11065   < clt 11198   ≤ cle 11199   / cdiv 11821  ℝ⁺crp 12924  ∞Metcxmet 20818  MetOpencmopn 20823   CnP ccnp 22613  NrmCVeccnv 29589   +_𝑣 cpv 29590  BaseSetcba 29591   ·_𝑠OLD cns 29592  0_veccn0v 29593   −_𝑣 cnsb 29594  norm_CVcnmcv 29595  IndMetcims 29596   LnOp clno 29745   BLnOp cblo 29747

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11116  ax-resscn 11117  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-addrcl 11121  ax-mulcl 11122  ax-mulrcl 11123  ax-mulcom 11124  ax-addass 11125  ax-mulass 11126  ax-distr 11127  ax-i2m1 11128  ax-1ne0 11129  ax-1rid 11130  ax-rnegex 11131  ax-rrecex 11132  ax-cnre 11133  ax-pre-lttri 11134  ax-pre-lttrn 11135  ax-pre-ltadd 11136  ax-pre-mulgt0 11137  ax-pre-sup 11138  ax-addf 11139  ax-mulf 11140

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-er 8655  df-map 8774  df-en 8891  df-dom 8892  df-sdom 8893  df-sup 9387  df-inf 9388  df-pnf 11200  df-mnf 11201  df-xr 11202  df-ltxr 11203  df-le 11204  df-sub 11396  df-neg 11397  df-div 11822  df-nn 12163  df-2 12225  df-3 12226  df-n0 12423  df-z 12509  df-uz 12773  df-q 12883  df-rp 12925  df-xneg 13042  df-xadd 13043  df-xmul 13044  df-seq 13917  df-exp 13978  df-cj 14996  df-re 14997  df-im 14998  df-sqrt 15132  df-abs 15133  df-topgen 17339  df-psmet 20825  df-xmet 20826  df-met 20827  df-bl 20828  df-mopn 20829  df-top 22280  df-topon 22297  df-bases 22333  df-cnp 22616  df-grpo 29498  df-gid 29499  df-ginv 29500  df-gdiv 29501  df-ablo 29550  df-vc 29564  df-nv 29597  df-va 29600  df-ba 29601  df-sm 29602  df-0v 29603  df-vs 29604  df-nmcv 29605  df-ims 29606  df-lno 29749  df-nmoo 29750  df-blo 29751  df-0o 29752

This theorem is referenced by:  blocni  29810  lnocni  29811