HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version
Theorem nmopunt 9854
Description: Norm of a unitary Hilbert space operator.
Assertion
Ref Expression
nmopunt |- ((H~ =/= 0H /\ T e. UniOp) -> (normop` T) = 1)
Proof of Theorem nmopunt
StepHypRef Expression
1 unoplint 9760 . . . . 5 |- (T e. UniOp -> T e. LinOp)
2 lnopft 9702 . . . . 5 |- (T e. LinOp -> T:H~-->H~)
31, 2syl 10 . . . 4 |- (T e. UniOp -> T:H~-->H~)
4 nmopvalt 9699 . . . 4 |- (T:H~-->H~ -> (normop` T) = sup({x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))}, RR*, < ))
53, 4syl 10 . . 3 |- (T e. UniOp -> (normop` T) = sup({x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))}, RR*, < ))
65adantl 388 . 2 |- ((H~ =/= 0H /\ T e. UniOp) -> (normop` T) = sup({x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))}, RR*, < ))
7 supxr2 6029 . . 3 |- ((({x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))} (_ RR* /\ 1 e. RR*) /\ (A.z e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))}z <_ 1 /\ A.z e. RR (z < 1 -> E.w e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))}z < w))) -> sup({x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))}, RR*, < ) = 1)
8 nmopsetretHIL 9708 . . . . . . 7 |- (T:H~-->H~ -> {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))} (_ RR)
9 ressxr 5470 . . . . . . . 8 |- RR (_ RR*
109a1i 8 . . . . . . 7 |- (T:H~-->H~ -> RR (_ RR*)
118, 10sstrd 2064 . . . . . 6 |- (T:H~-->H~ -> {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))} (_ RR*)
123, 11syl 10 . . . . 5 |- (T e. UniOp -> {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))} (_ RR*)
1312adantl 388 . . . 4 |- ((H~ =/= 0H /\ T e. UniOp) -> {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))} (_ RR*)
14 1re 5407 . . . . 5 |- 1 e. RR
15 rexrt 5471 . . . . 5 |- (1 e. RR -> 1 e. RR*)
1614, 15ax-mp 7 . . . 4 |- 1 e. RR*
1713, 16jctir 293 . . 3 |- ((H~ =/= 0H /\ T e. UniOp) -> ({x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))} (_ RR* /\ 1 e. RR*))
18 unopnormt 9757 . . . . . . . . . . . 12 |- ((T e. UniOp /\ y e. H~) -> (normh` (T` y)) = (normh` y))
1918eqeq2d 1478 . . . . . . . . . . 11 |- ((T e. UniOp /\ y e. H~) -> (z = (normh` (T` y)) <-> z = (normh` y)))
2019anbi2d 614 . . . . . . . . . 10 |- ((T e. UniOp /\ y e. H~) -> (((normh` y) <_ 1 /\ z = (normh` (T` y))) <-> ((normh` y) <_ 1 /\ z = (normh` y))))
21 breq1 2612 . . . . . . . . . . 11 |- (z = (normh` y) -> (z <_ 1 <-> (normh` y) <_ 1))
2221biimparc 419 . . . . . . . . . 10 |- (((normh` y) <_ 1 /\ z = (normh` y)) -> z <_ 1)
2320, 22syl6bi 214 . . . . . . . . 9 |- ((T e. UniOp /\ y e. H~) -> (((normh` y) <_ 1 /\ z = (normh` (T` y))) -> z <_ 1))
2423r19.23adva 1739 . . . . . . . 8 |- (T e. UniOp -> (E.y e. H~ ((normh` y) <_ 1 /\ z = (normh` (T` y))) -> z <_ 1))
2524imp 350 . . . . . . 7 |- ((T e. UniOp /\ E.y e. H~ ((normh` y) <_ 1 /\ z = (normh` (T` y)))) -> z <_ 1)
26 visset 1804 . . . . . . . 8 |- z e. V
27 eqeq1 1473 . . . . . . . . . 10 |- (x = z -> (x = (normh` (T` y)) <-> z = (normh` (T` y))))
2827anbi2d 614 . . . . . . . . 9 |- (x = z -> (((normh` y) <_ 1 /\ x = (normh` (T` y))) <-> ((normh` y) <_ 1 /\ z = (normh` (T` y)))))
2928rexbidv 1656 . . . . . . . 8 |- (x = z -> (E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y))) <-> E.y e. H~ ((normh` y) <_ 1 /\ z = (normh` (T` y)))))
3026, 29elab 1888 . . . . . . 7 |- (z e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))} <-> E.y e. H~ ((normh` y) <_ 1 /\ z = (normh` (T` y))))
3125, 30sylan2b 452 . . . . . 6 |- ((T e. UniOp /\ z e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))}) -> z <_ 1)
3231r19.21aiva 1706 . . . . 5 |- (T e. UniOp -> A.z e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))}z <_ 1)
3332adantl 388 . . . 4 |- ((H~ =/= 0H /\ T e. UniOp) -> A.z e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))}z <_ 1)
34 breq2 2613 . . . . . . . 8 |- (w = 1 -> (z < w <-> z < 1))
3534rcla4ev 1868 . . . . . . 7 |- ((1 e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))} /\ z < 1) -> E.w e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))}z < w)
36 hne0 9385 . . . . . . . . . . . . 13 |- (H~ =/= 0H <-> E.y e. H~ y =/= 0h)
37 norm1hext 9044 . . . . . . . . . . . . 13 |- (E.y e. H~ y =/= 0h <-> E.y e. H~ (normh` y) = 1)
3836, 37bitr 173 . . . . . . . . . . . 12 |- (H~ =/= 0H <-> E.y e. H~ (normh` y) = 1)
3938biimp 151 . . . . . . . . . . 11 |- (H~ =/= 0H -> E.y e. H~ (normh` y) = 1)
4039adantr 389 . . . . . . . . . 10 |- ((H~ =/= 0H /\ T e. UniOp) -> E.y e. H~ (normh` y) = 1)
4114leid 5584 . . . . . . . . . . . . . . 15 |- 1 <_ 1
42 breq1 2612 . . . . . . . . . . . . . . 15 |- ((normh` y) = 1 -> ((normh` y) <_ 1 <-> 1 <_ 1))
4341, 42mpbiri 194 . . . . . . . . . . . . . 14 |- ((normh` y) = 1 -> (normh` y) <_ 1)
4443a1i 8 . . . . . . . . . . . . 13 |- ((T e. UniOp /\ y e. H~) -> ((normh` y) = 1 -> (normh` y) <_ 1))
4518adantr 389 . . . . . . . . . . . . . . . 16 |- (((T e. UniOp /\ y e. H~) /\ (normh` y) = 1) -> (normh` (T` y)) = (normh` y))
46 eqeq2 1476 . . . . . . . . . . . . . . . . 17 |- ((normh` y) = 1 -> ((normh` (T` y)) = (normh` y) <-> (normh` (T` y)) = 1))
4746adantl 388 . . . . . . . . . . . . . . . 16 |- (((T e. UniOp /\ y e. H~) /\ (normh` y) = 1) -> ((normh` (T` y)) = (normh` y) <-> (normh` (T` y)) = 1))
4845, 47mpbid 195 . . . . . . . . . . . . . . 15 |- (((T e. UniOp /\ y e. H~) /\ (normh` y) = 1) -> (normh` (T` y)) = 1)
4948eqcomd 1472 . . . . . . . . . . . . . 14 |- (((T e. UniOp /\ y e. H~) /\ (normh` y) = 1) -> 1 = (normh` (T` y)))
5049ex 373 . . . . . . . . . . . . 13 |- ((T e. UniOp /\ y e. H~) -> ((normh` y) = 1 -> 1 = (normh` (T` y))))
5144, 50jcad 598 . . . . . . . . . . . 12 |- ((T e. UniOp /\ y e. H~) -> ((normh` y) = 1 -> ((normh` y) <_ 1 /\ 1 = (normh` (T` y)))))
5251adantll 392 . . . . . . . . . . 11 |- (((H~ =/= 0H /\ T e. UniOp) /\ y e. H~) -> ((normh` y) = 1 -> ((normh` y) <_ 1 /\ 1 = (normh` (T` y)))))
5352r19.22dva 1731 . . . . . . . . . 10 |- ((H~ =/= 0H /\ T e. UniOp) -> (E.y e. H~ (normh` y) = 1 -> E.y e. H~ ((normh` y) <_ 1 /\ 1 = (normh` (T` y)))))
5440, 53mpd 26 . . . . . . . . 9 |- ((H~ =/= 0H /\ T e. UniOp) -> E.y e. H~ ((normh` y) <_ 1 /\ 1 = (normh` (T` y))))
5514elisseti 1809 . . . . . . . . . 10 |- 1 e. V
56 eqeq1 1473 . . . . . . . . . . . 12 |- (x = 1 -> (x = (normh` (T` y)) <-> 1 = (normh` (T` y))))
5756anbi2d 614 . . . . . . . . . . 11 |- (x = 1 -> (((normh` y) <_ 1 /\ x = (normh` (T` y))) <-> ((normh` y) <_ 1 /\ 1 = (normh` (T` y)))))
5857rexbidv 1656 . . . . . . . . . 10 |- (x = 1 -> (E.y e. H~ ((normh`