nmoub3i - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > nmoub3i		Structured version Visualization version GIF version

Theorem nmoub3i 28640

Description: An upper bound for an operator norm. (Contributed by NM, 12-Dec-2007.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
nmoubi.1	⊢ 𝑋 = (BaseSet‘𝑈)
nmoubi.y	⊢ 𝑌 = (BaseSet‘𝑊)
nmoubi.l	⊢ 𝐿 = (norm_CV‘𝑈)
nmoubi.m	⊢ 𝑀 = (norm_CV‘𝑊)
nmoubi.3	⊢ 𝑁 = (𝑈 normOp_OLD 𝑊)
nmoubi.u	⊢ 𝑈 ∈ NrmCVec
nmoubi.w	⊢ 𝑊 ∈ NrmCVec

**Assertion**
Ref	Expression
nmoub3i	⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ ∧ ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥))) → (𝑁‘𝑇) ≤ (abs‘𝐴))

Distinct variable groups: 𝑥,𝐴 𝑥,𝐿 𝑥,𝑈 𝑥,𝑊 𝑥,𝑌 𝑥,𝑀 𝑥,𝑇 𝑥,𝑋 Allowed substitution hint: 𝑁(𝑥)

**Proof of Theorem nmoub3i**
Step	Hyp	Ref	Expression
1		nmoubi.u	. . . . . . . . . . . . 13 ⊢ 𝑈 ∈ NrmCVec
2		nmoubi.1	. . . . . . . . . . . . . 14 ⊢ 𝑋 = (BaseSet‘𝑈)
3		nmoubi.l	. . . . . . . . . . . . . 14 ⊢ 𝐿 = (norm_CV‘𝑈)
4	2, 3	nvcl 28528	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) → (𝐿‘𝑥) ∈ ℝ)
5	1, 4	mpan 690	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝑋 → (𝐿‘𝑥) ∈ ℝ)
6		remulcl 10645	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ (𝐿‘𝑥) ∈ ℝ) → (𝐴 · (𝐿‘𝑥)) ∈ ℝ)
7	5, 6	sylan2 596	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → (𝐴 · (𝐿‘𝑥)) ∈ ℝ)
8	7	adantr 485	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → (𝐴 · (𝐿‘𝑥)) ∈ ℝ)
9		recn 10650	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
10	9	abscld 14829	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → (abs‘𝐴) ∈ ℝ)
11		remulcl 10645	. . . . . . . . . . . 12 ⊢ (((abs‘𝐴) ∈ ℝ ∧ (𝐿‘𝑥) ∈ ℝ) → ((abs‘𝐴) · (𝐿‘𝑥)) ∈ ℝ)
12	10, 5, 11	syl2an 599	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → ((abs‘𝐴) · (𝐿‘𝑥)) ∈ ℝ)
13	12	adantr 485	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → ((abs‘𝐴) · (𝐿‘𝑥)) ∈ ℝ)
14	10	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → (abs‘𝐴) ∈ ℝ)
15		simpl 487	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℝ)
16	10	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → (abs‘𝐴) ∈ ℝ)
17	2, 3	nvge0 28540	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) → 0 ≤ (𝐿‘𝑥))
18	1, 17	mpan 690	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝑋 → 0 ≤ (𝐿‘𝑥))
19	5, 18	jca 516	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝑋 → ((𝐿‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐿‘𝑥)))
20	19	adantl 486	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → ((𝐿‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐿‘𝑥)))
21		leabs 14692	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (abs‘𝐴))
22	21	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → 𝐴 ≤ (abs‘𝐴))
23		lemul1a 11517	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ (abs‘𝐴) ∈ ℝ ∧ ((𝐿‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐿‘𝑥))) ∧ 𝐴 ≤ (abs‘𝐴)) → (𝐴 · (𝐿‘𝑥)) ≤ ((abs‘𝐴) · (𝐿‘𝑥)))
24	15, 16, 20, 22, 23	syl31anc 1371	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → (𝐴 · (𝐿‘𝑥)) ≤ ((abs‘𝐴) · (𝐿‘𝑥)))
25	24	adantr 485	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → (𝐴 · (𝐿‘𝑥)) ≤ ((abs‘𝐴) · (𝐿‘𝑥)))
26	5	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → (𝐿‘𝑥) ∈ ℝ)
27		1red 10665	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → 1 ∈ ℝ)
28	9	absge0d 14837	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℝ → 0 ≤ (abs‘𝐴))
29	28	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → 0 ≤ (abs‘𝐴))
30	16, 29	jca 516	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
31	26, 27, 30	3jca 1126	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) → ((𝐿‘𝑥) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴))))
32		lemul2a 11518	. . . . . . . . . . . 12 ⊢ ((((𝐿‘𝑥) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴))) ∧ (𝐿‘𝑥) ≤ 1) → ((abs‘𝐴) · (𝐿‘𝑥)) ≤ ((abs‘𝐴) · 1))
33	31, 32	sylan 584	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → ((abs‘𝐴) · (𝐿‘𝑥)) ≤ ((abs‘𝐴) · 1))
34	10	recnd 10692	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℝ → (abs‘𝐴) ∈ ℂ)
35	34	mulid1d 10681	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → ((abs‘𝐴) · 1) = (abs‘𝐴))
36	35	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → ((abs‘𝐴) · 1) = (abs‘𝐴))
37	33, 36	breqtrd 5051	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → ((abs‘𝐴) · (𝐿‘𝑥)) ≤ (abs‘𝐴))
38	8, 13, 14, 25, 37	letrd 10820	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → (𝐴 · (𝐿‘𝑥)) ≤ (abs‘𝐴))
39	38	adantlll 718	. . . . . . . 8 ⊢ ((((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → (𝐴 · (𝐿‘𝑥)) ≤ (abs‘𝐴))
40		nmoubi.w	. . . . . . . . . . . 12 ⊢ 𝑊 ∈ NrmCVec
41		ffvelrn 6833	. . . . . . . . . . . 12 ⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝑥 ∈ 𝑋) → (𝑇‘𝑥) ∈ 𝑌)
42		nmoubi.y	. . . . . . . . . . . . 13 ⊢ 𝑌 = (BaseSet‘𝑊)
43		nmoubi.m	. . . . . . . . . . . . 13 ⊢ 𝑀 = (norm_CV‘𝑊)
44	42, 43	nvcl 28528	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝑥) ∈ 𝑌) → (𝑀‘(𝑇‘𝑥)) ∈ ℝ)
45	40, 41, 44	sylancr 591	. . . . . . . . . . 11 ⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝑥 ∈ 𝑋) → (𝑀‘(𝑇‘𝑥)) ∈ ℝ)
46	45	adantlr 715	. . . . . . . . . 10 ⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → (𝑀‘(𝑇‘𝑥)) ∈ ℝ)
47	7	adantll 714	. . . . . . . . . 10 ⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → (𝐴 · (𝐿‘𝑥)) ∈ ℝ)
48	10	ad2antlr 727	. . . . . . . . . 10 ⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → (abs‘𝐴) ∈ ℝ)
49		letr 10757	. . . . . . . . . 10 ⊢ (((𝑀‘(𝑇‘𝑥)) ∈ ℝ ∧ (𝐴 · (𝐿‘𝑥)) ∈ ℝ ∧ (abs‘𝐴) ∈ ℝ) → (((𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) ∧ (𝐴 · (𝐿‘𝑥)) ≤ (abs‘𝐴)) → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴)))
50	46, 47, 48, 49	syl3anc 1369	. . . . . . . . 9 ⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → (((𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) ∧ (𝐴 · (𝐿‘𝑥)) ≤ (abs‘𝐴)) → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴)))
51	50	adantr 485	. . . . . . . 8 ⊢ ((((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → (((𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) ∧ (𝐴 · (𝐿‘𝑥)) ≤ (abs‘𝐴)) → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴)))
52	39, 51	mpan2d 694	. . . . . . 7 ⊢ ((((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝐿‘𝑥) ≤ 1) → ((𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴)))
53	52	ex 417	. . . . . 6 ⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → ((𝐿‘𝑥) ≤ 1 → ((𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴))))
54	53	com23 86	. . . . 5 ⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → ((𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) → ((𝐿‘𝑥) ≤ 1 → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴))))
55	54	ralimdva 3106	. . . 4 ⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) → (∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) → ∀𝑥 ∈ 𝑋 ((𝐿‘𝑥) ≤ 1 → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴))))
56	55	imp 411	. . 3 ⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥))) → ∀𝑥 ∈ 𝑋 ((𝐿‘𝑥) ≤ 1 → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴)))
57	10	rexrd 10714	. . . . 5 ⊢ (𝐴 ∈ ℝ → (abs‘𝐴) ∈ ℝ^*)
58		nmoubi.3	. . . . . 6 ⊢ 𝑁 = (𝑈 normOp_OLD 𝑊)
59	2, 42, 3, 43, 58, 1, 40	nmoubi 28639	. . . . 5 ⊢ ((𝑇:𝑋⟶𝑌 ∧ (abs‘𝐴) ∈ ℝ^*) → ((𝑁‘𝑇) ≤ (abs‘𝐴) ↔ ∀𝑥 ∈ 𝑋 ((𝐿‘𝑥) ≤ 1 → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴))))
60	57, 59	sylan2 596	. . . 4 ⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) → ((𝑁‘𝑇) ≤ (abs‘𝐴) ↔ ∀𝑥 ∈ 𝑋 ((𝐿‘𝑥) ≤ 1 → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴))))
61	60	biimpar 482	. . 3 ⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ ∀𝑥 ∈ 𝑋 ((𝐿‘𝑥) ≤ 1 → (𝑀‘(𝑇‘𝑥)) ≤ (abs‘𝐴))) → (𝑁‘𝑇) ≤ (abs‘𝐴))
62	56, 61	syldan 595	. 2 ⊢ (((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ) ∧ ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥))) → (𝑁‘𝑇) ≤ (abs‘𝐴))
63	62	3impa 1108	1 ⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ ∧ ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥))) → (𝑁‘𝑇) ≤ (abs‘𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1085 = wceq 1539 ∈ wcel 2112 ∀wral 3068 class class class wbr 5025 ⟶wf 6324 ‘cfv 6328 (class class class)co 7143 ℝcr 10559 0cc0 10560 1c1 10561 · cmul 10565 ℝ^*cxr 10697 ≤ cle 10699 abscabs 14626 NrmCVeccnv 28451 BaseSetcba 28453 norm_CVcnmcv 28457 normOp_OLD cnmoo 28608

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-rep 5149 ax-sep 5162 ax-nul 5169 ax-pow 5227 ax-pr 5291 ax-un 7452 ax-cnex 10616 ax-resscn 10617 ax-1cn 10618 ax-icn 10619 ax-addcl 10620 ax-addrcl 10621 ax-mulcl 10622 ax-mulrcl 10623 ax-mulcom 10624 ax-addass 10625 ax-mulass 10626 ax-distr 10627 ax-i2m1 10628 ax-1ne0 10629 ax-1rid 10630 ax-rnegex 10631 ax-rrecex 10632 ax-cnre 10633 ax-pre-lttri 10634 ax-pre-lttrn 10635 ax-pre-ltadd 10636 ax-pre-mulgt0 10637 ax-pre-sup 10638

This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2899 df-ne 2950 df-nel 3054 df-ral 3073 df-rex 3074 df-reu 3075 df-rmo 3076 df-rab 3077 df-v 3409 df-sbc 3694 df-csb 3802 df-dif 3857 df-un 3859 df-in 3861 df-ss 3871 df-pss 3873 df-nul 4222 df-if 4414 df-pw 4489 df-sn 4516 df-pr 4518 df-tp 4520 df-op 4522 df-uni 4792 df-iun 4878 df-br 5026 df-opab 5088 df-mpt 5106 df-tr 5132 df-id 5423 df-eprel 5428 df-po 5436 df-so 5437 df-fr 5476 df-we 5478 df-xp 5523 df-rel 5524 df-cnv 5525 df-co 5526 df-dm 5527 df-rn 5528 df-res 5529 df-ima 5530 df-pred 6119 df-ord 6165 df-on 6166 df-lim 6167 df-suc 6168 df-iota 6287 df-fun 6330 df-fn 6331 df-f 6332 df-f1 6333 df-fo 6334 df-f1o 6335 df-fv 6336 df-riota 7101 df-ov 7146 df-oprab 7147 df-mpo 7148 df-om 7573 df-1st 7686 df-2nd 7687 df-wrecs 7950 df-recs 8011 df-rdg 8049 df-er 8292 df-map 8411 df-en 8521 df-dom 8522 df-sdom 8523 df-sup 8924 df-pnf 10700 df-mnf 10701 df-xr 10702 df-ltxr 10703 df-le 10704 df-sub 10895 df-neg 10896 df-div 11321 df-nn 11660 df-2 11722 df-3 11723 df-n0 11920 df-z 12006 df-uz 12268 df-rp 12416 df-seq 13404 df-exp 13465 df-cj 14491 df-re 14492 df-im 14493 df-sqrt 14627 df-abs 14628 df-grpo 28360 df-gid 28361 df-ginv 28362 df-ablo 28412 df-vc 28426 df-nv 28459 df-va 28462 df-ba 28463 df-sm 28464 df-0v 28465 df-nmcv 28467 df-nmoo 28612

This theorem is referenced by: nmoub2i 28641 isblo3i 28668

W3C validator