Theorem blocnilem 9804

Description: Lemma for blocni 9805 and lnocni 9806. If a linear operator is continuous at any point, it is bounded. Warning: The HTML proof page is 0.7MB in size.

Hypotheses

Ref	Expression
blocni.8	|- C = (IndMet` U)
blocni.d	|- D = (IndMet` W)
blocni.j	|- J = (Open` C)
blocni.k	|- K = (Open` D)
blocni.4	|- L = (U LnOp W)
blocni.5	|- B = (U BLnOp W)
blocni.u	|- U e. NrmCVec
blocni.w	|- W e. NrmCVec
blocni.l	|- T e. L
blocnilem.1	|- X = (BaseSet` U)

Assertion

Ref	Expression
blocnilem	|- ((P e. X /\ T e. ((J CnP K)` P)) -> T e. B)

Proof of Theorem blocnilem

Step	Hyp	Ref	Expression
1		blocni.w	. . . . 5 |- W e. NrmCVec
2		blocni.u	. . . . . 6 |- U e. NrmCVec
3		1re 6598	. . . . . . 7 |- 1 e. RR
4		lt01 6871	. . . . . . . 8 |- 0 < 1
5		blocnilem.1	. . . . . . . . 9 |- X = (BaseSet` U)
6		eqid 1884	. . . . . . . . 9 |- (norm` U) = (norm` U)
7		eqid 1884	. . . . . . . . 9 |- (norm` W) = (norm` W)
8		eqid 1884	. . . . . . . . 9 |- (-v` U) = (-v` U)
9		blocni.8	. . . . . . . . 9 |- C = (IndMet` U)
10		blocni.d	. . . . . . . . 9 |- D = (IndMet` W)
11		blocni.j	. . . . . . . . 9 |- J = (Open` C)
12		blocni.k	. . . . . . . . 9 |- K = (Open` D)
13		blocni.4	. . . . . . . . 9 |- L = (U LnOp W)
14		blocni.l	. . . . . . . . 9 |- T e. L
15	5, 6, 7, 8, 9, 10, 11, 12, 13, 14	nvcnpi4 9762	. . . . . . . 8 |- (((U e. NrmCVec /\ W e. NrmCVec /\ P e. X) /\ (T e. ((J CnP K)` P) /\ 1 e. RR /\ 0 < 1)) -> E.z e. RR (0 < z /\ A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1)))
16	4, 15	mp3anr3 1190	. . . . . . 7 |- (((U e. NrmCVec /\ W e. NrmCVec /\ P e. X) /\ (T e. ((J CnP K)` P) /\ 1 e. RR)) -> E.z e. RR (0 < z /\ A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1)))
17	3, 16	mpanr2 776	. . . . . 6 |- (((U e. NrmCVec /\ W e. NrmCVec /\ P e. X) /\ T e. ((J CnP K)` P)) -> E.z e. RR (0 < z /\ A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1)))
18	2, 17	mp3anl1 1185	. . . . 5 |- (((W e. NrmCVec /\ P e. X) /\ T e. ((J CnP K)` P)) -> E.z e. RR (0 < z /\ A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1)))
19	1, 18	mpanl1 770	. . . 4 |- ((P e. X /\ T e. ((J CnP K)` P)) -> E.z e. RR (0 < z /\ A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1)))
20		gt0ne0 6800	. . . . . . . . . . 11 |- ((z e. RR /\ 0 < z) -> z =/= 0)
21		rereccl 6981	. . . . . . . . . . 11 |- ((z e. RR /\ z =/= 0) -> (1 / z) e. RR)
22	20, 21	syldan 516	. . . . . . . . . 10 |- ((z e. RR /\ 0 < z) -> (1 / z) e. RR)
23	22	ad2antlr 441	. . . . . . . . 9 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1)) -> (1 / z) e. RR)
24		fveq2 4681	. . . . . . . . . . . . 13 |- (w = (0v` U) -> (T` w) = (T` (0v` U)))
25	24	fveq2d 4685	. . . . . . . . . . . 12 |- (w = (0v` U) -> ((norm` W)` (T` w)) = ((norm` W)` (T` (0v` U))))
26		fveq2 4681	. . . . . . . . . . . . 13 |- (w = (0v` U) -> ((norm` U)` w) = ((norm` U)` (0v` U)))
27	26	opreq2d 4898	. . . . . . . . . . . 12 |- (w = (0v` U) -> ((1 / z) x. ((norm` U)` w)) = ((1 / z) x. ((norm` U)` (0v` U))))
28	25, 27	breq12d 3351	. . . . . . . . . . 11 |- (w = (0v` U) -> (((norm` W)` (T` w)) <_ ((1 / z) x. ((norm` U)` w)) <-> ((norm` W)` (T` (0v` U))) <_ ((1 / z) x. ((norm` U)` (0v` U)))))
29		simpll 448	. . . . . . . . . . . . . . . . . . . . . 22 |- (((P e. X /\ z e. RR) /\ (w e. X /\ w =/= (0v` U))) -> P e. X)
30		redivcl 6978	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((z e. RR /\ ((norm` U)` w) e. RR /\ ((norm` U)` w) =/= 0) -> (z / ((norm` U)` w)) e. RR)
31	30	3expb 1068	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((z e. RR /\ (((norm` U)` w) e. RR /\ ((norm` U)` w) =/= 0)) -> (z / ((norm` U)` w)) e. RR)
32	5, 6	nvcl 9619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((U e. NrmCVec /\ w e. X) -> ((norm` U)` w) e. RR)
33	2, 32	mpan 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w e. X -> ((norm` U)` w) e. RR)
34	33	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((w e. X /\ w =/= (0v` U)) -> ((norm` U)` w) e. RR)
35		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (0v` U) = (0v` U)
36	5, 35, 6	nvz 9629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((U e. NrmCVec /\ w e. X) -> (((norm` U)` w) = 0 <-> w = (0v` U)))
37	2, 36	mpan 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w e. X -> (((norm` U)` w) = 0 <-> w = (0v` U)))
38	37	necon3bid 2035	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w e. X -> (((norm` U)` w) =/= 0 <-> w =/= (0v` U)))
39	38	biimpar 461	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((w e. X /\ w =/= (0v` U)) -> ((norm` U)` w) =/= 0)
40	34, 39	jca 310	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((w e. X /\ w =/= (0v` U)) -> (((norm` U)` w) e. RR /\ ((norm` U)` w) =/= 0))
41	31, 40	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((z e. RR /\ (w e. X /\ w =/= (0v` U))) -> (z / ((norm` U)` w)) e. RR)
42	41	recnd 6468	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((z e. RR /\ (w e. X /\ w =/= (0v` U))) -> (z / ((norm` U)` w)) e. CC)
43		simprl 450	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((z e. RR /\ (w e. X /\ w =/= (0v` U))) -> w e. X)
44		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (.s` U) = (.s` U)
45	5, 44	nvscl 9579	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((U e. NrmCVec /\ (z / ((norm` U)` w)) e. CC /\ w e. X) -> ((z / ((norm` U)` w))(.s` U)w) e. X)
46	2, 45	mp3an1 1178	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((z / ((norm` U)` w)) e. CC /\ w e. X) -> ((z / ((norm` U)` w))(.s` U)w) e. X)
47	42, 43, 46	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((z e. RR /\ (w e. X /\ w =/= (0v` U))) -> ((z / ((norm` U)` w))(.s` U)w) e. X)
48	47	adantll 428	. . . . . . . . . . . . . . . . . . . . . 22 |- (((P e. X /\ z e. RR) /\ (w e. X /\ w =/= (0v` U))) -> ((z / ((norm` U)` w))(.s` U)w) e. X)
49	5, 8	nvnncan 9615	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((U e. NrmCVec /\ P e. X /\ ((z / ((norm` U)` w))(.s` U)w) e. X) -> (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w))) = ((z / ((norm` U)` w))(.s` U)w))
50	2, 49	mp3an1 1178	. . . . . . . . . . . . . . . . . . . . . 22 |- ((P e. X /\ ((z / ((norm` U)` w))(.s` U)w) e. X) -> (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w))) = ((z / ((norm` U)` w))(.s` U)w))
51	29, 48, 50	syl11anc 524	. . . . . . . . . . . . . . . . . . . . 21 |- (((P e. X /\ z e. RR) /\ (w e. X /\ w =/= (0v` U))) -> (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w))) = ((z / ((norm` U)` w))(.s` U)w))
52	51	adantlrr 435	. . . . . . . . . . . . . . . . . . . 20 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w))) = ((z / ((norm` U)` w))(.s` U)w))
53	52	fveq2d 4685	. . . . . . . . . . . . . . . . . . 19 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> ((norm` U)` (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w)))) = ((norm` U)` ((z / ((norm` U)` w))(.s` U)w)))
54	41	adantlr 429	. . . . . . . . . . . . . . . . . . . . . 22 |- (((z e. RR /\ 0 < z) /\ (w e. X /\ w =/= (0v` U))) -> (z / ((norm` U)` w)) e. RR)
55		divge0 7038	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((z e. RR /\ 0 <_ z) /\ (((norm` U)` w) e. RR /\ 0 < ((norm` U)` w))) -> 0 <_ (z / ((norm` U)` w)))
56		0re 6603	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 0 e. RR
57		ltle 6690	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((0 e. RR /\ z e. RR) -> (0 < z -> 0 <_ z))
58	56, 57	mpan 759	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z e. RR -> (0 < z -> 0 <_ z))
59	58	imdistani 491	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((z e. RR /\ 0 < z) -> (z e. RR /\ 0 <_ z))
60	5, 35, 6	nvgt0 9635	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((U e. NrmCVec /\ w e. X) -> (w =/= (0v` U) <-> 0 < ((norm` U)` w)))
61	2, 60	mpan 759	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w e. X -> (w =/= (0v` U) <-> 0 < ((norm` U)` w)))
62	61	biimpa 460	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((w e. X /\ w =/= (0v` U)) -> 0 < ((norm` U)` w))
63	34, 62	jca 310	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((w e. X /\ w =/= (0v` U)) -> (((norm` U)` w) e. RR /\ 0 < ((norm` U)` w)))
64	55, 59, 63	syl2an 503	. . . . . . . . . . . . . . . . . . . . . 22 |- (((z e. RR /\ 0 < z) /\ (w e. X /\ w =/= (0v` U))) -> 0 <_ (z / ((norm` U)` w)))
65		simprl 450	. . . . . . . . . . . . . . . . . . . . . 22 |- (((z e. RR /\ 0 < z) /\ (w e. X /\ w =/= (0v` U))) -> w e. X)
66	5, 44, 6	nvsge0 9623	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((U e. NrmCVec /\ ((z / ((norm` U)` w)) e. RR /\ 0 <_ (z / ((norm` U)` w))) /\ w e. X) -> ((norm` U)` ((z / ((norm` U)` w))(.s` U)w)) = ((z / ((norm` U)` w)) x. ((norm` U)` w)))
67	2, 66	mp3an1 1178	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((z / ((norm` U)` w)) e. RR /\ 0 <_ (z / ((norm` U)` w))) /\ w e. X) -> ((norm` U)` ((z / ((norm` U)` w))(.s` U)w)) = ((z / ((norm` U)` w)) x. ((norm` U)` w)))
68	54, 64, 65, 67	syl21anc 1099	. . . . . . . . . . . . . . . . . . . . 21 |- (((z e. RR /\ 0 < z) /\ (w e. X /\ w =/= (0v` U))) -> ((norm` U)` ((z / ((norm` U)` w))(.s` U)w)) = ((z / ((norm` U)` w)) x. ((norm` U)` w)))
69		recn 6466	. . . . . . . . . . . . . . . . . . . . . . 23 |- (z e. RR -> z e. CC)
70	69	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . 22 |- (((z e. RR /\ 0 < z) /\ (w e. X /\ w =/= (0v` U))) -> z e. CC)
71	34	recnd 6468	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((w e. X /\ w =/= (0v` U)) -> ((norm` U)` w) e. CC)
72	71	adantl 424	. . . . . . . . . . . . . . . . . . . . . 22 |- (((z e. RR /\ 0 < z) /\ (w e. X /\ w =/= (0v` U))) -> ((norm` U)` w) e. CC)
73	39	adantl 424	. . . . . . . . . . . . . . . . . . . . . 22 |- (((z e. RR /\ 0 < z) /\ (w e. X /\ w =/= (0v` U))) -> ((norm` U)` w) =/= 0)
74		divcan1 6909	. . . . . . . . . . . . . . . . . . . . . 22 |- ((z e. CC /\ ((norm` U)` w) e. CC /\ ((norm` U)` w) =/= 0) -> ((z / ((norm` U)` w)) x. ((norm` U)` w)) = z)
75	70, 72, 73, 74	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . 21 |- (((z e. RR /\ 0 < z) /\ (w e. X /\ w =/= (0v` U))) -> ((z / ((norm` U)` w)) x. ((norm` U)` w)) = z)
76	68, 75	eqtrd 1925	. . . . . . . . . . . . . . . . . . . 20 |- (((z e. RR /\ 0 < z) /\ (w e. X /\ w =/= (0v` U))) -> ((norm` U)` ((z / ((norm` U)` w))(.s` U)w)) = z)
77	76	adantll 428	. . . . . . . . . . . . . . . . . . 19 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> ((norm` U)` ((z / ((norm` U)` w))(.s` U)w)) = z)
78	53, 77	eqtrd 1925	. . . . . . . . . . . . . . . . . 18 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> ((norm` U)` (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w)))) = z)
79		leid 6701	. . . . . . . . . . . . . . . . . . . 20 |- (z e. RR -> z <_ z)
80	79	adantr 425	. . . . . . . . . . . . . . . . . . 19 |- ((z e. RR /\ 0 < z) -> z <_ z)
81	80	ad2antlr 441	. . . . . . . . . . . . . . . . . 18 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> z <_ z)
82	78, 81	eqbrtrd 3357	. . . . . . . . . . . . . . . . 17 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> ((norm` U)` (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w)))) <_ z)
83		simpll 448	. . . . . . . . . . . . . . . . . . 19 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> P e. X)
84	47	adantlr 429	. . . . . . . . . . . . . . . . . . . 20 |- (((z e. RR /\ 0 < z) /\ (w e. X /\ w =/= (0v` U))) -> ((z / ((norm` U)` w))(.s` U)w) e. X)
85	84	adantll 428	. . . . . . . . . . . . . . . . . . 19 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> ((z / ((norm` U)` w))(.s` U)w) e. X)
86	5, 8	nvmcl 9599	. . . . . . . . . . . . . . . . . . . 20 |- ((U e. NrmCVec /\ P e. X /\ ((z / ((norm` U)` w))(.s` U)w) e. X) -> (P(-v` U)((z / ((norm` U)` w))(.s` U)w)) e. X)
87	2, 86	mp3an1 1178	. . . . . . . . . . . . . . . . . . 19 |- ((P e. X /\ ((z / ((norm` U)` w))(.s` U)w) e. X) -> (P(-v` U)((z / ((norm` U)` w))(.s` U)w)) e. X)
88	83, 85, 87	syl11anc 524	. . . . . . . . . . . . . . . . . 18 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> (P(-v` U)((z / ((norm` U)` w))(.s` U)w)) e. X)
89		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = (P(-v` U)((z / ((norm` U)` w))(.s` U)w)) -> (P(-v` U)y) = (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w))))
90	89	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . 21 |- (y = (P(-v` U)((z / ((norm` U)` w))(.s` U)w)) -> ((norm` U)` (P(-v` U)y)) = ((norm` U)` (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w)))))
91	90	breq1d 3348	. . . . . . . . . . . . . . . . . . . 20 |- (y = (P(-v` U)((z / ((norm` U)` w))(.s` U)w)) -> (((norm` U)` (P(-v` U)y)) <_ z <-> ((norm` U)` (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w)))) <_ z))
92	89	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = (P(-v` U)((z / ((norm` U)` w))(.s` U)w)) -> (T` (P(-v` U)y)) = (T` (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w)))))
93	92	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . 21 |- (y = (P(-v` U)((z / ((norm` U)` w))(.s` U)w)) -> ((norm` W)` (T` (P(-v` U)y))) = ((norm` W)` (T` (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w))))))
94	93	breq1d 3348	. . . . . . . . . . . . . . . . . . . 20 |- (y = (P(-v` U)((z / ((norm` U)` w))(.s` U)w)) -> (((norm` W)` (T` (P(-v` U)y))) <_ 1 <-> ((norm` W)` (T` (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w))))) <_ 1))
95	91, 94	imbi12d 688	. . . . . . . . . . . . . . . . . . 19 |- (y = (P(-v` U)((z / ((norm` U)` w))(.s` U)w)) -> ((((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1) <-> (((norm` U)` (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w)))) <_ z -> ((norm` W)` (T` (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w))))) <_ 1)))
96	95	rcla4v 2376	. . . . . . . . . . . . . . . . . 18 |- ((P(-v` U)((z / ((norm` U)` w))(.s` U)w)) e. X -> (A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1) -> (((norm` U)` (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w)))) <_ z -> ((norm` W)` (T` (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w))))) <_ 1)))
97	88, 96	syl 12	. . . . . . . . . . . . . . . . 17 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> (A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1) -> (((norm` U)` (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w)))) <_ z -> ((norm` W)` (T` (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w))))) <_ 1)))
98	82, 97	mpid 58	. . . . . . . . . . . . . . . 16 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> (A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1) -> ((norm` W)` (T` (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w))))) <_ 1))
99	52	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . 21 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> (T` (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w)))) = (T` ((z / ((norm` U)` w))(.s` U)w)))
100	42	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((z e. RR /\ 0 < z) /\ (w e. X /\ w =/= (0v` U))) -> (z / ((norm` U)` w)) e. CC)
101	100	adantll 428	. . . . . . . . . . . . . . . . . . . . . 22 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> (z / ((norm` U)` w)) e. CC)
102		simprl 450	. . . . . . . . . . . . . . . . . . . . . 22 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> w e. X)
103	2, 1, 14	3pm3.2i 1048	. . . . . . . . . . . . . . . . . . . . . . 23 |- (U e. NrmCVec /\ W e. NrmCVec /\ T e. L)
104		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (.s` W) = (.s` W)
105	5, 44, 104, 13	lnomul 9760	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((U e. NrmCVec /\ W e. NrmCVec /\ T e. L) /\ ((z / ((norm` U)` w)) e. CC /\ w e. X)) -> (T` ((z / ((norm` U)` w))(.s` U)w)) = ((z / ((norm` U)` w))(.s` W)(T` w)))
106	103, 105	mpan 759	. . . . . . . . . . . . . . . . . . . . . 22 |- (((z / ((norm` U)` w)) e. CC /\ w e. X) -> (T` ((z / ((norm` U)` w))(.s` U)w)) = ((z / ((norm` U)` w))(.s` W)(T` w)))
107	101, 102, 106	syl11anc 524	. . . . . . . . . . . . . . . . . . . . 21 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> (T` ((z / ((norm` U)` w))(.s` U)w)) = ((z / ((norm` U)` w))(.s` W)(T` w)))
108	99, 107	eqtrd 1925	. . . . . . . . . . . . . . . . . . . 20 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> (T` (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w)))) = ((z / ((norm` U)` w))(.s` W)(T` w)))
109	108	fveq2d 4685	. . . . . . . . . . . . . . . . . . 19 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> ((norm` W)` (T` (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w))))) = ((norm` W)` ((z / ((norm` U)` w))(.s` W)(T` w))))
110		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (BaseSet` W) = (BaseSet` W)
111	5, 110, 13	lnof 9755	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((U e. NrmCVec /\ W e. NrmCVec /\ T e. L) -> T:X-->(BaseSet` W))
112	2, 1, 14, 111	mp3an 1191	. . . . . . . . . . . . . . . . . . . . . . 23 |- T:X-->(BaseSet` W)
113	112	ffvelrni 4788	. . . . . . . . . . . . . . . . . . . . . 22 |- (w e. X -> (T` w) e. (BaseSet` W))
114	113	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . 21 |- (((z e. RR /\ 0 < z) /\ (w e. X /\ w =/= (0v` U))) -> (T` w) e. (BaseSet` W))
115	110, 104, 7	nvsge0 9623	. . . . . . . . . . . . . . . . . . . . . 22 |- ((W e. NrmCVec /\ ((z / ((norm` U)` w)) e. RR /\ 0 <_ (z / ((norm` U)` w))) /\ (T` w) e. (BaseSet` W)) -> ((norm` W)` ((z / ((norm` U)` w))(.s` W)(T` w))) = ((z / ((norm` U)` w)) x. ((norm` W)` (T` w))))
116	1, 115	mp3an1 1178	. . . . . . . . . . . . . . . . . . . . 21 |- ((((z / ((norm` U)` w)) e. RR /\ 0 <_ (z / ((norm` U)` w))) /\ (T` w) e. (BaseSet` W)) -> ((norm` W)` ((z / ((norm` U)` w))(.s` W)(T` w))) = ((z / ((norm` U)` w)) x. ((norm` W)` (T` w))))
117	54, 64, 114, 116	syl21anc 1099	. . . . . . . . . . . . . . . . . . . 20 |- (((z e. RR /\ 0 < z) /\ (w e. X /\ w =/= (0v` U))) -> ((norm` W)` ((z / ((norm` U)` w))(.s` W)(T` w))) = ((z / ((norm` U)` w)) x. ((norm` W)` (T` w))))
118	117	adantll 428	. . . . . . . . . . . . . . . . . . 19 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> ((norm` W)` ((z / ((norm` U)` w))(.s` W)(T` w))) = ((z / ((norm` U)` w)) x. ((norm` W)` (T` w))))
119	109, 118	eqtrd 1925	. . . . . . . . . . . . . . . . . 18 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> ((norm` W)` (T` (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w))))) = ((z / ((norm` U)` w)) x. ((norm` W)` (T` w))))
120	119	breq1d 3348	. . . . . . . . . . . . . . . . 17 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> (((norm` W)` (T` (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w))))) <_ 1 <-> ((z / ((norm` U)` w)) x. ((norm` W)` (T` w))) <_ 1))
121	110, 7	nvcl 9619	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((W e. NrmCVec /\ (T` w) e. (BaseSet` W)) -> ((norm` W)` (T` w)) e. RR)
122	1, 121	mpan 759	. . . . . . . . . . . . . . . . . . . . . 22 |- ((T` w) e. (BaseSet` W) -> ((norm` W)` (T` w)) e. RR)
123	113, 122	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- (w e. X -> ((norm` W)` (T` w)) e. RR)
124	123	ad2antrl 442	. . . . . . . . . . . . . . . . . . . 20 |- (((z e. RR /\ 0 < z) /\ (w e. X /\ w =/= (0v` U))) -> ((norm` W)` (T` w)) e. RR)
125		divgt0 7037	. . . . . . . . . . . . . . . . . . . . 21 |- (((z e. RR /\ 0 < z) /\ (((norm` U)` w) e. RR /\ 0 < ((norm` U)` w))) -> 0 < (z / ((norm` U)` w)))
126	125, 63	sylan2 500	. . . . . . . . . . . . . . . . . . . 20 |- (((z e. RR /\ 0 < z) /\ (w e. X /\ w =/= (0v` U))) -> 0 < (z / ((norm` U)` w)))
127		lemuldiv2OLD 7060	. . . . . . . . . . . . . . . . . . . . 21 |- ((((z / ((norm` U)` w)) e. RR /\ ((norm` W)` (T` w)) e. RR /\ 1 e. RR) /\ 0 < (z / ((norm` U)` w))) -> (((z / ((norm` U)` w)) x. ((norm` W)` (T` w))) <_ 1 <-> ((norm` W)` (T` w)) <_ (1 / (z / ((norm` U)` w)))))
128	3, 127	mp3anl3 1187	. . . . . . . . . . . . . . . . . . . 20 |- ((((z / ((norm` U)` w)) e. RR /\ ((norm` W)` (T` w)) e. RR) /\ 0 < (z / ((norm` U)` w))) -> (((z / ((norm` U)` w)) x. ((norm` W)` (T` w))) <_ 1 <-> ((norm` W)` (T` w)) <_ (1 / (z / ((norm` U)` w)))))
129	54, 124, 126, 128	syl21anc 1099	. . . . . . . . . . . . . . . . . . 19 |- (((z e. RR /\ 0 < z) /\ (w e. X /\ w =/= (0v` U))) -> (((z / ((norm` U)` w)) x. ((norm` W)` (T` w))) <_ 1 <-> ((norm` W)` (T` w)) <_ (1 / (z / ((norm` U)` w)))))
130		recdiv 6967	. . . . . . . . . . . . . . . . . . . . . 22 |- (((z e. CC /\ z =/= 0) /\ (((norm` U)` w) e. CC /\ ((norm` U)` w) =/= 0)) -> (1 / (z / ((norm` U)` w))) = (((norm` U)` w) / z))
131	69	adantr 425	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((z e. RR /\ 0 < z) -> z e. CC)
132	131, 20	jca 310	. . . . . . . . . . . . . . . . . . . . . 22 |- ((z e. RR /\ 0 < z) -> (z e. CC /\ z =/= 0))
133	71, 39	jca 310	. . . . . . . . . . . . . . . . . . . . . 22 |- ((w e. X /\ w =/= (0v` U)) -> (((norm` U)` w) e. CC /\ ((norm` U)` w) =/= 0))
134	130, 132, 133	syl2an 503	. . . . . . . . . . . . . . . . . . . . 21 |- (((z e. RR /\ 0 < z) /\ (w e. X /\ w =/= (0v` U))) -> (1 / (z / ((norm` U)` w))) = (((norm` U)` w) / z))
135	20	adantr 425	. . . . . . . . . . . . . . . . . . . . . 22 |- (((z e. RR /\ 0 < z) /\ (w e. X /\ w =/= (0v` U))) -> z =/= 0)
136		divrec2 6923	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((norm` U)` w) e. CC /\ z e. CC /\ z =/= 0) -> (((norm` U)` w) / z) = ((1 / z) x. ((norm` U)` w)))
137	72, 70, 135, 136	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . 21 |- (((z e. RR /\ 0 < z) /\ (w e. X /\ w =/= (0v` U))) -> (((norm` U)` w) / z) = ((1 / z) x. ((norm` U)` w)))
138	134, 137	eqtrd 1925	. . . . . . . . . . . . . . . . . . . 20 |- (((z e. RR /\ 0 < z) /\ (w e. X /\ w =/= (0v` U))) -> (1 / (z / ((norm` U)` w))) = ((1 / z) x. ((norm` U)` w)))
139	138	breq2d 3350	. . . . . . . . . . . . . . . . . . 19 |- (((z e. RR /\ 0 < z) /\ (w e. X /\ w =/= (0v` U))) -> (((norm` W)` (T` w)) <_ (1 / (z / ((norm` U)` w))) <-> ((norm` W)` (T` w)) <_ ((1 / z) x. ((norm` U)` w))))
140	129, 139	bitrd 587	. . . . . . . . . . . . . . . . . 18 |- (((z e. RR /\ 0 < z) /\ (w e. X /\ w =/= (0v` U))) -> (((z / ((norm` U)` w)) x. ((norm` W)` (T` w))) <_ 1 <-> ((norm` W)` (T` w)) <_ ((1 / z) x. ((norm` U)` w))))
141	140	adantll 428	. . . . . . . . . . . . . . . . 17 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> (((z / ((norm` U)` w)) x. ((norm` W)` (T` w))) <_ 1 <-> ((norm` W)` (T` w)) <_ ((1 / z) x. ((norm` U)` w))))
142	120, 141	bitrd 587	. . . . . . . . . . . . . . . 16 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> (((norm` W)` (T` (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w))))) <_ 1 <-> ((norm` W)` (T` w)) <_ ((1 / z) x. ((norm` U)` w))))
143	98, 142	sylibd 219	. . . . . . . . . . . . . . 15 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ (w e. X /\ w =/= (0v` U))) -> (A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1) -> ((norm` W)` (T` w)) <_ ((1 / z) x. ((norm` U)` w))))
144	143	exp32 408	. . . . . . . . . . . . . 14 |- ((P e. X /\ (z e. RR /\ 0 < z)) -> (w e. X -> (w =/= (0v` U) -> (A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1) -> ((norm` W)` (T` w)) <_ ((1 / z) x. ((norm` U)` w))))))
145	144	com23 36	. . . . . . . . . . . . 13 |- ((P e. X /\ (z e. RR /\ 0 < z)) -> (w =/= (0v` U) -> (w e. X -> (A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1) -> ((norm` W)` (T` w)) <_ ((1 / z) x. ((norm` U)` w))))))
146	145	com24 41	. . . . . . . . . . . 12 |- ((P e. X /\ (z e. RR /\ 0 < z)) -> (A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1) -> (w e. X -> (w =/= (0v` U) -> ((norm` W)` (T` w)) <_ ((1 / z) x. ((norm` U)` w))))))
147	146	imp41 395	. . . . . . . . . . 11 |- (((((P e. X /\ (z e. RR /\ 0 < z)) /\ A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1)) /\ w e. X) /\ w =/= (0v` U)) -> ((norm` W)` (T` w)) <_ ((1 / z) x. ((norm` U)` w)))
148	22	recnd 6468	. . . . . . . . . . . . . . . . 17 |- ((z e. RR /\ 0 < z) -> (1 / z) e. CC)
149		mul01 6606	. . . . . . . . . . . . . . . . 17 |- ((1 / z) e. CC -> ((1 / z) x. 0) = 0)
150	148, 149	syl 12	. . . . . . . . . . . . . . . 16 |- ((z e. RR /\ 0 < z) -> ((1 / z) x. 0) = 0)
151	35, 6	nvz0 9628	. . . . . . . . . . . . . . . . . 18 |- (U e. NrmCVec -> ((norm` U)` (0v` U)) = 0)
152	2, 151	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- ((norm` U)` (0v` U)) = 0
153	152	opreq2i 4893	. . . . . . . . . . . . . . . 16 |- ((1 / z) x. ((norm` U)` (0v` U))) = ((1 / z) x. 0)
154	150, 153	syl5req 1941	. . . . . . . . . . . . . . 15 |- ((z e. RR /\ 0 < z) -> 0 = ((1 / z) x. ((norm` U)` (0v` U))))
155	56	leidi 6790	. . . . . . . . . . . . . . 15 |- 0 <_ 0
156	154, 155	syl5breq 3372	. . . . . . . . . . . . . 14 |- ((z e. RR /\ 0 < z) -> 0 <_ ((1 / z) x. ((norm` U)` (0v` U))))
157		eqid 1884	. . . . . . . . . . . . . . . . . 18 |- (0v` W) = (0v` W)
158	5, 110, 35, 157, 13	lno0 9756	. . . . . . . . . . . . . . . . 17 |- ((U e. NrmCVec /\ W e. NrmCVec /\ T e. L) -> (T` (0v` U)) = (0v` W))
159	2, 1, 14, 158	mp3an 1191	. . . . . . . . . . . . . . . 16 |- (T` (0v` U)) = (0v` W)
160	159	fveq2i 4684	. . . . . . . . . . . . . . 15 |- ((norm` W)` (T` (0v` U))) = ((norm` W)` (0v` W))
161	157, 7	nvz0 9628	. . . . . . . . . . . . . . . 16 |- (W e. NrmCVec -> ((norm` W)` (0v` W)) = 0)
162	1, 161	ax-mp 7	. . . . . . . . . . . . . . 15 |- ((norm` W)` (0v` W)) = 0
163	160, 162	eqtri 1908	. . . . . . . . . . . . . 14 |- ((norm` W)` (T` (0v` U))) = 0
164	156, 163	syl5eqbr 3370	. . . . . . . . . . . . 13 |- ((z e. RR /\ 0 < z) -> ((norm` W)` (T` (0v` U))) <_ ((1 / z) x. ((norm` U)` (0v` U))))
165	164	adantl 424	. . . . . . . . . . . 12 |- ((P e. X /\ (z e. RR /\ 0 < z)) -> ((norm` W)` (T` (0v` U))) <_ ((1 / z) x. ((norm` U)` (0v` U))))
166	165	ad2antrr 440	. . . . . . . . . . 11 |- ((((P e. X /\ (z e. RR /\ 0 < z)) /\ A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1)) /\ w e. X) -> ((norm` W)` (T` (0v` U))) <_ ((1 / z) x. ((norm` U)` (0v` U))))
167	28, 147, 166	pm2.61ne 2087	. . . . . . . . . 10 |- ((((P e. X /\ (z e. RR /\ 0 < z)) /\ A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1)) /\ w e. X) -> ((norm` W)` (T` w)) <_ ((1 / z) x. ((norm` U)` w)))
168	167	r19.21aiva 2176	. . . . . . . . 9 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1)) -> A.w e. X ((norm` W)` (T` w)) <_ ((1 / z) x. ((norm` U)` w)))
169		opreq1 4889	. . . . . . . . . . . 12 |- (x = (1 / z) -> (x x. ((norm` U)` w)) = ((1 / z) x. ((norm` U)` w)))
170	169	breq2d 3350	. . . . . . . . . . 11 |- (x = (1 / z) -> (((norm` W)` (T` w)) <_ (x x. ((norm` U)` w)) <-> ((norm` W)` (T` w)) <_ ((1 / z) x. ((norm` U)` w))))
171	170	ralbidv 2123	. . . . . . . . . 10 |- (x = (1 / z) -> (A.w e. X ((norm` W)` (T` w)) <_ (x x. ((norm` U)` w)) <-> A.w e. X ((norm` W)` (T` w)) <_ ((1 / z) x. ((norm` U)` w))))
172	171	rcla4ev 2381	. . . . . . . . 9 |- (((1 / z) e. RR /\ A.w e. X ((norm` W)` (T` w)) <_ ((1 / z) x. ((norm` U)` w))) -> E.x e. RR A.w e. X ((norm` W)` (T` w)) <_ (x x. ((norm` U)` w)))
173	23, 168, 172	syl11anc 524	. . . . . . . 8 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1)) -> E.x e. RR A.w e. X ((norm` W)` (T` w)) <_ (x x. ((norm` U)` w)))
174	173	exp42 414	. . . . . . 7 |- (P e. X -> (z e. RR -> (0 < z -> (A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1) -> E.x e. RR A.w e. X ((norm` W)` (T` w)) <_ (x x. ((norm` U)` w))))))
175	174	imp4a 391	. . . . . 6 |- (P e. X -> (z e. RR -> ((0 < z /\ A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1)) -> E.x e. RR A.w e. X ((norm` W)` (T` w)) <_ (x x. ((norm` U)` w)))))
176	175	r19.23adv 2215	. . . . 5 |- (P e. X -> (E.z e. RR (0 < z /\ A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1)) -> E.x e. RR A.w e. X ((norm` W)` (T` w)) <_ (x x. ((norm` U)` w))))
177	176	adantr 425	. . . 4 |- ((P e. X /\ T e. ((J CnP K)` P)) -> (E.z e. RR (0 < z /\ A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1)) -> E.x e. RR A.w e. X ((norm` W)` (T` w)) <_ (x x. ((norm` U)` w))))
178	19, 177	mpd 29	. . 3 |- ((P e. X /\ T e. ((J CnP K)` P)) -> E.x e. RR A.w e. X ((norm` W)` (T` w)) <_ (x x. ((norm` U)` w)))
179	178, 14	jctil 316	. 2 |- ((P e. X /\ T e. ((J CnP K)` P)) -> (T e. L /\ E.x e. RR A.w e. X ((norm` W)` (T` w)) <_ (x x. ((norm` U)` w))))
180		blocni.5	. . 3 |- B = (U BLnOp W)
181	5, 6, 7, 13, 180, 2, 1	isblo3i 9801	. 2 |- (T e. B <-> (T e. L /\ E.x e. RR A.w e. X ((norm` W)` (T` w)) <_ (x x. ((norm` U)` w))))
182	179, 181	sylibr 217	1 |- ((P e. X /\ T e. ((J CnP K)` P)) -> T e. B)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  E.wrex 2106   class class class wbr 3338  -->wf 3994  ` cfv 3998  (class class class)co 4884  CCcc 6384  RRcr 6385  0cc0 6386  1c1 6387   x. cmul 6391   / cdiv 6447   <_ cle 6448   < clt 6653   CnP ccnp 9029  Opencopn 9069  NrmCVeccnv 9535  BaseSetcba 9537  .scns 9538  0vcn0v 9539  -vcnsb 9540  normcnm 9541  IndMetcims 9542   LnOp clno 9740   BLnOp cblo 9742

This theorem is referenced by:  blocni 9805  lnocni 9806

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-map 5383  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-sup 5664  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-div 6892  df-n 7108  df-2 7154  df-n0 7309  df-z 7345  df-seq1 7721  df-exp 7812  df-sqr 7920  df-re 8001  df-im 8002  df-cj 8003  df-abs 8004  df-top 8861  df-cnp 9031  df-met 9070  df-bl 9072  df-opn 9073  df-grp 9316  df-gid 9317  df-ginv 9318  df-gdiv 9319  df-abl 9408  df-vc 9497  df-nv 9543  df-va 9546  df-ba 9547  df-sm 9548  df-0v 9549  df-vs 9550  df-nm 9551  df-ims 9552  df-lno 9744  df-nmo 9745  df-blo 9746  df-0o 9747

Copyright terms: Public domain