This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem adj2

Description: Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adj2 ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) = ( 𝐴 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 adj1 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐵 ·ih ( 𝑇 ‘ 𝐴 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐵 ) ·ih 𝐴 ) )
2 simp2 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → 𝐵 ∈ ℋ )
3 dmadjop ⊢ ( 𝑇 ∈ dom adjℎ → 𝑇 : ℋ ⟶ ℋ )
4 3 ffvelcdmda ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ) → ( 𝑇 ‘ 𝐴 ) ∈ ℋ )
5 4 3adant2 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝑇 ‘ 𝐴 ) ∈ ℋ )
6 ax-his1 ⊢ ( ( 𝐵 ∈ ℋ ∧ ( 𝑇 ‘ 𝐴 ) ∈ ℋ ) → ( 𝐵 ·ih ( 𝑇 ‘ 𝐴 ) ) = ( ∗ ‘ ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) ) )
7 2 5 6 syl2anc ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐵 ·ih ( 𝑇 ‘ 𝐴 ) ) = ( ∗ ‘ ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) ) )
8 adjcl ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐵 ∈ ℋ ) → ( ( adjℎ ‘ 𝑇 ) ‘ 𝐵 ) ∈ ℋ )
9 8 3adant3 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( adjℎ ‘ 𝑇 ) ‘ 𝐵 ) ∈ ℋ )
10 simp3 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → 𝐴 ∈ ℋ )
11 ax-his1 ⊢ ( ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐵 ) ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐵 ) ·ih 𝐴 ) = ( ∗ ‘ ( 𝐴 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝐵 ) ) ) )
12 9 10 11 syl2anc ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐵 ) ·ih 𝐴 ) = ( ∗ ‘ ( 𝐴 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝐵 ) ) ) )
13 1 7 12 3eqtr3d ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ∗ ‘ ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) ) = ( ∗ ‘ ( 𝐴 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝐵 ) ) ) )
14 hicl ⊢ ( ( ( 𝑇 ‘ 𝐴 ) ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) ∈ ℂ )
15 5 2 14 syl2anc ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) ∈ ℂ )
16 hicl ⊢ ( ( 𝐴 ∈ ℋ ∧ ( ( adjℎ ‘ 𝑇 ) ‘ 𝐵 ) ∈ ℋ ) → ( 𝐴 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝐵 ) ) ∈ ℂ )
17 10 9 16 syl2anc ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐴 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝐵 ) ) ∈ ℂ )
18 cj11 ⊢ ( ( ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) ∈ ℂ ∧ ( 𝐴 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝐵 ) ) ∈ ℂ ) → ( ( ∗ ‘ ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) ) = ( ∗ ‘ ( 𝐴 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝐵 ) ) ) ↔ ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) = ( 𝐴 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝐵 ) ) ) )
19 15 17 18 syl2anc ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( ∗ ‘ ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) ) = ( ∗ ‘ ( 𝐴 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝐵 ) ) ) ↔ ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) = ( 𝐴 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝐵 ) ) ) )
20 13 19 mpbid ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) = ( 𝐴 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝐵 ) ) )
21 20 3com23 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) = ( 𝐴 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝐵 ) ) )