Metamath Proof Explorer

Theorem lflvscl

Description: Closure of a scalar product with a functional. Note that this is the scalar product for a right vector space with the scalar after the vector; reversing these fails closure. (Contributed by NM, 9-Oct-2014) (Revised by Mario Carneiro, 22-Apr-2015)

Ref Expression
Hypotheses lflsccl.v 
|- V = ( Base ` W )
lflsccl.d 
|- D = ( Scalar ` W )
lflsccl.k 
|- K = ( Base ` D )
lflsccl.t 
|- .x. = ( .r ` D )
lflsccl.f 
|- F = ( LFnl ` W )
lflsccl.w 
|- ( ph -> W e. LMod )
lflsccl.g 
|- ( ph -> G e. F )
lflsccl.r 
|- ( ph -> R e. K )
Assertion lflvscl 
|- ( ph -> ( G oF .x. ( V X. { R } ) ) e. F )

Proof

Step Hyp Ref Expression
1 lflsccl.v 
 |-  V = ( Base ` W )
2 lflsccl.d 
 |-  D = ( Scalar ` W )
3 lflsccl.k 
 |-  K = ( Base ` D )
4 lflsccl.t 
 |-  .x. = ( .r ` D )
5 lflsccl.f 
 |-  F = ( LFnl ` W )
6 lflsccl.w 
 |-  ( ph -> W e. LMod )
7 lflsccl.g 
 |-  ( ph -> G e. F )
8 lflsccl.r 
 |-  ( ph -> R e. K )
9 1 a1i 
 |-  ( ph -> V = ( Base ` W ) )
10 eqidd 
 |-  ( ph -> ( +g ` W ) = ( +g ` W ) )
11 2 a1i 
 |-  ( ph -> D = ( Scalar ` W ) )
12 eqidd 
 |-  ( ph -> ( .s ` W ) = ( .s ` W ) )
13 3 a1i 
 |-  ( ph -> K = ( Base ` D ) )
14 eqidd 
 |-  ( ph -> ( +g ` D ) = ( +g ` D ) )
15 4 a1i 
 |-  ( ph -> .x. = ( .r ` D ) )
16 5 a1i 
 |-  ( ph -> F = ( LFnl ` W ) )
17 2 lmodring 
 |-  ( W e. LMod -> D e. Ring )
18 6 17 syl 
 |-  ( ph -> D e. Ring )
19 3 4 ringcl 
 |-  ( ( D e. Ring /\ x e. K /\ y e. K ) -> ( x .x. y ) e. K )
20 19 3expb 
 |-  ( ( D e. Ring /\ ( x e. K /\ y e. K ) ) -> ( x .x. y ) e. K )
21 18 20 sylan 
 |-  ( ( ph /\ ( x e. K /\ y e. K ) ) -> ( x .x. y ) e. K )
22 2 3 1 5 lflf 
 |-  ( ( W e. LMod /\ G e. F ) -> G : V --> K )
23 6 7 22 syl2anc 
 |-  ( ph -> G : V --> K )
24 fconst6g 
 |-  ( R e. K -> ( V X. { R } ) : V --> K )
25 8 24 syl 
 |-  ( ph -> ( V X. { R } ) : V --> K )
26 1 fvexi 
 |-  V e. _V
27 26 a1i 
 |-  ( ph -> V e. _V )
28 inidm 
 |-  ( V i^i V ) = V
29 21 23 25 27 27 28 off 
 |-  ( ph -> ( G oF .x. ( V X. { R } ) ) : V --> K )
30 6 adantr 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> W e. LMod )
31 7 adantr 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> G e. F )
32 simpr1 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> r e. K )
33 simpr2 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> x e. V )
34 simpr3 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> y e. V )
35 eqid 
 |-  ( +g ` W ) = ( +g ` W )
36 eqid 
 |-  ( .s ` W ) = ( .s ` W )
37 eqid 
 |-  ( +g ` D ) = ( +g ` D )
38 1 35 2 36 3 37 4 5 lfli 
 |-  ( ( W e. LMod /\ G e. F /\ ( r e. K /\ x e. V /\ y e. V ) ) -> ( G ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( r .x. ( G ` x ) ) ( +g ` D ) ( G ` y ) ) )
39 30 31 32 33 34 38 syl113anc 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> ( G ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( r .x. ( G ` x ) ) ( +g ` D ) ( G ` y ) ) )
40 39 oveq1d 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> ( ( G ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) .x. R ) = ( ( ( r .x. ( G ` x ) ) ( +g ` D ) ( G ` y ) ) .x. R ) )
41 18 adantr 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> D e. Ring )
42 2 3 1 5 lflcl 
 |-  ( ( W e. LMod /\ G e. F /\ x e. V ) -> ( G ` x ) e. K )
43 30 31 33 42 syl3anc 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> ( G ` x ) e. K )
44 3 4 ringcl 
 |-  ( ( D e. Ring /\ r e. K /\ ( G ` x ) e. K ) -> ( r .x. ( G ` x ) ) e. K )
45 41 32 43 44 syl3anc 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> ( r .x. ( G ` x ) ) e. K )
46 2 3 1 5 lflcl 
 |-  ( ( W e. LMod /\ G e. F /\ y e. V ) -> ( G ` y ) e. K )
47 30 31 34 46 syl3anc 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> ( G ` y ) e. K )
48 8 adantr 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> R e. K )
49 3 37 4 ringdir 
 |-  ( ( D e. Ring /\ ( ( r .x. ( G ` x ) ) e. K /\ ( G ` y ) e. K /\ R e. K ) ) -> ( ( ( r .x. ( G ` x ) ) ( +g ` D ) ( G ` y ) ) .x. R ) = ( ( ( r .x. ( G ` x ) ) .x. R ) ( +g ` D ) ( ( G ` y ) .x. R ) ) )
50 41 45 47 48 49 syl13anc 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> ( ( ( r .x. ( G ` x ) ) ( +g ` D ) ( G ` y ) ) .x. R ) = ( ( ( r .x. ( G ` x ) ) .x. R ) ( +g ` D ) ( ( G ` y ) .x. R ) ) )
51 3 4 ringass 
 |-  ( ( D e. Ring /\ ( r e. K /\ ( G ` x ) e. K /\ R e. K ) ) -> ( ( r .x. ( G ` x ) ) .x. R ) = ( r .x. ( ( G ` x ) .x. R ) ) )
52 41 32 43 48 51 syl13anc 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> ( ( r .x. ( G ` x ) ) .x. R ) = ( r .x. ( ( G ` x ) .x. R ) ) )
53 52 oveq1d 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> ( ( ( r .x. ( G ` x ) ) .x. R ) ( +g ` D ) ( ( G ` y ) .x. R ) ) = ( ( r .x. ( ( G ` x ) .x. R ) ) ( +g ` D ) ( ( G ` y ) .x. R ) ) )
54 40 50 53 3eqtrd 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> ( ( G ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) .x. R ) = ( ( r .x. ( ( G ` x ) .x. R ) ) ( +g ` D ) ( ( G ` y ) .x. R ) ) )
55 1 2 36 3 lmodvscl 
 |-  ( ( W e. LMod /\ r e. K /\ x e. V ) -> ( r ( .s ` W ) x ) e. V )
56 30 32 33 55 syl3anc 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> ( r ( .s ` W ) x ) e. V )
57 1 35 lmodvacl 
 |-  ( ( W e. LMod /\ ( r ( .s ` W ) x ) e. V /\ y e. V ) -> ( ( r ( .s ` W ) x ) ( +g ` W ) y ) e. V )
58 30 56 34 57 syl3anc 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> ( ( r ( .s ` W ) x ) ( +g ` W ) y ) e. V )
59 23 ffnd 
 |-  ( ph -> G Fn V )
60 eqidd 
 |-  ( ( ph /\ ( ( r ( .s ` W ) x ) ( +g ` W ) y ) e. V ) -> ( G ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( G ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) )
61 27 8 59 60 ofc2 
 |-  ( ( ph /\ ( ( r ( .s ` W ) x ) ( +g ` W ) y ) e. V ) -> ( ( G oF .x. ( V X. { R } ) ) ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( G ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) .x. R ) )
62 58 61 syldan 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> ( ( G oF .x. ( V X. { R } ) ) ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( G ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) .x. R ) )
63 eqidd 
 |-  ( ( ph /\ x e. V ) -> ( G ` x ) = ( G ` x ) )
64 27 8 59 63 ofc2 
 |-  ( ( ph /\ x e. V ) -> ( ( G oF .x. ( V X. { R } ) ) ` x ) = ( ( G ` x ) .x. R ) )
65 33 64 syldan 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> ( ( G oF .x. ( V X. { R } ) ) ` x ) = ( ( G ` x ) .x. R ) )
66 65 oveq2d 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> ( r .x. ( ( G oF .x. ( V X. { R } ) ) ` x ) ) = ( r .x. ( ( G ` x ) .x. R ) ) )
67 eqidd 
 |-  ( ( ph /\ y e. V ) -> ( G ` y ) = ( G ` y ) )
68 27 8 59 67 ofc2 
 |-  ( ( ph /\ y e. V ) -> ( ( G oF .x. ( V X. { R } ) ) ` y ) = ( ( G ` y ) .x. R ) )
69 34 68 syldan 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> ( ( G oF .x. ( V X. { R } ) ) ` y ) = ( ( G ` y ) .x. R ) )
70 66 69 oveq12d 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> ( ( r .x. ( ( G oF .x. ( V X. { R } ) ) ` x ) ) ( +g ` D ) ( ( G oF .x. ( V X. { R } ) ) ` y ) ) = ( ( r .x. ( ( G ` x ) .x. R ) ) ( +g ` D ) ( ( G ` y ) .x. R ) ) )
71 54 62 70 3eqtr4d 
 |-  ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> ( ( G oF .x. ( V X. { R } ) ) ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( r .x. ( ( G oF .x. ( V X. { R } ) ) ` x ) ) ( +g ` D ) ( ( G oF .x. ( V X. { R } ) ) ` y ) ) )
72 9 10 11 12 13 14 15 16 29 71 6 islfld 
 |-  ( ph -> ( G oF .x. ( V X. { R } ) ) e. F )