# Metamath Proof Explorer

## Theorem lnomul

Description: Scalar multiplication property of a linear operator. (Contributed by NM, 5-Dec-2007) (Revised by Mario Carneiro, 19-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses lnomul.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
lnomul.5 ${⊢}{R}={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
lnomul.6 ${⊢}{S}={\cdot }_{\mathrm{𝑠OLD}}\left({W}\right)$
lnomul.7 ${⊢}{L}={U}\mathrm{LnOp}{W}$
Assertion lnomul ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge \left({A}\in ℂ\wedge {B}\in {X}\right)\right)\to {T}\left({A}{R}{B}\right)={A}{S}{T}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 lnomul.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 lnomul.5 ${⊢}{R}={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
3 lnomul.6 ${⊢}{S}={\cdot }_{\mathrm{𝑠OLD}}\left({W}\right)$
4 lnomul.7 ${⊢}{L}={U}\mathrm{LnOp}{W}$
5 simpl ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge \left({A}\in ℂ\wedge {B}\in {X}\right)\right)\to \left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)$
6 simprl ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge \left({A}\in ℂ\wedge {B}\in {X}\right)\right)\to {A}\in ℂ$
7 simprr ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge \left({A}\in ℂ\wedge {B}\in {X}\right)\right)\to {B}\in {X}$
8 simpl1 ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge \left({A}\in ℂ\wedge {B}\in {X}\right)\right)\to {U}\in \mathrm{NrmCVec}$
9 eqid ${⊢}{0}_{\mathrm{vec}}\left({U}\right)={0}_{\mathrm{vec}}\left({U}\right)$
10 1 9 nvzcl ${⊢}{U}\in \mathrm{NrmCVec}\to {0}_{\mathrm{vec}}\left({U}\right)\in {X}$
11 8 10 syl ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge \left({A}\in ℂ\wedge {B}\in {X}\right)\right)\to {0}_{\mathrm{vec}}\left({U}\right)\in {X}$
12 eqid ${⊢}\mathrm{BaseSet}\left({W}\right)=\mathrm{BaseSet}\left({W}\right)$
13 eqid ${⊢}{+}_{v}\left({U}\right)={+}_{v}\left({U}\right)$
14 eqid ${⊢}{+}_{v}\left({W}\right)={+}_{v}\left({W}\right)$
15 1 12 13 14 2 3 4 lnolin ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge \left({A}\in ℂ\wedge {B}\in {X}\wedge {0}_{\mathrm{vec}}\left({U}\right)\in {X}\right)\right)\to {T}\left(\left({A}{R}{B}\right){+}_{v}\left({U}\right){0}_{\mathrm{vec}}\left({U}\right)\right)=\left({A}{S}{T}\left({B}\right)\right){+}_{v}\left({W}\right){T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)$
16 5 6 7 11 15 syl13anc ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge \left({A}\in ℂ\wedge {B}\in {X}\right)\right)\to {T}\left(\left({A}{R}{B}\right){+}_{v}\left({U}\right){0}_{\mathrm{vec}}\left({U}\right)\right)=\left({A}{S}{T}\left({B}\right)\right){+}_{v}\left({W}\right){T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)$
17 1 2 nvscl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\to {A}{R}{B}\in {X}$
18 8 6 7 17 syl3anc ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge \left({A}\in ℂ\wedge {B}\in {X}\right)\right)\to {A}{R}{B}\in {X}$
19 1 13 9 nv0rid ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}{R}{B}\in {X}\right)\to \left({A}{R}{B}\right){+}_{v}\left({U}\right){0}_{\mathrm{vec}}\left({U}\right)={A}{R}{B}$
20 8 18 19 syl2anc ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge \left({A}\in ℂ\wedge {B}\in {X}\right)\right)\to \left({A}{R}{B}\right){+}_{v}\left({U}\right){0}_{\mathrm{vec}}\left({U}\right)={A}{R}{B}$
21 20 fveq2d ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge \left({A}\in ℂ\wedge {B}\in {X}\right)\right)\to {T}\left(\left({A}{R}{B}\right){+}_{v}\left({U}\right){0}_{\mathrm{vec}}\left({U}\right)\right)={T}\left({A}{R}{B}\right)$
22 eqid ${⊢}{0}_{\mathrm{vec}}\left({W}\right)={0}_{\mathrm{vec}}\left({W}\right)$
23 1 12 9 22 4 lno0 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to {T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)={0}_{\mathrm{vec}}\left({W}\right)$
24 23 oveq2d ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to \left({A}{S}{T}\left({B}\right)\right){+}_{v}\left({W}\right){T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)=\left({A}{S}{T}\left({B}\right)\right){+}_{v}\left({W}\right){0}_{\mathrm{vec}}\left({W}\right)$
25 24 adantr ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge \left({A}\in ℂ\wedge {B}\in {X}\right)\right)\to \left({A}{S}{T}\left({B}\right)\right){+}_{v}\left({W}\right){T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)=\left({A}{S}{T}\left({B}\right)\right){+}_{v}\left({W}\right){0}_{\mathrm{vec}}\left({W}\right)$
26 simpl2 ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge \left({A}\in ℂ\wedge {B}\in {X}\right)\right)\to {W}\in \mathrm{NrmCVec}$
27 1 12 4 lnof ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to {T}:{X}⟶\mathrm{BaseSet}\left({W}\right)$
28 27 adantr ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge \left({A}\in ℂ\wedge {B}\in {X}\right)\right)\to {T}:{X}⟶\mathrm{BaseSet}\left({W}\right)$
29 28 7 ffvelrnd ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge \left({A}\in ℂ\wedge {B}\in {X}\right)\right)\to {T}\left({B}\right)\in \mathrm{BaseSet}\left({W}\right)$
30 12 3 nvscl ${⊢}\left({W}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {T}\left({B}\right)\in \mathrm{BaseSet}\left({W}\right)\right)\to {A}{S}{T}\left({B}\right)\in \mathrm{BaseSet}\left({W}\right)$
31 26 6 29 30 syl3anc ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge \left({A}\in ℂ\wedge {B}\in {X}\right)\right)\to {A}{S}{T}\left({B}\right)\in \mathrm{BaseSet}\left({W}\right)$
32 12 14 22 nv0rid ${⊢}\left({W}\in \mathrm{NrmCVec}\wedge {A}{S}{T}\left({B}\right)\in \mathrm{BaseSet}\left({W}\right)\right)\to \left({A}{S}{T}\left({B}\right)\right){+}_{v}\left({W}\right){0}_{\mathrm{vec}}\left({W}\right)={A}{S}{T}\left({B}\right)$
33 26 31 32 syl2anc ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge \left({A}\in ℂ\wedge {B}\in {X}\right)\right)\to \left({A}{S}{T}\left({B}\right)\right){+}_{v}\left({W}\right){0}_{\mathrm{vec}}\left({W}\right)={A}{S}{T}\left({B}\right)$
34 25 33 eqtrd ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge \left({A}\in ℂ\wedge {B}\in {X}\right)\right)\to \left({A}{S}{T}\left({B}\right)\right){+}_{v}\left({W}\right){T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)={A}{S}{T}\left({B}\right)$
35 16 21 34 3eqtr3d ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge \left({A}\in ℂ\wedge {B}\in {X}\right)\right)\to {T}\left({A}{R}{B}\right)={A}{S}{T}\left({B}\right)$