Step | Hyp | Ref
| Expression |
1 | | nfcv 2903 |
. . 3
โข
โฒ๐ฆ๐ด |
2 | | nfcv 2903 |
. . . 4
โข
โฒ๐ฆ
โ |
3 | | nfcv 2903 |
. . . . . 6
โข
โฒ๐ฆ๐ |
4 | | nfcv 2903 |
. . . . . 6
โข
โฒ๐ฆ
ยทih |
5 | | cnlnadjlem.5 |
. . . . . . . 8
โข ๐น = (๐ฆ โ โ โฆ ๐ต) |
6 | | nfmpt1 5255 |
. . . . . . . 8
โข
โฒ๐ฆ(๐ฆ โ โ โฆ ๐ต) |
7 | 5, 6 | nfcxfr 2901 |
. . . . . . 7
โข
โฒ๐ฆ๐น |
8 | 7, 1 | nffv 6898 |
. . . . . 6
โข
โฒ๐ฆ(๐นโ๐ด) |
9 | 3, 4, 8 | nfov 7435 |
. . . . 5
โข
โฒ๐ฆ(๐ ยทih (๐นโ๐ด)) |
10 | 9 | nfeq2 2920 |
. . . 4
โข
โฒ๐ฆ((๐โ๐) ยทih ๐ด) = (๐ ยทih (๐นโ๐ด)) |
11 | 2, 10 | nfralw 3308 |
. . 3
โข
โฒ๐ฆโ๐ โ โ ((๐โ๐) ยทih ๐ด) = (๐ ยทih (๐นโ๐ด)) |
12 | | oveq2 7413 |
. . . . 5
โข (๐ฆ = ๐ด โ ((๐โ๐) ยทih ๐ฆ) = ((๐โ๐) ยทih ๐ด)) |
13 | | fveq2 6888 |
. . . . . 6
โข (๐ฆ = ๐ด โ (๐นโ๐ฆ) = (๐นโ๐ด)) |
14 | 13 | oveq2d 7421 |
. . . . 5
โข (๐ฆ = ๐ด โ (๐ ยทih (๐นโ๐ฆ)) = (๐ ยทih (๐นโ๐ด))) |
15 | 12, 14 | eqeq12d 2748 |
. . . 4
โข (๐ฆ = ๐ด โ (((๐โ๐) ยทih ๐ฆ) = (๐ ยทih (๐นโ๐ฆ)) โ ((๐โ๐) ยทih ๐ด) = (๐ ยทih (๐นโ๐ด)))) |
16 | 15 | ralbidv 3177 |
. . 3
โข (๐ฆ = ๐ด โ (โ๐ โ โ ((๐โ๐) ยทih ๐ฆ) = (๐ ยทih (๐นโ๐ฆ)) โ โ๐ โ โ ((๐โ๐) ยทih ๐ด) = (๐ ยทih (๐นโ๐ด)))) |
17 | | cnlnadjlem.4 |
. . . . . . 7
โข ๐ต = (โฉ๐ค โ โ โ๐ฃ โ โ ((๐โ๐ฃ) ยทih ๐ฆ) = (๐ฃ ยทih ๐ค)) |
18 | | riotaex 7365 |
. . . . . . 7
โข
(โฉ๐ค
โ โ โ๐ฃ
โ โ ((๐โ๐ฃ) ยทih ๐ฆ) = (๐ฃ ยทih ๐ค)) โ V |
19 | 17, 18 | eqeltri 2829 |
. . . . . 6
โข ๐ต โ V |
20 | 5 | fvmpt2 7006 |
. . . . . 6
โข ((๐ฆ โ โ โง ๐ต โ V) โ (๐นโ๐ฆ) = ๐ต) |
21 | 19, 20 | mpan2 689 |
. . . . 5
โข (๐ฆ โ โ โ (๐นโ๐ฆ) = ๐ต) |
22 | | fveq2 6888 |
. . . . . . . . . . . . 13
โข (๐ฃ = ๐ โ (๐โ๐ฃ) = (๐โ๐)) |
23 | 22 | oveq1d 7420 |
. . . . . . . . . . . 12
โข (๐ฃ = ๐ โ ((๐โ๐ฃ) ยทih ๐ฆ) = ((๐โ๐) ยทih ๐ฆ)) |
24 | | oveq1 7412 |
. . . . . . . . . . . 12
โข (๐ฃ = ๐ โ (๐ฃ ยทih ๐ค) = (๐ ยทih ๐ค)) |
25 | 23, 24 | eqeq12d 2748 |
. . . . . . . . . . 11
โข (๐ฃ = ๐ โ (((๐โ๐ฃ) ยทih ๐ฆ) = (๐ฃ ยทih ๐ค) โ ((๐โ๐) ยทih ๐ฆ) = (๐ ยทih ๐ค))) |
26 | 25 | cbvralvw 3234 |
. . . . . . . . . 10
โข
(โ๐ฃ โ
โ ((๐โ๐ฃ)
ยทih ๐ฆ) = (๐ฃ ยทih ๐ค) โ โ๐ โ โ ((๐โ๐) ยทih ๐ฆ) = (๐ ยทih ๐ค)) |
27 | 26 | a1i 11 |
. . . . . . . . 9
โข (๐ค โ โ โ
(โ๐ฃ โ โ
((๐โ๐ฃ)
ยทih ๐ฆ) = (๐ฃ ยทih ๐ค) โ โ๐ โ โ ((๐โ๐) ยทih ๐ฆ) = (๐ ยทih ๐ค))) |
28 | | cnlnadjlem.1 |
. . . . . . . . . . . 12
โข ๐ โ LinOp |
29 | | cnlnadjlem.2 |
. . . . . . . . . . . 12
โข ๐ โ ContOp |
30 | | cnlnadjlem.3 |
. . . . . . . . . . . 12
โข ๐บ = (๐ โ โ โฆ ((๐โ๐) ยทih ๐ฆ)) |
31 | 28, 29, 30 | cnlnadjlem1 31307 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐บโ๐) = ((๐โ๐) ยทih ๐ฆ)) |
32 | 31 | eqeq1d 2734 |
. . . . . . . . . 10
โข (๐ โ โ โ ((๐บโ๐) = (๐ ยทih ๐ค) โ ((๐โ๐) ยทih ๐ฆ) = (๐ ยทih ๐ค))) |
33 | 32 | ralbiia 3091 |
. . . . . . . . 9
โข
(โ๐ โ
โ (๐บโ๐) = (๐ ยทih ๐ค) โ โ๐ โ โ ((๐โ๐) ยทih ๐ฆ) = (๐ ยทih ๐ค)) |
34 | 27, 33 | bitr4di 288 |
. . . . . . . 8
โข (๐ค โ โ โ
(โ๐ฃ โ โ
((๐โ๐ฃ)
ยทih ๐ฆ) = (๐ฃ ยทih ๐ค) โ โ๐ โ โ (๐บโ๐) = (๐ ยทih ๐ค))) |
35 | 34 | riotabiia 7382 |
. . . . . . 7
โข
(โฉ๐ค
โ โ โ๐ฃ
โ โ ((๐โ๐ฃ) ยทih ๐ฆ) = (๐ฃ ยทih ๐ค)) = (โฉ๐ค โ โ โ๐ โ โ (๐บโ๐) = (๐ ยทih ๐ค)) |
36 | 17, 35 | eqtri 2760 |
. . . . . 6
โข ๐ต = (โฉ๐ค โ โ โ๐ โ โ (๐บโ๐) = (๐ ยทih ๐ค)) |
37 | 28, 29, 30 | cnlnadjlem2 31308 |
. . . . . . . 8
โข (๐ฆ โ โ โ (๐บ โ LinFn โง ๐บ โ
ContFn)) |
38 | | elin 3963 |
. . . . . . . 8
โข (๐บ โ (LinFn โฉ ContFn)
โ (๐บ โ LinFn
โง ๐บ โ
ContFn)) |
39 | 37, 38 | sylibr 233 |
. . . . . . 7
โข (๐ฆ โ โ โ ๐บ โ (LinFn โฉ
ContFn)) |
40 | | riesz4 31304 |
. . . . . . 7
โข (๐บ โ (LinFn โฉ ContFn)
โ โ!๐ค โ
โ โ๐ โ
โ (๐บโ๐) = (๐ ยทih ๐ค)) |
41 | | riotacl2 7378 |
. . . . . . 7
โข
(โ!๐ค โ
โ โ๐ โ
โ (๐บโ๐) = (๐ ยทih ๐ค) โ (โฉ๐ค โ โ โ๐ โ โ (๐บโ๐) = (๐ ยทih ๐ค)) โ {๐ค โ โ โฃ โ๐ โ โ (๐บโ๐) = (๐ ยทih ๐ค)}) |
42 | 39, 40, 41 | 3syl 18 |
. . . . . 6
โข (๐ฆ โ โ โ
(โฉ๐ค โ
โ โ๐ โ
โ (๐บโ๐) = (๐ ยทih ๐ค)) โ {๐ค โ โ โฃ โ๐ โ โ (๐บโ๐) = (๐ ยทih ๐ค)}) |
43 | 36, 42 | eqeltrid 2837 |
. . . . 5
โข (๐ฆ โ โ โ ๐ต โ {๐ค โ โ โฃ โ๐ โ โ (๐บโ๐) = (๐ ยทih ๐ค)}) |
44 | 21, 43 | eqeltrd 2833 |
. . . 4
โข (๐ฆ โ โ โ (๐นโ๐ฆ) โ {๐ค โ โ โฃ โ๐ โ โ (๐บโ๐) = (๐ ยทih ๐ค)}) |
45 | | oveq2 7413 |
. . . . . . . . 9
โข (๐ค = (๐นโ๐ฆ) โ (๐ ยทih ๐ค) = (๐ ยทih (๐นโ๐ฆ))) |
46 | 45 | eqeq2d 2743 |
. . . . . . . 8
โข (๐ค = (๐นโ๐ฆ) โ (((๐โ๐) ยทih ๐ฆ) = (๐ ยทih ๐ค) โ ((๐โ๐) ยทih ๐ฆ) = (๐ ยทih (๐นโ๐ฆ)))) |
47 | 46 | ralbidv 3177 |
. . . . . . 7
โข (๐ค = (๐นโ๐ฆ) โ (โ๐ โ โ ((๐โ๐) ยทih ๐ฆ) = (๐ ยทih ๐ค) โ โ๐ โ โ ((๐โ๐) ยทih ๐ฆ) = (๐ ยทih (๐นโ๐ฆ)))) |
48 | 33, 47 | bitrid 282 |
. . . . . 6
โข (๐ค = (๐นโ๐ฆ) โ (โ๐ โ โ (๐บโ๐) = (๐ ยทih ๐ค) โ โ๐ โ โ ((๐โ๐) ยทih ๐ฆ) = (๐ ยทih (๐นโ๐ฆ)))) |
49 | 48 | elrab 3682 |
. . . . 5
โข ((๐นโ๐ฆ) โ {๐ค โ โ โฃ โ๐ โ โ (๐บโ๐) = (๐ ยทih ๐ค)} โ ((๐นโ๐ฆ) โ โ โง โ๐ โ โ ((๐โ๐) ยทih ๐ฆ) = (๐ ยทih (๐นโ๐ฆ)))) |
50 | 49 | simprbi 497 |
. . . 4
โข ((๐นโ๐ฆ) โ {๐ค โ โ โฃ โ๐ โ โ (๐บโ๐) = (๐ ยทih ๐ค)} โ โ๐ โ โ ((๐โ๐) ยทih ๐ฆ) = (๐ ยทih (๐นโ๐ฆ))) |
51 | 44, 50 | syl 17 |
. . 3
โข (๐ฆ โ โ โ
โ๐ โ โ
((๐โ๐)
ยทih ๐ฆ) = (๐ ยทih (๐นโ๐ฆ))) |
52 | 1, 11, 16, 51 | vtoclgaf 3564 |
. 2
โข (๐ด โ โ โ
โ๐ โ โ
((๐โ๐)
ยทih ๐ด) = (๐ ยทih (๐นโ๐ด))) |
53 | | fveq2 6888 |
. . . . 5
โข (๐ = ๐ถ โ (๐โ๐) = (๐โ๐ถ)) |
54 | 53 | oveq1d 7420 |
. . . 4
โข (๐ = ๐ถ โ ((๐โ๐) ยทih ๐ด) = ((๐โ๐ถ) ยทih ๐ด)) |
55 | | oveq1 7412 |
. . . 4
โข (๐ = ๐ถ โ (๐ ยทih (๐นโ๐ด)) = (๐ถ ยทih (๐นโ๐ด))) |
56 | 54, 55 | eqeq12d 2748 |
. . 3
โข (๐ = ๐ถ โ (((๐โ๐) ยทih ๐ด) = (๐ ยทih (๐นโ๐ด)) โ ((๐โ๐ถ) ยทih ๐ด) = (๐ถ ยทih (๐นโ๐ด)))) |
57 | 56 | rspccva 3611 |
. 2
โข
((โ๐ โ
โ ((๐โ๐)
ยทih ๐ด) = (๐ ยทih (๐นโ๐ด)) โง ๐ถ โ โ) โ ((๐โ๐ถ) ยทih ๐ด) = (๐ถ ยทih (๐นโ๐ด))) |
58 | 52, 57 | sylan 580 |
1
โข ((๐ด โ โ โง ๐ถ โ โ) โ ((๐โ๐ถ) ยทih ๐ด) = (๐ถ ยทih (๐นโ๐ด))) |