Step | Hyp | Ref
| Expression |
1 | | bdopadj 31066 |
. . . 4
โข (๐ โ BndLinOp โ ๐ โ dom
adjโ) |
2 | | adjval 30874 |
. . . 4
โข (๐ โ dom
adjโ โ (adjโโ๐) = (โฉ๐ก โ ( โ โm
โ)โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ))) |
3 | 1, 2 | syl 17 |
. . 3
โข (๐ โ BndLinOp โ
(adjโโ๐) = (โฉ๐ก โ ( โ โm
โ)โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ))) |
4 | | cnlnadj 31063 |
. . . . . 6
โข (๐ โ (LinOp โฉ ContOp)
โ โ๐ก โ
(LinOp โฉ ContOp)โ๐ฅ โ โ โ๐ฆ โ โ ((๐โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih (๐กโ๐ฆ))) |
5 | | lncnopbd 31021 |
. . . . . 6
โข (๐ โ (LinOp โฉ ContOp)
โ ๐ โ
BndLinOp) |
6 | | lncnbd 31022 |
. . . . . . 7
โข (LinOp
โฉ ContOp) = BndLinOp |
7 | 6 | rexeqi 3315 |
. . . . . 6
โข
(โ๐ก โ
(LinOp โฉ ContOp)โ๐ฅ โ โ โ๐ฆ โ โ ((๐โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih (๐กโ๐ฆ)) โ โ๐ก โ BndLinOp โ๐ฅ โ โ โ๐ฆ โ โ ((๐โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih (๐กโ๐ฆ))) |
8 | 4, 5, 7 | 3imtr3i 291 |
. . . . 5
โข (๐ โ BndLinOp โ
โ๐ก โ BndLinOp
โ๐ฅ โ โ
โ๐ฆ โ โ
((๐โ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐กโ๐ฆ))) |
9 | | bdopf 30846 |
. . . . . . . 8
โข (๐ โ BndLinOp โ ๐: โโถ
โ) |
10 | | bdopf 30846 |
. . . . . . . 8
โข (๐ก โ BndLinOp โ ๐ก: โโถ
โ) |
11 | | adjsym 30817 |
. . . . . . . 8
โข ((๐: โโถ โ โง
๐ก: โโถ โ)
โ (โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐กโ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ))) |
12 | 9, 10, 11 | syl2an 597 |
. . . . . . 7
โข ((๐ โ BndLinOp โง ๐ก โ BndLinOp) โ
(โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐กโ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ))) |
13 | | eqcom 2744 |
. . . . . . . 8
โข (((๐โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih (๐กโ๐ฆ)) โ (๐ฅ ยทih (๐กโ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ)) |
14 | 13 | 2ralbii 3128 |
. . . . . . 7
โข
(โ๐ฅ โ
โ โ๐ฆ โ
โ ((๐โ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐กโ๐ฆ)) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐กโ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ)) |
15 | 12, 14 | bitr4di 289 |
. . . . . 6
โข ((๐ โ BndLinOp โง ๐ก โ BndLinOp) โ
(โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ) โ โ๐ฅ โ โ โ๐ฆ โ โ ((๐โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih (๐กโ๐ฆ)))) |
16 | 15 | rexbidva 3174 |
. . . . 5
โข (๐ โ BndLinOp โ
(โ๐ก โ BndLinOp
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ) โ โ๐ก โ BndLinOp โ๐ฅ โ โ โ๐ฆ โ โ ((๐โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih (๐กโ๐ฆ)))) |
17 | 8, 16 | mpbird 257 |
. . . 4
โข (๐ โ BndLinOp โ
โ๐ก โ BndLinOp
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)) |
18 | | adjeu 30873 |
. . . . . 6
โข (๐: โโถ โ โ
(๐ โ dom
adjโ โ โ!๐ก โ ( โ โm
โ)โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ))) |
19 | 9, 18 | syl 17 |
. . . . 5
โข (๐ โ BndLinOp โ (๐ โ dom
adjโ โ โ!๐ก โ ( โ โm
โ)โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ))) |
20 | 1, 19 | mpbid 231 |
. . . 4
โข (๐ โ BndLinOp โ
โ!๐ก โ ( โ
โm โ)โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)) |
21 | | ax-hilex 29983 |
. . . . . . . 8
โข โ
โ V |
22 | 21, 21 | elmap 8816 |
. . . . . . 7
โข (๐ก โ ( โ
โm โ) โ ๐ก: โโถ โ) |
23 | 10, 22 | sylibr 233 |
. . . . . 6
โข (๐ก โ BndLinOp โ ๐ก โ ( โ
โm โ)) |
24 | 23 | ssriv 3953 |
. . . . 5
โข BndLinOp
โ ( โ โm โ) |
25 | | id 22 |
. . . . . 6
โข
(โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)) |
26 | 25 | rgenw 3069 |
. . . . 5
โข
โ๐ก โ
BndLinOp (โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)) |
27 | | riotass2 7349 |
. . . . 5
โข
(((BndLinOp โ ( โ โm โ) โง
โ๐ก โ BndLinOp
(โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ))) โง (โ๐ก โ BndLinOp โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ) โง โ!๐ก โ ( โ
โm โ)โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ))) โ (โฉ๐ก โ BndLinOp โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)) = (โฉ๐ก โ ( โ
โm โ)โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ))) |
28 | 24, 26, 27 | mpanl12 701 |
. . . 4
โข
((โ๐ก โ
BndLinOp โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ) โง โ!๐ก โ ( โ
โm โ)โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)) โ (โฉ๐ก โ BndLinOp โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)) = (โฉ๐ก โ ( โ
โm โ)โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ))) |
29 | 17, 20, 28 | syl2anc 585 |
. . 3
โข (๐ โ BndLinOp โ
(โฉ๐ก โ
BndLinOp โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)) = (โฉ๐ก โ ( โ
โm โ)โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ))) |
30 | 3, 29 | eqtr4d 2780 |
. 2
โข (๐ โ BndLinOp โ
(adjโโ๐) = (โฉ๐ก โ BndLinOp โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ))) |
31 | 24 | a1i 11 |
. . . 4
โข (๐ โ BndLinOp โ BndLinOp
โ ( โ โm โ)) |
32 | | reuss 4281 |
. . . 4
โข
((BndLinOp โ ( โ โm โ) โง
โ๐ก โ BndLinOp
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ) โง โ!๐ก โ ( โ
โm โ)โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)) โ โ!๐ก โ BndLinOp โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)) |
33 | 31, 17, 20, 32 | syl3anc 1372 |
. . 3
โข (๐ โ BndLinOp โ
โ!๐ก โ BndLinOp
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)) |
34 | | riotacl 7336 |
. . 3
โข
(โ!๐ก โ
BndLinOp โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ) โ (โฉ๐ก โ BndLinOp โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)) โ
BndLinOp) |
35 | 33, 34 | syl 17 |
. 2
โข (๐ โ BndLinOp โ
(โฉ๐ก โ
BndLinOp โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)) โ
BndLinOp) |
36 | 30, 35 | eqeltrd 2838 |
1
โข (๐ โ BndLinOp โ
(adjโโ๐) โ BndLinOp) |