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

Metamath Proof Explorer

Theorem adjeq

Description: A property that determines the adjoint of a Hilbert space operator. (Contributed by NM, 20-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adjeq ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) → ( adjℎ ‘ 𝑇 ) = 𝑆 )

Proof

Step Hyp Ref Expression
1 funadj ⊢ Fun adjℎ
2 df-adjh ⊢ adjℎ = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑧 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ) }
3 2 eleq2i ⊢ ( ⟨ 𝑇 , 𝑆 ⟩ ∈ adjℎ ↔ ⟨ 𝑇 , 𝑆 ⟩ ∈ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑧 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ) } )
4 ax-hilex ⊢ ℋ ∈ V
5 fex ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ ℋ ∈ V ) → 𝑇 ∈ V )
6 4 5 mpan2 ⊢ ( 𝑇 : ℋ ⟶ ℋ → 𝑇 ∈ V )
7 fex ⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ ℋ ∈ V ) → 𝑆 ∈ V )
8 4 7 mpan2 ⊢ ( 𝑆 : ℋ ⟶ ℋ → 𝑆 ∈ V )
9 feq1 ⊢ ( 𝑧 = 𝑇 → ( 𝑧 : ℋ ⟶ ℋ ↔ 𝑇 : ℋ ⟶ ℋ ) )
10 fveq1 ⊢ ( 𝑧 = 𝑇 → ( 𝑧 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) )
11 10 oveq1d ⊢ ( 𝑧 = 𝑇 → ( ( 𝑧 ‘ 𝑥 ) ·ih 𝑦 ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) )
12 11 eqeq1d ⊢ ( 𝑧 = 𝑇 → ( ( ( 𝑧 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ↔ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ) )
13 12 2ralbidv ⊢ ( 𝑧 = 𝑇 → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑧 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ) )
14 9 13 3anbi13d ⊢ ( 𝑧 = 𝑇 → ( ( 𝑧 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑧 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ) ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ) ) )
15 feq1 ⊢ ( 𝑤 = 𝑆 → ( 𝑤 : ℋ ⟶ ℋ ↔ 𝑆 : ℋ ⟶ ℋ ) )
16 fveq1 ⊢ ( 𝑤 = 𝑆 → ( 𝑤 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑦 ) )
17 16 oveq2d ⊢ ( 𝑤 = 𝑆 → ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) )
18 17 eqeq2d ⊢ ( 𝑤 = 𝑆 → ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ↔ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) )
19 18 2ralbidv ⊢ ( 𝑤 = 𝑆 → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) )
20 15 19 3anbi23d ⊢ ( 𝑤 = 𝑆 → ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ) ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) ) )
21 14 20 opelopabg ⊢ ( ( 𝑇 ∈ V ∧ 𝑆 ∈ V ) → ( ⟨ 𝑇 , 𝑆 ⟩ ∈ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑧 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ) } ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) ) )
22 6 8 21 syl2an ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) → ( ⟨ 𝑇 , 𝑆 ⟩ ∈ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑧 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ) } ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) ) )
23 3 22 bitrid ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) → ( ⟨ 𝑇 , 𝑆 ⟩ ∈ adjℎ ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) ) )
24 df-3an ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) ↔ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) )
25 24 baibr ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) ) )
26 23 25 bitr4d ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) → ( ⟨ 𝑇 , 𝑆 ⟩ ∈ adjℎ ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) )
27 26 biimp3ar ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) → ⟨ 𝑇 , 𝑆 ⟩ ∈ adjℎ )
28 funopfv ⊢ ( Fun adjℎ → ( ⟨ 𝑇 , 𝑆 ⟩ ∈ adjℎ → ( adjℎ ‘ 𝑇 ) = 𝑆 ) )
29 1 27 28 mpsyl ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) → ( adjℎ ‘ 𝑇 ) = 𝑆 )