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 = BaseSet U
lnoval.2 Y = BaseSet W
lnoval.3 G = + v U
lnoval.4 H = + v W
lnoval.5 R = 𝑠OLD U
lnoval.6 S = 𝑠OLD W
lnoval.7 L = U LnOp W
Assertion islno U NrmCVec W NrmCVec T L T : X Y x y X z X T x R y G z = x S T y H T z

Proof

Step Hyp Ref Expression
1 lnoval.1 X = BaseSet U
2 lnoval.2 Y = BaseSet W
3 lnoval.3 G = + v U
4 lnoval.4 H = + v W
5 lnoval.5 R = 𝑠OLD U
6 lnoval.6 S = 𝑠OLD W
7 lnoval.7 L = U LnOp W
8 1 2 3 4 5 6 7 lnoval U NrmCVec W NrmCVec L = w Y X | x y X z X w x R y G z = x S w y H w z
9 8 eleq2d U NrmCVec W NrmCVec T L T w Y X | x y X z X w x R y G z = x S w y H w z
10 fveq1 w = T w x R y G z = T x R y G z
11 fveq1 w = T w y = T y
12 11 oveq2d w = T x S w y = x S T y
13 fveq1 w = T w z = T z
14 12 13 oveq12d w = T x S w y H w z = x S T y H T z
15 10 14 eqeq12d w = T w x R y G z = x S w y H w z T x R y G z = x S T y H T z
16 15 2ralbidv w = T y X z X w x R y G z = x S w y H w z y X z X T x R y G z = x S T y H T z
17 16 ralbidv w = T x y X z X w x R y G z = x S w y H w z x y X z X T x R y G z = x S T y H T z
18 17 elrab T w Y X | x y X z X w x R y G z = x S w y H w z T Y X x y X z X T x R y G z = x S T y H T z
19 2 fvexi Y V
20 1 fvexi X V
21 19 20 elmap T Y X T : X Y
22 21 anbi1i T Y X x y X z X T x R y G z = x S T y H T z T : X Y x y X z X T x R y G z = x S T y H T z
23 18 22 bitri T w Y X | x y X z X w x R y G z = x S w y H w z T : X Y x y X z X T x R y G z = x S T y H T z
24 9 23 bitrdi U NrmCVec W NrmCVec T L T : X Y x y X z X T x R y G z = x S T y H T z