Metamath Proof Explorer

Theorem lnopmi

Description: The scalar product of a linear operator is a linear operator. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypothesis lnopm.1 ⊢ 𝑇 ∈ LinOp
Assertion lnopmi ( 𝐴 ∈ ℂ → ( 𝐴 ·op 𝑇 ) ∈ LinOp )

Proof

Step Hyp Ref Expression
1 lnopm.1 ⊢ 𝑇 ∈ LinOp
2 1 lnopfi ⊢ 𝑇 : ℋ ⟶ ℋ
3 homulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝐴 ·op 𝑇 ) : ℋ ⟶ ℋ )
4 2 3 mpan2 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ·op 𝑇 ) : ℋ ⟶ ℋ )
5 hvmulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ )
6 hvaddcl ⊢ ( ( ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ∈ ℋ )
7 5 6 sylan ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ∈ ℋ )
8 homval ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ∧ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ∈ ℋ ) → ( ( 𝐴 ·op 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( 𝐴 ·ℎ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ) )
9 2 8 mp3an2 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ∈ ℋ ) → ( ( 𝐴 ·op 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( 𝐴 ·ℎ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ) )
10 7 9 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( ( 𝐴 ·op 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( 𝐴 ·ℎ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ) )
11 id ⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
12 2 ffvelcdmi ⊢ ( 𝑦 ∈ ℋ → ( 𝑇 ‘ 𝑦 ) ∈ ℋ )
13 hvmulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑇 ‘ 𝑦 ) ∈ ℋ ) → ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ∈ ℋ )
14 12 13 sylan2 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ∈ ℋ )
15 2 ffvelcdmi ⊢ ( 𝑧 ∈ ℋ → ( 𝑇 ‘ 𝑧 ) ∈ ℋ )
16 ax-hvdistr1 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑧 ) ∈ ℋ ) → ( 𝐴 ·ℎ ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ) = ( ( 𝐴 ·ℎ ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ) +ℎ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑧 ) ) ) )
17 11 14 15 16 syl3an ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( 𝐴 ·ℎ ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ) = ( ( 𝐴 ·ℎ ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ) +ℎ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑧 ) ) ) )
18 17 3expb ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( 𝐴 ·ℎ ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ) = ( ( 𝐴 ·ℎ ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ) +ℎ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑧 ) ) ) )
19 1 lnopli ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) )
20 19 3expa ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) )
21 20 oveq2d ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( 𝐴 ·ℎ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ) = ( 𝐴 ·ℎ ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ) )
22 21 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( 𝐴 ·ℎ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ) = ( 𝐴 ·ℎ ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ) )
23 homval ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝐴 ·op 𝑇 ) ‘ 𝑦 ) = ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑦 ) ) )
24 2 23 mp3an2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ( ( 𝐴 ·op 𝑇 ) ‘ 𝑦 ) = ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑦 ) ) )
25 24 adantrl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝐴 ·op 𝑇 ) ‘ 𝑦 ) = ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑦 ) ) )
26 25 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ℎ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑦 ) ) = ( 𝑥 ·ℎ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ) )
27 hvmulcom ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ ( 𝑇 ‘ 𝑦 ) ∈ ℋ ) → ( 𝐴 ·ℎ ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ) = ( 𝑥 ·ℎ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ) )
28 12 27 syl3an3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ( 𝐴 ·ℎ ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ) = ( 𝑥 ·ℎ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ) )
29 28 3expb ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( 𝐴 ·ℎ ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ) = ( 𝑥 ·ℎ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ) )
30 26 29 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ℎ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑦 ) ) = ( 𝐴 ·ℎ ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ) )
31 homval ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝐴 ·op 𝑇 ) ‘ 𝑧 ) = ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑧 ) ) )
32 2 31 mp3an2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℋ ) → ( ( 𝐴 ·op 𝑇 ) ‘ 𝑧 ) = ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑧 ) ) )
33 30 32 oveqan12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℋ ) ) → ( ( 𝑥 ·ℎ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑧 ) ) = ( ( 𝐴 ·ℎ ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ) +ℎ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑧 ) ) ) )
34 33 anandis ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( ( 𝑥 ·ℎ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑧 ) ) = ( ( 𝐴 ·ℎ ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ) +ℎ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑧 ) ) ) )
35 18 22 34 3eqtr4rd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( ( 𝑥 ·ℎ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑧 ) ) = ( 𝐴 ·ℎ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) ) )
36 10 35 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ) → ( ( 𝐴 ·op 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑧 ) ) )
37 36 exp32 ⊢ ( 𝐴 ∈ ℂ → ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ( 𝑧 ∈ ℋ → ( ( 𝐴 ·op 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑧 ) ) ) ) )
38 37 ralrimdv ⊢ ( 𝐴 ∈ ℂ → ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ∀ 𝑧 ∈ ℋ ( ( 𝐴 ·op 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑧 ) ) ) )
39 38 ralrimivv ⊢ ( 𝐴 ∈ ℂ → ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝐴 ·op 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑧 ) ) )
40 ellnop ⊢ ( ( 𝐴 ·op 𝑇 ) ∈ LinOp ↔ ( ( 𝐴 ·op 𝑇 ) : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝐴 ·op 𝑇 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑦 ) ) +ℎ ( ( 𝐴 ·op 𝑇 ) ‘ 𝑧 ) ) ) )
41 4 39 40 sylanbrc ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ·op 𝑇 ) ∈ LinOp )