Description: The composition of two unitary operators is unitary. (Contributed by NM, 22-Jan-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | counop | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unopf1o | |
|
2 | unopf1o | |
|
3 | f1oco | |
|
4 | 1 2 3 | syl2an | |
5 | f1ofo | |
|
6 | 4 5 | syl | |
7 | f1of | |
|
8 | 2 7 | syl | |
9 | 8 | adantl | |
10 | simpl | |
|
11 | fvco3 | |
|
12 | 9 10 11 | syl2an | |
13 | simpr | |
|
14 | fvco3 | |
|
15 | 9 13 14 | syl2an | |
16 | 12 15 | oveq12d | |
17 | ffvelrn | |
|
18 | ffvelrn | |
|
19 | 17 18 | anim12dan | |
20 | 8 19 | sylan | |
21 | unop | |
|
22 | 21 | 3expb | |
23 | 20 22 | sylan2 | |
24 | 23 | anassrs | |
25 | unop | |
|
26 | 25 | 3expb | |
27 | 26 | adantll | |
28 | 16 24 27 | 3eqtrd | |
29 | 28 | ralrimivva | |
30 | elunop | |
|
31 | 6 29 30 | sylanbrc | |