This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem unoplin

Description: A unitary operator is linear. Theorem in AkhiezerGlazman p. 72. (Contributed by NM, 22-Jan-2006) (New usage is discouraged.)

Ref Expression
Assertion unoplin ( 𝑇 ∈ UniOp → 𝑇 ∈ LinOp )

Proof

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