Metamath Proof Explorer

Theorem islfld

Description: Properties that determine a linear functional. TODO: use this in place of islfl when it shortens the proof. (Contributed by NM, 19-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 islfld.v 
 |-  ( ph -> V = ( Base ` W ) )
2 islfld.a 
 |-  ( ph -> .+ = ( +g ` W ) )
3 islfld.d 
 |-  ( ph -> D = ( Scalar ` W ) )
4 islfld.s 
 |-  ( ph -> .x. = ( .s ` W ) )
5 islfld.k 
 |-  ( ph -> K = ( Base ` D ) )
6 islfld.p 
 |-  ( ph -> .+^ = ( +g ` D ) )
7 islfld.t 
 |-  ( ph -> .X. = ( .r ` D ) )
8 islfld.f 
 |-  ( ph -> F = ( LFnl ` W ) )
9 islfld.u 
 |-  ( ph -> G : V --> K )
10 islfld.l 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) )
11 islfld.w 
 |-  ( ph -> W e. X )
12 3 fveq2d 
 |-  ( ph -> ( Base ` D ) = ( Base ` ( Scalar ` W ) ) )
13 5 12 eqtrd 
 |-  ( ph -> K = ( Base ` ( Scalar ` W ) ) )
14 1 13 feq23d 
 |-  ( ph -> ( G : V --> K <-> G : ( Base ` W ) --> ( Base ` ( Scalar ` W ) ) ) )
15 9 14 mpbid 
 |-  ( ph -> G : ( Base ` W ) --> ( Base ` ( Scalar ` W ) ) )
16 10 ralrimivvva 
 |-  ( ph -> A. r e. K A. x e. V A. y e. V ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) )
17 4 oveqd 
 |-  ( ph -> ( r .x. x ) = ( r ( .s ` W ) x ) )
18 eqidd 
 |-  ( ph -> y = y )
19 2 17 18 oveq123d 
 |-  ( ph -> ( ( r .x. x ) .+ y ) = ( ( r ( .s ` W ) x ) ( +g ` W ) y ) )
20 19 fveq2d 
 |-  ( ph -> ( G ` ( ( r .x. x ) .+ y ) ) = ( G ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) )
21 3 fveq2d 
 |-  ( ph -> ( +g ` D ) = ( +g ` ( Scalar ` W ) ) )
22 6 21 eqtrd 
 |-  ( ph -> .+^ = ( +g ` ( Scalar ` W ) ) )
23 3 fveq2d 
 |-  ( ph -> ( .r ` D ) = ( .r ` ( Scalar ` W ) ) )
24 7 23 eqtrd 
 |-  ( ph -> .X. = ( .r ` ( Scalar ` W ) ) )
25 24 oveqd 
 |-  ( ph -> ( r .X. ( G ` x ) ) = ( r ( .r ` ( Scalar ` W ) ) ( G ` x ) ) )
26 eqidd 
 |-  ( ph -> ( G ` y ) = ( G ` y ) )
27 22 25 26 oveq123d 
 |-  ( ph -> ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) = ( ( r ( .r ` ( Scalar ` W ) ) ( G ` x ) ) ( +g ` ( Scalar ` W ) ) ( G ` y ) ) )
28 20 27 eqeq12d 
 |-  ( ph -> ( ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) <-> ( G ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( r ( .r ` ( Scalar ` W ) ) ( G ` x ) ) ( +g ` ( Scalar ` W ) ) ( G ` y ) ) ) )
29 1 28 raleqbidv 
 |-  ( ph -> ( A. y e. V ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) <-> A. y e. ( Base ` W ) ( G ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( r ( .r ` ( Scalar ` W ) ) ( G ` x ) ) ( +g ` ( Scalar ` W ) ) ( G ` y ) ) ) )
30 1 29 raleqbidv 
 |-  ( ph -> ( A. x e. V A. y e. V ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) <-> A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( G ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( r ( .r ` ( Scalar ` W ) ) ( G ` x ) ) ( +g ` ( Scalar ` W ) ) ( G ` y ) ) ) )
31 13 30 raleqbidv 
 |-  ( ph -> ( A. r e. K A. x e. V A. y e. V ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) <-> A. r e. ( Base ` ( Scalar ` W ) ) A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( G ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( r ( .r ` ( Scalar ` W ) ) ( G ` x ) ) ( +g ` ( Scalar ` W ) ) ( G ` y ) ) ) )
32 16 31 mpbid 
 |-  ( ph -> A. r e. ( Base ` ( Scalar ` W ) ) A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( G ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( r ( .r ` ( Scalar ` W ) ) ( G ` x ) ) ( +g ` ( Scalar ` W ) ) ( G ` y ) ) )
33 eqid 
 |-  ( Base ` W ) = ( Base ` W )
34 eqid 
 |-  ( +g ` W ) = ( +g ` W )
35 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
36 eqid 
 |-  ( .s ` W ) = ( .s ` W )
37 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
38 eqid 
 |-  ( +g ` ( Scalar ` W ) ) = ( +g ` ( Scalar ` W ) )
39 eqid 
 |-  ( .r ` ( Scalar ` W ) ) = ( .r ` ( Scalar ` W ) )
40 eqid 
 |-  ( LFnl ` W ) = ( LFnl ` W )
41 33 34 35 36 37 38 39 40 islfl 
 |-  ( W e. X -> ( G e. ( LFnl ` W ) <-> ( G : ( Base ` W ) --> ( Base ` ( Scalar ` W ) ) /\ A. r e. ( Base ` ( Scalar ` W ) ) A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( G ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( r ( .r ` ( Scalar ` W ) ) ( G ` x ) ) ( +g ` ( Scalar ` W ) ) ( G ` y ) ) ) ) )
42 41 biimpar 
 |-  ( ( W e. X /\ ( G : ( Base ` W ) --> ( Base ` ( Scalar ` W ) ) /\ A. r e. ( Base ` ( Scalar ` W ) ) A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( G ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( r ( .r ` ( Scalar ` W ) ) ( G ` x ) ) ( +g ` ( Scalar ` W ) ) ( G ` y ) ) ) ) -> G e. ( LFnl ` W ) )
43 11 15 32 42 syl12anc 
 |-  ( ph -> G e. ( LFnl ` W ) )
44 43 8 eleqtrrd 
 |-  ( ph -> G e. F )