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 ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ dom adjℎ ) → ( adjℎ ‘ ( 𝐴 ·op 𝑇 ) ) = ( ( ∗ ‘ 𝐴 ) ·op ( adjℎ ‘ 𝑇 ) ) )

Proof

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