nmlno0lem - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem nmlno0lem 8449

Description: Lemma for nmlno0i 8450.

**Hypotheses**
Ref	Expression
nmlno0.3	⊢ N = (U normOp W)
nmlno0.0	⊢ Z = (U 0_op W)
nmlno0.7	⊢ L = (U LnOp W)
nmlno0lem.u	⊢ U ∈ NrmCVec
nmlno0lem.w	⊢ W ∈ NrmCVec
nmlno0lem.l	⊢ T ∈ L
nmlno0lem.1	⊢ X = (Base ‘U)
nmlno0lem.2	⊢ Y = (Base ‘W)
nmlno0lem.r	⊢ R = ( ·_s ‘U)
nmlno0lem.s	⊢ S = ( ·_s ‘W)
nmlno0lem.p	⊢ P = (0_v ‘U)
nmlno0lem.q	⊢ Q = (0_v ‘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 5739	. . . . . . . . . . . . . 14 ⊢ (((K ‘x) ∈ ℂ ⋀ (K ‘x) ≠ 0) → (1 / (K ‘x)) ≠ 0)
2		nmlno0lem.u	. . . . . . . . . . . . . . . . 17 ⊢ U ∈ NrmCVec
3		nmlno0lem.1	. . . . . . . . . . . . . . . . . 18 ⊢ X = (Base ‘U)
4		nmlno0lem.k	. . . . . . . . . . . . . . . . . 18 ⊢ K = (norm ‘U)
5	3, 4	nvcl 8283	. . . . . . . . . . . . . . . . 17 ⊢ ((U ∈ NrmCVec ⋀ x ∈ X) → (K ‘x) ∈ ℝ)
6	2, 5	mpan 697	. . . . . . . . . . . . . . . 16 ⊢ (x ∈ X → (K ‘x) ∈ ℝ)
7	6	recnd 5327	. . . . . . . . . . . . . . 15 ⊢ (x ∈ X → (K ‘x) ∈ ℂ)
8	7	adantr 391	. . . . . . . . . . . . . 14 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → (K ‘x) ∈ ℂ)
9		nmlno0lem.p	. . . . . . . . . . . . . . . . . . 19 ⊢ P = (0_v ‘U)
10	3, 9, 4	nvz 8293	. . . . . . . . . . . . . . . . . 18 ⊢ ((U ∈ NrmCVec ⋀ x ∈ X) → ((K ‘x) = 0 ↔ x = P))
11	2, 10	mpan 697	. . . . . . . . . . . . . . . . 17 ⊢ (x ∈ X → ((K ‘x) = 0 ↔ x = P))
12		fveq2 3730	. . . . . . . . . . . . . . . . . 18 ⊢ (x = P → (T ‘x) = (T ‘P))
13		nmlno0lem.w	. . . . . . . . . . . . . . . . . . 19 ⊢ W ∈ NrmCVec
14		nmlno0lem.l	. . . . . . . . . . . . . . . . . . 19 ⊢ T ∈ L
15		nmlno0lem.2	. . . . . . . . . . . . . . . . . . . 20 ⊢ Y = (Base ‘W)
16		nmlno0lem.q	. . . . . . . . . . . . . . . . . . . 20 ⊢ Q = (0_v ‘W)
17		nmlno0.7	. . . . . . . . . . . . . . . . . . . 20 ⊢ L = (U LnOp W)
18	3, 15, 9, 16, 17	lno0 8413	. . . . . . . . . . . . . . . . . . 19 ⊢ ((U ∈ NrmCVec ⋀ W ∈ NrmCVec ⋀ T ∈ L) → (T ‘P) = Q)
19	2, 13, 14, 18	mp3an 918	. . . . . . . . . . . . . . . . . 18 ⊢ (T ‘P) = Q
20	12, 19	syl6eq 1526	. . . . . . . . . . . . . . . . 17 ⊢ (x = P → (T ‘x) = Q)
21	11, 20	syl6bi 214	. . . . . . . . . . . . . . . 16 ⊢ (x ∈ X → ((K ‘x) = 0 → (T ‘x) = Q))
22	21	necon3d 1607	. . . . . . . . . . . . . . 15 ⊢ (x ∈ X → ((T ‘x) ≠ Q → (K ‘x) ≠ 0))
23	22	imp 350	. . . . . . . . . . . . . 14 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → (K ‘x) ≠ 0)
24	1, 8, 23	sylanc 473	. . . . . . . . . . . . 13 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → (1 / (K ‘x)) ≠ 0)
25		pm3.27 323	. . . . . . . . . . . . 13 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → (T ‘x) ≠ Q)
26	24, 25	jca 288	. . . . . . . . . . . 12 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → ((1 / (K ‘x)) ≠ 0 ⋀ (T ‘x) ≠ Q))
27		nmlno0lem.s	. . . . . . . . . . . . . . . . 17 ⊢ S = ( ·_s ‘W)
28	15, 27, 16	nvmul0or 8268	. . . . . . . . . . . . . . . 16 ⊢ ((W ∈ NrmCVec ⋀ (1 / (K ‘x)) ∈ ℂ ⋀ (T ‘x) ∈ Y) → (((1 / (K ‘x))S(T ‘x)) = Q ↔ ((1 / (K ‘x)) = 0 ⋁ (T ‘x) = Q)))
29	13, 28	mp3an1 905	. . . . . . . . . . . . . . 15 ⊢ (((1 / (K ‘x)) ∈ ℂ ⋀ (T ‘x) ∈ Y) → (((1 / (K ‘x))S(T ‘x)) = Q ↔ ((1 / (K ‘x)) = 0 ⋁ (T ‘x) = Q)))
30		recclt 5727	. . . . . . . . . . . . . . . 16 ⊢ (((K ‘x) ∈ ℂ ⋀ (K ‘x) ≠ 0) → (1 / (K ‘x)) ∈ ℂ)
31	30, 8, 23	sylanc 473	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → (1 / (K ‘x)) ∈ ℂ)
32	3, 15, 17	lnof 8412	. . . . . . . . . . . . . . . . . 18 ⊢ ((U ∈ NrmCVec ⋀ W ∈ NrmCVec ⋀ T ∈ L) → T:X–→Y)
33	2, 13, 14, 32	mp3an 918	. . . . . . . . . . . . . . . . 17 ⊢ T:X–→Y
34	33	ffvelrni 3821	. . . . . . . . . . . . . . . 16 ⊢ (x ∈ X → (T ‘x) ∈ Y)
35	34	adantr 391	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → (T ‘x) ∈ Y)
36	29, 31, 35	sylanc 473	. . . . . . . . . . . . . 14 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → (((1 / (K ‘x))S(T ‘x)) = Q ↔ ((1 / (K ‘x)) = 0 ⋁ (T ‘x) = Q)))
37	36	necon3abid 1602	. . . . . . . . . . . . 13 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → (((1 / (K ‘x))S(T ‘x)) ≠ Q ↔ ¬ ((1 / (K ‘x)) = 0 ⋁ (T ‘x) = Q)))
38		neanior 1642	. . . . . . . . . . . . 13 ⊢ (((1 / (K ‘x)) ≠ 0 ⋀ (T ‘x) ≠ Q) ↔ ¬ ((1 / (K ‘x)) = 0 ⋁ (T ‘x) = Q))
39	37, 38	syl6bbr 540	. . . . . . . . . . . 12 ⊢ ((x ∈ 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 ∈ X ⋀ (T ‘x) ≠ Q) → ((1 / (K ‘x))S(T ‘x)) ≠ Q)
41	15, 27	nvscl 8243	. . . . . . . . . . . . . 14 ⊢ ((W ∈ NrmCVec ⋀ (1 / (K ‘x)) ∈ ℂ ⋀ (T ‘x) ∈ Y) → ((1 / (K ‘x))S(T ‘x)) ∈ Y)
42	13, 41	mp3an1 905	. . . . . . . . . . . . 13 ⊢ (((1 / (K ‘x)) ∈ ℂ ⋀ (T ‘x) ∈ Y) → ((1 / (K ‘x))S(T ‘x)) ∈ Y)
43	42, 31, 35	sylanc 473	. . . . . . . . . . . 12 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → ((1 / (K ‘x))S(T ‘x)) ∈ Y)
44		nmlno0lem.m	. . . . . . . . . . . . . 14 ⊢ M = (norm ‘W)
45	15, 16, 44	nvgt0 8299	. . . . . . . . . . . . 13 ⊢ ((W ∈ NrmCVec ⋀ ((1 / (K ‘x))S(T ‘x)) ∈ Y) → (((1 / (K ‘x))S(T ‘x)) ≠ Q ↔ 0 < (M ‘((1 / (K ‘x))S(T ‘x)))))
46	13, 45	mpan 697	. . . . . . . . . . . 12 ⊢ (((1 / (K ‘x))S(T ‘x)) ∈ Y → (((1 / (K ‘x))S(T ‘x)) ≠ Q ↔ 0 < (M ‘((1 / (K ‘x))S(T ‘x)))))
47	43, 46	syl 10	. . . . . . . . . . 11 ⊢ ((x ∈ 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 ∈ X ⋀ (T ‘x) ≠ Q) → 0 < (M ‘((1 / (K ‘x))S(T ‘x))))
49	48	ex 373	. . . . . . . . 9 ⊢ (x ∈ X → ((T ‘x) ≠ Q → 0 < (M ‘((1 / (K ‘x))S(T ‘x)))))
50	49	adantl 390	. . . . . . . 8 ⊢ (((N ‘T) = 0 ⋀ x ∈ X) → ((T ‘x) ≠ Q → 0 < (M ‘((1 / (K ‘x))S(T ‘x)))))
51		fveq2 3730	. . . . . . . . . . . . . . . . . 18 ⊢ (z = ((1 / (K ‘x))Rx) → (K ‘z) = (K ‘((1 / (K ‘x))Rx)))
52	51	breq1d 2634	. . . . . . . . . . . . . . . . 17 ⊢ (z = ((1 / (K ‘x))Rx) → ((K ‘z) ≤ 1 ↔ (K ‘((1 / (K ‘x))Rx)) ≤ 1))
53		fveq2 3730	. . . . . . . . . . . . . . . . . . 19 ⊢ (z = ((1 / (K ‘x))Rx) → (T ‘z) = (T ‘((1 / (K ‘x))Rx)))
54	53	fveq2d 3734	. . . . . . . . . . . . . . . . . 18 ⊢ (z = ((1 / (K ‘x))Rx) → (M ‘(T ‘z)) = (M ‘(T ‘((1 / (K ‘x))Rx))))
55	54	eqeq2d 1489	. . . . . . . . . . . . . . . . 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 630	. . . . . . . . . . . . . . . 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 1880	. . . . . . . . . . . . . . 15 ⊢ ((((1 / (K ‘x))Rx) ∈ X ⋀ ((K ‘((1 / (K ‘x))Rx)) ≤ 1 ⋀ (M ‘((1 / (K ‘x))S(T ‘x))) = (M ‘(T ‘((1 / (K ‘x))Rx))))) → ∃z ∈ X ((K ‘z) ≤ 1 ⋀ (M ‘((1 / (K ‘x))S(T ‘x))) = (M ‘(T ‘z))))
58		nmlno0lem.r	. . . . . . . . . . . . . . . . . 18 ⊢ R = ( ·_s ‘U)
59	3, 58	nvscl 8243	. . . . . . . . . . . . . . . . 17 ⊢ ((U ∈ NrmCVec ⋀ (1 / (K ‘x)) ∈ ℂ ⋀ x ∈ X) → ((1 / (K ‘x))Rx) ∈ X)
60	2, 59	mp3an1 905	. . . . . . . . . . . . . . . 16 ⊢ (((1 / (K ‘x)) ∈ ℂ ⋀ x ∈ X) → ((1 / (K ‘x))Rx) ∈ X)
61		pm3.26 319	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → x ∈ X)
62	60, 31, 61	sylanc 473	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → ((1 / (K ‘x))Rx) ∈ X)
63		eqlet 5583	. . . . . . . . . . . . . . . . 17 ⊢ (((K ‘((1 / (K ‘x))Rx)) ∈ ℝ ⋀ (K ‘((1 / (K ‘x))Rx)) = 1) → (K ‘((1 / (K ‘x))Rx)) ≤ 1)
64	3, 58, 9, 4	nv1 8300	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((U ∈ NrmCVec ⋀ x ∈ X ⋀ x ≠ P) → (K ‘((1 / (K ‘x))Rx)) = 1)
65	2, 64	mp3an1 905	. . . . . . . . . . . . . . . . . . 19 ⊢ ((x ∈ X ⋀ x ≠ P) → (K ‘((1 / (K ‘x))Rx)) = 1)
66	20	necon3i 1608	. . . . . . . . . . . . . . . . . . 19 ⊢ ((T ‘x) ≠ Q → x ≠ P)
67	65, 66	sylan2 453	. . . . . . . . . . . . . . . . . 18 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → (K ‘((1 / (K ‘x))Rx)) = 1)
68		1re 5447	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ
69	67, 68	syl6eqel 1559	. . . . . . . . . . . . . . . . 17 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → (K ‘((1 / (K ‘x))Rx)) ∈ ℝ)
70	63, 69, 67	sylanc 473	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → (K ‘((1 / (K ‘x))Rx)) ≤ 1)
71	2, 13, 14	3pm3.2i 820	. . . . . . . . . . . . . . . . . . . 20 ⊢ (U ∈ NrmCVec ⋀ W ∈ NrmCVec ⋀ T ∈ L)
72	3, 58, 27, 17	lnomul 8417	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((U ∈ NrmCVec ⋀ W ∈ NrmCVec ⋀ T ∈ L) ⋀ ((1 / (K ‘x)) ∈ ℂ ⋀ x ∈ X)) → (T ‘((1 / (K ‘x))Rx)) = ((1 / (K ‘x))S(T ‘x)))
73	71, 72	mpan 697	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1 / (K ‘x)) ∈ ℂ ⋀ x ∈ X) → (T ‘((1 / (K ‘x))Rx)) = ((1 / (K ‘x))S(T ‘x)))
74	73, 31, 61	sylanc 473	. . . . . . . . . . . . . . . . . 18 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → (T ‘((1 / (K ‘x))Rx)) = ((1 / (K ‘x))S(T ‘x)))
75	74	eqcomd 1483	. . . . . . . . . . . . . . . . 17 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → ((1 / (K ‘x))S(T ‘x)) = (T ‘((1 / (K ‘x))Rx)))
76	75	fveq2d 3734	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → (M ‘((1 / (K ‘x))S(T ‘x))) = (M ‘(T ‘((1 / (K ‘x))Rx))))
77	70, 76	jca 288	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → ((K ‘((1 / (K ‘x))Rx)) ≤ 1 ⋀ (M ‘((1 / (K ‘x))S(T ‘x))) = (M ‘(T ‘((1 / (K ‘x))Rx)))))
78	57, 62, 77	sylanc 473	. . . . . . . . . . . . . 14 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → ∃z ∈ X ((K ‘z) ≤ 1 ⋀ (M ‘((1 / (K ‘x))S(T ‘x))) = (M ‘(T ‘z))))
79		fvex 3738	. . . . . . . . . . . . . . 15 ⊢ (M ‘((1 / (K ‘x))S(T ‘x))) ∈ V
80		eqeq1 1484	. . . . . . . . . . . . . . . . 17 ⊢ (y = (M ‘((1 / (K ‘x))S(T ‘x))) → (y = (M ‘(T ‘z)) ↔ (M ‘((1 / (K ‘x))S(T ‘x))) = (M ‘(T ‘z))))
81	80	anbi2d 618	. . . . . . . . . . . . . . . 16 ⊢ (y = (M ‘((1 / (K ‘x))S(T ‘x))) → (((K ‘z) ≤ 1 ⋀ y = (M ‘(T ‘z))) ↔ ((K ‘z) ≤ 1 ⋀ (M ‘((1 / (K ‘x))S(T ‘x))) = (M ‘(T ‘z)))))
82	81	rexbidv 1667	. . . . . . . . . . . . . . 15 ⊢ (y = (M ‘((1 / (K ‘x))S(T ‘x))) → (∃z ∈ X ((K ‘z) ≤ 1 ⋀ y = (M ‘(T ‘z))) ↔ ∃z ∈ X ((K ‘z) ≤ 1 ⋀ (M ‘((1 / (K ‘x))S(T ‘x))) = (M ‘(T ‘z)))))
83	79, 82	elab 1900	. . . . . . . . . . . . . 14 ⊢ ((M ‘((1 / (K ‘x))S(T ‘x))) ∈ {y∣∃z ∈ X ((K ‘z) ≤ 1 ⋀ y = (M ‘(T ‘z)))} ↔ ∃z ∈ X ((K ‘z) ≤ 1 ⋀ (M ‘((1 / (K ‘x))S(T ‘x))) = (M ‘(T ‘z))))
84	78, 83	sylibr 200	. . . . . . . . . . . . 13 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → (M ‘((1 / (K ‘x))S(T ‘x))) ∈ {y∣∃z ∈ X ((K ‘z) ≤ 1 ⋀ y = (M ‘(T ‘z)))})
85	15, 44	nmosetre 8423	. . . . . . . . . . . . . . . 16 ⊢ ((W ∈ NrmCVec ⋀ T:X–→Y) → {y∣∃z ∈ X ((K ‘z) ≤ 1 ⋀ y = (M ‘(T ‘z)))} ⊆ ℝ)
86	13, 33, 85	mp2an 699	. . . . . . . . . . . . . . 15 ⊢ {y∣∃z ∈ X ((K ‘z) ≤ 1 ⋀ y = (M ‘(T ‘z)))} ⊆ ℝ
87		ressxr 5510	. . . . . . . . . . . . . . 15 ⊢ ℝ ⊆ ℝ^*
88	86, 87	sstri 2076	. . . . . . . . . . . . . 14 ⊢ {y∣∃z ∈ X ((K ‘z) ≤ 1 ⋀ y = (M ‘(T ‘z)))} ⊆ ℝ^*
89		supxrub 6100	. . . . . . . . . . . . . 14 ⊢ (({y∣∃z ∈ X ((K ‘z) ≤ 1 ⋀ y = (M ‘(T ‘z)))} ⊆ ℝ^* ⋀ (M ‘((1 / (K ‘x))S(T ‘x))) ∈ {y∣∃z ∈ X ((K ‘z) ≤ 1 ⋀ y = (M ‘(T ‘z)))}) → (M ‘((1 / (K ‘x))S(T ‘x))) ≤ sup({y∣∃z ∈ X ((K ‘z) ≤ 1 ⋀ y = (M ‘(T ‘z)))}, ℝ^*, < ))
90	88, 89	mpan 697	. . . . . . . . . . . . 13 ⊢ ((M ‘((1 / (K ‘x))S(T ‘x))) ∈ {y∣∃z ∈ X ((K ‘z) ≤ 1 ⋀ y = (M ‘(T ‘z)))} → (M ‘((1 / (K ‘x))S(T ‘x))) ≤ sup({y∣∃z ∈ X ((K ‘z) ≤ 1 ⋀ y = (M ‘(T ‘z)))}, ℝ^*, < ))
91	84, 90	syl 10	. . . . . . . . . . . 12 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → (M ‘((1 / (K ‘x))S(T ‘x))) ≤ sup({y∣∃z ∈ X ((K ‘z) ≤ 1 ⋀ y = (M ‘(T ‘z)))}, ℝ^*, < ))
92	91	adantll 394	. . . . . . . . . . 11 ⊢ ((((N ‘T) = 0 ⋀ x ∈ X) ⋀ (T ‘x) ≠ Q) → (M ‘((1 / (K ‘x))S(T ‘x))) ≤ sup({y∣∃z ∈ X ((K ‘z) ≤ 1 ⋀ y = (M ‘(T ‘z)))}, ℝ^*, < ))
93		nmlno0.3	. . . . . . . . . . . . . . . 16 ⊢ N = (U normOp W)
94	3, 15, 4, 44, 93	nmoval 8422	. . . . . . . . . . . . . . 15 ⊢ ((U ∈ NrmCVec ⋀ W ∈ NrmCVec ⋀ T:X–→Y) → (N ‘T) = sup({y∣∃z ∈ X ((K ‘z) ≤ 1 ⋀ y = (M ‘(T ‘z)))}, ℝ^*, < ))
95	2, 13, 33, 94	mp3an 918	. . . . . . . . . . . . . 14 ⊢ (N ‘T) = sup({y∣∃z ∈ X ((K ‘z) ≤ 1 ⋀ y = (M ‘(T ‘z)))}, ℝ^*, < )
96	95	eqeq1i 1485	. . . . . . . . . . . . 13 ⊢ ((N ‘T) = 0 ↔ sup({y∣∃z ∈ X ((K ‘z) ≤ 1 ⋀ y = (M ‘(T ‘z)))}, ℝ^*, < ) = 0)
97	96	biimp 151	. . . . . . . . . . . 12 ⊢ ((N ‘T) = 0 → sup({y∣∃z ∈ X ((K ‘z) ≤ 1 ⋀ y = (M ‘(T ‘z)))}, ℝ^*, < ) = 0)
98	97	ad2antrr 406	. . . . . . . . . . 11 ⊢ ((((N ‘T) = 0 ⋀ x ∈ X) ⋀ (T ‘x) ≠ Q) → sup({y∣∃z ∈ X ((K ‘z) ≤ 1 ⋀ y = (M ‘(T ‘z)))}, ℝ^*, < ) = 0)
99	92, 98	breqtrd 2644	. . . . . . . . . 10 ⊢ ((((N ‘T) = 0 ⋀ x ∈ X) ⋀ (T ‘x) ≠ Q) → (M ‘((1 / (K ‘x))S(T ‘x))) ≤ 0)
100	15, 44	nvcl 8283	. . . . . . . . . . . . . 14 ⊢ ((W ∈ NrmCVec ⋀ ((1 / (K ‘x))S(T ‘x)) ∈ Y) → (M ‘((1 / (K ‘x))S(T ‘x))) ∈ ℝ)
101	13, 100	mpan 697	. . . . . . . . . . . . 13 ⊢ (((1 / (K ‘x))S(T ‘x)) ∈ Y → (M ‘((1 / (K ‘x))S(T ‘x))) ∈ ℝ)
102	43, 101	syl 10	. . . . . . . . . . . 12 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → (M ‘((1 / (K ‘x))S(T ‘x))) ∈ ℝ)
103		0re 5452	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
104		lenltt 5522	. . . . . . . . . . . . 13 ⊢ (((M ‘((1 / (K ‘x))S(T ‘x))) ∈ ℝ ⋀ 0 ∈ ℝ) → ((M ‘((1 / (K ‘x))S(T ‘x))) ≤ 0 ↔ ¬ 0 < (M ‘((1 / (K ‘x))S(T ‘x)))))
105	103, 104	mpan2 698	. . . . . . . . . . . 12 ⊢ ((M ‘((1 / (K ‘x))S(T ‘x))) ∈ ℝ → ((M ‘((1 / (K ‘x))S(T ‘x))) ≤ 0 ↔ ¬ 0 < (M ‘((1 / (K ‘x))S(T ‘x)))))
106	102, 105	syl 10	. . . . . . . . . . 11 ⊢ ((x ∈ X ⋀ (T ‘x) ≠ Q) → ((M ‘((1 / (K ‘x))S(T ‘x))) ≤ 0 ↔ ¬ 0 < (M ‘((1 / (K ‘x))S(T ‘x)))))
107	106	adantll 394	. . . . . . . . . 10 ⊢ ((((N ‘T) = 0 ⋀ x ∈ X) ⋀ (T ‘x) ≠ Q) → ((M ‘((1 / (K ‘x))S(T ‘x))) ≤ 0 ↔ ¬ 0 < (M ‘((1 / (K ‘x))S(T ‘x)))))
108	99, 107	mpbid 195	. . . . . . . . 9 ⊢ ((((N ‘T) = 0 ⋀ x ∈ X) ⋀ (T ‘x) ≠ Q) → ¬ 0 < (M ‘((1 / (K ‘x))S(T ‘x))))
109	108	ex 373	. . . . . . . 8 ⊢ (((N ‘T) = 0 ⋀ x ∈ X) → ((T ‘x) ≠ Q → ¬ 0 < (M ‘((1 / (K ‘x))S(T ‘x)))))
110	50, 109	pm2.65d 136	. . . . . . 7 ⊢ (((N ‘T) = 0 ⋀ x ∈ X) → ¬ (T ‘x) ≠ Q)
111		nne 1592	. . . . . . 7 ⊢ (¬ (T ‘x) ≠ Q ↔ (T ‘x) = Q)
112	110, 111	sylib 198	. . . . . 6 ⊢ (((N ‘T) = 0 ⋀ x ∈ X) → (T ‘x) = Q)
113		nmlno0.0	. . . . . . . . 9 ⊢ Z = (U 0_op W)
114	3, 16, 113	0oval 8444	. . . . . . . 8 ⊢ ((U ∈ NrmCVec ⋀ W ∈ NrmCVec ⋀ x ∈ X) → (Z ‘x) = Q)
115	2, 13, 114	mp3an12 908	. . . . . . 7 ⊢ (x ∈ X → (Z ‘x) = Q)
116	115	adantl 390	. . . . . 6 ⊢ (((N ‘T) = 0 ⋀ x ∈ X) → (Z ‘x) = Q)
117	112, 116	eqtr4d 1513	. . . . 5 ⊢ (((N ‘T) = 0 ⋀ x ∈ X) → (T ‘x) = (Z ‘x))
118	117	r19.21aiva 1717	. . . 4 ⊢ ((N ‘T) = 0 → ∀x ∈ X (T ‘x) = (Z ‘x))
119		eqid 1478	. . . 4 ⊢ X = X
120	118, 119	jctil 292	. . 3 ⊢ ((N ‘T) = 0 → (X = X ⋀ ∀x ∈ X (T ‘x) = (Z ‘x)))
121		ffn 3633	. . . . 5 ⊢ (T:X–→Y → T Fn X)
122	33, 121	ax-mp 7	. . . 4 ⊢ T Fn X
123	3, 15, 113	0oo 8445	. . . . . 6 ⊢ ((U ∈ NrmCVec ⋀ W ∈ NrmCVec) → Z:X–→Y)
124	2, 13, 123	mp2an 699	. . . . 5 ⊢ Z:X–→Y
125		ffn 3633	. . . . 5 ⊢ (Z:X–→Y → Z Fn X)
126	124, 125	ax-mp 7	. . . 4 ⊢ Z Fn X
127		eqfnfv 3803	. . . 4 ⊢ ((T Fn X ⋀ Z Fn X) → (T = Z ↔ (X = X ⋀ ∀x ∈ X (T ‘x) = (Z ‘x))))
128	122, 126, 127	mp2an 699	. . 3 ⊢ (T = Z ↔ (X = X ⋀ ∀x ∈ X (T ‘x) = (Z ‘x)))
129	120, 128	sylibr 200	. 2 ⊢ ((N ‘T) = 0 → T = Z)
130		fveq2 3730	. . 3 ⊢ (T = Z → (N ‘T) = (N ‘Z))
131	93, 113	nmo0 8447	. . . 4 ⊢ ((U ∈ NrmCVec ⋀ W ∈ NrmCVec) → (N ‘Z) = 0)
132	2, 13, 131	mp2an 699	. . 3 ⊢ (N ‘Z) = 0
133	130, 132	syl6eq 1526	. 2 ⊢ (T = Z → (N ‘T) = 0)
134	129, 133	impbi 157	1 ⊢ ((N ‘T) = 0 ↔ T = Z)

Colors of variables: wff set class

Syntax hints: ¬ wn 2 → wi 3 ↔ wb 146 ⋁ wo 222 ⋀ wa 223 ⋀ w3a 777 = wceq 958 ∈ wcel 960 {cab 1466 ≠ wne 1588 ∀wral 1648 ∃wrex 1649 ⊆ wss 2050 class class class wbr 2624 Fn wfn 3183 –→wf 3184 ‘cfv 3188 (class class class)co 3969 supcsup 4582 ℂcc 5244 ℝcr 5245 0cc0 5246 1c1 5247 / cdiv 5306 ≤ cle 5307 ℝ^*cxr 5497 < clt 5498 NrmCVeccnv 8199 Basecba 8201 ·_s cns 8202 0_vcn0v 8203 normcnm 8205 LnOp clno 8397 normOp cnmo 8398 0_op c0o 8400

This theorem is referenced by: nmlno0i 8450

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 964 ax-gen 965 ax-8 966 ax-9 967 ax-10 968 ax-11 969 ax-12 970 ax-13 971 ax-14 972 ax-17 973 ax-4 975 ax-5o 977 ax-6o 980 ax-9o 1125 ax-10o 1142 ax-16 1212 ax-11o 1220 ax-ext 1462 ax-rep 2698 ax-sep 2708 ax-nul 2715 ax-pow 2748 ax-pr 2785 ax-un 2872 ax-inf2 4634

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 778 df-3an 779 df-ex 983 df-sb 1174 df-eu 1384 df-mo 1385 df-clab 1467 df-cleq 1472 df-clel 1475 df-ne 1590 df-nel 1591 df-ral 1652 df-rex 1653 df-reu 1654 df-rab 1655 df-v 1815 df-sbc 1945 df-csb 2005 df-dif 2052 df-un 2053 df-in 2054 df-ss 2056 df-pss 2058 df-nul 2284 df-if 2366 df-pw 2406 df-sn 2416 df-pr 2417 df-tp 2419 df-op 2420 df-uni 2508 df-int 2538 df-iun 2572 df-br 2625 df-opab 2672 df-tr 2686 df-eprel 2838 df-id 2841 df-po 2846 df-so 2856 df-fr 2923 df-we