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

 Description: The adjoint of the sum of two operators. Theorem 3.11(iii) of [Beran] p. 106. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
Assertion
Ref Expression

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dmadjop 28875 . . 3 (𝑆 ∈ dom adj𝑆: ℋ⟶ ℋ)
2 dmadjop 28875 . . 3 (𝑇 ∈ dom adj𝑇: ℋ⟶ ℋ)
3 hoaddcl 28745 . . 3 ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆 +op 𝑇): ℋ⟶ ℋ)
41, 2, 3syl2an 493 . 2 ((𝑆 ∈ dom adj𝑇 ∈ dom adj) → (𝑆 +op 𝑇): ℋ⟶ ℋ)
75, 6syl 17 . . 3 (𝑆 ∈ dom adj → (adj𝑆): ℋ⟶ ℋ)
108, 9syl 17 . . 3 (𝑇 ∈ dom adj → (adj𝑇): ℋ⟶ ℋ)
13 adj2 28921 . . . . . . . 8 ((𝑆 ∈ dom adj𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑆𝑥) ·ih 𝑦) = (𝑥 ·ih ((adj𝑆)‘𝑦)))
14133expb 1285 . . . . . . 7 ((𝑆 ∈ dom adj ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → ((𝑆𝑥) ·ih 𝑦) = (𝑥 ·ih ((adj𝑆)‘𝑦)))
1514adantlr 751 . . . . . 6 (((𝑆 ∈ dom adj𝑇 ∈ dom adj) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → ((𝑆𝑥) ·ih 𝑦) = (𝑥 ·ih ((adj𝑆)‘𝑦)))
16 adj2 28921 . . . . . . . 8 ((𝑇 ∈ dom adj𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇𝑥) ·ih 𝑦) = (𝑥 ·ih ((adj𝑇)‘𝑦)))
17163expb 1285 . . . . . . 7 ((𝑇 ∈ dom adj ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → ((𝑇𝑥) ·ih 𝑦) = (𝑥 ·ih ((adj𝑇)‘𝑦)))
1817adantll 750 . . . . . 6 (((𝑆 ∈ dom adj𝑇 ∈ dom adj) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → ((𝑇𝑥) ·ih 𝑦) = (𝑥 ·ih ((adj𝑇)‘𝑦)))
1915, 18oveq12d 6708 . . . . 5 (((𝑆 ∈ dom adj𝑇 ∈ dom adj) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (((𝑆𝑥) ·ih 𝑦) + ((𝑇𝑥) ·ih 𝑦)) = ((𝑥 ·ih ((adj𝑆)‘𝑦)) + (𝑥 ·ih ((adj𝑇)‘𝑦))))
201ffvelrnda 6399 . . . . . . 7 ((𝑆 ∈ dom adj𝑥 ∈ ℋ) → (𝑆𝑥) ∈ ℋ)
2120ad2ant2r 798 . . . . . 6 (((𝑆 ∈ dom adj𝑇 ∈ dom adj) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑆𝑥) ∈ ℋ)
222ffvelrnda 6399 . . . . . . 7 ((𝑇 ∈ dom adj𝑥 ∈ ℋ) → (𝑇𝑥) ∈ ℋ)
2322ad2ant2lr 799 . . . . . 6 (((𝑆 ∈ dom adj𝑇 ∈ dom adj) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑇𝑥) ∈ ℋ)
24 simprr 811 . . . . . 6 (((𝑆 ∈ dom adj𝑇 ∈ dom adj) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑦 ∈ ℋ)
25 ax-his2 28068 . . . . . 6 (((𝑆𝑥) ∈ ℋ ∧ (𝑇𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((𝑆𝑥) + (𝑇𝑥)) ·ih 𝑦) = (((𝑆𝑥) ·ih 𝑦) + ((𝑇𝑥) ·ih 𝑦)))
2621, 23, 24, 25syl3anc 1366 . . . . 5 (((𝑆 ∈ dom adj𝑇 ∈ dom adj) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (((𝑆𝑥) + (𝑇𝑥)) ·ih 𝑦) = (((𝑆𝑥) ·ih 𝑦) + ((𝑇𝑥) ·ih 𝑦)))
27 simprl 809 . . . . . 6 (((𝑆 ∈ dom adj𝑇 ∈ dom adj) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑥 ∈ ℋ)
28 adjcl 28919 . . . . . . 7 ((𝑆 ∈ dom adj𝑦 ∈ ℋ) → ((adj𝑆)‘𝑦) ∈ ℋ)
2928ad2ant2rl 800 . . . . . 6 (((𝑆 ∈ dom adj𝑇 ∈ dom adj) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → ((adj𝑆)‘𝑦) ∈ ℋ)
30 adjcl 28919 . . . . . . 7 ((𝑇 ∈ dom adj𝑦 ∈ ℋ) → ((adj𝑇)‘𝑦) ∈ ℋ)
3130ad2ant2l 797 . . . . . 6 (((𝑆 ∈ dom adj𝑇 ∈ dom adj) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → ((adj𝑇)‘𝑦) ∈ ℋ)
32 his7 28075 . . . . . 6 ((𝑥 ∈ ℋ ∧ ((adj𝑆)‘𝑦) ∈ ℋ ∧ ((adj𝑇)‘𝑦) ∈ ℋ) → (𝑥 ·ih (((adj𝑆)‘𝑦) + ((adj𝑇)‘𝑦))) = ((𝑥 ·ih ((adj𝑆)‘𝑦)) + (𝑥 ·ih ((adj𝑇)‘𝑦))))
3327, 29, 31, 32syl3anc 1366 . . . . 5 (((𝑆 ∈ dom adj𝑇 ∈ dom adj) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·ih (((adj𝑆)‘𝑦) + ((adj𝑇)‘𝑦))) = ((𝑥 ·ih ((adj𝑆)‘𝑦)) + (𝑥 ·ih ((adj𝑇)‘𝑦))))
3419, 26, 333eqtr4rd 2696 . . . 4 (((𝑆 ∈ dom adj𝑇 ∈ dom adj) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·ih (((adj𝑆)‘𝑦) + ((adj𝑇)‘𝑦))) = (((𝑆𝑥) + (𝑇𝑥)) ·ih 𝑦))
357, 10anim12i 589 . . . . . . 7 ((𝑆 ∈ dom adj𝑇 ∈ dom adj) → ((adj𝑆): ℋ⟶ ℋ ∧ (adj𝑇): ℋ⟶ ℋ))