HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version
Theorem nmopunt 9934
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 9839 . . . . 5 |- (T e. UniOp -> T e. LinOp)
2 lnopft 9780 . . . . 5 |- (T e. LinOp -> T:H~-->H~)
31, 2syl 10 . . . 4 |- (T e. UniOp -> T:H~-->H~)
4 nmopvalt 9777 . . . 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 390 . 2 |- ((H~ =/= 0H /\ T e. UniOp) -> (normop` T) = sup({x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))}, RR*, < ))
7 supxr2 6084 . . 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 9786 . . . . . . 7 |- (T:H~-->H~ -> {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))} (_ RR)
9 ressxr 5510 . . . . . . . 8 |- RR (_ RR*
109a1i 8 . . . . . . 7 |- (T:H~-->H~ -> RR (_ RR*)
118, 10sstrd 2077 . . . . . 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 390 . . . 4 |- ((H~ =/= 0H /\ T e. UniOp) -> {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))} (_ RR*)
14 1re 5447 . . . . 5 |- 1 e. RR
15 rexrt 5511 . . . . 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 9836 . . . . . . . . . . . 12 |- ((T e. UniOp /\ y e. H~) -> (normh` (T` y)) = (normh` y))
1918eqeq2d 1489 . . . . . . . . . . 11 |- ((T e. UniOp /\ y e. H~) -> (z = (normh` (T` y)) <-> z = (normh` y)))
2019anbi2d 618 . . . . . . . . . 10 |- ((T e. UniOp /\ y e. H~) -> (((normh` y) <_ 1 /\ z = (normh` (T` y))) <-> ((normh` y) <_ 1 /\ z = (normh` y))))
21 breq1 2627 . . . . . . . . . . 11 |- (z = (normh` y) -> (z <_ 1 <-> (normh` y) <_ 1))
2221biimparc 421 . . . . . . . . . 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 1750 . . . . . . . 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 1816 . . . . . . . 8 |- z e. V
27 eqeq1 1484 . . . . . . . . . 10 |- (x = z -> (x = (normh` (T` y)) <-> z = (normh` (T` y))))
2827anbi2d 618 . . . . . . . . 9 |- (x = z -> (((normh` y) <_ 1 /\ x = (normh` (T` y))) <-> ((normh` y) <_ 1 /\ z = (normh` (T` y)))))
2928rexbidv 1667 . . . . . . . 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 1900 . . . . . . 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 454 . . . . . 6 |- ((T e. UniOp /\ z e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))}) -> z <_ 1)
3231r19.21aiva 1717 . . . . 5 |- (T e. UniOp -> A.z e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` (T` y)))}z <_ 1)
3332adantl 390 . . . 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 2628 . . . . . . . 8 |- (w = 1 -> (z < w <-> z < 1))
3534rcla4ev 1880 . . . . . . 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 9465 . . . . . . . . . . . . 13 |- (H~ =/= 0H <-> E.y e. H~ y =/= 0h)
37 norm1hext 9118 . . . . . . . . . . . . 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 391 . . . . . . . . . 10 |- ((H~ =/= 0H /\ T e. UniOp) -> E.y e. H~ (normh` y) = 1)
4114leid 5622 . . . . . . . . . . . . . . 15 |- 1 <_ 1
42 breq1 2627 . . . . . . . . . . . . . . 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 391 . . . . . . . . . . . . . . . 16 |- (((T e. UniOp /\ y e. H~) /\ (normh` y) = 1) -> (normh` (T` y)) = (normh` y))
46 eqeq2 1487 . . . . . . . . . . . . . . . . 17 |- ((normh` y) = 1 -> ((normh` (T` y)) = (normh` y) <-> (normh` (T` y)) = 1))
4746adantl 390 . . . . . . . . . . . . . . . 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 1483 . . . . . . . . . . . . . 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 602 . . . . . . . . . . . 12 |- ((T e. UniOp /\ y e. H~) -> ((normh` y) = 1 -> ((normh` y) <_ 1 /\ 1 = (normh` (T` y)))))
5251adantll 394 . . . . . . . . . . 11 |- (((H~ =/= 0H /\ T e. UniOp) /\ y e. H~) -> ((normh` y) = 1 -> ((normh` y) <_ 1 /\ 1 = (normh` (T` y)))))
5352r19.22dva 1742 . . . . . . . . . 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 1821 . . . . . . . . . 10 |- 1 e. V
56 eqeq1 1484 . . . . . . . . . . . 12 |- (x = 1 -> (x = (normh` (T` y)) <-> 1 = (normh` (T` y))))
5756anbi2d 618 . . . . . . . . . . 11 |- (x = 1 -> (((normh` y) <_ 1 /\ x = (normh` (T` y))) <-> ((normh` y) <_ 1 /\ 1 = (normh` (T` y)))))
5857rexbidv 1667 . . . . . . . . . 10 |- (x = 1 -> (E.y e. H~ ((