Theorem nmoub3i 10796

Description: An upper bound for an operator norm.

Hypotheses

Ref	Expression
nmoubi.1	|- X = (BaseSet` U)
nmoubi.y	|- Y = (BaseSet` W)
nmoubi.l	|- L = (norm` U)
nmoubi.m	|- M = (norm` W)
nmoubi.3	|- N = (UnormOpW)
nmoubi.u	|- U e. NrmCVec
nmoubi.w	|- W e. NrmCVec

Assertion

Ref	Expression
nmoub3i	|- ((T:X-->Y /\ A e. RR /\ A.x e. X (M` (T` x)) <_ (A x. (L` x))) -> (N` T) <_ (abs` A))

Distinct variable groups:   x,A   x,L   x,M   x,T   x,X   x,Y

Proof of Theorem nmoub3i

Step	Hyp	Ref	Expression
1		nmoubi.u	. . . . . . . . . . . . 13 |- U e. NrmCVec
2		nmoubi.1	. . . . . . . . . . . . . 14 |- X = (BaseSet` U)
3		nmoubi.l	. . . . . . . . . . . . . 14 |- L = (norm` U)
4	2, 3	nvcl 10640	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ x e. X) -> (L` x) e. RR)
5	1, 4	mpan 773	. . . . . . . . . . . 12 |- (x e. X -> (L` x) e. RR)
6		remulcl 6913	. . . . . . . . . . . 12 |- ((A e. RR /\ (L` x) e. RR) -> (A x. (L` x)) e. RR)
7	5, 6	sylan2 696	. . . . . . . . . . 11 |- ((A e. RR /\ x e. X) -> (A x. (L` x)) e. RR)
8	7	adantr 543	. . . . . . . . . 10 |- (((A e. RR /\ x e. X) /\ (L` x) <_ 1) -> (A x. (L` x)) e. RR)
9		recn 6919	. . . . . . . . . . . . 13 |- (A e. RR -> A e. CC)
10		abscl 8584	. . . . . . . . . . . . 13 |- (A e. CC -> (abs` A) e. RR)
11	9, 10	syl 13	. . . . . . . . . . . 12 |- (A e. RR -> (abs` A) e. RR)
12		remulcl 6913	. . . . . . . . . . . 12 |- (((abs` A) e. RR /\ (L` x) e. RR) -> ((abs` A) x. (L` x)) e. RR)
13	11, 5, 12	syl2an 699	. . . . . . . . . . 11 |- ((A e. RR /\ x e. X) -> ((abs` A) x. (L` x)) e. RR)
14	13	adantr 543	. . . . . . . . . 10 |- (((A e. RR /\ x e. X) /\ (L` x) <_ 1) -> ((abs` A) x. (L` x)) e. RR)
15	11	ad2antrr 856	. . . . . . . . . 10 |- (((A e. RR /\ x e. X) /\ (L` x) <_ 1) -> (abs` A) e. RR)
16		simpl 533	. . . . . . . . . . . 12 |- ((A e. RR /\ x e. X) -> A e. RR)
17	11	adantr 543	. . . . . . . . . . . 12 |- ((A e. RR /\ x e. X) -> (abs` A) e. RR)
18	2, 3	nvge0 10655	. . . . . . . . . . . . . . 15 |- ((U e. NrmCVec /\ x e. X) -> 0 <_ (L` x))
19	1, 18	mpan 773	. . . . . . . . . . . . . 14 |- (x e. X -> 0 <_ (L` x))
20	5, 19	jca 590	. . . . . . . . . . . . 13 |- (x e. X -> ((L` x) e. RR /\ 0 <_ (L` x)))
21	20	adantl 544	. . . . . . . . . . . 12 |- ((A e. RR /\ x e. X) -> ((L` x) e. RR /\ 0 <_ (L` x)))
22		leabs 8615	. . . . . . . . . . . . 13 |- (A e. RR -> A <_ (abs` A))
23	22	adantr 543	. . . . . . . . . . . 12 |- ((A e. RR /\ x e. X) -> A <_ (abs` A))
24		lemul1a 7452	. . . . . . . . . . . 12 |- (((A e. RR /\ (abs` A) e. RR /\ ((L` x) e. RR /\ 0 <_ (L` x))) /\ A <_ (abs` A)) -> (A x. (L` x)) <_ ((abs` A) x. (L` x)))
25	16, 17, 21, 23, 24	syl31anc 1380	. . . . . . . . . . 11 |- ((A e. RR /\ x e. X) -> (A x. (L` x)) <_ ((abs` A) x. (L` x)))
26	25	adantr 543	. . . . . . . . . 10 |- (((A e. RR /\ x e. X) /\ (L` x) <_ 1) -> (A x. (L` x)) <_ ((abs` A) x. (L` x)))
27	5	adantl 544	. . . . . . . . . . . . 13 |- ((A e. RR /\ x e. X) -> (L` x) e. RR)
28		1re 6941	. . . . . . . . . . . . . 14 |- 1 e. RR
29	28	a1i 8	. . . . . . . . . . . . 13 |- ((A e. RR /\ x e. X) -> 1 e. RR)
30		absge0 8605	. . . . . . . . . . . . . . . 16 |- (A e. CC -> 0 <_ (abs` A))
31	9, 30	syl 13	. . . . . . . . . . . . . . 15 |- (A e. RR -> 0 <_ (abs` A))
32	31	adantr 543	. . . . . . . . . . . . . 14 |- ((A e. RR /\ x e. X) -> 0 <_ (abs` A))
33	17, 32	jca 590	. . . . . . . . . . . . 13 |- ((A e. RR /\ x e. X) -> ((abs` A) e. RR /\ 0 <_ (abs` A)))
34	27, 29, 33	3jca 1328	. . . . . . . . . . . 12 |- ((A e. RR /\ x e. X) -> ((L` x) e. RR /\ 1 e. RR /\ ((abs` A) e. RR /\ 0 <_ (abs` A))))
35		lemul2a 7454	. . . . . . . . . . . 12 |- ((((L` x) e. RR /\ 1 e. RR /\ ((abs` A) e. RR /\ 0 <_ (abs` A))) /\ (L` x) <_ 1) -> ((abs` A) x. (L` x)) <_ ((abs` A) x. 1))
36	34, 35	sylan 693	. . . . . . . . . . 11 |- (((A e. RR /\ x e. X) /\ (L` x) <_ 1) -> ((abs` A) x. (L` x)) <_ ((abs` A) x. 1))
37	11	recnd 6921	. . . . . . . . . . . . 13 |- (A e. RR -> (abs` A) e. CC)
38		mulid1 6934	. . . . . . . . . . . . 13 |- ((abs` A) e. CC -> ((abs` A) x. 1) = (abs` A))
39	37, 38	syl 13	. . . . . . . . . . . 12 |- (A e. RR -> ((abs` A) x. 1) = (abs` A))
40	39	ad2antrr 856	. . . . . . . . . . 11 |- (((A e. RR /\ x e. X) /\ (L` x) <_ 1) -> ((abs` A) x. 1) = (abs` A))
41	36, 40	breqtrd 3563	. . . . . . . . . 10 |- (((A e. RR /\ x e. X) /\ (L` x) <_ 1) -> ((abs` A) x. (L` x)) <_ (abs` A))
42	8, 14, 15, 26, 41	letrd 6987	. . . . . . . . 9 |- (((A e. RR /\ x e. X) /\ (L` x) <_ 1) -> (A x. (L` x)) <_ (abs` A))
43	42	adantlll 840	. . . . . . . 8 |- ((((T:X-->Y /\ A e. RR) /\ x e. X) /\ (L` x) <_ 1) -> (A x. (L` x)) <_ (abs` A))
44		nmoubi.w	. . . . . . . . . . . 12 |- W e. NrmCVec
45		ffvelrn 4916	. . . . . . . . . . . 12 |- ((T:X-->Y /\ x e. X) -> (T` x) e. Y)
46		nmoubi.y	. . . . . . . . . . . . 13 |- Y = (BaseSet` W)
47		nmoubi.m	. . . . . . . . . . . . 13 |- M = (norm` W)
48	46, 47	nvcl 10640	. . . . . . . . . . . 12 |- ((W e. NrmCVec /\ (T` x) e. Y) -> (M` (T` x)) e. RR)
49	44, 45, 48	sylancr 758	. . . . . . . . . . 11 |- ((T:X-->Y /\ x e. X) -> (M` (T` x)) e. RR)
50	49	adantlr 834	. . . . . . . . . 10 |- (((T:X-->Y /\ A e. RR) /\ x e. X) -> (M` (T` x)) e. RR)
51	7	adantll 832	. . . . . . . . . 10 |- (((T:X-->Y /\ A e. RR) /\ x e. X) -> (A x. (L` x)) e. RR)
52	11	ad2antlr 859	. . . . . . . . . 10 |- (((T:X-->Y /\ A e. RR) /\ x e. X) -> (abs` A) e. RR)
53		letr 6986	. . . . . . . . . 10 |- (((M` (T` x)) e. RR /\ (A x. (L` x)) e. RR /\ (abs` A) e. RR) -> (((M` (T` x)) <_ (A x. (L` x)) /\ (A x. (L` x)) <_ (abs` A)) -> (M` (T` x)) <_ (abs` A)))
54	50, 51, 52, 53	syl111anc 1377	. . . . . . . . 9 |- (((T:X-->Y /\ A e. RR) /\ x e. X) -> (((M` (T` x)) <_ (A x. (L` x)) /\ (A x. (L` x)) <_ (abs` A)) -> (M` (T` x)) <_ (abs` A)))
55	54	adantr 543	. . . . . . . 8 |- ((((T:X-->Y /\ A e. RR) /\ x e. X) /\ (L` x) <_ 1) -> (((M` (T` x)) <_ (A x. (L` x)) /\ (A x. (L` x)) <_ (abs` A)) -> (M` (T` x)) <_ (abs` A)))
56	43, 55	mpan2d 779	. . . . . . 7 |- ((((T:X-->Y /\ A e. RR) /\ x e. X) /\ (L` x) <_ 1) -> ((M` (T` x)) <_ (A x. (L` x)) -> (M` (T` x)) <_ (abs` A)))
57	56	ex 494	. . . . . 6 |- (((T:X-->Y /\ A e. RR) /\ x e. X) -> ((L` x) <_ 1 -> ((M` (T` x)) <_ (A x. (L` x)) -> (M` (T` x)) <_ (abs` A))))
58	57	com23 68	. . . . 5 |- (((T:X-->Y /\ A e. RR) /\ x e. X) -> ((M` (T` x)) <_ (A x. (L` x)) -> ((L` x) <_ 1 -> (M` (T` x)) <_ (abs` A))))
59	58	ralimdva 2451	. . . 4 |- ((T:X-->Y /\ A e. RR) -> (A.x e. X (M` (T` x)) <_ (A x. (L` x)) -> A.x e. X ((L` x) <_ 1 -> (M` (T` x)) <_ (abs` A))))
60	59	imp 489	. . 3 |- (((T:X-->Y /\ A e. RR) /\ A.x e. X (M` (T` x)) <_ (A x. (L` x))) -> A.x e. X ((L` x) <_ 1 -> (M` (T` x)) <_ (abs` A)))
61		rexr 6960	. . . . . 6 |- ((abs` A) e. RR -> (abs` A) e. RR*)
62	11, 61	syl 13	. . . . 5 |- (A e. RR -> (abs` A) e. RR*)
63		nmoubi.3	. . . . . 6 |- N = (UnormOpW)
64	2, 46, 3, 47, 63, 1, 44	nmoubi 10795	. . . . 5 |- ((T:X-->Y /\ (abs` A) e. RR* /\ A.x e. X ((L` x) <_ 1 -> (M` (T` x)) <_ (abs` A))) -> (N` T) <_ (abs` A))
65	62, 64	syl3an2 1411	. . . 4 |- ((T:X-->Y /\ A e. RR /\ A.x e. X ((L` x) <_ 1 -> (M` (T` x)) <_ (abs` A))) -> (N` T) <_ (abs` A))
66	65	3expa 1345	. . 3 |- (((T:X-->Y /\ A e. RR) /\ A.x e. X ((L` x) <_ 1 -> (M` (T` x)) <_ (abs` A))) -> (N` T) <_ (abs` A))
67	60, 66	syldan 691	. 2 |- (((T:X-->Y /\ A e. RR) /\ A.x e. X (M` (T` x)) <_ (A x. (L` x))) -> (N` T) <_ (abs` A))
68	67	3impa 1340	1 |- ((T:X-->Y /\ A e. RR /\ A.x e. X (M` (T` x)) <_ (A x. (L` x))) -> (N` T) <_ (abs` A))

Syntax hints:   -> wi 3   /\ wa 433   /\ w3a 1130   = wceq 1615   e. wcel 1617  A.wral 2385   class class class wbr 3539  -->wf 4159  ` cfv 4163  (class class class)co 5020  CCcc 6827  RRcr 6828  0cc0 6829  1c1 6830   x. cmul 6834   <_ cle 6943  RR*cxr 6946  abscabs 8500  NrmCVeccnv 10556  BaseSetcba 10558  normcnm 10562  normOpcnmo 10762

This theorem is referenced by:  nmoub2i 10797  isblo3i 10824

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961  ax-cnex 6885  ax-resscn 6886  ax-1cn 6887  ax-icn 6888  ax-addcl 6889  ax-addrcl 6890  ax-mulcl 6891  ax-mulrcl 6892  ax-mulcom 6893  ax-addass 6894  ax-mulass 6895  ax-distr 6896  ax-i2m1 6897  ax-1ne0 6898  ax-1rid 6899  ax-rnegex 6900  ax-rrecex 6901  ax-cnre 6902  ax-pre-lttri 6903  ax-pre-lttrn 6904  ax-pre-ltadd 6905  ax-pre-mulgt0 6906  ax-pre-sup 6907  ax-mulopr 6909

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3or 1131  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-nel 2298  df-ral 2389  df-rex 2390  df-reu 2391  df-rab 2392  df-v 2571  df-sbc 2731  df-csb 2806  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-pss 2870  df-nul 3115  df-if 3213  df-pw 3261  df-sn 3274  df-pr 3275  df-tp 3277  df-op 3278  df-uni 3399  df-int 3433  df-iun 3470  df-br 3540  df-opab 3598  df-tr 3612  df-eprel 3776  df-id 3779  df-po 3784  df-so 3796  df-fr 3814  df-we 3830  df-ord 3846  df-on 3847  df-lim 3848  df-suc 3849  df-om 4118  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-f 4175  df-f1 4176  df-fo 4177  df-f1o 4178  df-fv 4179  df-opr 5022  df-oprab 5023  df-mpt 5138  df-1st 5166  df-2nd 5167  df-iota 5259  df-rdg 5344  df-er 5519  df-map 5587  df-en 5631  df-dom 5632  df-sdom 5633  df-undef 5769  df-riota 5773  df-sup 5932  df-pnf 6948  df-mnf 6949  df-xr 6950  df-ltxr 6951  df-le 6952  df-sub 7111  df-neg 7113  df-div 7325  df-n 7543  df-2 7589  df-n0 7761  df-z 7798  df-seq1 8210  df-exp 8312  df-sqr 8420  df-re 8501  df-im 8502  df-cj 8503  df-abs 8504  df-grpo 10334  df-gid 10335  df-ginv 10336  df-ablo 10429  df-vc 10518  df-nv 10564  df-va 10567  df-ba 10568  df-sm 10569  df-0v 10570  df-nm 10572  df-nmo 10766

Copyright terms: Public domain