Metamath Proof Explorer


Theorem cnlnadjlem8

Description: Lemma for cnlnadji . F is continuous. (Contributed by NM, 17-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypotheses cnlnadjlem.1 โŠข ๐‘‡ โˆˆ LinOp
cnlnadjlem.2 โŠข ๐‘‡ โˆˆ ContOp
cnlnadjlem.3 โŠข ๐บ = ( ๐‘” โˆˆ โ„‹ โ†ฆ ( ( ๐‘‡ โ€˜ ๐‘” ) ยทih ๐‘ฆ ) )
cnlnadjlem.4 โŠข ๐ต = ( โ„ฉ ๐‘ค โˆˆ โ„‹ โˆ€ ๐‘ฃ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฃ ) ยทih ๐‘ฆ ) = ( ๐‘ฃ ยทih ๐‘ค ) )
cnlnadjlem.5 โŠข ๐น = ( ๐‘ฆ โˆˆ โ„‹ โ†ฆ ๐ต )
Assertion cnlnadjlem8 ๐น โˆˆ ContOp

Proof

Step Hyp Ref Expression
1 cnlnadjlem.1 โŠข ๐‘‡ โˆˆ LinOp
2 cnlnadjlem.2 โŠข ๐‘‡ โˆˆ ContOp
3 cnlnadjlem.3 โŠข ๐บ = ( ๐‘” โˆˆ โ„‹ โ†ฆ ( ( ๐‘‡ โ€˜ ๐‘” ) ยทih ๐‘ฆ ) )
4 cnlnadjlem.4 โŠข ๐ต = ( โ„ฉ ๐‘ค โˆˆ โ„‹ โˆ€ ๐‘ฃ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฃ ) ยทih ๐‘ฆ ) = ( ๐‘ฃ ยทih ๐‘ค ) )
5 cnlnadjlem.5 โŠข ๐น = ( ๐‘ฆ โˆˆ โ„‹ โ†ฆ ๐ต )
6 1 2 nmcopexi โŠข ( normop โ€˜ ๐‘‡ ) โˆˆ โ„
7 1 2 3 4 5 cnlnadjlem7 โŠข ( ๐‘ง โˆˆ โ„‹ โ†’ ( normโ„Ž โ€˜ ( ๐น โ€˜ ๐‘ง ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐‘ง ) ) )
8 7 rgen โŠข โˆ€ ๐‘ง โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐น โ€˜ ๐‘ง ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐‘ง ) )
9 oveq1 โŠข ( ๐‘ฅ = ( normop โ€˜ ๐‘‡ ) โ†’ ( ๐‘ฅ ยท ( normโ„Ž โ€˜ ๐‘ง ) ) = ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐‘ง ) ) )
10 9 breq2d โŠข ( ๐‘ฅ = ( normop โ€˜ ๐‘‡ ) โ†’ ( ( normโ„Ž โ€˜ ( ๐น โ€˜ ๐‘ง ) ) โ‰ค ( ๐‘ฅ ยท ( normโ„Ž โ€˜ ๐‘ง ) ) โ†” ( normโ„Ž โ€˜ ( ๐น โ€˜ ๐‘ง ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐‘ง ) ) ) )
11 10 ralbidv โŠข ( ๐‘ฅ = ( normop โ€˜ ๐‘‡ ) โ†’ ( โˆ€ ๐‘ง โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐น โ€˜ ๐‘ง ) ) โ‰ค ( ๐‘ฅ ยท ( normโ„Ž โ€˜ ๐‘ง ) ) โ†” โˆ€ ๐‘ง โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐น โ€˜ ๐‘ง ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐‘ง ) ) ) )
12 11 rspcev โŠข ( ( ( normop โ€˜ ๐‘‡ ) โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐น โ€˜ ๐‘ง ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐‘ง ) ) ) โ†’ โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ง โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐น โ€˜ ๐‘ง ) ) โ‰ค ( ๐‘ฅ ยท ( normโ„Ž โ€˜ ๐‘ง ) ) )
13 6 8 12 mp2an โŠข โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ง โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐น โ€˜ ๐‘ง ) ) โ‰ค ( ๐‘ฅ ยท ( normโ„Ž โ€˜ ๐‘ง ) )
14 1 2 3 4 5 cnlnadjlem6 โŠข ๐น โˆˆ LinOp
15 14 lnopconi โŠข ( ๐น โˆˆ ContOp โ†” โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ง โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐น โ€˜ ๐‘ง ) ) โ‰ค ( ๐‘ฅ ยท ( normโ„Ž โ€˜ ๐‘ง ) ) )
16 13 15 mpbir โŠข ๐น โˆˆ ContOp