Theorem nmlnop0iALT

Description: A linear operator with a zero norm is identically zero. (Contributed by NM, 8-Feb-2006) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	nmlnop0.1	⊢ 𝑇 ∈ LinOp
Assertion	nmlnop0iALT	⊢ ( ( normop ‘ 𝑇 ) = 0 ↔ 𝑇 = 0hop )

Proof

Step	Hyp	Ref	Expression
1		nmlnop0.1	⊢ 𝑇 ∈ LinOp
2		normcl	⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ 𝑥 ) ∈ ℝ )
3	2	recnd	⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ 𝑥 ) ∈ ℂ )
4	3	adantr	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( normℎ ‘ 𝑥 ) ∈ ℂ )
5		norm-i	⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ 𝑥 ) = 0 ↔ 𝑥 = 0ℎ ) )
6		fveq2	⊢ ( 𝑥 = 0ℎ → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 0ℎ ) )
7	1	lnop0i	⊢ ( 𝑇 ‘ 0ℎ ) = 0ℎ
8	6 7	eqtrdi	⊢ ( 𝑥 = 0ℎ → ( 𝑇 ‘ 𝑥 ) = 0ℎ )
9	5 8	syl6bi	⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ 𝑥 ) = 0 → ( 𝑇 ‘ 𝑥 ) = 0ℎ ) )
10	9	necon3d	⊢ ( 𝑥 ∈ ℋ → ( ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ → ( normℎ ‘ 𝑥 ) ≠ 0 ) )
11	10	imp	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( normℎ ‘ 𝑥 ) ≠ 0 )
12	4 11	recne0d	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( 1 / ( normℎ ‘ 𝑥 ) ) ≠ 0 )
13		simpr	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ )
14	4 11	reccld	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( 1 / ( normℎ ‘ 𝑥 ) ) ∈ ℂ )
15	1	lnopfi	⊢ 𝑇 : ℋ ⟶ ℋ
16	15	ffvelcdmi	⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
17	16	adantr	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
18		hvmul0or	⊢ ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ) → ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) = 0ℎ ↔ ( ( 1 / ( normℎ ‘ 𝑥 ) ) = 0 ∨ ( 𝑇 ‘ 𝑥 ) = 0ℎ ) ) )
19	14 17 18	syl2anc	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) = 0ℎ ↔ ( ( 1 / ( normℎ ‘ 𝑥 ) ) = 0 ∨ ( 𝑇 ‘ 𝑥 ) = 0ℎ ) ) )
20	19	necon3abid	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ≠ 0ℎ ↔ ¬ ( ( 1 / ( normℎ ‘ 𝑥 ) ) = 0 ∨ ( 𝑇 ‘ 𝑥 ) = 0ℎ ) ) )
21		neanior	⊢ ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ≠ 0 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) ↔ ¬ ( ( 1 / ( normℎ ‘ 𝑥 ) ) = 0 ∨ ( 𝑇 ‘ 𝑥 ) = 0ℎ ) )
22	20 21	bitr4di	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ≠ 0ℎ ↔ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ≠ 0 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) ) )
23	12 13 22	mpbir2and	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ≠ 0ℎ )
24		hvmulcl	⊢ ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ) → ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ )
25	14 17 24	syl2anc	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ )
26		normgt0	⊢ ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ → ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ≠ 0ℎ ↔ 0 < ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) )
27	25 26	syl	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ≠ 0ℎ ↔ 0 < ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) )
28	23 27	mpbid	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → 0 < ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) )
29	28	ex	⊢ ( 𝑥 ∈ ℋ → ( ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ → 0 < ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) )
30	29	adantl	⊢ ( ( ( normop ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ → 0 < ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) )
31		nmopsetretHIL	⊢ ( 𝑇 : ℋ ⟶ ℋ → { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ⊆ ℝ )
32	15 31	ax-mp	⊢ { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ⊆ ℝ
33		ressxr	⊢ ℝ ⊆ ℝ*
34	32 33	sstri	⊢ { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ⊆ ℝ*
35		simpl	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → 𝑥 ∈ ℋ )
36		hvmulcl	⊢ ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ∈ ℋ )
37	14 35 36	syl2anc	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ∈ ℋ )
38	8	necon3i	⊢ ( ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ → 𝑥 ≠ 0ℎ )
39		norm1	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑥 ≠ 0ℎ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) = 1 )
40	38 39	sylan2	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) = 1 )
41		1re	⊢ 1 ∈ ℝ
42	40 41	eqeltrdi	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) ∈ ℝ )
43		eqle	⊢ ( ( ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) ∈ ℝ ∧ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) = 1 ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) ≤ 1 )
44	42 40 43	syl2anc	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) ≤ 1 )
45	1	lnopmuli	⊢ ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) = ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) )
46	14 35 45	syl2anc	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) = ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) )
47	46	eqcomd	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) = ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) )
48	47	fveq2d	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( normℎ ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) ) )
49		fveq2	⊢ ( 𝑧 = ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) → ( normℎ ‘ 𝑧 ) = ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) )
50	49	breq1d	⊢ ( 𝑧 = ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) → ( ( normℎ ‘ 𝑧 ) ≤ 1 ↔ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) ≤ 1 ) )
51		fveq2	⊢ ( 𝑧 = ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) → ( 𝑇 ‘ 𝑧 ) = ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) )
52	51	fveq2d	⊢ ( 𝑧 = ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) → ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) = ( normℎ ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) ) )
53	52	eqeq2d	⊢ ( 𝑧 = ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) → ( ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ↔ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( normℎ ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) ) ) )
54	50 53	anbi12d	⊢ ( 𝑧 = ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) → ( ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) ↔ ( ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) ≤ 1 ∧ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( normℎ ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) ) ) ) )
55	54	rspcev	⊢ ( ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ∈ ℋ ∧ ( ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) ≤ 1 ∧ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( normℎ ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) ) ) ) → ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) )
56	37 44 48 55	syl12anc	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) )
57		fvex	⊢ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ∈ V
58		eqeq1	⊢ ( 𝑦 = ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) → ( 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ↔ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) )
59	58	anbi2d	⊢ ( 𝑦 = ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) → ( ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) ↔ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) ) )
60	59	rexbidv	⊢ ( 𝑦 = ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) → ( ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) ↔ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) ) )
61	57 60	elab	⊢ ( ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ∈ { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ↔ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) )
62	56 61	sylibr	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ∈ { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) } )
63		supxrub	⊢ ( ( { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ⊆ ℝ* ∧ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ∈ { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ≤ sup ( { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
64	34 62 63	sylancr	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ≤ sup ( { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
65	64	adantll	⊢ ( ( ( ( normop ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ≤ sup ( { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
66		nmopval	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( normop ‘ 𝑇 ) = sup ( { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
67	15 66	ax-mp	⊢ ( normop ‘ 𝑇 ) = sup ( { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < )
68	67	eqeq1i	⊢ ( ( normop ‘ 𝑇 ) = 0 ↔ sup ( { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) = 0 )
69	68	biimpi	⊢ ( ( normop ‘ 𝑇 ) = 0 → sup ( { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) = 0 )
70	69	ad2antrr	⊢ ( ( ( ( normop ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → sup ( { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) = 0 )
71	65 70	breqtrd	⊢ ( ( ( ( normop ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ≤ 0 )
72		normcl	⊢ ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ∈ ℝ )
73	25 72	syl	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ∈ ℝ )
74		0re	⊢ 0 ∈ ℝ
75		lenlt	⊢ ( ( ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ≤ 0 ↔ ¬ 0 < ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) )
76	73 74 75	sylancl	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ≤ 0 ↔ ¬ 0 < ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) )
77	76	adantll	⊢ ( ( ( ( normop ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ( ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ≤ 0 ↔ ¬ 0 < ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) )
78	71 77	mpbid	⊢ ( ( ( ( normop ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ) → ¬ 0 < ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) )
79	78	ex	⊢ ( ( ( normop ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ → ¬ 0 < ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) )
80	30 79	pm2.65d	⊢ ( ( ( normop ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) → ¬ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ )
81		nne	⊢ ( ¬ ( 𝑇 ‘ 𝑥 ) ≠ 0ℎ ↔ ( 𝑇 ‘ 𝑥 ) = 0ℎ )
82	80 81	sylib	⊢ ( ( ( normop ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ 𝑥 ) = 0ℎ )
83		ho0val	⊢ ( 𝑥 ∈ ℋ → ( 0hop ‘ 𝑥 ) = 0ℎ )
84	83	adantl	⊢ ( ( ( normop ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) → ( 0hop ‘ 𝑥 ) = 0ℎ )
85	82 84	eqtr4d	⊢ ( ( ( normop ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ 𝑥 ) = ( 0hop ‘ 𝑥 ) )
86	85	ralrimiva	⊢ ( ( normop ‘ 𝑇 ) = 0 → ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 0hop ‘ 𝑥 ) )
87		ffn	⊢ ( 𝑇 : ℋ ⟶ ℋ → 𝑇 Fn ℋ )
88	15 87	ax-mp	⊢ 𝑇 Fn ℋ
89		ho0f	⊢ 0hop : ℋ ⟶ ℋ
90		ffn	⊢ ( 0hop : ℋ ⟶ ℋ → 0hop Fn ℋ )
91	89 90	ax-mp	⊢ 0hop Fn ℋ
92		eqfnfv	⊢ ( ( 𝑇 Fn ℋ ∧ 0hop Fn ℋ ) → ( 𝑇 = 0hop ↔ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 0hop ‘ 𝑥 ) ) )
93	88 91 92	mp2an	⊢ ( 𝑇 = 0hop ↔ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 0hop ‘ 𝑥 ) )
94	86 93	sylibr	⊢ ( ( normop ‘ 𝑇 ) = 0 → 𝑇 = 0hop )
95		fveq2	⊢ ( 𝑇 = 0hop → ( normop ‘ 𝑇 ) = ( normop ‘ 0hop ) )
96		nmop0	⊢ ( normop ‘ 0hop ) = 0
97	95 96	eqtrdi	⊢ ( 𝑇 = 0hop → ( normop ‘ 𝑇 ) = 0 )
98	94 97	impbii	⊢ ( ( normop ‘ 𝑇 ) = 0 ↔ 𝑇 = 0hop )