# Metamath Proof Explorer

## Theorem islno

Description: The predicate "is 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 islno ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left({T}\in {L}↔\left({T}:{X}⟶{Y}\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{T}\left({y}\right)\right){H}{T}\left({z}\right)\right)\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 lnoval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {L}=\left\{{w}\in \left({{Y}}^{{X}}\right)|\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{w}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{w}\left({y}\right)\right){H}{w}\left({z}\right)\right\}$
9 8 eleq2d ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left({T}\in {L}↔{T}\in \left\{{w}\in \left({{Y}}^{{X}}\right)|\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{w}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{w}\left({y}\right)\right){H}{w}\left({z}\right)\right\}\right)$
10 fveq1 ${⊢}{w}={T}\to {w}\left(\left({x}{R}{y}\right){G}{z}\right)={T}\left(\left({x}{R}{y}\right){G}{z}\right)$
11 fveq1 ${⊢}{w}={T}\to {w}\left({y}\right)={T}\left({y}\right)$
12 11 oveq2d ${⊢}{w}={T}\to {x}{S}{w}\left({y}\right)={x}{S}{T}\left({y}\right)$
13 fveq1 ${⊢}{w}={T}\to {w}\left({z}\right)={T}\left({z}\right)$
14 12 13 oveq12d ${⊢}{w}={T}\to \left({x}{S}{w}\left({y}\right)\right){H}{w}\left({z}\right)=\left({x}{S}{T}\left({y}\right)\right){H}{T}\left({z}\right)$
15 10 14 eqeq12d ${⊢}{w}={T}\to \left({w}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{w}\left({y}\right)\right){H}{w}\left({z}\right)↔{T}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{T}\left({y}\right)\right){H}{T}\left({z}\right)\right)$
16 15 2ralbidv ${⊢}{w}={T}\to \left(\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{w}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{w}\left({y}\right)\right){H}{w}\left({z}\right)↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{T}\left({y}\right)\right){H}{T}\left({z}\right)\right)$
17 16 ralbidv ${⊢}{w}={T}\to \left(\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{w}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{w}\left({y}\right)\right){H}{w}\left({z}\right)↔\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{T}\left({y}\right)\right){H}{T}\left({z}\right)\right)$
18 17 elrab ${⊢}{T}\in \left\{{w}\in \left({{Y}}^{{X}}\right)|\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{w}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{w}\left({y}\right)\right){H}{w}\left({z}\right)\right\}↔\left({T}\in \left({{Y}}^{{X}}\right)\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{T}\left({y}\right)\right){H}{T}\left({z}\right)\right)$
19 2 fvexi ${⊢}{Y}\in \mathrm{V}$
20 1 fvexi ${⊢}{X}\in \mathrm{V}$
21 19 20 elmap ${⊢}{T}\in \left({{Y}}^{{X}}\right)↔{T}:{X}⟶{Y}$
22 21 anbi1i ${⊢}\left({T}\in \left({{Y}}^{{X}}\right)\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{T}\left({y}\right)\right){H}{T}\left({z}\right)\right)↔\left({T}:{X}⟶{Y}\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{T}\left({y}\right)\right){H}{T}\left({z}\right)\right)$
23 18 22 bitri ${⊢}{T}\in \left\{{w}\in \left({{Y}}^{{X}}\right)|\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{w}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{w}\left({y}\right)\right){H}{w}\left({z}\right)\right\}↔\left({T}:{X}⟶{Y}\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{T}\left({y}\right)\right){H}{T}\left({z}\right)\right)$
24 9 23 syl6bb ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left({T}\in {L}↔\left({T}:{X}⟶{Y}\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{T}\left({y}\right)\right){H}{T}\left({z}\right)\right)\right)$