This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem islfl

Description: The predicate "is a linear functional". (Contributed by NM, 15-Apr-2014)

Ref Expression
Hypotheses lflset.v 
|- V = ( Base ` W )
lflset.a 
|- .+ = ( +g ` W )
lflset.d 
|- D = ( Scalar ` W )
lflset.s 
|- .x. = ( .s ` W )
lflset.k 
|- K = ( Base ` D )
lflset.p 
|- .+^ = ( +g ` D )
lflset.t 
|- .X. = ( .r ` D )
lflset.f 
|- F = ( LFnl ` W )
Assertion islfl 
|- ( W e. X -> ( G e. F <-> ( G : V --> K /\ A. r e. K A. x e. V A. y e. V ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lflset.v 
 |-  V = ( Base ` W )
2 lflset.a 
 |-  .+ = ( +g ` W )
3 lflset.d 
 |-  D = ( Scalar ` W )
4 lflset.s 
 |-  .x. = ( .s ` W )
5 lflset.k 
 |-  K = ( Base ` D )
6 lflset.p 
 |-  .+^ = ( +g ` D )
7 lflset.t 
 |-  .X. = ( .r ` D )
8 lflset.f 
 |-  F = ( LFnl ` W )
9 1 2 3 4 5 6 7 8 lflset 
 |-  ( W e. X -> F = { f e. ( K ^m V ) | A. r e. K A. x e. V A. y e. V ( f ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( f ` x ) ) .+^ ( f ` y ) ) } )
10 9 eleq2d 
 |-  ( W e. X -> ( G e. F <-> G e. { f e. ( K ^m V ) | A. r e. K A. x e. V A. y e. V ( f ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( f ` x ) ) .+^ ( f ` y ) ) } ) )
11 fveq1 
 |-  ( f = G -> ( f ` ( ( r .x. x ) .+ y ) ) = ( G ` ( ( r .x. x ) .+ y ) ) )
12 fveq1 
 |-  ( f = G -> ( f ` x ) = ( G ` x ) )
13 12 oveq2d 
 |-  ( f = G -> ( r .X. ( f ` x ) ) = ( r .X. ( G ` x ) ) )
14 fveq1 
 |-  ( f = G -> ( f ` y ) = ( G ` y ) )
15 13 14 oveq12d 
 |-  ( f = G -> ( ( r .X. ( f ` x ) ) .+^ ( f ` y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) )
16 11 15 eqeq12d 
 |-  ( f = G -> ( ( f ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( f ` x ) ) .+^ ( f ` y ) ) <-> ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) ) )
17 16 2ralbidv 
 |-  ( f = G -> ( A. x e. V A. y e. V ( f ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( f ` x ) ) .+^ ( f ` y ) ) <-> A. x e. V A. y e. V ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) ) )
18 17 ralbidv 
 |-  ( f = G -> ( A. r e. K A. x e. V A. y e. V ( f ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( f ` x ) ) .+^ ( f ` y ) ) <-> A. r e. K A. x e. V A. y e. V ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) ) )
19 18 elrab 
 |-  ( G e. { f e. ( K ^m V ) | A. r e. K A. x e. V A. y e. V ( f ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( f ` x ) ) .+^ ( f ` y ) ) } <-> ( G e. ( K ^m V ) /\ A. r e. K A. x e. V A. y e. V ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) ) )
20 5 fvexi 
 |-  K e. _V
21 1 fvexi 
 |-  V e. _V
22 20 21 elmap 
 |-  ( G e. ( K ^m V ) <-> G : V --> K )
23 22 anbi1i 
 |-  ( ( G e. ( K ^m V ) /\ A. r e. K A. x e. V A. y e. V ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) ) <-> ( G : V --> K /\ A. r e. K A. x e. V A. y e. V ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) ) )
24 19 23 bitri 
 |-  ( G e. { f e. ( K ^m V ) | A. r e. K A. x e. V A. y e. V ( f ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( f ` x ) ) .+^ ( f ` y ) ) } <-> ( G : V --> K /\ A. r e. K A. x e. V A. y e. V ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) ) )
25 10 24 bitrdi 
 |-  ( W e. X -> ( G e. F <-> ( G : V --> K /\ A. r e. K A. x e. V A. y e. V ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) ) ) )