Metamath Proof Explorer


Theorem counop

Description: The composition of two unitary operators is unitary. (Contributed by NM, 22-Jan-2006) (New usage is discouraged.)

Ref Expression
Assertion counop SUniOpTUniOpSTUniOp

Proof

Step Hyp Ref Expression
1 unopf1o SUniOpS:1-1 onto
2 unopf1o TUniOpT:1-1 onto
3 f1oco S:1-1 ontoT:1-1 ontoST:1-1 onto
4 1 2 3 syl2an SUniOpTUniOpST:1-1 onto
5 f1ofo ST:1-1 ontoST:onto
6 4 5 syl SUniOpTUniOpST:onto
7 f1of T:1-1 ontoT:
8 2 7 syl TUniOpT:
9 8 adantl SUniOpTUniOpT:
10 simpl xyx
11 fvco3 T:xSTx=STx
12 9 10 11 syl2an SUniOpTUniOpxySTx=STx
13 simpr xyy
14 fvco3 T:ySTy=STy
15 9 13 14 syl2an SUniOpTUniOpxySTy=STy
16 12 15 oveq12d SUniOpTUniOpxySTxihSTy=STxihSTy
17 ffvelrn T:xTx
18 ffvelrn T:yTy
19 17 18 anim12dan T:xyTxTy
20 8 19 sylan TUniOpxyTxTy
21 unop SUniOpTxTySTxihSTy=TxihTy
22 21 3expb SUniOpTxTySTxihSTy=TxihTy
23 20 22 sylan2 SUniOpTUniOpxySTxihSTy=TxihTy
24 23 anassrs SUniOpTUniOpxySTxihSTy=TxihTy
25 unop TUniOpxyTxihTy=xihy
26 25 3expb TUniOpxyTxihTy=xihy
27 26 adantll SUniOpTUniOpxyTxihTy=xihy
28 16 24 27 3eqtrd SUniOpTUniOpxySTxihSTy=xihy
29 28 ralrimivva SUniOpTUniOpxySTxihSTy=xihy
30 elunop STUniOpST:ontoxySTxihSTy=xihy
31 6 29 30 sylanbrc SUniOpTUniOpSTUniOp