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 syl6bb 
 |-  ( ( 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 ) ) ) ) )