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 
|- ( ( S e. UniOp /\ T e. UniOp ) -> ( S o. T ) e. UniOp )

Proof

Step Hyp Ref Expression
1 unopf1o 
 |-  ( S e. UniOp -> S : ~H -1-1-onto-> ~H )
2 unopf1o 
 |-  ( T e. UniOp -> T : ~H -1-1-onto-> ~H )
3 f1oco 
 |-  ( ( S : ~H -1-1-onto-> ~H /\ T : ~H -1-1-onto-> ~H ) -> ( S o. T ) : ~H -1-1-onto-> ~H )
4 1 2 3 syl2an 
 |-  ( ( S e. UniOp /\ T e. UniOp ) -> ( S o. T ) : ~H -1-1-onto-> ~H )
5 f1ofo 
 |-  ( ( S o. T ) : ~H -1-1-onto-> ~H -> ( S o. T ) : ~H -onto-> ~H )
6 4 5 syl 
 |-  ( ( S e. UniOp /\ T e. UniOp ) -> ( S o. T ) : ~H -onto-> ~H )
7 f1of 
 |-  ( T : ~H -1-1-onto-> ~H -> T : ~H --> ~H )
8 2 7 syl 
 |-  ( T e. UniOp -> T : ~H --> ~H )
9 8 adantl 
 |-  ( ( S e. UniOp /\ T e. UniOp ) -> T : ~H --> ~H )
10 simpl 
 |-  ( ( x e. ~H /\ y e. ~H ) -> x e. ~H )
11 fvco3 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( ( S o. T ) ` x ) = ( S ` ( T ` x ) ) )
12 9 10 11 syl2an 
 |-  ( ( ( S e. UniOp /\ T e. UniOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( S o. T ) ` x ) = ( S ` ( T ` x ) ) )
13 simpr 
 |-  ( ( x e. ~H /\ y e. ~H ) -> y e. ~H )
14 fvco3 
 |-  ( ( T : ~H --> ~H /\ y e. ~H ) -> ( ( S o. T ) ` y ) = ( S ` ( T ` y ) ) )
15 9 13 14 syl2an 
 |-  ( ( ( S e. UniOp /\ T e. UniOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( S o. T ) ` y ) = ( S ` ( T ` y ) ) )
16 12 15 oveq12d 
 |-  ( ( ( S e. UniOp /\ T e. UniOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( S o. T ) ` x ) .ih ( ( S o. T ) ` y ) ) = ( ( S ` ( T ` x ) ) .ih ( S ` ( T ` y ) ) ) )
17 ffvelcdm 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( T ` x ) e. ~H )
18 ffvelcdm 
 |-  ( ( T : ~H --> ~H /\ y e. ~H ) -> ( T ` y ) e. ~H )
19 17 18 anim12dan 
 |-  ( ( T : ~H --> ~H /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( T ` x ) e. ~H /\ ( T ` y ) e. ~H ) )
20 8 19 sylan 
 |-  ( ( T e. UniOp /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( T ` x ) e. ~H /\ ( T ` y ) e. ~H ) )
21 unop 
 |-  ( ( S e. UniOp /\ ( T ` x ) e. ~H /\ ( T ` y ) e. ~H ) -> ( ( S ` ( T ` x ) ) .ih ( S ` ( T ` y ) ) ) = ( ( T ` x ) .ih ( T ` y ) ) )
22 21 3expb 
 |-  ( ( S e. UniOp /\ ( ( T ` x ) e. ~H /\ ( T ` y ) e. ~H ) ) -> ( ( S ` ( T ` x ) ) .ih ( S ` ( T ` y ) ) ) = ( ( T ` x ) .ih ( T ` y ) ) )
23 20 22 sylan2 
 |-  ( ( S e. UniOp /\ ( T e. UniOp /\ ( x e. ~H /\ y e. ~H ) ) ) -> ( ( S ` ( T ` x ) ) .ih ( S ` ( T ` y ) ) ) = ( ( T ` x ) .ih ( T ` y ) ) )
24 23 anassrs 
 |-  ( ( ( S e. UniOp /\ T e. UniOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( S ` ( T ` x ) ) .ih ( S ` ( T ` y ) ) ) = ( ( T ` x ) .ih ( T ` y ) ) )
25 unop 
 |-  ( ( T e. UniOp /\ x e. ~H /\ y e. ~H ) -> ( ( T ` x ) .ih ( T ` y ) ) = ( x .ih y ) )
26 25 3expb 
 |-  ( ( T e. UniOp /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( T ` x ) .ih ( T ` y ) ) = ( x .ih y ) )
27 26 adantll 
 |-  ( ( ( S e. UniOp /\ T e. UniOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( T ` x ) .ih ( T ` y ) ) = ( x .ih y ) )
28 16 24 27 3eqtrd 
 |-  ( ( ( S e. UniOp /\ T e. UniOp ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( S o. T ) ` x ) .ih ( ( S o. T ) ` y ) ) = ( x .ih y ) )
29 28 ralrimivva 
 |-  ( ( S e. UniOp /\ T e. UniOp ) -> A. x e. ~H A. y e. ~H ( ( ( S o. T ) ` x ) .ih ( ( S o. T ) ` y ) ) = ( x .ih y ) )
30 elunop 
 |-  ( ( S o. T ) e. UniOp <-> ( ( S o. T ) : ~H -onto-> ~H /\ A. x e. ~H A. y e. ~H ( ( ( S o. T ) ` x ) .ih ( ( S o. T ) ` y ) ) = ( x .ih y ) ) )
31 6 29 30 sylanbrc 
 |-  ( ( S e. UniOp /\ T e. UniOp ) -> ( S o. T ) e. UniOp )