# Metamath Proof Explorer

## Theorem lnolin

Description: Basic linearity property of a linear operator. (Contributed by NM, 4-Dec-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses lnoval.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
lnoval.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
lnoval.3 ${⊢}{G}={+}_{v}\left({U}\right)$
lnoval.4 ${⊢}{H}={+}_{v}\left({W}\right)$
lnoval.5 ${⊢}{R}={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
lnoval.6 ${⊢}{S}={\cdot }_{\mathrm{𝑠OLD}}\left({W}\right)$
lnoval.7 ${⊢}{L}={U}\mathrm{LnOp}{W}$
Assertion 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 {C}\in {X}\right)\right)\to {T}\left(\left({A}{R}{B}\right){G}{C}\right)=\left({A}{S}{T}\left({B}\right)\right){H}{T}\left({C}\right)$

### Proof

Step Hyp Ref Expression
1 lnoval.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 lnoval.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
3 lnoval.3 ${⊢}{G}={+}_{v}\left({U}\right)$
4 lnoval.4 ${⊢}{H}={+}_{v}\left({W}\right)$
5 lnoval.5 ${⊢}{R}={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
6 lnoval.6 ${⊢}{S}={\cdot }_{\mathrm{𝑠OLD}}\left({W}\right)$
7 lnoval.7 ${⊢}{L}={U}\mathrm{LnOp}{W}$
8 1 2 3 4 5 6 7 islno ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left({T}\in {L}↔\left({T}:{X}⟶{Y}\wedge \forall {u}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {w}\in {X}\phantom{\rule{.4em}{0ex}}\forall {t}\in {X}\phantom{\rule{.4em}{0ex}}{T}\left(\left({u}{R}{w}\right){G}{t}\right)=\left({u}{S}{T}\left({w}\right)\right){H}{T}\left({t}\right)\right)\right)$
9 8 biimp3a ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to \left({T}:{X}⟶{Y}\wedge \forall {u}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {w}\in {X}\phantom{\rule{.4em}{0ex}}\forall {t}\in {X}\phantom{\rule{.4em}{0ex}}{T}\left(\left({u}{R}{w}\right){G}{t}\right)=\left({u}{S}{T}\left({w}\right)\right){H}{T}\left({t}\right)\right)$
10 9 simprd ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to \forall {u}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {w}\in {X}\phantom{\rule{.4em}{0ex}}\forall {t}\in {X}\phantom{\rule{.4em}{0ex}}{T}\left(\left({u}{R}{w}\right){G}{t}\right)=\left({u}{S}{T}\left({w}\right)\right){H}{T}\left({t}\right)$
11 oveq1 ${⊢}{u}={A}\to {u}{R}{w}={A}{R}{w}$
12 11 fvoveq1d ${⊢}{u}={A}\to {T}\left(\left({u}{R}{w}\right){G}{t}\right)={T}\left(\left({A}{R}{w}\right){G}{t}\right)$
13 oveq1 ${⊢}{u}={A}\to {u}{S}{T}\left({w}\right)={A}{S}{T}\left({w}\right)$
14 13 oveq1d ${⊢}{u}={A}\to \left({u}{S}{T}\left({w}\right)\right){H}{T}\left({t}\right)=\left({A}{S}{T}\left({w}\right)\right){H}{T}\left({t}\right)$
15 12 14 eqeq12d ${⊢}{u}={A}\to \left({T}\left(\left({u}{R}{w}\right){G}{t}\right)=\left({u}{S}{T}\left({w}\right)\right){H}{T}\left({t}\right)↔{T}\left(\left({A}{R}{w}\right){G}{t}\right)=\left({A}{S}{T}\left({w}\right)\right){H}{T}\left({t}\right)\right)$
16 oveq2 ${⊢}{w}={B}\to {A}{R}{w}={A}{R}{B}$
17 16 fvoveq1d ${⊢}{w}={B}\to {T}\left(\left({A}{R}{w}\right){G}{t}\right)={T}\left(\left({A}{R}{B}\right){G}{t}\right)$
18 fveq2 ${⊢}{w}={B}\to {T}\left({w}\right)={T}\left({B}\right)$
19 18 oveq2d ${⊢}{w}={B}\to {A}{S}{T}\left({w}\right)={A}{S}{T}\left({B}\right)$
20 19 oveq1d ${⊢}{w}={B}\to \left({A}{S}{T}\left({w}\right)\right){H}{T}\left({t}\right)=\left({A}{S}{T}\left({B}\right)\right){H}{T}\left({t}\right)$
21 17 20 eqeq12d ${⊢}{w}={B}\to \left({T}\left(\left({A}{R}{w}\right){G}{t}\right)=\left({A}{S}{T}\left({w}\right)\right){H}{T}\left({t}\right)↔{T}\left(\left({A}{R}{B}\right){G}{t}\right)=\left({A}{S}{T}\left({B}\right)\right){H}{T}\left({t}\right)\right)$
22 oveq2 ${⊢}{t}={C}\to \left({A}{R}{B}\right){G}{t}=\left({A}{R}{B}\right){G}{C}$
23 22 fveq2d ${⊢}{t}={C}\to {T}\left(\left({A}{R}{B}\right){G}{t}\right)={T}\left(\left({A}{R}{B}\right){G}{C}\right)$
24 fveq2 ${⊢}{t}={C}\to {T}\left({t}\right)={T}\left({C}\right)$
25 24 oveq2d ${⊢}{t}={C}\to \left({A}{S}{T}\left({B}\right)\right){H}{T}\left({t}\right)=\left({A}{S}{T}\left({B}\right)\right){H}{T}\left({C}\right)$
26 23 25 eqeq12d ${⊢}{t}={C}\to \left({T}\left(\left({A}{R}{B}\right){G}{t}\right)=\left({A}{S}{T}\left({B}\right)\right){H}{T}\left({t}\right)↔{T}\left(\left({A}{R}{B}\right){G}{C}\right)=\left({A}{S}{T}\left({B}\right)\right){H}{T}\left({C}\right)\right)$
27 15 21 26 rspc3v ${⊢}\left({A}\in ℂ\wedge {B}\in {X}\wedge {C}\in {X}\right)\to \left(\forall {u}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {w}\in {X}\phantom{\rule{.4em}{0ex}}\forall {t}\in {X}\phantom{\rule{.4em}{0ex}}{T}\left(\left({u}{R}{w}\right){G}{t}\right)=\left({u}{S}{T}\left({w}\right)\right){H}{T}\left({t}\right)\to {T}\left(\left({A}{R}{B}\right){G}{C}\right)=\left({A}{S}{T}\left({B}\right)\right){H}{T}\left({C}\right)\right)$
28 10 27 mpan9 ${⊢}\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 {C}\in {X}\right)\right)\to {T}\left(\left({A}{R}{B}\right){G}{C}\right)=\left({A}{S}{T}\left({B}\right)\right){H}{T}\left({C}\right)$