Metamath Proof Explorer

Theorem hmopco

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

Ref Expression
Assertion hmopco ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑈 ) = ( 𝑈 ∘ 𝑇 ) ) → ( 𝑇 ∘ 𝑈 ) ∈ HrmOp )

Proof

Step Hyp Ref Expression
1 hmopf ⊢ ( 𝑇 ∈ HrmOp → 𝑇 : ℋ ⟶ ℋ )
2 hmopf ⊢ ( 𝑈 ∈ HrmOp → 𝑈 : ℋ ⟶ ℋ )
3 fco ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑇 ∘ 𝑈 ) : ℋ ⟶ ℋ )
4 1 2 3 syl2an ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 ∘ 𝑈 ) : ℋ ⟶ ℋ )
5 4 3adant3 ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑈 ) = ( 𝑈 ∘ 𝑇 ) ) → ( 𝑇 ∘ 𝑈 ) : ℋ ⟶ ℋ )
6 fvco3 ⊢ ( ( 𝑈 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ∘ 𝑈 ) ‘ 𝑦 ) = ( 𝑇 ‘ ( 𝑈 ‘ 𝑦 ) ) )
7 2 6 sylan ⊢ ( ( 𝑈 ∈ HrmOp ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ∘ 𝑈 ) ‘ 𝑦 ) = ( 𝑇 ‘ ( 𝑈 ‘ 𝑦 ) ) )
8 7 oveq2d ⊢ ( ( 𝑈 ∈ HrmOp ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ih ( ( 𝑇 ∘ 𝑈 ) ‘ 𝑦 ) ) = ( 𝑥 ·ih ( 𝑇 ‘ ( 𝑈 ‘ 𝑦 ) ) ) )
9 8 ad2ant2l ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ih ( ( 𝑇 ∘ 𝑈 ) ‘ 𝑦 ) ) = ( 𝑥 ·ih ( 𝑇 ‘ ( 𝑈 ‘ 𝑦 ) ) ) )
10 simpll ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → 𝑇 ∈ HrmOp )
11 simprl ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → 𝑥 ∈ ℋ )
12 2 ffvelrnda ⊢ ( ( 𝑈 ∈ HrmOp ∧ 𝑦 ∈ ℋ ) → ( 𝑈 ‘ 𝑦 ) ∈ ℋ )
13 12 ad2ant2l ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑈 ‘ 𝑦 ) ∈ ℋ )
14 hmop ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ∧ ( 𝑈 ‘ 𝑦 ) ∈ ℋ ) → ( 𝑥 ·ih ( 𝑇 ‘ ( 𝑈 ‘ 𝑦 ) ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑈 ‘ 𝑦 ) ) )
15 10 11 13 14 syl3anc ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ih ( 𝑇 ‘ ( 𝑈 ‘ 𝑦 ) ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑈 ‘ 𝑦 ) ) )
16 simplr ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → 𝑈 ∈ HrmOp )
17 1 ffvelrnda ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
18 17 ad2ant2r ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
19 simprr ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → 𝑦 ∈ ℋ )
20 hmop ⊢ ( ( 𝑈 ∈ HrmOp ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑈 ‘ 𝑦 ) ) = ( ( 𝑈 ‘ ( 𝑇 ‘ 𝑥 ) ) ·ih 𝑦 ) )
21 16 18 19 20 syl3anc ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑈 ‘ 𝑦 ) ) = ( ( 𝑈 ‘ ( 𝑇 ‘ 𝑥 ) ) ·ih 𝑦 ) )
22 9 15 21 3eqtrd ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ih ( ( 𝑇 ∘ 𝑈 ) ‘ 𝑦 ) ) = ( ( 𝑈 ‘ ( 𝑇 ‘ 𝑥 ) ) ·ih 𝑦 ) )
23 fvco3 ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑈 ∘ 𝑇 ) ‘ 𝑥 ) = ( 𝑈 ‘ ( 𝑇 ‘ 𝑥 ) ) )
24 1 23 sylan ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ) → ( ( 𝑈 ∘ 𝑇 ) ‘ 𝑥 ) = ( 𝑈 ‘ ( 𝑇 ‘ 𝑥 ) ) )
25 24 oveq1d ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑈 ∘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) = ( ( 𝑈 ‘ ( 𝑇 ‘ 𝑥 ) ) ·ih 𝑦 ) )
26 25 ad2ant2r ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( ( 𝑈 ∘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) = ( ( 𝑈 ‘ ( 𝑇 ‘ 𝑥 ) ) ·ih 𝑦 ) )
27 22 26 eqtr4d ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ih ( ( 𝑇 ∘ 𝑈 ) ‘ 𝑦 ) ) = ( ( ( 𝑈 ∘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) )
28 27 3adantl3 ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑈 ) = ( 𝑈 ∘ 𝑇 ) ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ih ( ( 𝑇 ∘ 𝑈 ) ‘ 𝑦 ) ) = ( ( ( 𝑈 ∘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) )
29 fveq1 ⊢ ( ( 𝑇 ∘ 𝑈 ) = ( 𝑈 ∘ 𝑇 ) → ( ( 𝑇 ∘ 𝑈 ) ‘ 𝑥 ) = ( ( 𝑈 ∘ 𝑇 ) ‘ 𝑥 ) )
30 29 oveq1d ⊢ ( ( 𝑇 ∘ 𝑈 ) = ( 𝑈 ∘ 𝑇 ) → ( ( ( 𝑇 ∘ 𝑈 ) ‘ 𝑥 ) ·ih 𝑦 ) = ( ( ( 𝑈 ∘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) )
31 30 3ad2ant3 ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑈 ) = ( 𝑈 ∘ 𝑇 ) ) → ( ( ( 𝑇 ∘ 𝑈 ) ‘ 𝑥 ) ·ih 𝑦 ) = ( ( ( 𝑈 ∘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) )
32 31 adantr ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑈 ) = ( 𝑈 ∘ 𝑇 ) ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( ( 𝑇 ∘ 𝑈 ) ‘ 𝑥 ) ·ih 𝑦 ) = ( ( ( 𝑈 ∘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) )
33 28 32 eqtr4d ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑈 ) = ( 𝑈 ∘ 𝑇 ) ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ih ( ( 𝑇 ∘ 𝑈 ) ‘ 𝑦 ) ) = ( ( ( 𝑇 ∘ 𝑈 ) ‘ 𝑥 ) ·ih 𝑦 ) )
34 33 ralrimivva ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑈 ) = ( 𝑈 ∘ 𝑇 ) ) → ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( ( 𝑇 ∘ 𝑈 ) ‘ 𝑦 ) ) = ( ( ( 𝑇 ∘ 𝑈 ) ‘ 𝑥 ) ·ih 𝑦 ) )
35 elhmop ⊢ ( ( 𝑇 ∘ 𝑈 ) ∈ HrmOp ↔ ( ( 𝑇 ∘ 𝑈 ) : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( ( 𝑇 ∘ 𝑈 ) ‘ 𝑦 ) ) = ( ( ( 𝑇 ∘ 𝑈 ) ‘ 𝑥 ) ·ih 𝑦 ) ) )
36 5 34 35 sylanbrc ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑈 ) = ( 𝑈 ∘ 𝑇 ) ) → ( 𝑇 ∘ 𝑈 ) ∈ HrmOp )