Theorem nmlnop0ALT 9920

Description: A linear operator with a zero norm is identically zero.

Hypothesis

Ref	Expression
nmlnop0.1	|- T e. LinOp

Assertion

Ref	Expression
nmlnop0ALT	|- ((normop` T) = 0 <-> T = 0hop)

Proof of Theorem nmlnop0ALT

Step	Hyp	Ref	Expression
1		recne0t 5732	. . . . . . . . . . . . . 14 |- (((normh` x) e. CC /\ (normh` x) =/= 0) -> (1 / (normh` x)) =/= 0)
2		normclt 8991	. . . . . . . . . . . . . . . 16 |- (x e. H~ -> (normh` x) e. RR)
3	2	recnd 5315	. . . . . . . . . . . . . . 15 |- (x e. H~ -> (normh` x) e. CC)
4	3	adantr 389	. . . . . . . . . . . . . 14 |- ((x e. H~ /\ (T` x) =/= 0h) -> (normh` x) e. CC)
5		norm-it 8996	. . . . . . . . . . . . . . . . 17 |- (x e. H~ -> ((normh` x) = 0 <-> x = 0h))
6		fveq2 3724	. . . . . . . . . . . . . . . . . 18 |- (x = 0h -> (T` x) = (T` 0h))
7		nmlnop0.1	. . . . . . . . . . . . . . . . . . 19 |- T e. LinOp
8	7	lnop0 9894	. . . . . . . . . . . . . . . . . 18 |- (T` 0h) = 0h
9	6, 8	syl6eq 1523	. . . . . . . . . . . . . . . . 17 |- (x = 0h -> (T` x) = 0h)
10	5, 9	syl6bi 214	. . . . . . . . . . . . . . . 16 |- (x e. H~ -> ((normh` x) = 0 -> (T` x) = 0h))
11	10	necon3d 1604	. . . . . . . . . . . . . . 15 |- (x e. H~ -> ((T` x) =/= 0h -> (normh` x) =/= 0))
12	11	imp 350	. . . . . . . . . . . . . 14 |- ((x e. H~ /\ (T` x) =/= 0h) -> (normh` x) =/= 0)
13	1, 4, 12	sylanc 471	. . . . . . . . . . . . 13 |- ((x e. H~ /\ (T` x) =/= 0h) -> (1 / (normh` x)) =/= 0)
14		pm3.27 323	. . . . . . . . . . . . 13 |- ((x e. H~ /\ (T` x) =/= 0h) -> (T` x) =/= 0h)
15	13, 14	jca 288	. . . . . . . . . . . 12 |- ((x e. H~ /\ (T` x) =/= 0h) -> ((1 / (normh` x)) =/= 0 /\ (T` x) =/= 0h))
16		hvmul0ort 8894	. . . . . . . . . . . . . . 15 |- (((1 / (normh` x)) e. CC /\ (T` x) e. H~) -> (((1 / (normh` x)) .h (T` x)) = 0h <-> ((1 / (normh` x)) = 0 \/ (T` x) = 0h)))
17		recclt 5715	. . . . . . . . . . . . . . . 16 |- (((normh` x) e. CC /\ (normh` x) =/= 0) -> (1 / (normh` x)) e. CC)
18	17, 4, 12	sylanc 471	. . . . . . . . . . . . . . 15 |- ((x e. H~ /\ (T` x) =/= 0h) -> (1 / (normh` x)) e. CC)
19	7	lnopf 9893	. . . . . . . . . . . . . . . . 17 |- T:H~-->H~
20	19	ffvelrni 3815	. . . . . . . . . . . . . . . 16 |- (x e. H~ -> (T` x) e. H~)
21	20	adantr 389	. . . . . . . . . . . . . . 15 |- ((x e. H~ /\ (T` x) =/= 0h) -> (T` x) e. H~)
22	16, 18, 21	sylanc 471	. . . . . . . . . . . . . 14 |- ((x e. H~ /\ (T` x) =/= 0h) -> (((1 / (normh` x)) .h (T` x)) = 0h <-> ((1 / (normh` x)) = 0 \/ (T` x) = 0h)))
23	22	necon3abid 1599	. . . . . . . . . . . . 13 |- ((x e. H~ /\ (T` x) =/= 0h) -> (((1 / (normh` x)) .h (T` x)) =/= 0h <-> -. ((1 / (normh` x)) = 0 \/ (T` x) = 0h)))
24		neanior 1639	. . . . . . . . . . . . 13 |- (((1 / (normh` x)) =/= 0 /\ (T` x) =/= 0h) <-> -. ((1 / (normh` x)) = 0 \/ (T` x) = 0h))
25	23, 24	syl6bbr 538	. . . . . . . . . . . 12 |- ((x e. H~ /\ (T` x) =/= 0h) -> (((1 / (normh` x)) .h (T` x)) =/= 0h <-> ((1 / (normh` x)) =/= 0 /\ (T` x) =/= 0h)))
26	15, 25	mpbird 196	. . . . . . . . . . 11 |- ((x e. H~ /\ (T` x) =/= 0h) -> ((1 / (normh` x)) .h (T` x)) =/= 0h)
27		hvmulclt 8883	. . . . . . . . . . . . 13 |- (((1 / (normh` x)) e. CC /\ (T` x) e. H~) -> ((1 / (normh` x)) .h (T` x)) e. H~)
28	27, 18, 21	sylanc 471	. . . . . . . . . . . 12 |- ((x e. H~ /\ (T` x) =/= 0h) -> ((1 / (normh` x)) .h (T` x)) e. H~)
29		normgt0t 8994	. . . . . . . . . . . 12 |- (((1 / (normh` x)) .h (T` x)) e. H~ -> (((1 / (normh` x)) .h (T` x)) =/= 0h <-> 0 < (normh` ((1 / (normh` x)) .h (T` x)))))
30	28, 29	syl 10	. . . . . . . . . . 11 |- ((x e. H~ /\ (T` x) =/= 0h) -> (((1 / (normh` x)) .h (T` x)) =/= 0h <-> 0 < (normh` ((1 / (normh` x)) .h (T` x)))))
31	26, 30	mpbid 195	. . . . . . . . . 10 |- ((x e. H~ /\ (T` x) =/= 0h) -> 0 < (normh` ((1 / (normh` x)) .h (T` x))))
32	31	ex 373	. . . . . . . . 9 |- (x e. H~ -> ((T` x) =/= 0h -> 0 < (normh` ((1 / (normh` x)) .h (T` x)))))
33	32	adantl 388	. . . . . . . 8 |- (((normop` T) = 0 /\ x e. H~) -> ((T` x) =/= 0h -> 0 < (normh` ((1 / (normh` x)) .h (T` x)))))
34		fveq2 3724	. . . . . . . . . . . . . . . . . 18 |- (z = ((1 / (normh` x)) .h x) -> (normh` z) = (normh` ((1 / (normh` x)) .h x)))
35	34	breq1d 2629	. . . . . . . . . . . . . . . . 17 |- (z = ((1 / (normh` x)) .h x) -> ((normh` z) <_ 1 <-> (normh` ((1 / (normh` x)) .h x)) <_ 1))
36		fveq2 3724	. . . . . . . . . . . . . . . . . . 19 |- (z = ((1 / (normh` x)) .h x) -> (T` z) = (T` ((1 / (normh` x)) .h x)))
37	36	fveq2d 3728	. . . . . . . . . . . . . . . . . 18 |- (z = ((1 / (normh` x)) .h x) -> (normh` (T` z)) = (normh` (T` ((1 / (normh` x)) .h x))))
38	37	eqeq2d 1486	. . . . . . . . . . . . . . . . 17 |- (z = ((1 / (normh` x)) .h x) -> ((normh` ((1 / (normh` x)) .h (T` x))) = (normh` (T` z)) <-> (normh` ((1 / (normh` x)) .h (T` x))) = (normh` (T` ((1 / (normh` x)) .h x)))))
39	35, 38	anbi12d 628	. . . . . . . . . . . . . . . 16 |- (z = ((1 / (normh` x)) .h x) -> (((normh` z) <_ 1 /\ (normh` ((1 / (normh` x)) .h (T` x))) = (normh` (T` z))) <-> ((normh` ((1 / (normh` x)) .h x)) <_ 1 /\ (normh` ((1 / (normh` x)) .h (T` x))) = (normh` (T` ((1 / (normh` x)) .h x))))))
40	39	rcla4ev 1877	. . . . . . . . . . . . . . 15 |- ((((1 / (normh` x)) .h x) e. H~ /\ ((normh` ((1 / (normh` x)) .h x)) <_ 1 /\ (normh` ((1 / (normh` x)) .h (T` x))) = (normh` (T` ((1 / (normh` x)) .h x))))) -> E.z e. H~ ((normh` z) <_ 1 /\ (normh` ((1 / (normh` x)) .h (T` x))) = (normh` (T` z))))
41		hvmulclt 8883	. . . . . . . . . . . . . . . 16 |- (((1 / (normh` x)) e. CC /\ x e. H~) -> ((1 / (normh` x)) .h x) e. H~)
42		pm3.26 319	. . . . . . . . . . . . . . . 16 |- ((x e. H~ /\ (T` x) =/= 0h) -> x e. H~)
43	41, 18, 42	sylanc 471	. . . . . . . . . . . . . . 15 |- ((x e. H~ /\ (T` x) =/= 0h) -> ((1 / (normh` x)) .h x) e. H~)
44		eqlet 5571	. . . . . . . . . . . . . . . . 17 |- (((normh` ((1 / (normh` x)) .h x)) e. RR /\ (normh` ((1 / (normh` x)) .h x)) = 1) -> (normh` ((1 / (normh` x)) .h x)) <_ 1)
45		norm1t 9121	. . . . . . . . . . . . . . . . . . 19 |- ((x e. H~ /\ x =/= 0h) -> (normh` ((1 / (normh` x)) .h x)) = 1)
46	9	necon3i 1605	. . . . . . . . . . . . . . . . . . 19 |- ((T` x) =/= 0h -> x =/= 0h)
47	45, 46	sylan2 451	. . . . . . . . . . . . . . . . . 18 |- ((x e. H~ /\ (T` x) =/= 0h) -> (normh` ((1 / (normh` x)) .h x)) = 1)
48		1re 5435	. . . . . . . . . . . . . . . . . 18 |- 1 e. RR
49	47, 48	syl6eqel 1556	. . . . . . . . . . . . . . . . 17 |- ((x e. H~ /\ (T` x) =/= 0h) -> (normh` ((1 / (normh` x)) .h x)) e. RR)
50	44, 49, 47	sylanc 471	. . . . . . . . . . . . . . . 16 |- ((x e. H~ /\ (T` x) =/= 0h) -> (normh` ((1 / (normh` x)) .h x)) <_ 1)
51	7	lnopmul 9896	. . . . . . . . . . . . . . . . . . 19 |- (((1 / (normh` x)) e. CC /\ x e. H~) -> (T` ((1 / (normh` x)) .h x)) = ((1 / (normh` x)) .h (T` x)))
52	51, 18, 42	sylanc 471	. . . . . . . . . . . . . . . . . 18 |- ((x e. H~ /\ (T` x) =/= 0h) -> (T` (