Metamath Proof Explorer


Theorem nmopcoadji

Description: The norm of an operator composed with its adjoint. Part of Theorem 3.11(vi) of Beran p. 106. (Contributed by NM, 8-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypothesis nmopcoadj.1 โŠข ๐‘‡ โˆˆ BndLinOp
Assertion nmopcoadji ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) = ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 )

Proof

Step Hyp Ref Expression
1 nmopcoadj.1 โŠข ๐‘‡ โˆˆ BndLinOp
2 adjbdlnb โŠข ( ๐‘‡ โˆˆ BndLinOp โ†” ( adjโ„Ž โ€˜ ๐‘‡ ) โˆˆ BndLinOp )
3 1 2 mpbi โŠข ( adjโ„Ž โ€˜ ๐‘‡ ) โˆˆ BndLinOp
4 bdopf โŠข ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆˆ BndLinOp โ†’ ( adjโ„Ž โ€˜ ๐‘‡ ) : โ„‹ โŸถ โ„‹ )
5 3 4 ax-mp โŠข ( adjโ„Ž โ€˜ ๐‘‡ ) : โ„‹ โŸถ โ„‹
6 bdopf โŠข ( ๐‘‡ โˆˆ BndLinOp โ†’ ๐‘‡ : โ„‹ โŸถ โ„‹ )
7 1 6 ax-mp โŠข ๐‘‡ : โ„‹ โŸถ โ„‹
8 5 7 hocofi โŠข ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) : โ„‹ โŸถ โ„‹
9 nmopre โŠข ( ๐‘‡ โˆˆ BndLinOp โ†’ ( normop โ€˜ ๐‘‡ ) โˆˆ โ„ )
10 1 9 ax-mp โŠข ( normop โ€˜ ๐‘‡ ) โˆˆ โ„
11 10 resqcli โŠข ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 ) โˆˆ โ„
12 rexr โŠข ( ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 ) โˆˆ โ„ โ†’ ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 ) โˆˆ โ„* )
13 11 12 ax-mp โŠข ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 ) โˆˆ โ„*
14 nmopub โŠข ( ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) : โ„‹ โŸถ โ„‹ โˆง ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 ) โˆˆ โ„* ) โ†’ ( ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 ) โ†” โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 โ†’ ( normโ„Ž โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 ) ) ) )
15 8 13 14 mp2an โŠข ( ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 ) โ†” โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 โ†’ ( normโ„Ž โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 ) ) )
16 5 7 hocoi โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) = ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) )
17 16 fveq2d โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( normโ„Ž โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) )
18 17 adantr โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( normโ„Ž โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) )
19 7 ffvelrni โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ )
20 5 ffvelrni โŠข ( ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ โ†’ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โˆˆ โ„‹ )
21 normcl โŠข ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โˆˆ โ„‹ โ†’ ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) โˆˆ โ„ )
22 19 20 21 3syl โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) โˆˆ โ„ )
23 22 adantr โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) โˆˆ โ„ )
24 nmopre โŠข ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆˆ BndLinOp โ†’ ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) โˆˆ โ„ )
25 3 24 ax-mp โŠข ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) โˆˆ โ„
26 normcl โŠข ( ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โˆˆ โ„ )
27 19 26 syl โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โˆˆ โ„ )
28 remulcl โŠข ( ( ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) โˆˆ โ„ โˆง ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โˆˆ โ„ ) โ†’ ( ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) ยท ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) โˆˆ โ„ )
29 25 27 28 sylancr โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) ยท ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) โˆˆ โ„ )
30 29 adantr โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) ยท ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) โˆˆ โ„ )
31 25 10 remulcli โŠข ( ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) ยท ( normop โ€˜ ๐‘‡ ) ) โˆˆ โ„
32 31 a1i โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) ยท ( normop โ€˜ ๐‘‡ ) ) โˆˆ โ„ )
33 3 nmbdoplbi โŠข ( ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ โ†’ ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) โ‰ค ( ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) ยท ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) )
34 19 33 syl โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) โ‰ค ( ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) ยท ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) )
35 34 adantr โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) โ‰ค ( ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) ยท ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) )
36 27 adantr โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โˆˆ โ„ )
37 10 a1i โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( normop โ€˜ ๐‘‡ ) โˆˆ โ„ )
38 normcl โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( normโ„Ž โ€˜ ๐‘ฅ ) โˆˆ โ„ )
39 remulcl โŠข ( ( ( normop โ€˜ ๐‘‡ ) โˆˆ โ„ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โˆˆ โ„ ) โ†’ ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โˆˆ โ„ )
40 10 38 39 sylancr โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โˆˆ โ„ )
41 40 adantr โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โˆˆ โ„ )
42 1 nmbdoplbi โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) )
43 42 adantr โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) )
44 1re โŠข 1 โˆˆ โ„
45 nmopge0 โŠข ( ๐‘‡ : โ„‹ โŸถ โ„‹ โ†’ 0 โ‰ค ( normop โ€˜ ๐‘‡ ) )
46 1 6 45 mp2b โŠข 0 โ‰ค ( normop โ€˜ ๐‘‡ )
47 10 46 pm3.2i โŠข ( ( normop โ€˜ ๐‘‡ ) โˆˆ โ„ โˆง 0 โ‰ค ( normop โ€˜ ๐‘‡ ) )
48 lemul2a โŠข ( ( ( ( normโ„Ž โ€˜ ๐‘ฅ ) โˆˆ โ„ โˆง 1 โˆˆ โ„ โˆง ( ( normop โ€˜ ๐‘‡ ) โˆˆ โ„ โˆง 0 โ‰ค ( normop โ€˜ ๐‘‡ ) ) ) โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท 1 ) )
49 47 48 mp3anl3 โŠข ( ( ( ( normโ„Ž โ€˜ ๐‘ฅ ) โˆˆ โ„ โˆง 1 โˆˆ โ„ ) โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท 1 ) )
50 44 49 mpanl2 โŠข ( ( ( normโ„Ž โ€˜ ๐‘ฅ ) โˆˆ โ„ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท 1 ) )
51 38 50 sylan โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท 1 ) )
52 10 recni โŠข ( normop โ€˜ ๐‘‡ ) โˆˆ โ„‚
53 52 mulid1i โŠข ( ( normop โ€˜ ๐‘‡ ) ยท 1 ) = ( normop โ€˜ ๐‘‡ )
54 51 53 breqtrdi โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โ‰ค ( normop โ€˜ ๐‘‡ ) )
55 36 41 37 43 54 letrd โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ‰ค ( normop โ€˜ ๐‘‡ ) )
56 nmopge0 โŠข ( ( adjโ„Ž โ€˜ ๐‘‡ ) : โ„‹ โŸถ โ„‹ โ†’ 0 โ‰ค ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) )
57 3 4 56 mp2b โŠข 0 โ‰ค ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) )
58 25 57 pm3.2i โŠข ( ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) โˆˆ โ„ โˆง 0 โ‰ค ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) )
59 lemul2a โŠข ( ( ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โˆˆ โ„ โˆง ( normop โ€˜ ๐‘‡ ) โˆˆ โ„ โˆง ( ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) โˆˆ โ„ โˆง 0 โ‰ค ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) ) ) โˆง ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ‰ค ( normop โ€˜ ๐‘‡ ) ) โ†’ ( ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) ยท ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) โ‰ค ( ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) ยท ( normop โ€˜ ๐‘‡ ) ) )
60 58 59 mp3anl3 โŠข ( ( ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โˆˆ โ„ โˆง ( normop โ€˜ ๐‘‡ ) โˆˆ โ„ ) โˆง ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ‰ค ( normop โ€˜ ๐‘‡ ) ) โ†’ ( ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) ยท ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) โ‰ค ( ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) ยท ( normop โ€˜ ๐‘‡ ) ) )
61 36 37 55 60 syl21anc โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) ยท ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) โ‰ค ( ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) ยท ( normop โ€˜ ๐‘‡ ) ) )
62 23 30 32 35 61 letrd โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) โ‰ค ( ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) ยท ( normop โ€˜ ๐‘‡ ) ) )
63 18 62 eqbrtrd โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( normโ„Ž โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ) โ‰ค ( ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) ยท ( normop โ€˜ ๐‘‡ ) ) )
64 1 nmopadji โŠข ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) = ( normop โ€˜ ๐‘‡ )
65 64 oveq1i โŠข ( ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) ยท ( normop โ€˜ ๐‘‡ ) ) = ( ( normop โ€˜ ๐‘‡ ) ยท ( normop โ€˜ ๐‘‡ ) )
66 52 sqvali โŠข ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 ) = ( ( normop โ€˜ ๐‘‡ ) ยท ( normop โ€˜ ๐‘‡ ) )
67 65 66 eqtr4i โŠข ( ( normop โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) ยท ( normop โ€˜ ๐‘‡ ) ) = ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 )
68 63 67 breqtrdi โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( normโ„Ž โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 ) )
69 68 ex โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 โ†’ ( normโ„Ž โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 ) ) )
70 15 69 mprgbir โŠข ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 )
71 nmopge0 โŠข ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) : โ„‹ โŸถ โ„‹ โ†’ 0 โ‰ค ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) )
72 8 71 ax-mp โŠข 0 โ‰ค ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) )
73 3 1 bdopcoi โŠข ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) โˆˆ BndLinOp
74 nmopre โŠข ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) โˆˆ BndLinOp โ†’ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) โˆˆ โ„ )
75 73 74 ax-mp โŠข ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) โˆˆ โ„
76 75 sqrtcli โŠข ( 0 โ‰ค ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) โ†’ ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โˆˆ โ„ )
77 rexr โŠข ( ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โˆˆ โ„ โ†’ ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โˆˆ โ„* )
78 72 76 77 mp2b โŠข ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โˆˆ โ„*
79 nmopub โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โˆˆ โ„* ) โ†’ ( ( normop โ€˜ ๐‘‡ ) โ‰ค ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โ†” โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ‰ค ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) ) ) )
80 7 78 79 mp2an โŠข ( ( normop โ€˜ ๐‘‡ ) โ‰ค ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โ†” โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ‰ค ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) ) )
81 19 20 syl โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โˆˆ โ„‹ )
82 hicl โŠข ( ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โˆˆ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฅ ) โˆˆ โ„‚ )
83 81 82 mpancom โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฅ ) โˆˆ โ„‚ )
84 83 abscld โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( abs โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฅ ) ) โˆˆ โ„ )
85 84 adantr โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( abs โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฅ ) ) โˆˆ โ„ )
86 22 38 remulcld โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โˆˆ โ„ )
87 86 adantr โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โˆˆ โ„ )
88 75 a1i โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) โˆˆ โ„ )
89 bcs โŠข ( ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โˆˆ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( abs โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฅ ) ) โ‰ค ( ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) )
90 81 89 mpancom โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( abs โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฅ ) ) โ‰ค ( ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) )
91 90 adantr โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( abs โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฅ ) ) โ‰ค ( ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) )
92 5 7 hococli โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) โˆˆ โ„‹ )
93 normcl โŠข ( ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) โˆˆ โ„‹ โ†’ ( normโ„Ž โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ) โˆˆ โ„ )
94 92 93 syl โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( normโ„Ž โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ) โˆˆ โ„ )
95 94 adantr โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( normโ„Ž โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ) โˆˆ โ„ )
96 38 adantr โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( normโ„Ž โ€˜ ๐‘ฅ ) โˆˆ โ„ )
97 normge0 โŠข ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โˆˆ โ„‹ โ†’ 0 โ‰ค ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) )
98 19 20 97 3syl โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ 0 โ‰ค ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) )
99 22 98 jca โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) โˆˆ โ„ โˆง 0 โ‰ค ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) ) )
100 99 adantr โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) โˆˆ โ„ โˆง 0 โ‰ค ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) ) )
101 simpr โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 )
102 lemul2a โŠข ( ( ( ( normโ„Ž โ€˜ ๐‘ฅ ) โˆˆ โ„ โˆง 1 โˆˆ โ„ โˆง ( ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) โˆˆ โ„ โˆง 0 โ‰ค ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) ) ) โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โ‰ค ( ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) ยท 1 ) )
103 44 102 mp3anl2 โŠข ( ( ( ( normโ„Ž โ€˜ ๐‘ฅ ) โˆˆ โ„ โˆง ( ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) โˆˆ โ„ โˆง 0 โ‰ค ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) ) ) โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โ‰ค ( ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) ยท 1 ) )
104 96 100 101 103 syl21anc โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โ‰ค ( ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) ยท 1 ) )
105 22 recnd โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) โˆˆ โ„‚ )
106 105 mulid1d โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) ยท 1 ) = ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) )
107 106 17 eqtr4d โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) ยท 1 ) = ( normโ„Ž โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ) )
108 107 adantr โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) ยท 1 ) = ( normโ„Ž โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ) )
109 104 108 breqtrd โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โ‰ค ( normโ„Ž โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ) )
110 remulcl โŠข ( ( ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) โˆˆ โ„ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โˆˆ โ„ ) โ†’ ( ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โˆˆ โ„ )
111 75 38 110 sylancr โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โˆˆ โ„ )
112 111 adantr โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โˆˆ โ„ )
113 73 nmbdoplbi โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( normโ„Ž โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ) โ‰ค ( ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) )
114 113 adantr โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( normโ„Ž โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ) โ‰ค ( ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) )
115 75 72 pm3.2i โŠข ( ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) โˆˆ โ„ โˆง 0 โ‰ค ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) )
116 lemul2a โŠข ( ( ( ( normโ„Ž โ€˜ ๐‘ฅ ) โˆˆ โ„ โˆง 1 โˆˆ โ„ โˆง ( ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) โˆˆ โ„ โˆง 0 โ‰ค ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) ) โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โ‰ค ( ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ยท 1 ) )
117 115 116 mp3anl3 โŠข ( ( ( ( normโ„Ž โ€˜ ๐‘ฅ ) โˆˆ โ„ โˆง 1 โˆˆ โ„ ) โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โ‰ค ( ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ยท 1 ) )
118 44 117 mpanl2 โŠข ( ( ( normโ„Ž โ€˜ ๐‘ฅ ) โˆˆ โ„ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โ‰ค ( ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ยท 1 ) )
119 38 118 sylan โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โ‰ค ( ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ยท 1 ) )
120 75 recni โŠข ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) โˆˆ โ„‚
121 120 mulid1i โŠข ( ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ยท 1 ) = ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) )
122 119 121 breqtrdi โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โ‰ค ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) )
123 95 112 88 114 122 letrd โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( normโ„Ž โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ) โ‰ค ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) )
124 87 95 88 109 123 letrd โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normโ„Ž โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) โ‰ค ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) )
125 85 87 88 91 124 letrd โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( abs โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฅ ) ) โ‰ค ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) )
126 resqcl โŠข ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โˆˆ โ„ โ†’ ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ†‘ 2 ) โˆˆ โ„ )
127 sqge0 โŠข ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โˆˆ โ„ โ†’ 0 โ‰ค ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ†‘ 2 ) )
128 126 127 absidd โŠข ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โˆˆ โ„ โ†’ ( abs โ€˜ ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ†‘ 2 ) ) = ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ†‘ 2 ) )
129 19 26 128 3syl โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( abs โ€˜ ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ†‘ 2 ) ) = ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ†‘ 2 ) )
130 normsq โŠข ( ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ โ†’ ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ†‘ 2 ) = ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ( ๐‘‡ โ€˜ ๐‘ฅ ) ) )
131 19 130 syl โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ†‘ 2 ) = ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ( ๐‘‡ โ€˜ ๐‘ฅ ) ) )
132 bdopadj โŠข ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆˆ BndLinOp โ†’ ( adjโ„Ž โ€˜ ๐‘‡ ) โˆˆ dom adjโ„Ž )
133 3 132 ax-mp โŠข ( adjโ„Ž โ€˜ ๐‘‡ ) โˆˆ dom adjโ„Ž
134 adj2 โŠข ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆˆ dom adjโ„Ž โˆง ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฅ ) = ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ( ( adjโ„Ž โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) โ€˜ ๐‘ฅ ) ) )
135 133 134 mp3an1 โŠข ( ( ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฅ ) = ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ( ( adjโ„Ž โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) โ€˜ ๐‘ฅ ) ) )
136 19 135 mpancom โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฅ ) = ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ( ( adjโ„Ž โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) โ€˜ ๐‘ฅ ) ) )
137 bdopadj โŠข ( ๐‘‡ โˆˆ BndLinOp โ†’ ๐‘‡ โˆˆ dom adjโ„Ž )
138 adjadj โŠข ( ๐‘‡ โˆˆ dom adjโ„Ž โ†’ ( adjโ„Ž โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) = ๐‘‡ )
139 1 137 138 mp2b โŠข ( adjโ„Ž โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) = ๐‘‡
140 139 fveq1i โŠข ( ( adjโ„Ž โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) โ€˜ ๐‘ฅ ) = ( ๐‘‡ โ€˜ ๐‘ฅ )
141 140 oveq2i โŠข ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ( ( adjโ„Ž โ€˜ ( adjโ„Ž โ€˜ ๐‘‡ ) ) โ€˜ ๐‘ฅ ) ) = ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ( ๐‘‡ โ€˜ ๐‘ฅ ) )
142 136 141 eqtr2di โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฅ ) )
143 131 142 eqtrd โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ†‘ 2 ) = ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฅ ) )
144 143 fveq2d โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( abs โ€˜ ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ†‘ 2 ) ) = ( abs โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฅ ) ) )
145 129 144 eqtr3d โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ†‘ 2 ) = ( abs โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฅ ) ) )
146 145 adantr โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ†‘ 2 ) = ( abs โ€˜ ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฅ ) ) )
147 75 sqsqrti โŠข ( 0 โ‰ค ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) โ†’ ( ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โ†‘ 2 ) = ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) )
148 8 71 147 mp2b โŠข ( ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โ†‘ 2 ) = ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) )
149 148 a1i โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โ†‘ 2 ) = ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) )
150 125 146 149 3brtr4d โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ†‘ 2 ) โ‰ค ( ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โ†‘ 2 ) )
151 normge0 โŠข ( ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ โ†’ 0 โ‰ค ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) )
152 19 151 syl โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ 0 โ‰ค ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) )
153 8 71 76 mp2b โŠข ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โˆˆ โ„
154 75 sqrtge0i โŠข ( 0 โ‰ค ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) โ†’ 0 โ‰ค ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) )
155 8 71 154 mp2b โŠข 0 โ‰ค ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) )
156 le2sq โŠข ( ( ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โˆˆ โ„ โˆง 0 โ‰ค ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) โˆง ( ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โˆˆ โ„ โˆง 0 โ‰ค ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) ) ) โ†’ ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ‰ค ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โ†” ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ†‘ 2 ) โ‰ค ( ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โ†‘ 2 ) ) )
157 153 155 156 mpanr12 โŠข ( ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โˆˆ โ„ โˆง 0 โ‰ค ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) โ†’ ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ‰ค ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โ†” ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ†‘ 2 ) โ‰ค ( ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โ†‘ 2 ) ) )
158 27 152 157 syl2anc โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ‰ค ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โ†” ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ†‘ 2 ) โ‰ค ( ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โ†‘ 2 ) ) )
159 158 adantr โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ‰ค ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โ†” ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ†‘ 2 ) โ‰ค ( ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โ†‘ 2 ) ) )
160 150 159 mpbird โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 ) โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ‰ค ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) )
161 160 ex โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( normโ„Ž โ€˜ ๐‘ฅ ) โ‰ค 1 โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โ‰ค ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) ) )
162 80 161 mprgbir โŠข ( normop โ€˜ ๐‘‡ ) โ‰ค ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) )
163 10 153 le2sqi โŠข ( ( 0 โ‰ค ( normop โ€˜ ๐‘‡ ) โˆง 0 โ‰ค ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) ) โ†’ ( ( normop โ€˜ ๐‘‡ ) โ‰ค ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โ†” ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 ) โ‰ค ( ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โ†‘ 2 ) ) )
164 46 155 163 mp2an โŠข ( ( normop โ€˜ ๐‘‡ ) โ‰ค ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โ†” ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 ) โ‰ค ( ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โ†‘ 2 ) )
165 162 164 mpbi โŠข ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 ) โ‰ค ( ( โˆš โ€˜ ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) โ†‘ 2 )
166 165 148 breqtri โŠข ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 ) โ‰ค ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) )
167 75 11 letri3i โŠข ( ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) = ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 ) โ†” ( ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 ) โˆง ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 ) โ‰ค ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) ) )
168 70 166 167 mpbir2an โŠข ( normop โ€˜ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆ˜ ๐‘‡ ) ) = ( ( normop โ€˜ ๐‘‡ ) โ†‘ 2 )