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 = ( .sOLD ` U )
lnoval.6
|- S = ( .sOLD ` W )
lnoval.7
|- L = ( U LnOp W )
Assertion islno
|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( T e. L <-> ( T : X --> Y /\ A. x e. CC A. y e. X A. z e. 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 = ( .sOLD ` U )
6 lnoval.6
 |-  S = ( .sOLD ` W )
7 lnoval.7
 |-  L = ( U LnOp W )
8 1 2 3 4 5 6 7 lnoval
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> L = { w e. ( Y ^m X ) | A. x e. CC A. y e. X A. z e. X ( w ` ( ( x R y ) G z ) ) = ( ( x S ( w ` y ) ) H ( w ` z ) ) } )
9 8 eleq2d
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( T e. L <-> T e. { w e. ( Y ^m X ) | A. x e. CC A. y e. X A. z e. 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 -> ( A. y e. X A. z e. X ( w ` ( ( x R y ) G z ) ) = ( ( x S ( w ` y ) ) H ( w ` z ) ) <-> A. y e. X A. z e. X ( T ` ( ( x R y ) G z ) ) = ( ( x S ( T ` y ) ) H ( T ` z ) ) ) )
17 16 ralbidv
 |-  ( w = T -> ( A. x e. CC A. y e. X A. z e. X ( w ` ( ( x R y ) G z ) ) = ( ( x S ( w ` y ) ) H ( w ` z ) ) <-> A. x e. CC A. y e. X A. z e. X ( T ` ( ( x R y ) G z ) ) = ( ( x S ( T ` y ) ) H ( T ` z ) ) ) )
18 17 elrab
 |-  ( T e. { w e. ( Y ^m X ) | A. x e. CC A. y e. X A. z e. X ( w ` ( ( x R y ) G z ) ) = ( ( x S ( w ` y ) ) H ( w ` z ) ) } <-> ( T e. ( Y ^m X ) /\ A. x e. CC A. y e. X A. z e. X ( T ` ( ( x R y ) G z ) ) = ( ( x S ( T ` y ) ) H ( T ` z ) ) ) )
19 2 fvexi
 |-  Y e. _V
20 1 fvexi
 |-  X e. _V
21 19 20 elmap
 |-  ( T e. ( Y ^m X ) <-> T : X --> Y )
22 21 anbi1i
 |-  ( ( T e. ( Y ^m X ) /\ A. x e. CC A. y e. X A. z e. X ( T ` ( ( x R y ) G z ) ) = ( ( x S ( T ` y ) ) H ( T ` z ) ) ) <-> ( T : X --> Y /\ A. x e. CC A. y e. X A. z e. X ( T ` ( ( x R y ) G z ) ) = ( ( x S ( T ` y ) ) H ( T ` z ) ) ) )
23 18 22 bitri
 |-  ( T e. { w e. ( Y ^m X ) | A. x e. CC A. y e. X A. z e. X ( w ` ( ( x R y ) G z ) ) = ( ( x S ( w ` y ) ) H ( w ` z ) ) } <-> ( T : X --> Y /\ A. x e. CC A. y e. X A. z e. X ( T ` ( ( x R y ) G z ) ) = ( ( x S ( T ` y ) ) H ( T ` z ) ) ) )
24 9 23 bitrdi
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( T e. L <-> ( T : X --> Y /\ A. x e. CC A. y e. X A. z e. X ( T ` ( ( x R y ) G z ) ) = ( ( x S ( T ` y ) ) H ( T ` z ) ) ) ) )