Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  nmopadjlei Unicode version

 Description: Property of the norm of an adjoint. Part of proof of Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
Hypothesis
Ref Expression
Assertion
Ref Expression

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bdopssadj 23504 . . . . . 6
2 nmopadjle.1 . . . . . 6
31, 2sselii 3302 . . . . 5
4 adjvalval 23360 . . . . 5
53, 4mpan 652 . . . 4
6 oveq2 6042 . . . . . . . 8
76eqeq1d 2409 . . . . . . 7
87ralbidv 2683 . . . . . 6
98riotabidv 6501 . . . . 5
10 eqid 2401 . . . . 5
11 riotaex 6503 . . . . 5
129, 10, 11fvmpt 5759 . . . 4
135, 12eqtr4d 2436 . . 3
1413fveq2d 5686 . 2
15 inss1 3518 . . . 4
16 lncnbd 23461 . . . . 5
172, 16eleqtrri 2474 . . . 4
1815, 17sselii 3302 . . 3
19 inss2 3519 . . . 4
2019, 17sselii 3302 . . 3
21 eqid 2401 . . 3
22 oveq2 6042 . . . . . 6
2322eqeq2d 2412 . . . . 5
2423ralbidv 2683 . . . 4
2524cbvriotav 6511 . . 3
2618, 20, 21, 25, 10cnlnadjlem7 23496 . 2
2714, 26eqbrtrd 4187 1