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