Metamath Proof Explorer

Theorem hmoplin

Description: A Hermitian operator is linear. (Contributed by NM, 24-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion hmoplin ( 𝑇 ∈ HrmOp → 𝑇 ∈ LinOp )

Proof

Step Hyp Ref Expression
1 hmopf ⊢ ( 𝑇 ∈ HrmOp → 𝑇 : ℋ ⟶ ℋ )
2 simplll ⊢ ( ( ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → 𝑇 ∈ HrmOp )
3 hvmulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ )
4 hvaddcl ⊢ ( ( ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ∈ ℋ )
5 3 4 sylan ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ∈ ℋ )
6 5 adantll ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ∈ ℋ )
7 6 adantr ⊢ ( ( ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ∈ ℋ )
8 simpr ⊢ ( ( ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → 𝑤 ∈ ℋ )
9 hmop ⊢ ( ( 𝑇 ∈ HrmOp ∧ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ·ih ( 𝑇 ‘ 𝑤 ) ) = ( ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ·ih 𝑤 ) )
10 9 eqcomd ⊢ ( ( 𝑇 ∈ HrmOp ∧ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ·ih 𝑤 ) = ( ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ·ih ( 𝑇 ‘ 𝑤 ) ) )
11 2 7 8 10 syl3anc ⊢ ( ( ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ·ih 𝑤 ) = ( ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ·ih ( 𝑇 ‘ 𝑤 ) ) )
12 simprl ⊢ ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → 𝑥 ∈ ℂ )
13 12 ad2antrr ⊢ ( ( ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → 𝑥 ∈ ℂ )
14 simprr ⊢ ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → 𝑦 ∈ ℋ )
15 14 ad2antrr ⊢ ( ( ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → 𝑦 ∈ ℋ )
16 simplr ⊢ ( ( ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → 𝑧 ∈ ℋ )
17 1 ffvelcdmda ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑤 ∈ ℋ ) → ( 𝑇 ‘ 𝑤 ) ∈ ℋ )
18 17 adantlr ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑧 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( 𝑇 ‘ 𝑤 ) ∈ ℋ )
19 18 adantllr ⊢ ( ( ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( 𝑇 ‘ 𝑤 ) ∈ ℋ )
20 hiassdi ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ ( 𝑇 ‘ 𝑤 ) ∈ ℋ ) ) → ( ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ·ih ( 𝑇 ‘ 𝑤 ) ) = ( ( 𝑥 · ( 𝑦 ·ih ( 𝑇 ‘ 𝑤 ) ) ) + ( 𝑧 ·ih ( 𝑇 ‘ 𝑤 ) ) ) )
21 13 15 16 19 20 syl22anc ⊢ ( ( ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ·ih ( 𝑇 ‘ 𝑤 ) ) = ( ( 𝑥 · ( 𝑦 ·ih ( 𝑇 ‘ 𝑤 ) ) ) + ( 𝑧 ·ih ( 𝑇 ‘ 𝑤 ) ) ) )
22 1 ffvelcdmda ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑦 ∈ ℋ ) → ( 𝑇 ‘ 𝑦 ) ∈ ℋ )
23 22 adantrl ⊢ ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑇 ‘ 𝑦 ) ∈ ℋ )
24 23 ad2antrr ⊢ ( ( ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( 𝑇 ‘ 𝑦 ) ∈ ℋ )
25 1 ffvelcdmda ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑧 ∈ ℋ ) → ( 𝑇 ‘ 𝑧 ) ∈ ℋ )
26 25 adantr ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑧 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( 𝑇 ‘ 𝑧 ) ∈ ℋ )
27 26 adantllr ⊢ ( ( ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( 𝑇 ‘ 𝑧 ) ∈ ℋ )
28 hiassdi ⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( 𝑇 ‘ 𝑦 ) ∈ ℋ ) ∧ ( ( 𝑇 ‘ 𝑧 ) ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ·ih 𝑤 ) = ( ( 𝑥 · ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑤 ) ) + ( ( 𝑇 ‘ 𝑧 ) ·ih 𝑤 ) ) )
29 13 24 27 8 28 syl22anc ⊢ ( ( ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ·ih 𝑤 ) = ( ( 𝑥 · ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑤 ) ) + ( ( 𝑇 ‘ 𝑧 ) ·ih 𝑤 ) ) )
30 hmop ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( 𝑦 ·ih ( 𝑇 ‘ 𝑤 ) ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑤 ) )
31 30 eqcomd ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑤 ) = ( 𝑦 ·ih ( 𝑇 ‘ 𝑤 ) ) )
32 31 3expa ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑦 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑤 ) = ( 𝑦 ·ih ( 𝑇 ‘ 𝑤 ) ) )
33 32 oveq2d ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑦 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( 𝑥 · ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑤 ) ) = ( 𝑥 · ( 𝑦 ·ih ( 𝑇 ‘ 𝑤 ) ) ) )
34 33 adantlrl ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑤 ∈ ℋ ) → ( 𝑥 · ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑤 ) ) = ( 𝑥 · ( 𝑦 ·ih ( 𝑇 ‘ 𝑤 ) ) ) )
35 34 adantlr ⊢ ( ( ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( 𝑥 · ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑤 ) ) = ( 𝑥 · ( 𝑦 ·ih ( 𝑇 ‘ 𝑤 ) ) ) )
36 hmop ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( 𝑧 ·ih ( 𝑇 ‘ 𝑤 ) ) = ( ( 𝑇 ‘ 𝑧 ) ·ih 𝑤 ) )
37 36 eqcomd ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑧 ) ·ih 𝑤 ) = ( 𝑧 ·ih ( 𝑇 ‘ 𝑤 ) ) )
38 37 3expa ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑧 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑧 ) ·ih 𝑤 ) = ( 𝑧 ·ih ( 𝑇 ‘ 𝑤 ) ) )
39 38 adantllr ⊢ ( ( ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑧 ) ·ih 𝑤 ) = ( 𝑧 ·ih ( 𝑇 ‘ 𝑤 ) ) )
40 35 39 oveq12d ⊢ ( ( ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ( 𝑥 · ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑤 ) ) + ( ( 𝑇 ‘ 𝑧 ) ·ih 𝑤 ) ) = ( ( 𝑥 · ( 𝑦 ·ih ( 𝑇 ‘ 𝑤 ) ) ) + ( 𝑧 ·ih ( 𝑇 ‘ 𝑤 ) ) ) )
41 29 40 eqtr2d ⊢ ( ( ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ( 𝑥 · ( 𝑦 ·ih ( 𝑇 ‘ 𝑤 ) ) ) + ( 𝑧 ·ih ( 𝑇 ‘ 𝑤 ) ) ) = ( ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ·ih 𝑤 ) )
42 11 21 41 3eqtrd ⊢ ( ( ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ·ih 𝑤 ) = ( ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ·ih 𝑤 ) )
43 42 ralrimiva ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) → ∀ 𝑤 ∈ ℋ ( ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ·ih 𝑤 ) = ( ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ·ih 𝑤 ) )
44 ffvelcdm ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ∈ ℋ )
45 5 44 sylan2 ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ∈ ℋ )
46 45 anassrs ⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ∈ ℋ )
47 ffvelcdm ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑇 ‘ 𝑦 ) ∈ ℋ )
48 hvmulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑇 ‘ 𝑦 ) ∈ ℋ ) → ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ∈ ℋ )
49 47 48 sylan2 ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ∈ ℋ )
50 49 an12s ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ∈ ℋ )
51 50 adantr ⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) → ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ∈ ℋ )
52 ffvelcdm ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑇 ‘ 𝑧 ) ∈ ℋ )
53 52 adantlr ⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) → ( 𝑇 ‘ 𝑧 ) ∈ ℋ )
54 hvaddcl ⊢ ( ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑧 ) ∈ ℋ ) → ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ∈ ℋ )
55 51 53 54 syl2anc ⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ∈ ℋ )
56 hial2eq ⊢ ( ( ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ∈ ℋ ∧ ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ∈ ℋ ) → ( ∀ 𝑤 ∈ ℋ ( ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ·ih 𝑤 ) = ( ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ·ih 𝑤 ) ↔ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ) )
57 46 55 56 syl2anc ⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) → ( ∀ 𝑤 ∈ ℋ ( ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ·ih 𝑤 ) = ( ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ·ih 𝑤 ) ↔ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ) )
58 1 57 sylanl1 ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) → ( ∀ 𝑤 ∈ ℋ ( ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ·ih 𝑤 ) = ( ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ·ih 𝑤 ) ↔ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ) )
59 43 58 mpbid ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) )
60 59 ralrimiva ⊢ ( ( 𝑇 ∈ HrmOp ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ∀ 𝑧 ∈ ℋ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) )
61 60 ralrimivva ⊢ ( 𝑇 ∈ HrmOp → ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) )
62 ellnop ⊢ ( 𝑇 ∈ LinOp ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ) )
63 1 61 62 sylanbrc ⊢ ( 𝑇 ∈ HrmOp → 𝑇 ∈ LinOp )