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 ( ๐น โ ๐ด ) ) ) |