HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  leopnmid Structured version   Visualization version   GIF version

Theorem leopnmid 31976
Description: A bounded Hermitian operator is less than or equal to its norm times the identity operator. (Contributed by NM, 11-Aug-2006.) (New usage is discouraged.)
Assertion
Ref Expression
leopnmid ((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โ†’ ๐‘‡ โ‰คop ((normopโ€˜๐‘‡) ยทop Iop ))

Proof of Theorem leopnmid
Dummy variable ๐‘ฅ is distinct from all other variables.
StepHypRef Expression
1 hmopre 31761 . . . . 5 ((๐‘‡ โˆˆ HrmOp โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ ((๐‘‡โ€˜๐‘ฅ) ยทih ๐‘ฅ) โˆˆ โ„)
21adantlr 713 . . . 4 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ ((๐‘‡โ€˜๐‘ฅ) ยทih ๐‘ฅ) โˆˆ โ„)
31recnd 11282 . . . . . 6 ((๐‘‡ โˆˆ HrmOp โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ ((๐‘‡โ€˜๐‘ฅ) ยทih ๐‘ฅ) โˆˆ โ„‚)
43abscld 15425 . . . . 5 ((๐‘‡ โˆˆ HrmOp โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (absโ€˜((๐‘‡โ€˜๐‘ฅ) ยทih ๐‘ฅ)) โˆˆ โ„)
54adantlr 713 . . . 4 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (absโ€˜((๐‘‡โ€˜๐‘ฅ) ยทih ๐‘ฅ)) โˆˆ โ„)
6 idhmop 31820 . . . . . . 7 Iop โˆˆ HrmOp
7 hmopm 31859 . . . . . . 7 (((normopโ€˜๐‘‡) โˆˆ โ„ โˆง Iop โˆˆ HrmOp) โ†’ ((normopโ€˜๐‘‡) ยทop Iop ) โˆˆ HrmOp)
86, 7mpan2 689 . . . . . 6 ((normopโ€˜๐‘‡) โˆˆ โ„ โ†’ ((normopโ€˜๐‘‡) ยทop Iop ) โˆˆ HrmOp)
9 hmopre 31761 . . . . . 6 ((((normopโ€˜๐‘‡) ยทop Iop ) โˆˆ HrmOp โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ ((((normopโ€˜๐‘‡) ยทop Iop )โ€˜๐‘ฅ) ยทih ๐‘ฅ) โˆˆ โ„)
108, 9sylan 578 . . . . 5 (((normopโ€˜๐‘‡) โˆˆ โ„ โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ ((((normopโ€˜๐‘‡) ยทop Iop )โ€˜๐‘ฅ) ยทih ๐‘ฅ) โˆˆ โ„)
1110adantll 712 . . . 4 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ ((((normopโ€˜๐‘‡) ยทop Iop )โ€˜๐‘ฅ) ยทih ๐‘ฅ) โˆˆ โ„)
121leabsd 15403 . . . . 5 ((๐‘‡ โˆˆ HrmOp โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ ((๐‘‡โ€˜๐‘ฅ) ยทih ๐‘ฅ) โ‰ค (absโ€˜((๐‘‡โ€˜๐‘ฅ) ยทih ๐‘ฅ)))
1312adantlr 713 . . . 4 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ ((๐‘‡โ€˜๐‘ฅ) ยทih ๐‘ฅ) โ‰ค (absโ€˜((๐‘‡โ€˜๐‘ฅ) ยทih ๐‘ฅ)))
14 hmopf 31712 . . . . . . . 8 (๐‘‡ โˆˆ HrmOp โ†’ ๐‘‡: โ„‹โŸถ โ„‹)
15 ffvelcdm 7096 . . . . . . . . 9 ((๐‘‡: โ„‹โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (๐‘‡โ€˜๐‘ฅ) โˆˆ โ„‹)
16 normcl 30963 . . . . . . . . 9 ((๐‘‡โ€˜๐‘ฅ) โˆˆ โ„‹ โ†’ (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„)
1715, 16syl 17 . . . . . . . 8 ((๐‘‡: โ„‹โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„)
1814, 17sylan 578 . . . . . . 7 ((๐‘‡ โˆˆ HrmOp โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„)
1918adantlr 713 . . . . . 6 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„)
20 normcl 30963 . . . . . . 7 (๐‘ฅ โˆˆ โ„‹ โ†’ (normโ„Žโ€˜๐‘ฅ) โˆˆ โ„)
2120adantl 480 . . . . . 6 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (normโ„Žโ€˜๐‘ฅ) โˆˆ โ„)
2219, 21remulcld 11284 . . . . 5 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ ((normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) ยท (normโ„Žโ€˜๐‘ฅ)) โˆˆ โ„)
2314, 15sylan 578 . . . . . . 7 ((๐‘‡ โˆˆ HrmOp โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (๐‘‡โ€˜๐‘ฅ) โˆˆ โ„‹)
24 bcs 31019 . . . . . . 7 (((๐‘‡โ€˜๐‘ฅ) โˆˆ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (absโ€˜((๐‘‡โ€˜๐‘ฅ) ยทih ๐‘ฅ)) โ‰ค ((normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) ยท (normโ„Žโ€˜๐‘ฅ)))
2523, 24sylancom 586 . . . . . 6 ((๐‘‡ โˆˆ HrmOp โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (absโ€˜((๐‘‡โ€˜๐‘ฅ) ยทih ๐‘ฅ)) โ‰ค ((normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) ยท (normโ„Žโ€˜๐‘ฅ)))
2625adantlr 713 . . . . 5 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (absโ€˜((๐‘‡โ€˜๐‘ฅ) ยทih ๐‘ฅ)) โ‰ค ((normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) ยท (normโ„Žโ€˜๐‘ฅ)))
27 remulcl 11233 . . . . . . . . 9 (((normopโ€˜๐‘‡) โˆˆ โ„ โˆง (normโ„Žโ€˜๐‘ฅ) โˆˆ โ„) โ†’ ((normopโ€˜๐‘‡) ยท (normโ„Žโ€˜๐‘ฅ)) โˆˆ โ„)
2820, 27sylan2 591 . . . . . . . 8 (((normopโ€˜๐‘‡) โˆˆ โ„ โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ ((normopโ€˜๐‘‡) ยท (normโ„Žโ€˜๐‘ฅ)) โˆˆ โ„)
2928adantll 712 . . . . . . 7 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ ((normopโ€˜๐‘‡) ยท (normโ„Žโ€˜๐‘ฅ)) โˆˆ โ„)
30 normge0 30964 . . . . . . . . 9 (๐‘ฅ โˆˆ โ„‹ โ†’ 0 โ‰ค (normโ„Žโ€˜๐‘ฅ))
3120, 30jca 510 . . . . . . . 8 (๐‘ฅ โˆˆ โ„‹ โ†’ ((normโ„Žโ€˜๐‘ฅ) โˆˆ โ„ โˆง 0 โ‰ค (normโ„Žโ€˜๐‘ฅ)))
3231adantl 480 . . . . . . 7 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ ((normโ„Žโ€˜๐‘ฅ) โˆˆ โ„ โˆง 0 โ‰ค (normโ„Žโ€˜๐‘ฅ)))
33 hmoplin 31780 . . . . . . . . 9 (๐‘‡ โˆˆ HrmOp โ†’ ๐‘‡ โˆˆ LinOp)
34 elbdop2 31709 . . . . . . . . . 10 (๐‘‡ โˆˆ BndLinOp โ†” (๐‘‡ โˆˆ LinOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„))
3534biimpri 227 . . . . . . . . 9 ((๐‘‡ โˆˆ LinOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โ†’ ๐‘‡ โˆˆ BndLinOp)
3633, 35sylan 578 . . . . . . . 8 ((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โ†’ ๐‘‡ โˆˆ BndLinOp)
37 nmbdoplb 31863 . . . . . . . 8 ((๐‘‡ โˆˆ BndLinOp โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) โ‰ค ((normopโ€˜๐‘‡) ยท (normโ„Žโ€˜๐‘ฅ)))
3836, 37sylan 578 . . . . . . 7 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) โ‰ค ((normopโ€˜๐‘‡) ยท (normโ„Žโ€˜๐‘ฅ)))
39 lemul1a 12108 . . . . . . 7 ((((normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„ โˆง ((normopโ€˜๐‘‡) ยท (normโ„Žโ€˜๐‘ฅ)) โˆˆ โ„ โˆง ((normโ„Žโ€˜๐‘ฅ) โˆˆ โ„ โˆง 0 โ‰ค (normโ„Žโ€˜๐‘ฅ))) โˆง (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) โ‰ค ((normopโ€˜๐‘‡) ยท (normโ„Žโ€˜๐‘ฅ))) โ†’ ((normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) ยท (normโ„Žโ€˜๐‘ฅ)) โ‰ค (((normopโ€˜๐‘‡) ยท (normโ„Žโ€˜๐‘ฅ)) ยท (normโ„Žโ€˜๐‘ฅ)))
4019, 29, 32, 38, 39syl31anc 1370 . . . . . 6 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ ((normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) ยท (normโ„Žโ€˜๐‘ฅ)) โ‰ค (((normopโ€˜๐‘‡) ยท (normโ„Žโ€˜๐‘ฅ)) ยท (normโ„Žโ€˜๐‘ฅ)))
41 recn 11238 . . . . . . . . . 10 ((normopโ€˜๐‘‡) โˆˆ โ„ โ†’ (normopโ€˜๐‘‡) โˆˆ โ„‚)
4241ad2antlr 725 . . . . . . . . 9 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (normopโ€˜๐‘‡) โˆˆ โ„‚)
4321recnd 11282 . . . . . . . . 9 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (normโ„Žโ€˜๐‘ฅ) โˆˆ โ„‚)
4442, 43, 43mulassd 11277 . . . . . . . 8 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (((normopโ€˜๐‘‡) ยท (normโ„Žโ€˜๐‘ฅ)) ยท (normโ„Žโ€˜๐‘ฅ)) = ((normopโ€˜๐‘‡) ยท ((normโ„Žโ€˜๐‘ฅ) ยท (normโ„Žโ€˜๐‘ฅ))))
45 simpr 483 . . . . . . . . . 10 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ ๐‘ฅ โˆˆ โ„‹)
46 ax-his3 30922 . . . . . . . . . 10 (((normopโ€˜๐‘‡) โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (((normopโ€˜๐‘‡) ยทโ„Ž ๐‘ฅ) ยทih ๐‘ฅ) = ((normopโ€˜๐‘‡) ยท (๐‘ฅ ยทih ๐‘ฅ)))
4742, 45, 45, 46syl3anc 1368 . . . . . . . . 9 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (((normopโ€˜๐‘‡) ยทโ„Ž ๐‘ฅ) ยทih ๐‘ฅ) = ((normopโ€˜๐‘‡) ยท (๐‘ฅ ยทih ๐‘ฅ)))
4820recnd 11282 . . . . . . . . . . . . 13 (๐‘ฅ โˆˆ โ„‹ โ†’ (normโ„Žโ€˜๐‘ฅ) โˆˆ โ„‚)
4948sqvald 14149 . . . . . . . . . . . 12 (๐‘ฅ โˆˆ โ„‹ โ†’ ((normโ„Žโ€˜๐‘ฅ)โ†‘2) = ((normโ„Žโ€˜๐‘ฅ) ยท (normโ„Žโ€˜๐‘ฅ)))
50 normsq 30972 . . . . . . . . . . . 12 (๐‘ฅ โˆˆ โ„‹ โ†’ ((normโ„Žโ€˜๐‘ฅ)โ†‘2) = (๐‘ฅ ยทih ๐‘ฅ))
5149, 50eqtr3d 2770 . . . . . . . . . . 11 (๐‘ฅ โˆˆ โ„‹ โ†’ ((normโ„Žโ€˜๐‘ฅ) ยท (normโ„Žโ€˜๐‘ฅ)) = (๐‘ฅ ยทih ๐‘ฅ))
5251oveq2d 7442 . . . . . . . . . 10 (๐‘ฅ โˆˆ โ„‹ โ†’ ((normopโ€˜๐‘‡) ยท ((normโ„Žโ€˜๐‘ฅ) ยท (normโ„Žโ€˜๐‘ฅ))) = ((normopโ€˜๐‘‡) ยท (๐‘ฅ ยทih ๐‘ฅ)))
5352adantl 480 . . . . . . . . 9 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ ((normopโ€˜๐‘‡) ยท ((normโ„Žโ€˜๐‘ฅ) ยท (normโ„Žโ€˜๐‘ฅ))) = ((normopโ€˜๐‘‡) ยท (๐‘ฅ ยทih ๐‘ฅ)))
5447, 53eqtr4d 2771 . . . . . . . 8 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (((normopโ€˜๐‘‡) ยทโ„Ž ๐‘ฅ) ยทih ๐‘ฅ) = ((normopโ€˜๐‘‡) ยท ((normโ„Žโ€˜๐‘ฅ) ยท (normโ„Žโ€˜๐‘ฅ))))
5544, 54eqtr4d 2771 . . . . . . 7 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (((normopโ€˜๐‘‡) ยท (normโ„Žโ€˜๐‘ฅ)) ยท (normโ„Žโ€˜๐‘ฅ)) = (((normopโ€˜๐‘‡) ยทโ„Ž ๐‘ฅ) ยทih ๐‘ฅ))
56 hoif 31592 . . . . . . . . . . 11 Iop : โ„‹โ€“1-1-ontoโ†’ โ„‹
57 f1of 6844 . . . . . . . . . . 11 ( Iop : โ„‹โ€“1-1-ontoโ†’ โ„‹ โ†’ Iop : โ„‹โŸถ โ„‹)
5856, 57mp1i 13 . . . . . . . . . 10 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ Iop : โ„‹โŸถ โ„‹)
59 homval 31579 . . . . . . . . . 10 (((normopโ€˜๐‘‡) โˆˆ โ„‚ โˆง Iop : โ„‹โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (((normopโ€˜๐‘‡) ยทop Iop )โ€˜๐‘ฅ) = ((normopโ€˜๐‘‡) ยทโ„Ž ( Iop โ€˜๐‘ฅ)))
6042, 58, 45, 59syl3anc 1368 . . . . . . . . 9 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (((normopโ€˜๐‘‡) ยทop Iop )โ€˜๐‘ฅ) = ((normopโ€˜๐‘‡) ยทโ„Ž ( Iop โ€˜๐‘ฅ)))
61 hoival 31593 . . . . . . . . . . 11 (๐‘ฅ โˆˆ โ„‹ โ†’ ( Iop โ€˜๐‘ฅ) = ๐‘ฅ)
6261oveq2d 7442 . . . . . . . . . 10 (๐‘ฅ โˆˆ โ„‹ โ†’ ((normopโ€˜๐‘‡) ยทโ„Ž ( Iop โ€˜๐‘ฅ)) = ((normopโ€˜๐‘‡) ยทโ„Ž ๐‘ฅ))
6362adantl 480 . . . . . . . . 9 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ ((normopโ€˜๐‘‡) ยทโ„Ž ( Iop โ€˜๐‘ฅ)) = ((normopโ€˜๐‘‡) ยทโ„Ž ๐‘ฅ))
6460, 63eqtrd 2768 . . . . . . . 8 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (((normopโ€˜๐‘‡) ยทop Iop )โ€˜๐‘ฅ) = ((normopโ€˜๐‘‡) ยทโ„Ž ๐‘ฅ))
6564oveq1d 7441 . . . . . . 7 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ ((((normopโ€˜๐‘‡) ยทop Iop )โ€˜๐‘ฅ) ยทih ๐‘ฅ) = (((normopโ€˜๐‘‡) ยทโ„Ž ๐‘ฅ) ยทih ๐‘ฅ))
6655, 65eqtr4d 2771 . . . . . 6 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (((normopโ€˜๐‘‡) ยท (normโ„Žโ€˜๐‘ฅ)) ยท (normโ„Žโ€˜๐‘ฅ)) = ((((normopโ€˜๐‘‡) ยทop Iop )โ€˜๐‘ฅ) ยทih ๐‘ฅ))
6740, 66breqtrd 5178 . . . . 5 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ ((normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) ยท (normโ„Žโ€˜๐‘ฅ)) โ‰ค ((((normopโ€˜๐‘‡) ยทop Iop )โ€˜๐‘ฅ) ยทih ๐‘ฅ))
685, 22, 11, 26, 67letrd 11411 . . . 4 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ (absโ€˜((๐‘‡โ€˜๐‘ฅ) ยทih ๐‘ฅ)) โ‰ค ((((normopโ€˜๐‘‡) ยทop Iop )โ€˜๐‘ฅ) ยทih ๐‘ฅ))
692, 5, 11, 13, 68letrd 11411 . . 3 (((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โˆง ๐‘ฅ โˆˆ โ„‹) โ†’ ((๐‘‡โ€˜๐‘ฅ) ยทih ๐‘ฅ) โ‰ค ((((normopโ€˜๐‘‡) ยทop Iop )โ€˜๐‘ฅ) ยทih ๐‘ฅ))
7069ralrimiva 3143 . 2 ((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โ†’ โˆ€๐‘ฅ โˆˆ โ„‹ ((๐‘‡โ€˜๐‘ฅ) ยทih ๐‘ฅ) โ‰ค ((((normopโ€˜๐‘‡) ยทop Iop )โ€˜๐‘ฅ) ยทih ๐‘ฅ))
71 leop2 31962 . . 3 ((๐‘‡ โˆˆ HrmOp โˆง ((normopโ€˜๐‘‡) ยทop Iop ) โˆˆ HrmOp) โ†’ (๐‘‡ โ‰คop ((normopโ€˜๐‘‡) ยทop Iop ) โ†” โˆ€๐‘ฅ โˆˆ โ„‹ ((๐‘‡โ€˜๐‘ฅ) ยทih ๐‘ฅ) โ‰ค ((((normopโ€˜๐‘‡) ยทop Iop )โ€˜๐‘ฅ) ยทih ๐‘ฅ)))
728, 71sylan2 591 . 2 ((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โ†’ (๐‘‡ โ‰คop ((normopโ€˜๐‘‡) ยทop Iop ) โ†” โˆ€๐‘ฅ โˆˆ โ„‹ ((๐‘‡โ€˜๐‘ฅ) ยทih ๐‘ฅ) โ‰ค ((((normopโ€˜๐‘‡) ยทop Iop )โ€˜๐‘ฅ) ยทih ๐‘ฅ)))
7370, 72mpbird 256 1 ((๐‘‡ โˆˆ HrmOp โˆง (normopโ€˜๐‘‡) โˆˆ โ„) โ†’ ๐‘‡ โ‰คop ((normopโ€˜๐‘‡) ยทop Iop ))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 394   = wceq 1533   โˆˆ wcel 2098  โˆ€wral 3058   class class class wbr 5152  โŸถwf 6549  โ€“1-1-ontoโ†’wf1o 6552  โ€˜cfv 6553  (class class class)co 7426  โ„‚cc 11146  โ„cr 11147  0cc0 11148   ยท cmul 11153   โ‰ค cle 11289  2c2 12307  โ†‘cexp 14068  abscabs 15223   โ„‹chba 30757   ยทโ„Ž csm 30759   ยทih csp 30760  normโ„Žcno 30761   ยทop chot 30777   Iop chio 30782  normopcnop 30783  LinOpclo 30785  BndLinOpcbo 30786  HrmOpcho 30788   โ‰คop cleo 30796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7748  ax-inf2 9674  ax-cc 10468  ax-cnex 11204  ax-resscn 11205  ax-1cn 11206  ax-icn 11207  ax-addcl 11208  ax-addrcl 11209  ax-mulcl 11210  ax-mulrcl 11211  ax-mulcom 11212  ax-addass 11213  ax-mulass 11214  ax-distr 11215  ax-i2m1 11216  ax-1ne0 11217  ax-1rid 11218  ax-rnegex 11219  ax-rrecex 11220  ax-cnre 11221  ax-pre-lttri 11222  ax-pre-lttrn 11223  ax-pre-ltadd 11224  ax-pre-mulgt0 11225  ax-pre-sup 11226  ax-addf 11227  ax-mulf 11228  ax-hilex 30837  ax-hfvadd 30838  ax-hvcom 30839  ax-hvass 30840  ax-hv0cl 30841  ax-hvaddid 30842  ax-hfvmul 30843  ax-hvmulid 30844  ax-hvmulass 30845  ax-hvdistr1 30846  ax-hvdistr2 30847  ax-hvmul0 30848  ax-hfi 30917  ax-his1 30920  ax-his2 30921  ax-his3 30922  ax-his4 30923  ax-hcompl 31040
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-iin 5003  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-isom 6562  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-of 7692  df-om 7879  df-1st 8001  df-2nd 8002  df-supp 8174  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-1o 8495  df-2o 8496  df-oadd 8499  df-omul 8500  df-er 8733  df-map 8855  df-pm 8856  df-ixp 8925  df-en 8973  df-dom 8974  df-sdom 8975  df-fin 8976  df-fsupp 9396  df-fi 9444  df-sup 9475  df-inf 9476  df-oi 9543  df-card 9972  df-acn 9975  df-pnf 11290  df-mnf 11291  df-xr 11292  df-ltxr 11293  df-le 11294  df-sub 11486  df-neg 11487  df-div 11912  df-nn 12253  df-2 12315  df-3 12316  df-4 12317  df-5 12318  df-6 12319  df-7 12320  df-8 12321  df-9 12322  df-n0 12513  df-z 12599  df-dec 12718  df-uz 12863  df-q 12973  df-rp 13017  df-xneg 13134  df-xadd 13135  df-xmul 13136  df-ioo 13370  df-ico 13372  df-icc 13373  df-fz 13527  df-fzo 13670  df-fl 13799  df-seq 14009  df-exp 14069  df-hash 14332  df-cj 15088  df-re 15089  df-im 15090  df-sqrt 15224  df-abs 15225  df-clim 15474  df-rlim 15475  df-sum 15675  df-struct 17125  df-sets 17142  df-slot 17160  df-ndx 17172  df-base 17190  df-ress 17219  df-plusg 17255  df-mulr 17256  df-starv 17257  df-sca 17258  df-vsca 17259  df-ip 17260  df-tset 17261  df-ple 17262  df-ds 17264  df-unif 17265  df-hom 17266  df-cco 17267  df-rest 17413  df-topn 17414  df-0g 17432  df-gsum 17433  df-topgen 17434  df-pt 17435  df-prds 17438  df-xrs 17493  df-qtop 17498  df-imas 17499  df-xps 17501  df-mre 17575  df-mrc 17576  df-acs 17578  df-mgm 18609  df-sgrp 18688  df-mnd 18704  df-submnd 18750  df-mulg 19038  df-cntz 19282  df-cmn 19751  df-psmet 21285  df-xmet 21286  df-met 21287  df-bl 21288  df-mopn 21289  df-fbas 21290  df-fg 21291  df-cnfld 21294  df-top 22824  df-topon 22841  df-topsp 22863  df-bases 22877  df-cld 22951  df-ntr 22952  df-cls 22953  df-nei 23030  df-cn 23159  df-cnp 23160  df-lm 23161  df-t1 23246  df-haus 23247  df-tx 23494  df-hmeo 23687  df-fil 23778  df-fm 23870  df-flim 23871  df-flf 23872  df-xms 24254  df-ms 24255  df-tms 24256  df-cfil 25211  df-cau 25212  df-cmet 25213  df-grpo 30331  df-gid 30332  df-ginv 30333  df-gdiv 30334  df-ablo 30383  df-vc 30397  df-nv 30430  df-va 30433  df-ba 30434  df-sm 30435  df-0v 30436  df-vs 30437  df-nmcv 30438  df-ims 30439  df-dip 30539  df-ssp 30560  df-ph 30651  df-cbn 30701  df-hnorm 30806  df-hba 30807  df-hvsub 30809  df-hlim 30810  df-hcau 30811  df-sh 31045  df-ch 31059  df-oc 31090  df-ch0 31091  df-shs 31146  df-pjh 31233  df-hosum 31568  df-homul 31569  df-hodif 31570  df-h0op 31586  df-iop 31587  df-nmop 31677  df-lnop 31679  df-bdop 31680  df-hmop 31682  df-leop 31690
This theorem is referenced by:  nmopleid  31977
  Copyright terms: Public domain W3C validator