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 ⊢ T ∈ LinOp
Assertion lnopmi ⊢ A ∈ ℂ → A · op T ∈ LinOp

Proof

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