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 ( ( 𝑆 ∈ UniOp ∧ 𝑇 ∈ UniOp ) → ( 𝑆 ∘ 𝑇 ) ∈ UniOp )

Proof

Step Hyp Ref Expression
1 unopf1o ⊢ ( 𝑆 ∈ UniOp → 𝑆 : ℋ –1-1-onto→ ℋ )
2 unopf1o ⊢ ( 𝑇 ∈ UniOp → 𝑇 : ℋ –1-1-onto→ ℋ )
3 f1oco ⊢ ( ( 𝑆 : ℋ –1-1-onto→ ℋ ∧ 𝑇 : ℋ –1-1-onto→ ℋ ) → ( 𝑆 ∘ 𝑇 ) : ℋ –1-1-onto→ ℋ )
4 1 2 3 syl2an ⊢ ( ( 𝑆 ∈ UniOp ∧ 𝑇 ∈ UniOp ) → ( 𝑆 ∘ 𝑇 ) : ℋ –1-1-onto→ ℋ )
5 f1ofo ⊢ ( ( 𝑆 ∘ 𝑇 ) : ℋ –1-1-onto→ ℋ → ( 𝑆 ∘ 𝑇 ) : ℋ –onto→ ℋ )
6 4 5 syl ⊢ ( ( 𝑆 ∈ UniOp ∧ 𝑇 ∈ UniOp ) → ( 𝑆 ∘ 𝑇 ) : ℋ –onto→ ℋ )
7 f1of ⊢ ( 𝑇 : ℋ –1-1-onto→ ℋ → 𝑇 : ℋ ⟶ ℋ )
8 2 7 syl ⊢ ( 𝑇 ∈ UniOp → 𝑇 : ℋ ⟶ ℋ )
9 8 adantl ⊢ ( ( 𝑆 ∈ UniOp ∧ 𝑇 ∈ UniOp ) → 𝑇 : ℋ ⟶ ℋ )
10 simpl ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → 𝑥 ∈ ℋ )
11 fvco3 ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝑇 ‘ 𝑥 ) ) )
12 9 10 11 syl2an ⊢ ( ( ( 𝑆 ∈ UniOp ∧ 𝑇 ∈ UniOp ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝑇 ‘ 𝑥 ) ) )
13 simpr ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → 𝑦 ∈ ℋ )
14 fvco3 ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑦 ) = ( 𝑆 ‘ ( 𝑇 ‘ 𝑦 ) ) )
15 9 13 14 syl2an ⊢ ( ( ( 𝑆 ∈ UniOp ∧ 𝑇 ∈ UniOp ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑦 ) = ( 𝑆 ‘ ( 𝑇 ‘ 𝑦 ) ) )
16 12 15 oveq12d ⊢ ( ( ( 𝑆 ∈ UniOp ∧ 𝑇 ∈ UniOp ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ·ih ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑦 ) ) = ( ( 𝑆 ‘ ( 𝑇 ‘ 𝑥 ) ) ·ih ( 𝑆 ‘ ( 𝑇 ‘ 𝑦 ) ) ) )
17 ffvelrn ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
18 ffvelrn ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑇 ‘ 𝑦 ) ∈ ℋ )
19 17 18 anim12dan ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑇 ‘ 𝑥 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑦 ) ∈ ℋ ) )
20 8 19 sylan ⊢ ( ( 𝑇 ∈ UniOp ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑇 ‘ 𝑥 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑦 ) ∈ ℋ ) )
21 unop ⊢ ( ( 𝑆 ∈ UniOp ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑦 ) ∈ ℋ ) → ( ( 𝑆 ‘ ( 𝑇 ‘ 𝑥 ) ) ·ih ( 𝑆 ‘ ( 𝑇 ‘ 𝑦 ) ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) )
22 21 3expb ⊢ ( ( 𝑆 ∈ UniOp ∧ ( ( 𝑇 ‘ 𝑥 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑦 ) ∈ ℋ ) ) → ( ( 𝑆 ‘ ( 𝑇 ‘ 𝑥 ) ) ·ih ( 𝑆 ‘ ( 𝑇 ‘ 𝑦 ) ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) )
23 20 22 sylan2 ⊢ ( ( 𝑆 ∈ UniOp ∧ ( 𝑇 ∈ UniOp ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) ) → ( ( 𝑆 ‘ ( 𝑇 ‘ 𝑥 ) ) ·ih ( 𝑆 ‘ ( 𝑇 ‘ 𝑦 ) ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) )
24 23 anassrs ⊢ ( ( ( 𝑆 ∈ UniOp ∧ 𝑇 ∈ UniOp ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑆 ‘ ( 𝑇 ‘ 𝑥 ) ) ·ih ( 𝑆 ‘ ( 𝑇 ‘ 𝑦 ) ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) )
25 unop ⊢ ( ( 𝑇 ∈ UniOp ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) )
26 25 3expb ⊢ ( ( 𝑇 ∈ UniOp ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) )
27 26 adantll ⊢ ( ( ( 𝑆 ∈ UniOp ∧ 𝑇 ∈ UniOp ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) )
28 16 24 27 3eqtrd ⊢ ( ( ( 𝑆 ∈ UniOp ∧ 𝑇 ∈ UniOp ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ·ih ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) )
29 28 ralrimivva ⊢ ( ( 𝑆 ∈ UniOp ∧ 𝑇 ∈ UniOp ) → ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ·ih ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) )
30 elunop ⊢ ( ( 𝑆 ∘ 𝑇 ) ∈ UniOp ↔ ( ( 𝑆 ∘ 𝑇 ) : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ·ih ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) ) )
31 6 29 30 sylanbrc ⊢ ( ( 𝑆 ∈ UniOp ∧ 𝑇 ∈ UniOp ) → ( 𝑆 ∘ 𝑇 ) ∈ UniOp )