Theorem nmopun 31989

Description: Norm of a unitary Hilbert space operator. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.)

Assertion

Ref	Expression
nmopun	⊢ (( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → (normop‘𝑇) = 1)

Proof of Theorem nmopun

Dummy variables 𝑥 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		unoplin 31895	. . . . 5 ⊢ (𝑇 ∈ UniOp → 𝑇 ∈ LinOp)
2		lnopf 31834	. . . . 5 ⊢ (𝑇 ∈ LinOp → 𝑇: ℋ⟶ ℋ)
3	1, 2	syl 17	. . . 4 ⊢ (𝑇 ∈ UniOp → 𝑇: ℋ⟶ ℋ)
4		nmopval 31831	. . . 4 ⊢ (𝑇: ℋ⟶ ℋ → (normop‘𝑇) = sup({𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}, ℝ*, < ))
5	3, 4	syl 17	. . 3 ⊢ (𝑇 ∈ UniOp → (normop‘𝑇) = sup({𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}, ℝ*, < ))
6	5	adantl 480	. 2 ⊢ (( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → (normop‘𝑇) = sup({𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}, ℝ*, < ))
7		nmopsetretHIL 31839	. . . . . . 7 ⊢ (𝑇: ℋ⟶ ℋ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ)
8		ressxr 11309	. . . . . . 7 ⊢ ℝ ⊆ ℝ*
9	7, 8	sstrdi 4003	. . . . . 6 ⊢ (𝑇: ℋ⟶ ℋ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ*)
10	3, 9	syl 17	. . . . 5 ⊢ (𝑇 ∈ UniOp → {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ*)
11	10	adantl 480	. . . 4 ⊢ (( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ*)
12		1xr 11324	. . . 4 ⊢ 1 ∈ ℝ*
13	11, 12	jctir 519	. . 3 ⊢ (( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → ({𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ* ∧ 1 ∈ ℝ*))
14		vex 3476	. . . . . . 7 ⊢ 𝑧 ∈ V
15		eqeq1 2733	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑥 = (normℎ‘(𝑇‘𝑦)) ↔ 𝑧 = (normℎ‘(𝑇‘𝑦))))
16	15	anbi2d 628	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦))) ↔ ((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘(𝑇‘𝑦)))))
17	16	rexbidv 3172	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦))) ↔ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘(𝑇‘𝑦)))))
18	14, 17	elab 3678	. . . . . 6 ⊢ (𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ↔ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘(𝑇‘𝑦))))
19		unopnorm 31892	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) → (normℎ‘(𝑇‘𝑦)) = (normℎ‘𝑦))
20	19	eqeq2d 2740	. . . . . . . . . 10 ⊢ ((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) → (𝑧 = (normℎ‘(𝑇‘𝑦)) ↔ 𝑧 = (normℎ‘𝑦)))
21	20	anbi2d 628	. . . . . . . . 9 ⊢ ((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) → (((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘(𝑇‘𝑦))) ↔ ((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘𝑦))))
22		breq1 5157	. . . . . . . . . 10 ⊢ (𝑧 = (normℎ‘𝑦) → (𝑧 ≤ 1 ↔ (normℎ‘𝑦) ≤ 1))
23	22	biimparc 478	. . . . . . . . 9 ⊢ (((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘𝑦)) → 𝑧 ≤ 1)
24	21, 23	biimtrdi 252	. . . . . . . 8 ⊢ ((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) → (((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘(𝑇‘𝑦))) → 𝑧 ≤ 1))
25	24	rexlimdva 3148	. . . . . . 7 ⊢ (𝑇 ∈ UniOp → (∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘(𝑇‘𝑦))) → 𝑧 ≤ 1))
26	25	imp 405	. . . . . 6 ⊢ ((𝑇 ∈ UniOp ∧ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘(𝑇‘𝑦)))) → 𝑧 ≤ 1)
27	18, 26	sylan2b 592	. . . . 5 ⊢ ((𝑇 ∈ UniOp ∧ 𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}) → 𝑧 ≤ 1)
28	27	ralrimiva 3139	. . . 4 ⊢ (𝑇 ∈ UniOp → ∀𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 ≤ 1)
29	28	adantl 480	. . 3 ⊢ (( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → ∀𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 ≤ 1)
30		hne0 31522	. . . . . . . . . . 11 ⊢ ( ℋ ≠ 0ℋ ↔ ∃𝑦 ∈ ℋ 𝑦 ≠ 0ℎ)
31		norm1hex 31226	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ ℋ 𝑦 ≠ 0ℎ ↔ ∃𝑦 ∈ ℋ (normℎ‘𝑦) = 1)
32	30, 31	sylbb 218	. . . . . . . . . 10 ⊢ ( ℋ ≠ 0ℋ → ∃𝑦 ∈ ℋ (normℎ‘𝑦) = 1)
33	32	adantr 479	. . . . . . . . 9 ⊢ (( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → ∃𝑦 ∈ ℋ (normℎ‘𝑦) = 1)
34		1le1 11893	. . . . . . . . . . . . . 14 ⊢ 1 ≤ 1
35		breq1 5157	. . . . . . . . . . . . . 14 ⊢ ((normℎ‘𝑦) = 1 → ((normℎ‘𝑦) ≤ 1 ↔ 1 ≤ 1))
36	34, 35	mpbiri 257	. . . . . . . . . . . . 13 ⊢ ((normℎ‘𝑦) = 1 → (normℎ‘𝑦) ≤ 1)
37	36	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) → ((normℎ‘𝑦) = 1 → (normℎ‘𝑦) ≤ 1))
38	19	adantr 479	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) ∧ (normℎ‘𝑦) = 1) → (normℎ‘(𝑇‘𝑦)) = (normℎ‘𝑦))
39		eqeq2 2741	. . . . . . . . . . . . . . . 16 ⊢ ((normℎ‘𝑦) = 1 → ((normℎ‘(𝑇‘𝑦)) = (normℎ‘𝑦) ↔ (normℎ‘(𝑇‘𝑦)) = 1))
40	39	adantl 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) ∧ (normℎ‘𝑦) = 1) → ((normℎ‘(𝑇‘𝑦)) = (normℎ‘𝑦) ↔ (normℎ‘(𝑇‘𝑦)) = 1))
41	38, 40	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) ∧ (normℎ‘𝑦) = 1) → (normℎ‘(𝑇‘𝑦)) = 1)
42	41	eqcomd 2735	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) ∧ (normℎ‘𝑦) = 1) → 1 = (normℎ‘(𝑇‘𝑦)))
43	42	ex 411	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) → ((normℎ‘𝑦) = 1 → 1 = (normℎ‘(𝑇‘𝑦))))
44	37, 43	jcad 511	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) → ((normℎ‘𝑦) = 1 → ((normℎ‘𝑦) ≤ 1 ∧ 1 = (normℎ‘(𝑇‘𝑦)))))
45	44	adantll 712	. . . . . . . . . 10 ⊢ ((( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) ∧ 𝑦 ∈ ℋ) → ((normℎ‘𝑦) = 1 → ((normℎ‘𝑦) ≤ 1 ∧ 1 = (normℎ‘(𝑇‘𝑦)))))
46	45	reximdva 3161	. . . . . . . . 9 ⊢ (( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → (∃𝑦 ∈ ℋ (normℎ‘𝑦) = 1 → ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 1 = (normℎ‘(𝑇‘𝑦)))))
47	33, 46	mpd 15	. . . . . . . 8 ⊢ (( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 1 = (normℎ‘(𝑇‘𝑦))))
48		1ex 11261	. . . . . . . . 9 ⊢ 1 ∈ V
49		eqeq1 2733	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (𝑥 = (normℎ‘(𝑇‘𝑦)) ↔ 1 = (normℎ‘(𝑇‘𝑦))))
50	49	anbi2d 628	. . . . . . . . . 10 ⊢ (𝑥 = 1 → (((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦))) ↔ ((normℎ‘𝑦) ≤ 1 ∧ 1 = (normℎ‘(𝑇‘𝑦)))))
51	50	rexbidv 3172	. . . . . . . . 9 ⊢ (𝑥 = 1 → (∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦))) ↔ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 1 = (normℎ‘(𝑇‘𝑦)))))
52	48, 51	elab 3678	. . . . . . . 8 ⊢ (1 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ↔ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 1 = (normℎ‘(𝑇‘𝑦))))
53	47, 52	sylibr 233	. . . . . . 7 ⊢ (( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → 1 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))})
54	53	adantr 479	. . . . . 6 ⊢ ((( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) ∧ 𝑧 ∈ ℝ) → 1 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))})
55		breq2 5158	. . . . . . 7 ⊢ (𝑤 = 1 → (𝑧 < 𝑤 ↔ 𝑧 < 1))
56	55	rspcev 3620	. . . . . 6 ⊢ ((1 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ∧ 𝑧 < 1) → ∃𝑤 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 < 𝑤)
57	54, 56	sylan 578	. . . . 5 ⊢ (((( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < 1) → ∃𝑤 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 < 𝑤)
58	57	ex 411	. . . 4 ⊢ ((( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) ∧ 𝑧 ∈ ℝ) → (𝑧 < 1 → ∃𝑤 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 < 𝑤))
59	58	ralrimiva 3139	. . 3 ⊢ (( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → ∀𝑧 ∈ ℝ (𝑧 < 1 → ∃𝑤 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 < 𝑤))
60		supxr2 13351	. . 3 ⊢ ((({𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ* ∧ 1 ∈ ℝ*) ∧ (∀𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 ≤ 1 ∧ ∀𝑧 ∈ ℝ (𝑧 < 1 → ∃𝑤 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 < 𝑤))) → sup({𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}, ℝ*, < ) = 1)
61	13, 29, 59, 60	syl12anc 835	. 2 ⊢ (( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → sup({𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}, ℝ*, < ) = 1)
62	6, 61	eqtrd 2769	1 ⊢ (( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → (normop‘𝑇) = 1)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1534   ∈ wcel 2100  {cab 2706   ≠ wne 2933  ∀wral 3054  ∃wrex 3063   ⊆ wss 3958   class class class wbr 5154  ⟶wf 6552  ‘cfv 6556  supcsup 9484  ℝcr 11158  1c1 11160  ℝ^*cxr 11298   < clt 11299   ≤ cle 11300   ℋchba 30894  norm_ℎcno 30898  0_ℎc0v 30899  0_ℋc0h 30910  norm_opcnop 30920  LinOpclo 30922  UniOpcuo 30924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-rep 5291  ax-sep 5305  ax-nul 5312  ax-pow 5371  ax-pr 5435  ax-un 7748  ax-cnex 11215  ax-resscn 11216  ax-1cn 11217  ax-icn 11218  ax-addcl 11219  ax-addrcl 11220  ax-mulcl 11221  ax-mulrcl 11222  ax-mulcom 11223  ax-addass 11224  ax-mulass 11225  ax-distr 11226  ax-i2m1 11227  ax-1ne0 11228  ax-1rid 11229  ax-rnegex 11230  ax-rrecex 11231  ax-cnre 11232  ax-pre-lttri 11233  ax-pre-lttrn 11234  ax-pre-ltadd 11235  ax-pre-mulgt0 11236  ax-pre-sup 11237  ax-hilex 30974  ax-hfvadd 30975  ax-hvcom 30976  ax-hvass 30977  ax-hv0cl 30978  ax-hvaddid 30979  ax-hfvmul 30980  ax-hvmulid 30981  ax-hvmulass 30982  ax-hvdistr1 30983  ax-hvdistr2 30984  ax-hvmul0 30985  ax-hfi 31054  ax-his1 31057  ax-his2 31058  ax-his3 31059  ax-his4 31060

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-nel 3040  df-ral 3055  df-rex 3064  df-rmo 3373  df-reu 3374  df-rab 3429  df-v 3474  df-sbc 3788  df-csb 3904  df-dif 3961  df-un 3963  df-in 3965  df-ss 3975  df-pss 3978  df-nul 4334  df-if 4535  df-pw 4610  df-sn 4635  df-pr 4637  df-op 4641  df-uni 4917  df-iun 5006  df-br 5155  df-opab 5217  df-mpt 5238  df-tr 5272  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5639  df-we 5641  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6315  df-ord 6381  df-on 6382  df-lim 6383  df-suc 6384  df-iota 6508  df-fun 6558  df-fn 6559  df-f 6560  df-f1 6561  df-fo 6562  df-f1o 6563  df-fv 6564  df-riota 7383  df-ov 7430  df-oprab 7431  df-mpo 7432  df-om 7882  df-1st 8008  df-2nd 8009  df-frecs 8300  df-wrecs 8331  df-recs 8405  df-rdg 8444  df-er 8738  df-map 8861  df-en 8979  df-dom 8980  df-sdom 8981  df-sup 9486  df-pnf 11301  df-mnf 11302  df-xr 11303  df-ltxr 11304  df-le 11305  df-sub 11497  df-neg 11498  df-div 11923  df-nn 12269  df-2 12331  df-3 12332  df-4 12333  df-n0 12529  df-z 12615  df-uz 12879  df-rp 13033  df-seq 14027  df-exp 14087  df-cj 15117  df-re 15118  df-im 15119  df-sqrt 15253  df-abs 15254  df-grpo 30468  df-gid 30469  df-ablo 30520  df-vc 30534  df-nv 30567  df-va 30570  df-ba 30571  df-sm 30572  df-0v 30573  df-nmcv 30575  df-hnorm 30943  df-hba 30944  df-hvsub 30946  df-hlim 30947  df-sh 31182  df-ch 31196  df-ch0 31228  df-nmop 31814  df-lnop 31816  df-unop 31818

This theorem is referenced by:  unopbd  31990  unierri  32079