Metamath Proof Explorer

Theorem adjmul

Description: The adjoint of the scalar product of an operator. Theorem 3.11(ii) of Beran p. 106. (Contributed by NM, 21-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adjmul ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h → adj h ⁡ A · op T = A ‾ · op adj h ⁡ T

Proof

Step Hyp Ref Expression
1 dmadjop ⊢ T ∈ dom ⁡ adj h → T : ℋ ⟶ ℋ
2 homulcl ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ → A · op T : ℋ ⟶ ℋ
3 1 2 sylan2 ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h → A · op T : ℋ ⟶ ℋ
4 cjcl ⊢ A ∈ ℂ → A ‾ ∈ ℂ
5 dmadjrn ⊢ T ∈ dom ⁡ adj h → adj h ⁡ T ∈ dom ⁡ adj h
6 dmadjop ⊢ adj h ⁡ T ∈ dom ⁡ adj h → adj h ⁡ T : ℋ ⟶ ℋ
7 5 6 syl ⊢ T ∈ dom ⁡ adj h → adj h ⁡ T : ℋ ⟶ ℋ
8 homulcl ⊢ A ‾ ∈ ℂ ∧ adj h ⁡ T : ℋ ⟶ ℋ → A ‾ · op adj h ⁡ T : ℋ ⟶ ℋ
9 4 7 8 syl2an ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h → A ‾ · op adj h ⁡ T : ℋ ⟶ ℋ
10 adj2 ⊢ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x ⋅ ih y = x ⋅ ih adj h ⁡ T ⁡ y
11 10 3expb ⊢ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x ⋅ ih y = x ⋅ ih adj h ⁡ T ⁡ y
12 11 adantll ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x ⋅ ih y = x ⋅ ih adj h ⁡ T ⁡ y
13 12 oveq2d ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ y ∈ ℋ → A ⁢ T ⁡ x ⋅ ih y = A ⁢ x ⋅ ih adj h ⁡ T ⁡ y
14 1 ffvelcdmda ⊢ T ∈ dom ⁡ adj h ∧ x ∈ ℋ → T ⁡ x ∈ ℋ
15 ax-his3 ⊢ A ∈ ℂ ∧ T ⁡ x ∈ ℋ ∧ y ∈ ℋ → A ⋅ ℎ T ⁡ x ⋅ ih y = A ⁢ T ⁡ x ⋅ ih y
16 14 15 syl3an2 ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ y ∈ ℋ → A ⋅ ℎ T ⁡ x ⋅ ih y = A ⁢ T ⁡ x ⋅ ih y
17 16 3exp ⊢ A ∈ ℂ → T ∈ dom ⁡ adj h ∧ x ∈ ℋ → y ∈ ℋ → A ⋅ ℎ T ⁡ x ⋅ ih y = A ⁢ T ⁡ x ⋅ ih y
18 17 expd ⊢ A ∈ ℂ → T ∈ dom ⁡ adj h → x ∈ ℋ → y ∈ ℋ → A ⋅ ℎ T ⁡ x ⋅ ih y = A ⁢ T ⁡ x ⋅ ih y
19 18 imp43 ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ y ∈ ℋ → A ⋅ ℎ T ⁡ x ⋅ ih y = A ⁢ T ⁡ x ⋅ ih y
20 simpll ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ y ∈ ℋ → A ∈ ℂ
21 simprl ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ y ∈ ℋ → x ∈ ℋ
22 adjcl ⊢ T ∈ dom ⁡ adj h ∧ y ∈ ℋ → adj h ⁡ T ⁡ y ∈ ℋ
23 22 ad2ant2l ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ y ∈ ℋ → adj h ⁡ T ⁡ y ∈ ℋ
24 his52 ⊢ A ∈ ℂ ∧ x ∈ ℋ ∧ adj h ⁡ T ⁡ y ∈ ℋ → x ⋅ ih A ‾ ⋅ ℎ adj h ⁡ T ⁡ y = A ⁢ x ⋅ ih adj h ⁡ T ⁡ y
25 20 21 23 24 syl3anc ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih A ‾ ⋅ ℎ adj h ⁡ T ⁡ y = A ⁢ x ⋅ ih adj h ⁡ T ⁡ y
26 13 19 25 3eqtr4d ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ y ∈ ℋ → A ⋅ ℎ T ⁡ x ⋅ ih y = x ⋅ ih A ‾ ⋅ ℎ adj h ⁡ T ⁡ y
27 homval ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A · op T ⁡ x = A ⋅ ℎ T ⁡ x
28 1 27 syl3an2 ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h ∧ x ∈ ℋ → A · op T ⁡ x = A ⋅ ℎ T ⁡ x
29 28 3expa ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h ∧ x ∈ ℋ → A · op T ⁡ x = A ⋅ ℎ T ⁡ x
30 29 adantrr ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ y ∈ ℋ → A · op T ⁡ x = A ⋅ ℎ T ⁡ x
31 30 oveq1d ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ y ∈ ℋ → A · op T ⁡ x ⋅ ih y = A ⋅ ℎ T ⁡ x ⋅ ih y
32 id ⊢ y ∈ ℋ → y ∈ ℋ
33 homval ⊢ A ‾ ∈ ℂ ∧ adj h ⁡ T : ℋ ⟶ ℋ ∧ y ∈ ℋ → A ‾ · op adj h ⁡ T ⁡ y = A ‾ ⋅ ℎ adj h ⁡ T ⁡ y
34 4 7 32 33 syl3an ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h ∧ y ∈ ℋ → A ‾ · op adj h ⁡ T ⁡ y = A ‾ ⋅ ℎ adj h ⁡ T ⁡ y
35 34 3expa ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h ∧ y ∈ ℋ → A ‾ · op adj h ⁡ T ⁡ y = A ‾ ⋅ ℎ adj h ⁡ T ⁡ y
36 35 adantrl ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ y ∈ ℋ → A ‾ · op adj h ⁡ T ⁡ y = A ‾ ⋅ ℎ adj h ⁡ T ⁡ y
37 36 oveq2d ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih A ‾ · op adj h ⁡ T ⁡ y = x ⋅ ih A ‾ ⋅ ℎ adj h ⁡ T ⁡ y
38 26 31 37 3eqtr4d ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ y ∈ ℋ → A · op T ⁡ x ⋅ ih y = x ⋅ ih A ‾ · op adj h ⁡ T ⁡ y
39 38 ralrimivva ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h → ∀ x ∈ ℋ ∀ y ∈ ℋ A · op T ⁡ x ⋅ ih y = x ⋅ ih A ‾ · op adj h ⁡ T ⁡ y
40 adjeq ⊢ A · op T : ℋ ⟶ ℋ ∧ A ‾ · op adj h ⁡ T : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ A · op T ⁡ x ⋅ ih y = x ⋅ ih A ‾ · op adj h ⁡ T ⁡ y → adj h ⁡ A · op T = A ‾ · op adj h ⁡ T
41 3 9 39 40 syl3anc ⊢ A ∈ ℂ ∧ T ∈ dom ⁡ adj h → adj h ⁡ A · op T = A ‾ · op adj h ⁡ T