Metamath Proof Explorer

Theorem lfli

Description: Property of a linear functional. ( lnfnli analog.) (Contributed by NM, 16-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 lfli 
|- ( ( W e. Z /\ G e. F /\ ( R e. K /\ X e. V /\ 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 islfl 
 |-  ( W e. Z -> ( 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 ) ) ) ) )
10 9 simplbda 
 |-  ( ( W e. Z /\ G e. F ) -> A. r e. K A. x e. V A. y e. V ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) )
11 10 3adant3 
 |-  ( ( W e. Z /\ G e. F /\ ( R e. K /\ X e. V /\ Y e. V ) ) -> A. r e. K A. x e. V A. y e. V ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) )
12 oveq1 
 |-  ( r = R -> ( r .x. x ) = ( R .x. x ) )
13 12 fvoveq1d 
 |-  ( r = R -> ( G ` ( ( r .x. x ) .+ y ) ) = ( G ` ( ( R .x. x ) .+ y ) ) )
14 oveq1 
 |-  ( r = R -> ( r .X. ( G ` x ) ) = ( R .X. ( G ` x ) ) )
15 14 oveq1d 
 |-  ( r = R -> ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) = ( ( R .X. ( G ` x ) ) .+^ ( G ` y ) ) )
16 13 15 eqeq12d 
 |-  ( r = R -> ( ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) <-> ( G ` ( ( R .x. x ) .+ y ) ) = ( ( R .X. ( G ` x ) ) .+^ ( G ` y ) ) ) )
17 oveq2 
 |-  ( x = X -> ( R .x. x ) = ( R .x. X ) )
18 17 fvoveq1d 
 |-  ( x = X -> ( G ` ( ( R .x. x ) .+ y ) ) = ( G ` ( ( R .x. X ) .+ y ) ) )
19 fveq2 
 |-  ( x = X -> ( G ` x ) = ( G ` X ) )
20 19 oveq2d 
 |-  ( x = X -> ( R .X. ( G ` x ) ) = ( R .X. ( G ` X ) ) )
21 20 oveq1d 
 |-  ( x = X -> ( ( R .X. ( G ` x ) ) .+^ ( G ` y ) ) = ( ( R .X. ( G ` X ) ) .+^ ( G ` y ) ) )
22 18 21 eqeq12d 
 |-  ( x = X -> ( ( G ` ( ( R .x. x ) .+ y ) ) = ( ( R .X. ( G ` x ) ) .+^ ( G ` y ) ) <-> ( G ` ( ( R .x. X ) .+ y ) ) = ( ( R .X. ( G ` X ) ) .+^ ( G ` y ) ) ) )
23 oveq2 
 |-  ( y = Y -> ( ( R .x. X ) .+ y ) = ( ( R .x. X ) .+ Y ) )
24 23 fveq2d 
 |-  ( y = Y -> ( G ` ( ( R .x. X ) .+ y ) ) = ( G ` ( ( R .x. X ) .+ Y ) ) )
25 fveq2 
 |-  ( y = Y -> ( G ` y ) = ( G ` Y ) )
26 25 oveq2d 
 |-  ( y = Y -> ( ( R .X. ( G ` X ) ) .+^ ( G ` y ) ) = ( ( R .X. ( G ` X ) ) .+^ ( G ` Y ) ) )
27 24 26 eqeq12d 
 |-  ( y = Y -> ( ( G ` ( ( R .x. X ) .+ y ) ) = ( ( R .X. ( G ` X ) ) .+^ ( G ` y ) ) <-> ( G ` ( ( R .x. X ) .+ Y ) ) = ( ( R .X. ( G ` X ) ) .+^ ( G ` Y ) ) ) )
28 16 22 27 rspc3v 
 |-  ( ( R e. K /\ X e. V /\ Y e. 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 ` ( ( R .x. X ) .+ Y ) ) = ( ( R .X. ( G ` X ) ) .+^ ( G ` Y ) ) ) )
29 28 3ad2ant3 
 |-  ( ( W e. Z /\ G e. F /\ ( R e. K /\ X e. V /\ Y e. 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 ` ( ( R .x. X ) .+ Y ) ) = ( ( R .X. ( G ` X ) ) .+^ ( G ` Y ) ) ) )
30 11 29 mpd 
 |-  ( ( W e. Z /\ G e. F /\ ( R e. K /\ X e. V /\ Y e. V ) ) -> ( G ` ( ( R .x. X ) .+ Y ) ) = ( ( R .X. ( G ` X ) ) .+^ ( G ` Y ) ) )