Step | Hyp | Ref
| Expression |
1 | | nmoptri.2 |
. . . . . . . 8
โข ๐ โ
BndLinOp |
2 | | adjbdln 31336 |
. . . . . . . 8
โข (๐ โ BndLinOp โ
(adjโโ๐) โ BndLinOp) |
3 | | bdopf 31115 |
. . . . . . . 8
โข
((adjโโ๐) โ BndLinOp โ
(adjโโ๐): โโถ โ) |
4 | 1, 2, 3 | mp2b 10 |
. . . . . . 7
โข
(adjโโ๐): โโถ โ |
5 | | nmoptri.1 |
. . . . . . . 8
โข ๐ โ
BndLinOp |
6 | | adjbdln 31336 |
. . . . . . . 8
โข (๐ โ BndLinOp โ
(adjโโ๐) โ BndLinOp) |
7 | | bdopf 31115 |
. . . . . . . 8
โข
((adjโโ๐) โ BndLinOp โ
(adjโโ๐): โโถ โ) |
8 | 5, 6, 7 | mp2b 10 |
. . . . . . 7
โข
(adjโโ๐): โโถ โ |
9 | 4, 8 | hocoi 31017 |
. . . . . 6
โข (๐ฆ โ โ โ
(((adjโโ๐) โ
(adjโโ๐))โ๐ฆ) = ((adjโโ๐)โ((adjโโ๐)โ๐ฆ))) |
10 | 9 | oveq2d 7425 |
. . . . 5
โข (๐ฆ โ โ โ (๐ฅ
ยทih (((adjโโ๐) โ
(adjโโ๐))โ๐ฆ)) = (๐ฅ ยทih
((adjโโ๐)โ((adjโโ๐)โ๐ฆ)))) |
11 | 10 | adantl 483 |
. . . 4
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ
ยทih (((adjโโ๐) โ
(adjโโ๐))โ๐ฆ)) = (๐ฅ ยทih
((adjโโ๐)โ((adjโโ๐)โ๐ฆ)))) |
12 | | bdopf 31115 |
. . . . . . . . 9
โข (๐ โ BndLinOp โ ๐: โโถ
โ) |
13 | 5, 12 | ax-mp 5 |
. . . . . . . 8
โข ๐: โโถ
โ |
14 | | bdopf 31115 |
. . . . . . . . 9
โข (๐ โ BndLinOp โ ๐: โโถ
โ) |
15 | 1, 14 | ax-mp 5 |
. . . . . . . 8
โข ๐: โโถ
โ |
16 | 13, 15 | hocoi 31017 |
. . . . . . 7
โข (๐ฅ โ โ โ ((๐ โ ๐)โ๐ฅ) = (๐โ(๐โ๐ฅ))) |
17 | 16 | oveq1d 7424 |
. . . . . 6
โข (๐ฅ โ โ โ (((๐ โ ๐)โ๐ฅ) ยทih ๐ฆ) = ((๐โ(๐โ๐ฅ)) ยทih ๐ฆ)) |
18 | 17 | adantr 482 |
. . . . 5
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (((๐ โ ๐)โ๐ฅ) ยทih ๐ฆ) = ((๐โ(๐โ๐ฅ)) ยทih ๐ฆ)) |
19 | 15 | ffvelcdmi 7086 |
. . . . . 6
โข (๐ฅ โ โ โ (๐โ๐ฅ) โ โ) |
20 | | bdopadj 31335 |
. . . . . . . 8
โข (๐ โ BndLinOp โ ๐ โ dom
adjโ) |
21 | 5, 20 | ax-mp 5 |
. . . . . . 7
โข ๐ โ dom
adjโ |
22 | | adj2 31187 |
. . . . . . 7
โข ((๐ โ dom
adjโ โง (๐โ๐ฅ) โ โ โง ๐ฆ โ โ) โ ((๐โ(๐โ๐ฅ)) ยทih ๐ฆ) = ((๐โ๐ฅ) ยทih
((adjโโ๐)โ๐ฆ))) |
23 | 21, 22 | mp3an1 1449 |
. . . . . 6
โข (((๐โ๐ฅ) โ โ โง ๐ฆ โ โ) โ ((๐โ(๐โ๐ฅ)) ยทih ๐ฆ) = ((๐โ๐ฅ) ยทih
((adjโโ๐)โ๐ฆ))) |
24 | 19, 23 | sylan 581 |
. . . . 5
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐โ(๐โ๐ฅ)) ยทih ๐ฆ) = ((๐โ๐ฅ) ยทih
((adjโโ๐)โ๐ฆ))) |
25 | 8 | ffvelcdmi 7086 |
. . . . . 6
โข (๐ฆ โ โ โ
((adjโโ๐)โ๐ฆ) โ โ) |
26 | | bdopadj 31335 |
. . . . . . . 8
โข (๐ โ BndLinOp โ ๐ โ dom
adjโ) |
27 | 1, 26 | ax-mp 5 |
. . . . . . 7
โข ๐ โ dom
adjโ |
28 | | adj2 31187 |
. . . . . . 7
โข ((๐ โ dom
adjโ โง ๐ฅ โ โ โง
((adjโโ๐)โ๐ฆ) โ โ) โ ((๐โ๐ฅ) ยทih
((adjโโ๐)โ๐ฆ)) = (๐ฅ ยทih
((adjโโ๐)โ((adjโโ๐)โ๐ฆ)))) |
29 | 27, 28 | mp3an1 1449 |
. . . . . 6
โข ((๐ฅ โ โ โง
((adjโโ๐)โ๐ฆ) โ โ) โ ((๐โ๐ฅ) ยทih
((adjโโ๐)โ๐ฆ)) = (๐ฅ ยทih
((adjโโ๐)โ((adjโโ๐)โ๐ฆ)))) |
30 | 25, 29 | sylan2 594 |
. . . . 5
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐โ๐ฅ) ยทih
((adjโโ๐)โ๐ฆ)) = (๐ฅ ยทih
((adjโโ๐)โ((adjโโ๐)โ๐ฆ)))) |
31 | 18, 24, 30 | 3eqtrd 2777 |
. . . 4
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (((๐ โ ๐)โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
((adjโโ๐)โ((adjโโ๐)โ๐ฆ)))) |
32 | 5, 1 | bdopcoi 31351 |
. . . . . 6
โข (๐ โ ๐) โ BndLinOp |
33 | | bdopadj 31335 |
. . . . . 6
โข ((๐ โ ๐) โ BndLinOp โ (๐ โ ๐) โ dom
adjโ) |
34 | 32, 33 | ax-mp 5 |
. . . . 5
โข (๐ โ ๐) โ dom
adjโ |
35 | | adj2 31187 |
. . . . 5
โข (((๐ โ ๐) โ dom adjโ โง
๐ฅ โ โ โง
๐ฆ โ โ) โ
(((๐ โ ๐)โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
((adjโโ(๐ โ ๐))โ๐ฆ))) |
36 | 34, 35 | mp3an1 1449 |
. . . 4
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (((๐ โ ๐)โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
((adjโโ(๐ โ ๐))โ๐ฆ))) |
37 | 11, 31, 36 | 3eqtr2rd 2780 |
. . 3
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ
ยทih ((adjโโ(๐ โ ๐))โ๐ฆ)) = (๐ฅ ยทih
(((adjโโ๐) โ
(adjโโ๐))โ๐ฆ))) |
38 | 37 | rgen2 3198 |
. 2
โข
โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih ((adjโโ(๐ โ ๐))โ๐ฆ)) = (๐ฅ ยทih
(((adjโโ๐) โ
(adjโโ๐))โ๐ฆ)) |
39 | | adjbdln 31336 |
. . . 4
โข ((๐ โ ๐) โ BndLinOp โ
(adjโโ(๐ โ ๐)) โ BndLinOp) |
40 | | bdopf 31115 |
. . . 4
โข
((adjโโ(๐ โ ๐)) โ BndLinOp โ
(adjโโ(๐ โ ๐)): โโถ
โ) |
41 | 32, 39, 40 | mp2b 10 |
. . 3
โข
(adjโโ(๐ โ ๐)): โโถ โ |
42 | 4, 8 | hocofi 31019 |
. . 3
โข
((adjโโ๐) โ
(adjโโ๐)): โโถ โ |
43 | | hoeq2 31084 |
. . 3
โข
(((adjโโ(๐ โ ๐)): โโถ โ โง
((adjโโ๐) โ
(adjโโ๐)): โโถ โ) โ
(โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih ((adjโโ(๐ โ ๐))โ๐ฆ)) = (๐ฅ ยทih
(((adjโโ๐) โ
(adjโโ๐))โ๐ฆ)) โ
(adjโโ(๐ โ ๐)) = ((adjโโ๐) โ
(adjโโ๐)))) |
44 | 41, 42, 43 | mp2an 691 |
. 2
โข
(โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih ((adjโโ(๐ โ ๐))โ๐ฆ)) = (๐ฅ ยทih
(((adjโโ๐) โ
(adjโโ๐))โ๐ฆ)) โ
(adjโโ(๐ โ ๐)) = ((adjโโ๐) โ
(adjโโ๐))) |
45 | 38, 44 | mpbi 229 |
1
โข
(adjโโ(๐ โ ๐)) = ((adjโโ๐) โ
(adjโโ๐)) |