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 ffvelrnda ( ( 𝑇 ∈ 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 )