# 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}\in \mathrm{LinOp}$
Assertion lnopmi ${⊢}{A}\in ℂ\to {A}{·}_{\mathrm{op}}{T}\in \mathrm{LinOp}$

### Proof

Step Hyp Ref Expression
1 lnopm.1 ${⊢}{T}\in \mathrm{LinOp}$
2 1 lnopfi ${⊢}{T}:ℋ⟶ℋ$
3 homulcl ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
4 2 3 mpan2 ${⊢}{A}\in ℂ\to \left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
5 hvmulcl ${⊢}\left({x}\in ℂ\wedge {y}\in ℋ\right)\to {x}{\cdot }_{ℎ}{y}\in ℋ$
6 hvaddcl ${⊢}\left({x}{\cdot }_{ℎ}{y}\in ℋ\wedge {z}\in ℋ\right)\to \left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\in ℋ$
7 5 6 sylan ${⊢}\left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\to \left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\in ℋ$
8 homval ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge \left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={A}{\cdot }_{ℎ}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)$
9 2 8 mp3an2 ${⊢}\left({A}\in ℂ\wedge \left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={A}{\cdot }_{ℎ}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)$
10 7 9 sylan2 ${⊢}\left({A}\in ℂ\wedge \left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={A}{\cdot }_{ℎ}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)$
11 id ${⊢}{A}\in ℂ\to {A}\in ℂ$
12 2 ffvelrni ${⊢}{y}\in ℋ\to {T}\left({y}\right)\in ℋ$
13 hvmulcl ${⊢}\left({x}\in ℂ\wedge {T}\left({y}\right)\in ℋ\right)\to {x}{\cdot }_{ℎ}{T}\left({y}\right)\in ℋ$
14 12 13 sylan2 ${⊢}\left({x}\in ℂ\wedge {y}\in ℋ\right)\to {x}{\cdot }_{ℎ}{T}\left({y}\right)\in ℋ$
15 2 ffvelrni ${⊢}{z}\in ℋ\to {T}\left({z}\right)\in ℋ$
16 ax-hvdistr1 ${⊢}\left({A}\in ℂ\wedge {x}{\cdot }_{ℎ}{T}\left({y}\right)\in ℋ\wedge {T}\left({z}\right)\in ℋ\right)\to {A}{\cdot }_{ℎ}\left(\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right)=\left({A}{\cdot }_{ℎ}\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right)\right){+}_{ℎ}\left({A}{\cdot }_{ℎ}{T}\left({z}\right)\right)$
17 11 14 15 16 syl3an ${⊢}\left({A}\in ℂ\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\to {A}{\cdot }_{ℎ}\left(\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right)=\left({A}{\cdot }_{ℎ}\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right)\right){+}_{ℎ}\left({A}{\cdot }_{ℎ}{T}\left({z}\right)\right)$
18 17 3expb ${⊢}\left({A}\in ℂ\wedge \left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\right)\to {A}{\cdot }_{ℎ}\left(\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right)=\left({A}{\cdot }_{ℎ}\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right)\right){+}_{ℎ}\left({A}{\cdot }_{ℎ}{T}\left({z}\right)\right)$
19 1 lnopli ${⊢}\left({x}\in ℂ\wedge {y}\in ℋ\wedge {z}\in ℋ\right)\to {T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)$
20 19 3expa ${⊢}\left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\to {T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)$
21 20 oveq2d ${⊢}\left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\to {A}{\cdot }_{ℎ}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={A}{\cdot }_{ℎ}\left(\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right)$
22 21 adantl ${⊢}\left({A}\in ℂ\wedge \left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\right)\to {A}{\cdot }_{ℎ}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={A}{\cdot }_{ℎ}\left(\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right)$
23 homval ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({y}\right)={A}{\cdot }_{ℎ}{T}\left({y}\right)$
24 2 23 mp3an2 ${⊢}\left({A}\in ℂ\wedge {y}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({y}\right)={A}{\cdot }_{ℎ}{T}\left({y}\right)$
25 24 adantrl ${⊢}\left({A}\in ℂ\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({y}\right)={A}{\cdot }_{ℎ}{T}\left({y}\right)$
26 25 oveq2d ${⊢}\left({A}\in ℂ\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{ℎ}\left({A}{·}_{\mathrm{op}}{T}\right)\left({y}\right)={x}{\cdot }_{ℎ}\left({A}{\cdot }_{ℎ}{T}\left({y}\right)\right)$
27 hvmulcom ${⊢}\left({A}\in ℂ\wedge {x}\in ℂ\wedge {T}\left({y}\right)\in ℋ\right)\to {A}{\cdot }_{ℎ}\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right)={x}{\cdot }_{ℎ}\left({A}{\cdot }_{ℎ}{T}\left({y}\right)\right)$
28 12 27 syl3an3 ${⊢}\left({A}\in ℂ\wedge {x}\in ℂ\wedge {y}\in ℋ\right)\to {A}{\cdot }_{ℎ}\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right)={x}{\cdot }_{ℎ}\left({A}{\cdot }_{ℎ}{T}\left({y}\right)\right)$
29 28 3expb ${⊢}\left({A}\in ℂ\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\to {A}{\cdot }_{ℎ}\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right)={x}{\cdot }_{ℎ}\left({A}{\cdot }_{ℎ}{T}\left({y}\right)\right)$
30 26 29 eqtr4d ${⊢}\left({A}\in ℂ\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{ℎ}\left({A}{·}_{\mathrm{op}}{T}\right)\left({y}\right)={A}{\cdot }_{ℎ}\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right)$
31 homval ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {z}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({z}\right)={A}{\cdot }_{ℎ}{T}\left({z}\right)$
32 2 31 mp3an2 ${⊢}\left({A}\in ℂ\wedge {z}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({z}\right)={A}{\cdot }_{ℎ}{T}\left({z}\right)$
33 30 32 oveqan12d ${⊢}\left(\left({A}\in ℂ\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge \left({A}\in ℂ\wedge {z}\in ℋ\right)\right)\to \left({x}{\cdot }_{ℎ}\left({A}{·}_{\mathrm{op}}{T}\right)\left({y}\right)\right){+}_{ℎ}\left({A}{·}_{\mathrm{op}}{T}\right)\left({z}\right)=\left({A}{\cdot }_{ℎ}\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right)\right){+}_{ℎ}\left({A}{\cdot }_{ℎ}{T}\left({z}\right)\right)$
34 33 anandis ${⊢}\left({A}\in ℂ\wedge \left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\right)\to \left({x}{\cdot }_{ℎ}\left({A}{·}_{\mathrm{op}}{T}\right)\left({y}\right)\right){+}_{ℎ}\left({A}{·}_{\mathrm{op}}{T}\right)\left({z}\right)=\left({A}{\cdot }_{ℎ}\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right)\right){+}_{ℎ}\left({A}{\cdot }_{ℎ}{T}\left({z}\right)\right)$
35 18 22 34 3eqtr4rd ${⊢}\left({A}\in ℂ\wedge \left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\right)\to \left({x}{\cdot }_{ℎ}\left({A}{·}_{\mathrm{op}}{T}\right)\left({y}\right)\right){+}_{ℎ}\left({A}{·}_{\mathrm{op}}{T}\right)\left({z}\right)={A}{\cdot }_{ℎ}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)$
36 10 35 eqtr4d ${⊢}\left({A}\in ℂ\wedge \left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}\left({A}{·}_{\mathrm{op}}{T}\right)\left({y}\right)\right){+}_{ℎ}\left({A}{·}_{\mathrm{op}}{T}\right)\left({z}\right)$
37 36 exp32 ${⊢}{A}\in ℂ\to \left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\to \left({z}\in ℋ\to \left({A}{·}_{\mathrm{op}}{T}\right)\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}\left({A}{·}_{\mathrm{op}}{T}\right)\left({y}\right)\right){+}_{ℎ}\left({A}{·}_{\mathrm{op}}{T}\right)\left({z}\right)\right)\right)$
38 37 ralrimdv ${⊢}{A}\in ℂ\to \left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\to \forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({A}{·}_{\mathrm{op}}{T}\right)\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}\left({A}{·}_{\mathrm{op}}{T}\right)\left({y}\right)\right){+}_{ℎ}\left({A}{·}_{\mathrm{op}}{T}\right)\left({z}\right)\right)$
39 38 ralrimivv ${⊢}{A}\in ℂ\to \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({A}{·}_{\mathrm{op}}{T}\right)\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}\left({A}{·}_{\mathrm{op}}{T}\right)\left({y}\right)\right){+}_{ℎ}\left({A}{·}_{\mathrm{op}}{T}\right)\left({z}\right)$
40 ellnop ${⊢}{A}{·}_{\mathrm{op}}{T}\in \mathrm{LinOp}↔\left(\left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({A}{·}_{\mathrm{op}}{T}\right)\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}\left({A}{·}_{\mathrm{op}}{T}\right)\left({y}\right)\right){+}_{ℎ}\left({A}{·}_{\mathrm{op}}{T}\right)\left({z}\right)\right)$
41 4 39 40 sylanbrc ${⊢}{A}\in ℂ\to {A}{·}_{\mathrm{op}}{T}\in \mathrm{LinOp}$