Metamath Proof Explorer


Theorem cnlnadjlem5

Description: Lemma for cnlnadji . F is an adjoint of T (later, we will show it is unique). (Contributed by NM, 18-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 cnlnadjlem5 ( ( ๐ด โˆˆ โ„‹ โˆง ๐ถ โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ๐ถ ) ยทih ๐ด ) = ( ๐ถ ยทih ( ๐น โ€˜ ๐ด ) ) )

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 nfcv โŠข โ„ฒ ๐‘ฆ ๐ด
7 nfcv โŠข โ„ฒ ๐‘ฆ โ„‹
8 nfcv โŠข โ„ฒ ๐‘ฆ ๐‘“
9 nfcv โŠข โ„ฒ ๐‘ฆ ยทih
10 nfmpt1 โŠข โ„ฒ ๐‘ฆ ( ๐‘ฆ โˆˆ โ„‹ โ†ฆ ๐ต )
11 5 10 nfcxfr โŠข โ„ฒ ๐‘ฆ ๐น
12 11 6 nffv โŠข โ„ฒ ๐‘ฆ ( ๐น โ€˜ ๐ด )
13 8 9 12 nfov โŠข โ„ฒ ๐‘ฆ ( ๐‘“ ยทih ( ๐น โ€˜ ๐ด ) )
14 13 nfeq2 โŠข โ„ฒ ๐‘ฆ ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐ด ) = ( ๐‘“ ยทih ( ๐น โ€˜ ๐ด ) )
15 7 14 nfralw โŠข โ„ฒ ๐‘ฆ โˆ€ ๐‘“ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐ด ) = ( ๐‘“ ยทih ( ๐น โ€˜ ๐ด ) )
16 oveq2 โŠข ( ๐‘ฆ = ๐ด โ†’ ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐‘ฆ ) = ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐ด ) )
17 fveq2 โŠข ( ๐‘ฆ = ๐ด โ†’ ( ๐น โ€˜ ๐‘ฆ ) = ( ๐น โ€˜ ๐ด ) )
18 17 oveq2d โŠข ( ๐‘ฆ = ๐ด โ†’ ( ๐‘“ ยทih ( ๐น โ€˜ ๐‘ฆ ) ) = ( ๐‘“ ยทih ( ๐น โ€˜ ๐ด ) ) )
19 16 18 eqeq12d โŠข ( ๐‘ฆ = ๐ด โ†’ ( ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐‘ฆ ) = ( ๐‘“ ยทih ( ๐น โ€˜ ๐‘ฆ ) ) โ†” ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐ด ) = ( ๐‘“ ยทih ( ๐น โ€˜ ๐ด ) ) ) )
20 19 ralbidv โŠข ( ๐‘ฆ = ๐ด โ†’ ( โˆ€ ๐‘“ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐‘ฆ ) = ( ๐‘“ ยทih ( ๐น โ€˜ ๐‘ฆ ) ) โ†” โˆ€ ๐‘“ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐ด ) = ( ๐‘“ ยทih ( ๐น โ€˜ ๐ด ) ) ) )
21 riotaex โŠข ( โ„ฉ ๐‘ค โˆˆ โ„‹ โˆ€ ๐‘ฃ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฃ ) ยทih ๐‘ฆ ) = ( ๐‘ฃ ยทih ๐‘ค ) ) โˆˆ V
22 4 21 eqeltri โŠข ๐ต โˆˆ V
23 5 fvmpt2 โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐ต โˆˆ V ) โ†’ ( ๐น โ€˜ ๐‘ฆ ) = ๐ต )
24 22 23 mpan2 โŠข ( ๐‘ฆ โˆˆ โ„‹ โ†’ ( ๐น โ€˜ ๐‘ฆ ) = ๐ต )
25 fveq2 โŠข ( ๐‘ฃ = ๐‘“ โ†’ ( ๐‘‡ โ€˜ ๐‘ฃ ) = ( ๐‘‡ โ€˜ ๐‘“ ) )
26 25 oveq1d โŠข ( ๐‘ฃ = ๐‘“ โ†’ ( ( ๐‘‡ โ€˜ ๐‘ฃ ) ยทih ๐‘ฆ ) = ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐‘ฆ ) )
27 oveq1 โŠข ( ๐‘ฃ = ๐‘“ โ†’ ( ๐‘ฃ ยทih ๐‘ค ) = ( ๐‘“ ยทih ๐‘ค ) )
28 26 27 eqeq12d โŠข ( ๐‘ฃ = ๐‘“ โ†’ ( ( ( ๐‘‡ โ€˜ ๐‘ฃ ) ยทih ๐‘ฆ ) = ( ๐‘ฃ ยทih ๐‘ค ) โ†” ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐‘ฆ ) = ( ๐‘“ ยทih ๐‘ค ) ) )
29 28 cbvralvw โŠข ( โˆ€ ๐‘ฃ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฃ ) ยทih ๐‘ฆ ) = ( ๐‘ฃ ยทih ๐‘ค ) โ†” โˆ€ ๐‘“ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐‘ฆ ) = ( ๐‘“ ยทih ๐‘ค ) )
30 29 a1i โŠข ( ๐‘ค โˆˆ โ„‹ โ†’ ( โˆ€ ๐‘ฃ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฃ ) ยทih ๐‘ฆ ) = ( ๐‘ฃ ยทih ๐‘ค ) โ†” โˆ€ ๐‘“ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐‘ฆ ) = ( ๐‘“ ยทih ๐‘ค ) ) )
31 1 2 3 cnlnadjlem1 โŠข ( ๐‘“ โˆˆ โ„‹ โ†’ ( ๐บ โ€˜ ๐‘“ ) = ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐‘ฆ ) )
32 31 eqeq1d โŠข ( ๐‘“ โˆˆ โ„‹ โ†’ ( ( ๐บ โ€˜ ๐‘“ ) = ( ๐‘“ ยทih ๐‘ค ) โ†” ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐‘ฆ ) = ( ๐‘“ ยทih ๐‘ค ) ) )
33 32 ralbiia โŠข ( โˆ€ ๐‘“ โˆˆ โ„‹ ( ๐บ โ€˜ ๐‘“ ) = ( ๐‘“ ยทih ๐‘ค ) โ†” โˆ€ ๐‘“ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐‘ฆ ) = ( ๐‘“ ยทih ๐‘ค ) )
34 30 33 bitr4di โŠข ( ๐‘ค โˆˆ โ„‹ โ†’ ( โˆ€ ๐‘ฃ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฃ ) ยทih ๐‘ฆ ) = ( ๐‘ฃ ยทih ๐‘ค ) โ†” โˆ€ ๐‘“ โˆˆ โ„‹ ( ๐บ โ€˜ ๐‘“ ) = ( ๐‘“ ยทih ๐‘ค ) ) )
35 34 riotabiia โŠข ( โ„ฉ ๐‘ค โˆˆ โ„‹ โˆ€ ๐‘ฃ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฃ ) ยทih ๐‘ฆ ) = ( ๐‘ฃ ยทih ๐‘ค ) ) = ( โ„ฉ ๐‘ค โˆˆ โ„‹ โˆ€ ๐‘“ โˆˆ โ„‹ ( ๐บ โ€˜ ๐‘“ ) = ( ๐‘“ ยทih ๐‘ค ) )
36 4 35 eqtri โŠข ๐ต = ( โ„ฉ ๐‘ค โˆˆ โ„‹ โˆ€ ๐‘“ โˆˆ โ„‹ ( ๐บ โ€˜ ๐‘“ ) = ( ๐‘“ ยทih ๐‘ค ) )
37 1 2 3 cnlnadjlem2 โŠข ( ๐‘ฆ โˆˆ โ„‹ โ†’ ( ๐บ โˆˆ LinFn โˆง ๐บ โˆˆ ContFn ) )
38 elin โŠข ( ๐บ โˆˆ ( LinFn โˆฉ ContFn ) โ†” ( ๐บ โˆˆ LinFn โˆง ๐บ โˆˆ ContFn ) )
39 37 38 sylibr โŠข ( ๐‘ฆ โˆˆ โ„‹ โ†’ ๐บ โˆˆ ( LinFn โˆฉ ContFn ) )
40 riesz4 โŠข ( ๐บ โˆˆ ( LinFn โˆฉ ContFn ) โ†’ โˆƒ! ๐‘ค โˆˆ โ„‹ โˆ€ ๐‘“ โˆˆ โ„‹ ( ๐บ โ€˜ ๐‘“ ) = ( ๐‘“ ยทih ๐‘ค ) )
41 riotacl2 โŠข ( โˆƒ! ๐‘ค โˆˆ โ„‹ โˆ€ ๐‘“ โˆˆ โ„‹ ( ๐บ โ€˜ ๐‘“ ) = ( ๐‘“ ยทih ๐‘ค ) โ†’ ( โ„ฉ ๐‘ค โˆˆ โ„‹ โˆ€ ๐‘“ โˆˆ โ„‹ ( ๐บ โ€˜ ๐‘“ ) = ( ๐‘“ ยทih ๐‘ค ) ) โˆˆ { ๐‘ค โˆˆ โ„‹ โˆฃ โˆ€ ๐‘“ โˆˆ โ„‹ ( ๐บ โ€˜ ๐‘“ ) = ( ๐‘“ ยทih ๐‘ค ) } )
42 39 40 41 3syl โŠข ( ๐‘ฆ โˆˆ โ„‹ โ†’ ( โ„ฉ ๐‘ค โˆˆ โ„‹ โˆ€ ๐‘“ โˆˆ โ„‹ ( ๐บ โ€˜ ๐‘“ ) = ( ๐‘“ ยทih ๐‘ค ) ) โˆˆ { ๐‘ค โˆˆ โ„‹ โˆฃ โˆ€ ๐‘“ โˆˆ โ„‹ ( ๐บ โ€˜ ๐‘“ ) = ( ๐‘“ ยทih ๐‘ค ) } )
43 36 42 eqeltrid โŠข ( ๐‘ฆ โˆˆ โ„‹ โ†’ ๐ต โˆˆ { ๐‘ค โˆˆ โ„‹ โˆฃ โˆ€ ๐‘“ โˆˆ โ„‹ ( ๐บ โ€˜ ๐‘“ ) = ( ๐‘“ ยทih ๐‘ค ) } )
44 24 43 eqeltrd โŠข ( ๐‘ฆ โˆˆ โ„‹ โ†’ ( ๐น โ€˜ ๐‘ฆ ) โˆˆ { ๐‘ค โˆˆ โ„‹ โˆฃ โˆ€ ๐‘“ โˆˆ โ„‹ ( ๐บ โ€˜ ๐‘“ ) = ( ๐‘“ ยทih ๐‘ค ) } )
45 oveq2 โŠข ( ๐‘ค = ( ๐น โ€˜ ๐‘ฆ ) โ†’ ( ๐‘“ ยทih ๐‘ค ) = ( ๐‘“ ยทih ( ๐น โ€˜ ๐‘ฆ ) ) )
46 45 eqeq2d โŠข ( ๐‘ค = ( ๐น โ€˜ ๐‘ฆ ) โ†’ ( ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐‘ฆ ) = ( ๐‘“ ยทih ๐‘ค ) โ†” ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐‘ฆ ) = ( ๐‘“ ยทih ( ๐น โ€˜ ๐‘ฆ ) ) ) )
47 46 ralbidv โŠข ( ๐‘ค = ( ๐น โ€˜ ๐‘ฆ ) โ†’ ( โˆ€ ๐‘“ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐‘ฆ ) = ( ๐‘“ ยทih ๐‘ค ) โ†” โˆ€ ๐‘“ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐‘ฆ ) = ( ๐‘“ ยทih ( ๐น โ€˜ ๐‘ฆ ) ) ) )
48 33 47 bitrid โŠข ( ๐‘ค = ( ๐น โ€˜ ๐‘ฆ ) โ†’ ( โˆ€ ๐‘“ โˆˆ โ„‹ ( ๐บ โ€˜ ๐‘“ ) = ( ๐‘“ ยทih ๐‘ค ) โ†” โˆ€ ๐‘“ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐‘ฆ ) = ( ๐‘“ ยทih ( ๐น โ€˜ ๐‘ฆ ) ) ) )
49 48 elrab โŠข ( ( ๐น โ€˜ ๐‘ฆ ) โˆˆ { ๐‘ค โˆˆ โ„‹ โˆฃ โˆ€ ๐‘“ โˆˆ โ„‹ ( ๐บ โ€˜ ๐‘“ ) = ( ๐‘“ ยทih ๐‘ค ) } โ†” ( ( ๐น โ€˜ ๐‘ฆ ) โˆˆ โ„‹ โˆง โˆ€ ๐‘“ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐‘ฆ ) = ( ๐‘“ ยทih ( ๐น โ€˜ ๐‘ฆ ) ) ) )
50 49 simprbi โŠข ( ( ๐น โ€˜ ๐‘ฆ ) โˆˆ { ๐‘ค โˆˆ โ„‹ โˆฃ โˆ€ ๐‘“ โˆˆ โ„‹ ( ๐บ โ€˜ ๐‘“ ) = ( ๐‘“ ยทih ๐‘ค ) } โ†’ โˆ€ ๐‘“ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐‘ฆ ) = ( ๐‘“ ยทih ( ๐น โ€˜ ๐‘ฆ ) ) )
51 44 50 syl โŠข ( ๐‘ฆ โˆˆ โ„‹ โ†’ โˆ€ ๐‘“ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐‘ฆ ) = ( ๐‘“ ยทih ( ๐น โ€˜ ๐‘ฆ ) ) )
52 6 15 20 51 vtoclgaf โŠข ( ๐ด โˆˆ โ„‹ โ†’ โˆ€ ๐‘“ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐ด ) = ( ๐‘“ ยทih ( ๐น โ€˜ ๐ด ) ) )
53 fveq2 โŠข ( ๐‘“ = ๐ถ โ†’ ( ๐‘‡ โ€˜ ๐‘“ ) = ( ๐‘‡ โ€˜ ๐ถ ) )
54 53 oveq1d โŠข ( ๐‘“ = ๐ถ โ†’ ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐ด ) = ( ( ๐‘‡ โ€˜ ๐ถ ) ยทih ๐ด ) )
55 oveq1 โŠข ( ๐‘“ = ๐ถ โ†’ ( ๐‘“ ยทih ( ๐น โ€˜ ๐ด ) ) = ( ๐ถ ยทih ( ๐น โ€˜ ๐ด ) ) )
56 54 55 eqeq12d โŠข ( ๐‘“ = ๐ถ โ†’ ( ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐ด ) = ( ๐‘“ ยทih ( ๐น โ€˜ ๐ด ) ) โ†” ( ( ๐‘‡ โ€˜ ๐ถ ) ยทih ๐ด ) = ( ๐ถ ยทih ( ๐น โ€˜ ๐ด ) ) ) )
57 56 rspccva โŠข ( ( โˆ€ ๐‘“ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘“ ) ยทih ๐ด ) = ( ๐‘“ ยทih ( ๐น โ€˜ ๐ด ) ) โˆง ๐ถ โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ๐ถ ) ยทih ๐ด ) = ( ๐ถ ยทih ( ๐น โ€˜ ๐ด ) ) )
58 52 57 sylan โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ถ โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ๐ถ ) ยทih ๐ด ) = ( ๐ถ ยทih ( ๐น โ€˜ ๐ด ) ) )