Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  adj1 Structured version   Visualization version   GIF version

 Description: Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
Assertion
Ref Expression
adj1 ((𝑇 ∈ dom adj𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih (𝑇𝐵)) = (((adj𝑇)‘𝐴) ·ih 𝐵))

Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 funadj 28129 . . . . . . 7 Fun adj
31, 2mpan 702 . . . . . 6 (𝑇 ∈ dom adj → ⟨𝑇, (adj𝑇)⟩ ∈ adj)
4 dfadj2 28128 . . . . . 6 adj = {⟨𝑧, 𝑤⟩ ∣ (𝑧: ℋ⟶ ℋ ∧ 𝑤: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑧𝑦)) = ((𝑤𝑥) ·ih 𝑦))}
53, 4syl6eleq 2698 . . . . 5 (𝑇 ∈ dom adj → ⟨𝑇, (adj𝑇)⟩ ∈ {⟨𝑧, 𝑤⟩ ∣ (𝑧: ℋ⟶ ℋ ∧ 𝑤: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑧𝑦)) = ((𝑤𝑥) ·ih 𝑦))})
6 fvex 6113 . . . . . 6 (adj𝑇) ∈ V
7 feq1 5939 . . . . . . . 8 (𝑧 = 𝑇 → (𝑧: ℋ⟶ ℋ ↔ 𝑇: ℋ⟶ ℋ))
8 fveq1 6102 . . . . . . . . . . 11 (𝑧 = 𝑇 → (𝑧𝑦) = (𝑇𝑦))
98oveq2d 6565 . . . . . . . . . 10 (𝑧 = 𝑇 → (𝑥 ·ih (𝑧𝑦)) = (𝑥 ·ih (𝑇𝑦)))
109eqeq1d 2612 . . . . . . . . 9 (𝑧 = 𝑇 → ((𝑥 ·ih (𝑧𝑦)) = ((𝑤𝑥) ·ih 𝑦) ↔ (𝑥 ·ih (𝑇𝑦)) = ((𝑤𝑥) ·ih 𝑦)))
11102ralbidv 2972 . . . . . . . 8 (𝑧 = 𝑇 → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑧𝑦)) = ((𝑤𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑤𝑥) ·ih 𝑦)))
127, 113anbi13d 1393 . . . . . . 7 (𝑧 = 𝑇 → ((𝑧: ℋ⟶ ℋ ∧ 𝑤: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑧𝑦)) = ((𝑤𝑥) ·ih 𝑦)) ↔ (𝑇: ℋ⟶ ℋ ∧ 𝑤: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑤𝑥) ·ih 𝑦))))
13 feq1 5939 . . . . . . . 8 (𝑤 = (adj𝑇) → (𝑤: ℋ⟶ ℋ ↔ (adj𝑇): ℋ⟶ ℋ))
14 fveq1 6102 . . . . . . . . . . 11 (𝑤 = (adj𝑇) → (𝑤𝑥) = ((adj𝑇)‘𝑥))
1514oveq1d 6564 . . . . . . . . . 10 (𝑤 = (adj𝑇) → ((𝑤𝑥) ·ih 𝑦) = (((adj𝑇)‘𝑥) ·ih 𝑦))
1615eqeq2d 2620 . . . . . . . . 9 (𝑤 = (adj𝑇) → ((𝑥 ·ih (𝑇𝑦)) = ((𝑤𝑥) ·ih 𝑦) ↔ (𝑥 ·ih (𝑇𝑦)) = (((adj𝑇)‘𝑥) ·ih 𝑦)))
17162ralbidv 2972 . . . . . . . 8 (𝑤 = (adj𝑇) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑤𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = (((adj𝑇)‘𝑥) ·ih 𝑦)))
1813, 173anbi23d 1394 . . . . . . 7 (𝑤 = (adj𝑇) → ((𝑇: ℋ⟶ ℋ ∧ 𝑤: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑤𝑥) ·ih 𝑦)) ↔ (𝑇: ℋ⟶ ℋ ∧ (adj𝑇): ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = (((adj𝑇)‘𝑥) ·ih 𝑦))))
1912, 18opelopabg 4918 . . . . . 6 ((𝑇 ∈ dom adj ∧ (adj𝑇) ∈ V) → (⟨𝑇, (adj𝑇)⟩ ∈ {⟨𝑧, 𝑤⟩ ∣ (𝑧: ℋ⟶ ℋ ∧ 𝑤: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑧𝑦)) = ((𝑤𝑥) ·ih 𝑦))} ↔ (𝑇: ℋ⟶ ℋ ∧ (adj𝑇): ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = (((adj𝑇)‘𝑥) ·ih 𝑦))))
206, 19mpan2 703 . . . . 5 (𝑇 ∈ dom adj → (⟨𝑇, (adj𝑇)⟩ ∈ {⟨𝑧, 𝑤⟩ ∣ (𝑧: ℋ⟶ ℋ ∧ 𝑤: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑧𝑦)) = ((𝑤𝑥) ·ih 𝑦))} ↔ (𝑇: ℋ⟶ ℋ ∧ (adj𝑇): ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = (((adj𝑇)‘𝑥) ·ih 𝑦))))
215, 20mpbid 221 . . . 4 (𝑇 ∈ dom adj → (𝑇: ℋ⟶ ℋ ∧ (adj𝑇): ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = (((adj𝑇)‘𝑥) ·ih 𝑦)))
2221simp3d 1068 . . 3 (𝑇 ∈ dom adj → ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = (((adj𝑇)‘𝑥) ·ih 𝑦))
23 oveq1 6556 . . . . 5 (𝑥 = 𝐴 → (𝑥 ·ih (𝑇𝑦)) = (𝐴 ·ih (𝑇𝑦)))
24 fveq2 6103 . . . . . 6 (𝑥 = 𝐴 → ((adj𝑇)‘𝑥) = ((adj𝑇)‘𝐴))
2524oveq1d 6564 . . . . 5 (𝑥 = 𝐴 → (((adj𝑇)‘𝑥) ·ih 𝑦) = (((adj𝑇)‘𝐴) ·ih 𝑦))
2623, 25eqeq12d 2625 . . . 4 (𝑥 = 𝐴 → ((𝑥 ·ih (𝑇𝑦)) = (((adj𝑇)‘𝑥) ·ih 𝑦) ↔ (𝐴 ·ih (𝑇𝑦)) = (((adj𝑇)‘𝐴) ·ih 𝑦)))
27 fveq2 6103 . . . . . 6 (𝑦 = 𝐵 → (𝑇𝑦) = (𝑇𝐵))
2827oveq2d 6565 . . . . 5 (𝑦 = 𝐵 → (𝐴 ·ih (𝑇𝑦)) = (𝐴 ·ih (𝑇𝐵)))
29 oveq2 6557 . . . . 5 (𝑦 = 𝐵 → (((adj𝑇)‘𝐴) ·ih 𝑦) = (((adj𝑇)‘𝐴) ·ih 𝐵))
3028, 29eqeq12d 2625 . . . 4 (𝑦 = 𝐵 → ((𝐴 ·ih (𝑇𝑦)) = (((adj𝑇)‘𝐴) ·ih 𝑦) ↔ (𝐴 ·ih (𝑇𝐵)) = (((adj𝑇)‘𝐴) ·ih 𝐵)))
3126, 30rspc2v 3293 . . 3 ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = (((adj𝑇)‘𝑥) ·ih 𝑦) → (𝐴 ·ih (𝑇𝐵)) = (((adj𝑇)‘𝐴) ·ih 𝐵)))
3222, 31syl5com 31 . 2 (𝑇 ∈ dom adj → ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih (𝑇𝐵)) = (((adj𝑇)‘𝐴) ·ih 𝐵)))
33323impib 1254 1 ((𝑇 ∈ dom adj𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih (𝑇𝐵)) = (((adj𝑇)‘𝐴) ·ih 𝐵))