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·opT∈LinOp

Proof

Step Hyp Ref Expression
1 lnopm.1 ⊢T∈LinOp
2 1 lnopfi ⊢T:ℋ⟶ℋ
3 homulcl ⊢A∈ℂ∧T:ℋ⟶ℋ→A·opT:ℋ⟶ℋ
4 2 3 mpan2 ⊢A∈ℂ→A·opT:ℋ⟶ℋ
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·opT⁡x⋅ℎy+ℎz=A⋅ℎT⁡x⋅ℎy+ℎz
9 2 8 mp3an2 ⊢A∈ℂ∧x⋅ℎy+ℎz∈ℋ→A·opT⁡x⋅ℎy+ℎz=A⋅ℎT⁡x⋅ℎy+ℎz
10 7 9 sylan2 ⊢A∈ℂ∧x∈ℂ∧y∈ℋ∧z∈ℋ→A·opT⁡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·opT⁡y=A⋅ℎT⁡y
24 2 23 mp3an2 ⊢A∈ℂ∧y∈ℋ→A·opT⁡y=A⋅ℎT⁡y
25 24 adantrl ⊢A∈ℂ∧x∈ℂ∧y∈ℋ→A·opT⁡y=A⋅ℎT⁡y
26 25 oveq2d ⊢A∈ℂ∧x∈ℂ∧y∈ℋ→x⋅ℎA·opT⁡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·opT⁡y=A⋅ℎx⋅ℎT⁡y
31 homval ⊢A∈ℂ∧T:ℋ⟶ℋ∧z∈ℋ→A·opT⁡z=A⋅ℎT⁡z
32 2 31 mp3an2 ⊢A∈ℂ∧z∈ℋ→A·opT⁡z=A⋅ℎT⁡z
33 30 32 oveqan12d ⊢A∈ℂ∧x∈ℂ∧y∈ℋ∧A∈ℂ∧z∈ℋ→x⋅ℎA·opT⁡y+ℎA·opT⁡z=A⋅ℎx⋅ℎT⁡y+ℎA⋅ℎT⁡z
34 33 anandis ⊢A∈ℂ∧x∈ℂ∧y∈ℋ∧z∈ℋ→x⋅ℎA·opT⁡y+ℎA·opT⁡z=A⋅ℎx⋅ℎT⁡y+ℎA⋅ℎT⁡z
35 18 22 34 3eqtr4rd ⊢A∈ℂ∧x∈ℂ∧y∈ℋ∧z∈ℋ→x⋅ℎA·opT⁡y+ℎA·opT⁡z=A⋅ℎT⁡x⋅ℎy+ℎz
36 10 35 eqtr4d ⊢A∈ℂ∧x∈ℂ∧y∈ℋ∧z∈ℋ→A·opT⁡x⋅ℎy+ℎz=x⋅ℎA·opT⁡y+ℎA·opT⁡z
37 36 exp32 ⊢A∈ℂ→x∈ℂ∧y∈ℋ→z∈ℋ→A·opT⁡x⋅ℎy+ℎz=x⋅ℎA·opT⁡y+ℎA·opT⁡z
38 37 ralrimdv ⊢A∈ℂ→x∈ℂ∧y∈ℋ→∀z∈ℋA·opT⁡x⋅ℎy+ℎz=x⋅ℎA·opT⁡y+ℎA·opT⁡z
39 38 ralrimivv ⊢A∈ℂ→∀x∈ℂ∀y∈ℋ∀z∈ℋA·opT⁡x⋅ℎy+ℎz=x⋅ℎA·opT⁡y+ℎA·opT⁡z
40 ellnop ⊢A·opT∈LinOp↔A·opT:ℋ⟶ℋ∧∀x∈ℂ∀y∈ℋ∀z∈ℋA·opT⁡x⋅ℎy+ℎz=x⋅ℎA·opT⁡y+ℎA·opT⁡z
41 4 39 40 sylanbrc ⊢A∈ℂ→A·opT∈LinOp