Theorem nmcopexlem6 9951

Description: Lemma for nmcopex 9952. Combine lemmas to obtain the result (with hypotheses to be eliminated).

Hypotheses

Ref	Expression
nmcopex.1	|- T e. LinOp
nmcopex.2	|- T e. ConOp
nmcopexlem4.3	|- A = {k e. NN | (1 / k) < y}
nmcopexlem4.4	|- M = sup(A, RR, `' < )

Assertion

Ref	Expression
nmcopexlem6	|- (normop` T) e. RR

Distinct variable groups:   k,M   y,k,T

Proof of Theorem nmcopexlem6

Step	Hyp	Ref	Expression
1		nmcopex.1	. . 3 |- T e. LinOp
2		nmcopex.2	. . 3 |- T e. ConOp
3	1, 2	nmcopexlem2 9947	. 2 |- E.y e. RR (0 < y /\ A.z e. H~ ((normh` z) < y -> (normh` (T` z)) < 1))
4		nmcopexlem4.3	. . . . . . . 8 |- A = {k e. NN | (1 / k) < y}
5		nmcopexlem4.4	. . . . . . . 8 |- M = sup(A, RR, `' < )
6	1, 2, 4, 5	nmcopexlem4 9949	. . . . . . 7 |- ((y e. RR /\ 0 < y) -> (M e. NN /\ (1 / M) < y))
7	6	pm3.26d 321	. . . . . 6 |- ((y e. RR /\ 0 < y) -> M e. NN)
8	7	ex 373	. . . . 5 |- (y e. RR -> (0 < y -> M e. NN))
9	8	adantrd 393	. . . 4 |- (y e. RR -> ((0 < y /\ A.z e. H~ ((normh` z) < y -> (normh` (T` z)) < 1)) -> M e. NN))
10	1, 2, 4, 5	nmcopexlem5 9950	. . . . . . . . . . . . . . . . . 18 |- (((y e. RR /\ 0 < y) /\ (k e. NN /\ M <_ k) /\ (x e. H~ /\ (normh` x) <_ 1)) -> (normh` ((1 / k) .h x)) < y)
11	10	3expb 836	. . . . . . . . . . . . . . . . 17 |- (((y e. RR /\ 0 < y) /\ ((k e. NN /\ M <_ k) /\ (x e. H~ /\ (normh` x) <_ 1))) -> (normh` ((1 / k) .h x)) < y)
12		hvmulclt 8878	. . . . . . . . . . . . . . . . . . . . . 22 |- (((1 / k) e. CC /\ x e. H~) -> ((1 / k) .h x) e. H~)
13		rerecclt 5805	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((k e. RR /\ k =/= 0) -> (1 / k) e. RR)
14		nnret 5931	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (k e. NN -> k e. RR)
15		nnne0t 5951	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (k e. NN -> k =/= 0)
16	13, 14, 15	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . 23 |- (k e. NN -> (1 / k) e. RR)
17	16	recnd 5327	. . . . . . . . . . . . . . . . . . . . . 22 |- (k e. NN -> (1 / k) e. CC)
18	12, 17	sylan 450	. . . . . . . . . . . . . . . . . . . . 21 |- ((k e. NN /\ x e. H~) -> ((1 / k) .h x) e. H~)
19		fveq2 3730	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z = ((1 / k) .h x) -> (normh` z) = (normh` ((1 / k) .h x)))
20	19	breq1d 2634	. . . . . . . . . . . . . . . . . . . . . . 23 |- (z = ((1 / k) .h x) -> ((normh` z) < y <-> (normh` ((1 / k) .h x)) < y))
21		fveq2 3730	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z = ((1 / k) .h x) -> (T` z) = (T` ((1 / k) .h x)))
22	21	fveq2d 3734	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z = ((1 / k) .h x) -> (normh` (T` z)) = (normh` (T` ((1 / k) .h x))))
23	22	breq1d 2634	. . . . . . . . . . . . . . . . . . . . . . 23 |- (z = ((1 / k) .h x) -> ((normh` (T` z)) < 1 <-> (normh` (T` ((1 / k) .h x))) < 1))
24	20, 23	imbi12d 628	. . . . . . . . . . . . . . . . . . . . . 22 |- (z = ((1 / k) .h x) -> (((normh` z) < y -> (normh` (T` z)) < 1) <-> ((normh` ((1 / k) .h x)) < y -> (normh` (T` ((1 / k) .h x))) < 1)))
25	24	rcla4v 1876	. . . . . . . . . . . . . . . . . . . . 21 |- (((1 / k) .h x) e. H~ -> (A.z e. H~ ((normh` z) < y -> (normh` (T` z)) < 1) -> ((normh` ((1 / k) .h x)) < y -> (normh` (T` ((1 / k) .h x))) < 1)))
26	18, 25	syl 10	. . . . . . . . . . . . . . . . . . . 20 |- ((k e. NN /\ x e. H~) -> (A.z e. H~ ((normh` z) < y -> (normh` (T` z)) < 1) -> ((normh` ((1 / k) .h x)) < y -> (normh` (T` ((1 / k) .h x))) < 1)))
27	1, 2	nmcopexlem3 9948	. . . . . . . . . . . . . . . . . . . . 21 |- ((k e. NN /\ x e. H~) -> ((normh` (T` x)) < k <-> (normh` (T` ((1 / k) .h x))) < 1))
28		ltnsymt 5544	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((normh` (T` x)) e. RR /\ k e. RR) -> ((normh` (T` x)) < k -> -. k < (normh` (T` x))))
29	1	lnopf 9888	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- T:H~-->H~
30	29	ffvelrni 3821	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x e. H~ -> (T` x) e. H~)
31		normclt 8986	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((T` x) e. H~ -> (normh` (T` x)) e. RR)
32	30, 31	syl 10	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x e. H~ -> (normh` (T` x)) e. RR)
33	28, 32, 14	syl2an 456	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x e. H~ /\ k e. NN) -> ((normh` (T` x)) < k -> -. k < (normh` (T` x))))
34	33	ancoms 438	. . . . . . . . . . . . . . . . . . . . 21 |- ((k e. NN /\ x e. H~) -> ((normh` (T` x)) < k -> -. k < (normh` (T` x))))
35	27, 34	sylbird 205	. . . . . . . . . . . . . . . . . . . 20 |- ((k e. NN /\ x e. H~) -> ((normh` (T` ((1 / k) .h x))) < 1 -> -. k < (normh` (T` x))))
36	26, 35	syl6d 56	. . . . . . . . . . . . . . . . . . 19 |- ((k e. NN /\ x e. H~) -> (A.z e. H~ ((normh` z) < y -> (normh` (T` z)) < 1) -> ((normh` ((1 / k) .h x)) < y -> -. k < (normh` (T` x)))))
37	36	ad2ant2r 411	. . . . . . . . . . . . . . . . . 18 |- (((k e. NN /\ M <_ k) /\ (x e. H~ /\ (normh` x) <_ 1)) -> (A.z e. H~ ((normh` z) < y -> (normh` (T` z)) < 1) -> ((normh` ((1 / k) .h x)) < y -> -. k < (normh` (T` x)))))
38	37	adantl 390	. . . . . . . . . . . . . . . . 17 |- (((y e. RR /\ 0 < y) /\ ((k e. NN /\ M <_ k) /\ (x e. H~ /\ (normh` x) <_ 1))) -> (A.z e. H~ ((normh` z) < y -> (normh` (T` z)) < 1) -> ((normh` ((1 / k) .h x)) < y -> -. k < (normh` (T` x)))))
39	11, 38	mpid 47	. . . . . . . . . . . . . . . 16 |- (((y e. RR /\ 0 < y) /\ ((k e. NN /\ M <_ k) /\ (x e. H~ /\ (normh` x) <_ 1))) -> (A.z e. H~ ((normh` z) < y -> (normh` (T` z)) < 1) -> -. k < (normh` (T` x))))
40	39	ex 373	. . . . . . . . . . . . . . 15 |- ((y e. RR /\ 0 < y) -> (((k e. NN /\ M <_ k) /\ (x e. H~ /\ (normh` x) <_ 1)) -> (A.z e. H~ ((normh` z) < y -> (normh` (T` z)) < 1) -> -. k < (normh` (T` x)))))
41	40	com23 32	. . . . . . . . . . . . . 14 |- ((y e. RR /\ 0 < y) -> (A.z e. H~ ((normh` z) < y -> (normh` (T` z)) < 1) -> (((k e. NN /\ M <_ k) /\ (x e. H~ /\ (normh` x) <_ 1)) -> -. k < (normh` (T` x)))))
42	41	imp 350	. . . . . . . . . . . . 13 |- (((y e. RR /\ 0 < y) /\ A.z e. H~ ((normh` z) < y -> (normh` (T` z)) < 1)) -> (((k e. NN /\ M <_ k) /\ (x e. H~ /\ (normh` x) <_ 1)) -> -. k < (normh` (T` x))))
43	42	exp4d 383	. . . . . . . . . . . 12 |- (((y e. RR /\ 0 < y) /\ A.z e. H~ ((normh` z) < y -> (normh` (T` z)) < 1)) -> ((k e. NN /\ M <_ k) -> (x e. H~ -> ((normh` x) <_ 1 -> -. k < (normh` (T` x))))))
44	43	anasss 442	. . . . . . . . . . 11 |- ((y e. RR /\ (0 < y /\ A.z e. H~ ((normh` z) < y -> (normh` (T` z)) < 1))) -> ((k e. NN /\ M <_ k) -> (x e. H~ -> ((normh` x) <_ 1 -> -. k < (normh` (T` x))))))
45	44	imp 350	. . . . . . . . . 10 |- (((y e. RR /\ (0 < y /\ A.z e. H~ ((normh` z) < y -> (normh` (T` z)) < 1))) /\ (k e. NN /\ M <_ k)) -> (x e. H~ -> ((normh` x) <_ 1 -> -. k < (normh` (T` x)))))
46	45	r19.21aiv 1716	. . . . . . . . 9 |- (((y e. RR /\ (0 < y /\ A.z e. H~ ((normh` z) < y -> (normh` (T` z)) < 1))) /\ (k e. NN /\ M <_ k)) -> A.x e. H~ ((normh` x) <_ 1 -> -. k < (