Metamath Proof Explorer

Theorem adjlnop

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

Ref Expression
Assertion adjlnop ( 𝑇 ∈ dom adjℎ → ( adjℎ ‘ 𝑇 ) ∈ LinOp )

Proof

Step Hyp Ref Expression
1 dmadjrn ⊢ ( 𝑇 ∈ dom adjℎ → ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ )
2 dmadjop ⊢ ( ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ → ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ )
3 1 2 syl ⊢ ( 𝑇 ∈ dom adjℎ → ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ )
4 simp2 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → 𝑤 ∈ ℋ )
5 adjcl ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑦 ∈ ℋ ) → ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ∈ ℋ )
6 hvmulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ∈ ℋ ) → ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ∈ ℋ )
7 5 6 sylan2 ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑇 ∈ dom adjℎ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ∈ ℋ )
8 7 an12s ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ∈ ℋ )
9 8 adantrr ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ∈ ℋ )
10 9 3adant2 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ∈ ℋ )
11 adjcl ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑧 ∈ ℋ ) → ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ∈ ℋ )
12 11 adantrl ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ∈ ℋ )
13 12 3adant2 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ∈ ℋ )
14 his7 ⊢ ( ( 𝑤 ∈ ℋ ∧ ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ∈ ℋ ∧ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ∈ ℋ ) → ( 𝑤 ·ih ( ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) ) = ( ( 𝑤 ·ih ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ) + ( 𝑤 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) ) )
15 4 10 13 14 syl3anc ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( 𝑤 ·ih ( ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) ) = ( ( 𝑤 ·ih ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ) + ( 𝑤 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) ) )
16 adj2 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑤 ) ·ih 𝑦 ) = ( 𝑤 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) )
17 16 3adant3l ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑇 ‘ 𝑤 ) ·ih 𝑦 ) = ( 𝑤 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) )
18 17 oveq2d ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( ( ∗ ‘ 𝑥 ) · ( ( 𝑇 ‘ 𝑤 ) ·ih 𝑦 ) ) = ( ( ∗ ‘ 𝑥 ) · ( 𝑤 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ) )
19 simp3l ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → 𝑥 ∈ ℂ )
20 dmadjop ⊢ ( 𝑇 ∈ dom adjℎ → 𝑇 : ℋ ⟶ ℋ )
21 20 ffvelcdmda ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ) → ( 𝑇 ‘ 𝑤 ) ∈ ℋ )
22 21 3adant3 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑇 ‘ 𝑤 ) ∈ ℋ )
23 simp3r ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → 𝑦 ∈ ℋ )
24 his5 ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑇 ‘ 𝑤 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑤 ) ·ih ( 𝑥 ·ℎ 𝑦 ) ) = ( ( ∗ ‘ 𝑥 ) · ( ( 𝑇 ‘ 𝑤 ) ·ih 𝑦 ) ) )
25 19 22 23 24 syl3anc ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑇 ‘ 𝑤 ) ·ih ( 𝑥 ·ℎ 𝑦 ) ) = ( ( ∗ ‘ 𝑥 ) · ( ( 𝑇 ‘ 𝑤 ) ·ih 𝑦 ) ) )
26 simp2 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → 𝑤 ∈ ℋ )
27 5 adantrl ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ∈ ℋ )
28 27 3adant2 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ∈ ℋ )
29 his5 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ ∧ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ∈ ℋ ) → ( 𝑤 ·ih ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ) = ( ( ∗ ‘ 𝑥 ) · ( 𝑤 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ) )
30 19 26 28 29 syl3anc ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑤 ·ih ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ) = ( ( ∗ ‘ 𝑥 ) · ( 𝑤 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ) )
31 18 25 30 3eqtr4d ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑇 ‘ 𝑤 ) ·ih ( 𝑥 ·ℎ 𝑦 ) ) = ( 𝑤 ·ih ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ) )
32 31 3adant3r ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( ( 𝑇 ‘ 𝑤 ) ·ih ( 𝑥 ·ℎ 𝑦 ) ) = ( 𝑤 ·ih ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ) )
33 adj2 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑤 ) ·ih 𝑧 ) = ( 𝑤 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) )
34 33 3adant3l ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( ( 𝑇 ‘ 𝑤 ) ·ih 𝑧 ) = ( 𝑤 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) )
35 32 34 oveq12d ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( ( ( 𝑇 ‘ 𝑤 ) ·ih ( 𝑥 ·ℎ 𝑦 ) ) + ( ( 𝑇 ‘ 𝑤 ) ·ih 𝑧 ) ) = ( ( 𝑤 ·ih ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ) + ( 𝑤 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) ) )
36 21 3adant3 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( 𝑇 ‘ 𝑤 ) ∈ ℋ )
37 hvmulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ )
38 37 adantr ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ )
39 38 3ad2ant3 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ )
40 simp3r ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → 𝑧 ∈ ℋ )
41 his7 ⊢ ( ( ( 𝑇 ‘ 𝑤 ) ∈ ℋ ∧ ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑤 ) ·ih ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( ( 𝑇 ‘ 𝑤 ) ·ih ( 𝑥 ·ℎ 𝑦 ) ) + ( ( 𝑇 ‘ 𝑤 ) ·ih 𝑧 ) ) )
42 36 39 40 41 syl3anc ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( ( 𝑇 ‘ 𝑤 ) ·ih ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( ( 𝑇 ‘ 𝑤 ) ·ih ( 𝑥 ·ℎ 𝑦 ) ) + ( ( 𝑇 ‘ 𝑤 ) ·ih 𝑧 ) ) )
43 hvaddcl ⊢ ( ( ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ∈ ℋ )
44 37 43 sylan ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ∈ ℋ )
45 adj2 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ∈ ℋ ) → ( ( 𝑇 ‘ 𝑤 ) ·ih ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( 𝑤 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ) )
46 44 45 syl3an3 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( ( 𝑇 ‘ 𝑤 ) ·ih ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( 𝑤 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ) )
47 42 46 eqtr3d ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( ( ( 𝑇 ‘ 𝑤 ) ·ih ( 𝑥 ·ℎ 𝑦 ) ) + ( ( 𝑇 ‘ 𝑤 ) ·ih 𝑧 ) ) = ( 𝑤 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ) )
48 15 35 47 3eqtr2rd ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑤 ∈ ℋ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( 𝑤 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ) = ( 𝑤 ·ih ( ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) ) )
49 48 3com23 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( 𝑤 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ) = ( 𝑤 ·ih ( ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) ) )
50 49 3expa ⊢ ( ( ( 𝑇 ∈ dom adjℎ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) ∧ 𝑤 ∈ ℋ ) → ( 𝑤 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ) = ( 𝑤 ·ih ( ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) ) )
51 50 ralrimiva ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ∀ 𝑤 ∈ ℋ ( 𝑤 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ) = ( 𝑤 ·ih ( ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) ) )
52 adjcl ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ∈ ℋ ) → ( ( adjℎ ‘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ∈ ℋ )
53 44 52 sylan2 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( ( adjℎ ‘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ∈ ℋ )
54 hvaddcl ⊢ ( ( ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ∈ ℋ ∧ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ∈ ℋ ) → ( ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) ∈ ℋ )
55 8 11 54 syl2an ⊢ ( ( ( 𝑇 ∈ dom adjℎ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ ( 𝑇 ∈ dom adjℎ ∧ 𝑧 ∈ ℋ ) ) → ( ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) ∈ ℋ )
56 55 anandis ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) ∈ ℋ )
57 hial2eq2 ⊢ ( ( ( ( adjℎ ‘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ∈ ℋ ∧ ( ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) ∈ ℋ ) → ( ∀ 𝑤 ∈ ℋ ( 𝑤 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ) = ( 𝑤 ·ih ( ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) ) ↔ ( ( adjℎ ‘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) ) )
58 53 56 57 syl2anc ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( ∀ 𝑤 ∈ ℋ ( 𝑤 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ) = ( 𝑤 ·ih ( ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) ) ↔ ( ( adjℎ ‘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) ) )
59 51 58 mpbid ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( ( adjℎ ‘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) )
60 59 exp32 ⊢ ( 𝑇 ∈ dom adjℎ → ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ( 𝑧 ∈ ℋ → ( ( adjℎ ‘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) ) ) )
61 60 ralrimdv ⊢ ( 𝑇 ∈ dom adjℎ → ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ∀ 𝑧 ∈ ℋ ( ( adjℎ ‘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) ) )
62 61 ralrimivv ⊢ ( 𝑇 ∈ dom adjℎ → ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( adjℎ ‘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) )
63 ellnop ⊢ ( ( adjℎ ‘ 𝑇 ) ∈ LinOp ↔ ( ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( adjℎ ‘ 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑧 ) ) ) )
64 3 62 63 sylanbrc ⊢ ( 𝑇 ∈ dom adjℎ → ( adjℎ ‘ 𝑇 ) ∈ LinOp )