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

 Description: The adjoint of an operator is linear. Proposition 1 of [AkhiezerGlazman] p. 80. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.)
Assertion
Ref Expression

Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
31, 2syl 17 . 2 (𝑇 ∈ dom adj → (adj𝑇): ℋ⟶ ℋ)
4 simp2 1055 . . . . . . . . . . 11 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → 𝑤 ∈ ℋ)
5 adjcl 28175 . . . . . . . . . . . . . . 15 ((𝑇 ∈ dom adj𝑦 ∈ ℋ) → ((adj𝑇)‘𝑦) ∈ ℋ)
6 hvmulcl 27254 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℂ ∧ ((adj𝑇)‘𝑦) ∈ ℋ) → (𝑥 · ((adj𝑇)‘𝑦)) ∈ ℋ)
75, 6sylan2 490 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℂ ∧ (𝑇 ∈ dom adj𝑦 ∈ ℋ)) → (𝑥 · ((adj𝑇)‘𝑦)) ∈ ℋ)
87an12s 839 . . . . . . . . . . . . 13 ((𝑇 ∈ dom adj ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) → (𝑥 · ((adj𝑇)‘𝑦)) ∈ ℋ)
98adantrr 749 . . . . . . . . . . . 12 ((𝑇 ∈ dom adj ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → (𝑥 · ((adj𝑇)‘𝑦)) ∈ ℋ)
1093adant2 1073 . . . . . . . . . . 11 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → (𝑥 · ((adj𝑇)‘𝑦)) ∈ ℋ)
11 adjcl 28175 . . . . . . . . . . . . 13 ((𝑇 ∈ dom adj𝑧 ∈ ℋ) → ((adj𝑇)‘𝑧) ∈ ℋ)
1211adantrl 748 . . . . . . . . . . . 12 ((𝑇 ∈ dom adj ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → ((adj𝑇)‘𝑧) ∈ ℋ)
13123adant2 1073 . . . . . . . . . . 11 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → ((adj𝑇)‘𝑧) ∈ ℋ)
14 his7 27331 . . . . . . . . . . 11 ((𝑤 ∈ ℋ ∧ (𝑥 · ((adj𝑇)‘𝑦)) ∈ ℋ ∧ ((adj𝑇)‘𝑧) ∈ ℋ) → (𝑤 ·ih ((𝑥 · ((adj𝑇)‘𝑦)) + ((adj𝑇)‘𝑧))) = ((𝑤 ·ih (𝑥 · ((adj𝑇)‘𝑦))) + (𝑤 ·ih ((adj𝑇)‘𝑧))))
154, 10, 13, 14syl3anc 1318 . . . . . . . . . 10 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → (𝑤 ·ih ((𝑥 · ((adj𝑇)‘𝑦)) + ((adj𝑇)‘𝑧))) = ((𝑤 ·ih (𝑥 · ((adj𝑇)‘𝑦))) + (𝑤 ·ih ((adj𝑇)‘𝑧))))
16 adj2 28177 . . . . . . . . . . . . . . 15 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇𝑤) ·ih 𝑦) = (𝑤 ·ih ((adj𝑇)‘𝑦)))
17163adant3l 1314 . . . . . . . . . . . . . 14 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) → ((𝑇𝑤) ·ih 𝑦) = (𝑤 ·ih ((adj𝑇)‘𝑦)))
1817oveq2d 6565 . . . . . . . . . . . . 13 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) → ((∗‘𝑥) · ((𝑇𝑤) ·ih 𝑦)) = ((∗‘𝑥) · (𝑤 ·ih ((adj𝑇)‘𝑦))))
19 simp3l 1082 . . . . . . . . . . . . . 14 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) → 𝑥 ∈ ℂ)
20 dmadjop 28131 . . . . . . . . . . . . . . . 16 (𝑇 ∈ dom adj𝑇: ℋ⟶ ℋ)
2120ffvelrnda 6267 . . . . . . . . . . . . . . 15 ((𝑇 ∈ dom adj𝑤 ∈ ℋ) → (𝑇𝑤) ∈ ℋ)
22213adant3 1074 . . . . . . . . . . . . . 14 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) → (𝑇𝑤) ∈ ℋ)
23 simp3r 1083 . . . . . . . . . . . . . 14 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) → 𝑦 ∈ ℋ)
24 his5 27327 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℂ ∧ (𝑇𝑤) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇𝑤) ·ih (𝑥 · 𝑦)) = ((∗‘𝑥) · ((𝑇𝑤) ·ih 𝑦)))
2519, 22, 23, 24syl3anc 1318 . . . . . . . . . . . . 13 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) → ((𝑇𝑤) ·ih (𝑥 · 𝑦)) = ((∗‘𝑥) · ((𝑇𝑤) ·ih 𝑦)))
26 simp2 1055 . . . . . . . . . . . . . 14 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) → 𝑤 ∈ ℋ)
275adantrl 748 . . . . . . . . . . . . . . 15 ((𝑇 ∈ dom adj ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) → ((adj𝑇)‘𝑦) ∈ ℋ)
28273adant2 1073 . . . . . . . . . . . . . 14 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) → ((adj𝑇)‘𝑦) ∈ ℋ)
29 his5 27327 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ ∧ ((adj𝑇)‘𝑦) ∈ ℋ) → (𝑤 ·ih (𝑥 · ((adj𝑇)‘𝑦))) = ((∗‘𝑥) · (𝑤 ·ih ((adj𝑇)‘𝑦))))
3019, 26, 28, 29syl3anc 1318 . . . . . . . . . . . . 13 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) → (𝑤 ·ih (𝑥 · ((adj𝑇)‘𝑦))) = ((∗‘𝑥) · (𝑤 ·ih ((adj𝑇)‘𝑦))))
3118, 25, 303eqtr4d 2654 . . . . . . . . . . . 12 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) → ((𝑇𝑤) ·ih (𝑥 · 𝑦)) = (𝑤 ·ih (𝑥 · ((adj𝑇)‘𝑦))))
32313adant3r 1315 . . . . . . . . . . 11 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → ((𝑇𝑤) ·ih (𝑥 · 𝑦)) = (𝑤 ·ih (𝑥 · ((adj𝑇)‘𝑦))))
33 adj2 28177 . . . . . . . . . . . 12 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑇𝑤) ·ih 𝑧) = (𝑤 ·ih ((adj𝑇)‘𝑧)))
34333adant3l 1314 . . . . . . . . . . 11 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → ((𝑇𝑤) ·ih 𝑧) = (𝑤 ·ih ((adj𝑇)‘𝑧)))
3532, 34oveq12d 6567 . . . . . . . . . 10 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → (((𝑇𝑤) ·ih (𝑥 · 𝑦)) + ((𝑇𝑤) ·ih 𝑧)) = ((𝑤 ·ih (𝑥 · ((adj𝑇)‘𝑦))) + (𝑤 ·ih ((adj𝑇)‘𝑧))))
36213adant3 1074 . . . . . . . . . . . 12 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → (𝑇𝑤) ∈ ℋ)
37 hvmulcl 27254 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑥 · 𝑦) ∈ ℋ)
3837adantr 480 . . . . . . . . . . . . 13 (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → (𝑥 · 𝑦) ∈ ℋ)
39383ad2ant3 1077 . . . . . . . . . . . 12 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → (𝑥 · 𝑦) ∈ ℋ)
40 simp3r 1083 . . . . . . . . . . . 12 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → 𝑧 ∈ ℋ)
41 his7 27331 . . . . . . . . . . . 12 (((𝑇𝑤) ∈ ℋ ∧ (𝑥 · 𝑦) ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑇𝑤) ·ih ((𝑥 · 𝑦) + 𝑧)) = (((𝑇𝑤) ·ih (𝑥 · 𝑦)) + ((𝑇𝑤) ·ih 𝑧)))
4236, 39, 40, 41syl3anc 1318 . . . . . . . . . . 11 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → ((𝑇𝑤) ·ih ((𝑥 · 𝑦) + 𝑧)) = (((𝑇𝑤) ·ih (𝑥 · 𝑦)) + ((𝑇𝑤) ·ih 𝑧)))
43 hvaddcl 27253 . . . . . . . . . . . . 13 (((𝑥 · 𝑦) ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑥 · 𝑦) + 𝑧) ∈ ℋ)
4437, 43sylan 487 . . . . . . . . . . . 12 (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑥 · 𝑦) + 𝑧) ∈ ℋ)
45 adj2 28177 . . . . . . . . . . . 12 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ ((𝑥 · 𝑦) + 𝑧) ∈ ℋ) → ((𝑇𝑤) ·ih ((𝑥 · 𝑦) + 𝑧)) = (𝑤 ·ih ((adj𝑇)‘((𝑥 · 𝑦) + 𝑧))))
4644, 45syl3an3 1353 . . . . . . . . . . 11 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → ((𝑇𝑤) ·ih ((𝑥 · 𝑦) + 𝑧)) = (𝑤 ·ih ((adj𝑇)‘((𝑥 · 𝑦) + 𝑧))))
4742, 46eqtr3d 2646 . . . . . . . . . 10 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → (((𝑇𝑤) ·ih (𝑥 · 𝑦)) + ((𝑇𝑤) ·ih 𝑧)) = (𝑤 ·ih ((adj𝑇)‘((𝑥 · 𝑦) + 𝑧))))
4815, 35, 473eqtr2rd 2651 . . . . . . . . 9 ((𝑇 ∈ dom adj𝑤 ∈ ℋ ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → (𝑤 ·ih ((adj𝑇)‘((𝑥 · 𝑦) + 𝑧))) = (𝑤 ·ih ((𝑥 · ((adj𝑇)‘𝑦)) + ((adj𝑇)‘𝑧))))
49483com23 1263 . . . . . . . 8 ((𝑇 ∈ dom adj ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → (𝑤 ·ih ((adj𝑇)‘((𝑥 · 𝑦) + 𝑧))) = (𝑤 ·ih ((𝑥 · ((adj𝑇)‘𝑦)) + ((adj𝑇)‘𝑧))))
50493expa 1257 . . . . . . 7 (((𝑇 ∈ dom adj ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) ∧ 𝑤 ∈ ℋ) → (𝑤 ·ih ((adj𝑇)‘((𝑥 · 𝑦) + 𝑧))) = (𝑤 ·ih ((𝑥 · ((adj𝑇)‘𝑦)) + ((adj𝑇)‘𝑧))))
5150ralrimiva 2949 . . . . . 6 ((𝑇 ∈ dom adj ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → ∀𝑤 ∈ ℋ (𝑤 ·ih ((adj𝑇)‘((𝑥 · 𝑦) + 𝑧))) = (𝑤 ·ih ((𝑥 · ((adj𝑇)‘𝑦)) + ((adj𝑇)‘𝑧))))
52 adjcl 28175 . . . . . . . 8 ((𝑇 ∈ dom adj ∧ ((𝑥 · 𝑦) + 𝑧) ∈ ℋ) → ((adj𝑇)‘((𝑥 · 𝑦) + 𝑧)) ∈ ℋ)
5344, 52sylan2 490 . . . . . . 7 ((𝑇 ∈ dom adj ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → ((adj𝑇)‘((𝑥 · 𝑦) + 𝑧)) ∈ ℋ)
54 hvaddcl 27253 . . . . . . . . 9 (((𝑥 · ((adj𝑇)‘𝑦)) ∈ ℋ ∧ ((adj𝑇)‘𝑧) ∈ ℋ) → ((𝑥 · ((adj𝑇)‘𝑦)) + ((adj𝑇)‘𝑧)) ∈ ℋ)
558, 11, 54syl2an 493 . . . . . . . 8 (((𝑇 ∈ dom adj ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ (𝑇 ∈ dom adj𝑧 ∈ ℋ)) → ((𝑥 · ((adj𝑇)‘𝑦)) + ((adj𝑇)‘𝑧)) ∈ ℋ)
5655anandis 869 . . . . . . 7 ((𝑇 ∈ dom adj ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → ((𝑥 · ((adj𝑇)‘𝑦)) + ((adj𝑇)‘𝑧)) ∈ ℋ)
57 hial2eq2 27348 . . . . . . 7 ((((adj𝑇)‘((𝑥 · 𝑦) + 𝑧)) ∈ ℋ ∧ ((𝑥 · ((adj𝑇)‘𝑦)) + ((adj𝑇)‘𝑧)) ∈ ℋ) → (∀𝑤 ∈ ℋ (𝑤 ·ih ((adj𝑇)‘((𝑥 · 𝑦) + 𝑧))) = (𝑤 ·ih ((𝑥 · ((adj𝑇)‘𝑦)) + ((adj𝑇)‘𝑧))) ↔ ((adj𝑇)‘((𝑥 · 𝑦) + 𝑧)) = ((𝑥 · ((adj𝑇)‘𝑦)) + ((adj𝑇)‘𝑧))))
5853, 56, 57syl2anc 691 . . . . . 6 ((𝑇 ∈ dom adj ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → (∀𝑤 ∈ ℋ (𝑤 ·ih ((adj𝑇)‘((𝑥 · 𝑦) + 𝑧))) = (𝑤 ·ih ((𝑥 · ((adj𝑇)‘𝑦)) + ((adj𝑇)‘𝑧))) ↔ ((adj𝑇)‘((𝑥 · 𝑦) + 𝑧)) = ((𝑥 · ((adj𝑇)‘𝑦)) + ((adj𝑇)‘𝑧))))
5951, 58mpbid 221 . . . . 5 ((𝑇 ∈ dom adj ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → ((adj𝑇)‘((𝑥 · 𝑦) + 𝑧)) = ((𝑥 · ((adj𝑇)‘𝑦)) + ((adj𝑇)‘𝑧)))
6059exp32 629 . . . 4 (𝑇 ∈ dom adj → ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑧 ∈ ℋ → ((adj𝑇)‘((𝑥 · 𝑦) + 𝑧)) = ((𝑥 · ((adj𝑇)‘𝑦)) + ((adj𝑇)‘𝑧)))))
6160ralrimdv 2951 . . 3 (𝑇 ∈ dom adj → ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → ∀𝑧 ∈ ℋ ((adj𝑇)‘((𝑥 · 𝑦) + 𝑧)) = ((𝑥 · ((adj𝑇)‘𝑦)) + ((adj𝑇)‘𝑧))))
6261ralrimivv 2953 . 2 (𝑇 ∈ dom adj → ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ ((adj𝑇)‘((𝑥 · 𝑦) + 𝑧)) = ((𝑥 · ((adj𝑇)‘𝑦)) + ((adj𝑇)‘𝑧)))
63 ellnop 28101 . 2 ((adj𝑇) ∈ LinOp ↔ ((adj𝑇): ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ ((adj𝑇)‘((𝑥 · 𝑦) + 𝑧)) = ((𝑥 · ((adj𝑇)‘𝑦)) + ((adj𝑇)‘𝑧))))
643, 62, 63sylanbrc 695 1 (𝑇 ∈ dom adj → (adj𝑇) ∈ LinOp)