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

Metamath Proof Explorer

Theorem adj1

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

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

Proof

Step Hyp Ref Expression
1 funadj ⊢ Fun adjℎ
2 funfvop ⊢ ( ( Fun adjℎ ∧ 𝑇 ∈ dom adjℎ ) → ⟨ 𝑇 , ( adjℎ ‘ 𝑇 ) ⟩ ∈ adjℎ )
3 1 2 mpan ⊢ ( 𝑇 ∈ dom adjℎ → ⟨ 𝑇 , ( adjℎ ‘ 𝑇 ) ⟩ ∈ adjℎ )
4 dfadj2 ⊢ adjℎ = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑧 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ) }
5 3 4 eleqtrdi ⊢ ( 𝑇 ∈ dom adjℎ → ⟨ 𝑇 , ( adjℎ ‘ 𝑇 ) ⟩ ∈ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑧 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ) } )
6 fvex ⊢ ( adjℎ ‘ 𝑇 ) ∈ V
7 feq1 ⊢ ( 𝑧 = 𝑇 → ( 𝑧 : ℋ ⟶ ℋ ↔ 𝑇 : ℋ ⟶ ℋ ) )
8 fveq1 ⊢ ( 𝑧 = 𝑇 → ( 𝑧 ‘ 𝑦 ) = ( 𝑇 ‘ 𝑦 ) )
9 8 oveq2d ⊢ ( 𝑧 = 𝑇 → ( 𝑥 ·ih ( 𝑧 ‘ 𝑦 ) ) = ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) )
10 9 eqeq1d ⊢ ( 𝑧 = 𝑇 → ( ( 𝑥 ·ih ( 𝑧 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ) )
11 10 2ralbidv ⊢ ( 𝑧 = 𝑇 → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑧 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ) )
12 7 11 3anbi13d ⊢ ( 𝑧 = 𝑇 → ( ( 𝑧 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑧 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ) ) )
13 feq1 ⊢ ( 𝑤 = ( adjℎ ‘ 𝑇 ) → ( 𝑤 : ℋ ⟶ ℋ ↔ ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ ) )
14 fveq1 ⊢ ( 𝑤 = ( adjℎ ‘ 𝑇 ) → ( 𝑤 ‘ 𝑥 ) = ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) )
15 14 oveq1d ⊢ ( 𝑤 = ( adjℎ ‘ 𝑇 ) → ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) )
16 15 eqeq2d ⊢ ( 𝑤 = ( adjℎ ‘ 𝑇 ) → ( ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) ) )
17 16 2ralbidv ⊢ ( 𝑤 = ( adjℎ ‘ 𝑇 ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) ) )
18 13 17 3anbi23d ⊢ ( 𝑤 = ( adjℎ ‘ 𝑇 ) → ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) ) ) )
19 12 18 opelopabg ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( adjℎ ‘ 𝑇 ) ∈ V ) → ( ⟨ 𝑇 , ( adjℎ ‘ 𝑇 ) ⟩ ∈ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑧 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ) } ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) ) ) )
20 6 19 mpan2 ⊢ ( 𝑇 ∈ dom adjℎ → ( ⟨ 𝑇 , ( adjℎ ‘ 𝑇 ) ⟩ ∈ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑧 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ) } ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) ) ) )
21 5 20 mpbid ⊢ ( 𝑇 ∈ dom adjℎ → ( 𝑇 : ℋ ⟶ ℋ ∧ ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) ) )
22 21 simp3d ⊢ ( 𝑇 ∈ dom adjℎ → ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) )
23 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝐴 ·ih ( 𝑇 ‘ 𝑦 ) ) )
24 fveq2 ⊢ ( 𝑥 = 𝐴 → ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) = ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) )
25 24 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ·ih 𝑦 ) )
26 23 25 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) ↔ ( 𝐴 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ·ih 𝑦 ) ) )
27 fveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝑇 ‘ 𝑦 ) = ( 𝑇 ‘ 𝐵 ) )
28 27 oveq2d ⊢ ( 𝑦 = 𝐵 → ( 𝐴 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) )
29 oveq2 ⊢ ( 𝑦 = 𝐵 → ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ·ih 𝑦 ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ·ih 𝐵 ) )
30 28 29 eqeq12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ·ih 𝑦 ) ↔ ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ·ih 𝐵 ) ) )
31 26 30 rspc2v ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) → ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ·ih 𝐵 ) ) )
32 22 31 syl5com ⊢ ( 𝑇 ∈ dom adjℎ → ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ·ih 𝐵 ) ) )
33 32 3impib ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ·ih 𝐵 ) )