Theorem nmlno0lem 8453

Description: Lemma for nmlno0i 8454.

Hypotheses

Ref	Expression
nmlno0.3	|- N = (UnormOpW)
nmlno0.0	|- Z = (U 0op W)
nmlno0.7	|- L = (U LnOp W)
nmlno0lem.u	|- U e. NrmCVec
nmlno0lem.w	|- W e. NrmCVec
nmlno0lem.l	|- T e. L
nmlno0lem.1	|- X = (Base` U)
nmlno0lem.2	|- Y = (Base` W)
nmlno0lem.r	|- R = (.s` U)
nmlno0lem.s	|- S = (.s` W)
nmlno0lem.p	|- P = (0v` U)
nmlno0lem.q	|- Q = (0v` W)
nmlno0lem.k	|- K = (norm` U)
nmlno0lem.m	|- M = (norm` W)

Assertion

Ref	Expression
nmlno0lem	|- ((N` T) = 0 <-> T = Z)

Proof of Theorem nmlno0lem

Step	Hyp	Ref	Expression
1		recne0t 5732	. . . . . . . . . . . . . 14 |- (((K` x) e. CC /\ (K` x) =/= 0) -> (1 / (K` x)) =/= 0)
2		nmlno0lem.u	. . . . . . . . . . . . . . . . 17 |- U e. NrmCVec
3		nmlno0lem.1	. . . . . . . . . . . . . . . . . 18 |- X = (Base` U)
4		nmlno0lem.k	. . . . . . . . . . . . . . . . . 18 |- K = (norm` U)
5	3, 4	nvcl 8287	. . . . . . . . . . . . . . . . 17 |- ((U e. NrmCVec /\ x e. X) -> (K` x) e. RR)
6	2, 5	mpan 695	. . . . . . . . . . . . . . . 16 |- (x e. X -> (K` x) e. RR)
7	6	recnd 5315	. . . . . . . . . . . . . . 15 |- (x e. X -> (K` x) e. CC)
8	7	adantr 389	. . . . . . . . . . . . . 14 |- ((x e. X /\ (T` x) =/= Q) -> (K` x) e. CC)
9		nmlno0lem.p	. . . . . . . . . . . . . . . . . . 19 |- P = (0v` U)
10	3, 9, 4	nvz 8297	. . . . . . . . . . . . . . . . . 18 |- ((U e. NrmCVec /\ x e. X) -> ((K` x) = 0 <-> x = P))
11	2, 10	mpan 695	. . . . . . . . . . . . . . . . 17 |- (x e. X -> ((K` x) = 0 <-> x = P))
12		fveq2 3724	. . . . . . . . . . . . . . . . . 18 |- (x = P -> (T` x) = (T` P))
13		nmlno0lem.w	. . . . . . . . . . . . . . . . . . 19 |- W e. NrmCVec
14		nmlno0lem.l	. . . . . . . . . . . . . . . . . . 19 |- T e. L
15		nmlno0lem.2	. . . . . . . . . . . . . . . . . . . 20 |- Y = (Base` W)
16		nmlno0lem.q	. . . . . . . . . . . . . . . . . . . 20 |- Q = (0v` W)
17		nmlno0.7	. . . . . . . . . . . . . . . . . . . 20 |- L = (U LnOp W)
18	3, 15, 9, 16, 17	lno0 8417	. . . . . . . . . . . . . . . . . . 19 |- ((U e. NrmCVec /\ W e. NrmCVec /\ T e. L) -> (T` P) = Q)
19	2, 13, 14, 18	mp3an 916	. . . . . . . . . . . . . . . . . 18 |- (T` P) = Q
20	12, 19	syl6eq 1523	. . . . . . . . . . . . . . . . 17 |- (x = P -> (T` x) = Q)
21	11, 20	syl6bi 214	. . . . . . . . . . . . . . . 16 |- (x e. X -> ((K` x) = 0 -> (T` x) = Q))
22	21	necon3d 1604	. . . . . . . . . . . . . . 15 |- (x e. X -> ((T` x) =/= Q -> (K` x) =/= 0))
23	22	imp 350	. . . . . . . . . . . . . 14 |- ((x e. X /\ (T` x) =/= Q) -> (K` x) =/= 0)
24	1, 8, 23	sylanc 471	. . . . . . . . . . . . 13 |- ((x e. X /\ (T` x) =/= Q) -> (1 / (K` x)) =/= 0)
25		pm3.27 323	. . . . . . . . . . . . 13 |- ((x e. X /\ (T` x) =/= Q) -> (T` x) =/= Q)
26	24, 25	jca 288	. . . . . . . . . . . 12 |- ((x e. X /\ (T` x) =/= Q) -> ((1 / (K` x)) =/= 0 /\ (T` x) =/= Q))
27		nmlno0lem.s	. . . . . . . . . . . . . . . . 17 |- S = (.s` W)
28	15, 27, 16	nvmul0or 8272	. . . . . . . . . . . . . . . 16 |- ((W e. NrmCVec /\ (1 / (K` x)) e. CC /\ (T` x) e. Y) -> (((1 / (K` x))S(T` x)) = Q <-> ((1 / (K` x)) = 0 \/ (T` x) = Q)))
29	13, 28	mp3an1 903	. . . . . . . . . . . . . . 15 |- (((1 / (K` x)) e. CC /\ (T` x) e. Y) -> (((1 / (K` x))S(T` x)) = Q <-> ((1 / (K` x)) = 0 \/ (T` x) = Q)))
30		recclt 5715	. . . . . . . . . . . . . . . 16 |- (((K` x) e. CC /\ (K` x) =/= 0) -> (1 / (K` x)) e. CC)
31	30, 8, 23	sylanc 471	. . . . . . . . . . . . . . 15 |- ((x e. X /\ (T` x) =/= Q) -> (1 / (K` x)) e. CC)
32	3, 15, 17	lnof 8416	. . . . . . . . . . . . . . . . . 18 |- ((U e. NrmCVec /\ W e. NrmCVec /\ T e. L) -> T:X-->Y)
33	2, 13, 14, 32	mp3an 916	. . . . . . . . . . . . . . . . 17 |- T:X-->Y
34	33	ffvelrni 3815	. . . . . . . . . . . . . . . 16 |- (x e. X -> (T` x) e. Y)
35	34	adantr 389	. . . . . . . . . . . . . . 15 |- ((x e. X /\ (T` x) =/= Q) -> (T` x) e. Y)
36	29, 31, 35	sylanc 471	. . . . . . . . . . . . . 14 |- ((x e. X /\ (T` x) =/= Q) -> (((1 / (K` x))S(T` x)) = Q <-> ((1 / (K` x)) = 0 \/ (T` x) = Q)))
37	36	necon3abid 1599	. . . . . . . . . . . . 13 |- ((x e. X /\ (T` x) =/= Q) -> (((1 / (K` x))S(T` x)) =/= Q <-> -. ((1 / (K` x)) = 0 \/ (T` x) = Q)))
38		neanior 1639	. . . . . . . . . . . . 13 |- (((1 / (K` x)) =/= 0 /\ (T` x) =/= Q) <-> -. ((1 / (K` x)) = 0 \/ (T` x) = Q))
39	37, 38	syl6bbr 538	. . . . . . . . . . . 12 |- ((x e. X /\ (T` x) =/= Q) -> (((1 / (K` x))S(T` x)) =/= Q <-> ((1 / (K` x)) =/= 0 /\ (T` x) =/= Q)))
40	26, 39	mpbird 196	. . . . . . . . . . 11 |- ((x e. X /\ (T` x) =/= Q) -> ((1 / (K` x))S(T` x)) =/= Q)
41	15, 27	nvscl 8247	. . . . . . . . . . . . . 14 |- ((W e. NrmCVec /\ (1 / (K` x)) e. CC /\ (T` x) e. Y) -> ((1 / (K` x))S(T` x)) e. Y)
42	13, 41	mp3an1 903	. . . . . . . . . . . . 13 |- (((1 / (K` x)) e. CC /\ (T` x) e. Y) -> ((1 / (K` x))S(T` x)) e. Y)
43	42, 31, 35	sylanc 471	. . . . . . . . . . . 12 |- ((x e. X /\ (T` x) =/= Q) -> ((1 / (K` x))S(T` x)) e. Y)
44		nmlno0lem.m	. . . . . . . . . . . . . 14 |- M = (norm` W)
45	15, 16, 44	nvgt0 8303	. . . . . . . . . . . . 13 |- ((W e. NrmCVec /\ ((1 / (K` x))S(T` x)) e. Y) -> (((1 / (K` x))S(T` x)) =/= Q <-> 0 < (M` ((1 / (K` x))S(T` x)))))
46	13, 45	mpan 695	. . . . . . . . . . . 12 |- (((1 / (K` x))S(T` x)) e. Y -> (((1 / (K` x))S(T` x)) =/= Q <-> 0 < (M` ((1 / (K` x))S(T` x)))))
47	43, 46	syl 10	. . . . . . . . . . 11 |- ((x e. X /\ (T` x) =/= Q) -> (((1 / (K` x))S(T` x)) =/= Q <-> 0 < (M` ((1 / (K` x))S(T` x)))))
48	40, 47	mpbid 195	. . . . . . . . . 10 |- ((x e. X /\ (T` x) =/= Q) -> 0 < (M` ((1 / (K` x))S(T` x))))
49	48	ex 373	. . . . . . . . 9 |- (x e. X -> ((T` x) =/= Q -> 0 < (M` ((1 / (K` x))S(T` x)))))
50	49	adantl 388	. . . . . . . 8 |- (((N` T) = 0 /\ x e. X) -> ((T` x) =/= Q -> 0 < (M` ((1 / (K` x))S(T` x)))))
51		fveq2 3724	. . . . . . . . . . . . . . . . . 18 |- (z = ((1 / (K` x))Rx) -> (K` z) = (K` ((1 / (K` x))Rx)))
52	51	breq1d 2629	. . . . . . . . . . . . . . . . 17 |- (z = ((1 / (K` x))Rx) -> ((K` z) <_ 1 <-> (K` ((1 / (K` x))Rx)) <_ 1))
53		fveq2 3724	. . . . . . . . . . . . . . . . . . 19 |- (z = ((1 / (K` x))Rx) -> (T` z) = (T` ((1 / (K` x))Rx)))
54	53	fveq2d 3728	. . . . . . . . . . . . . . . . . 18 |- (z = ((1 / (K` x))Rx) -> (M` (T` z)) = (M` (T` ((1 / (K` x))Rx))))
55	54	eqeq2d 1486	. . . . . . . . . . . . . . . . 17 |- (z = ((1 / (K` x))Rx) -> ((M` ((1 / (K` x))S(T` x))) = (M` (T` z)) <-> (M` ((1 / (K` x))S(T` x))) = (M` (T` ((1 / (K` x))Rx)))))
56	52, 55	anbi12d 628	. . . . . . . . . . . . . . . 16 |- (z = ((1 / (K` x))Rx) -> (((K` z) <_ 1 /\ (M` ((1 / (K` x))S(T` x))) = (M` (T` z))) <-> ((K` ((1 / (K` x))Rx)) <_ 1 /\ (M` ((1 / (K` x))S(T` x))) = (M` (T` ((1 / (K` x))Rx))))))
57	56	rcla4ev 1877	. . . . . . . . . . . . . . 15 |- ((((1 / (K` x))Rx) e. X /\ ((K` ((1 / (K` x))Rx)) <_ 1 /\ (M` ((1 / (K` x))S(T` x))) = (M` (T` ((1 / (K` x))Rx))