Metamath Proof Explorer

Theorem lflnegcl

Description: Closure of the negative of a functional. (This is specialized for the purpose of proving ldualgrp , and we do not define a general operation here.) (Contributed by NM, 22-Oct-2014)

Ref Expression
Hypotheses lflnegcl.v 
|- V = ( Base ` W )
lflnegcl.r 
|- R = ( Scalar ` W )
lflnegcl.i 
|- I = ( invg ` R )
lflnegcl.n 
|- N = ( x e. V |-> ( I ` ( G ` x ) ) )
lflnegcl.f 
|- F = ( LFnl ` W )
lflnegcl.w 
|- ( ph -> W e. LMod )
lflnegcl.g 
|- ( ph -> G e. F )
Assertion lflnegcl 
|- ( ph -> N e. F )

Proof

Step Hyp Ref Expression
1 lflnegcl.v 
 |-  V = ( Base ` W )
2 lflnegcl.r 
 |-  R = ( Scalar ` W )
3 lflnegcl.i 
 |-  I = ( invg ` R )
4 lflnegcl.n 
 |-  N = ( x e. V |-> ( I ` ( G ` x ) ) )
5 lflnegcl.f 
 |-  F = ( LFnl ` W )
6 lflnegcl.w 
 |-  ( ph -> W e. LMod )
7 lflnegcl.g 
 |-  ( ph -> G e. F )
8 2 lmodring 
 |-  ( W e. LMod -> R e. Ring )
9 6 8 syl 
 |-  ( ph -> R e. Ring )
10 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
11 9 10 syl 
 |-  ( ph -> R e. Grp )
12 11 adantr 
 |-  ( ( ph /\ x e. V ) -> R e. Grp )
13 6 adantr 
 |-  ( ( ph /\ x e. V ) -> W e. LMod )
14 7 adantr 
 |-  ( ( ph /\ x e. V ) -> G e. F )
15 simpr 
 |-  ( ( ph /\ x e. V ) -> x e. V )
16 eqid 
 |-  ( Base ` R ) = ( Base ` R )
17 2 16 1 5 lflcl 
 |-  ( ( W e. LMod /\ G e. F /\ x e. V ) -> ( G ` x ) e. ( Base ` R ) )
18 13 14 15 17 syl3anc 
 |-  ( ( ph /\ x e. V ) -> ( G ` x ) e. ( Base ` R ) )
19 16 3 grpinvcl 
 |-  ( ( R e. Grp /\ ( G ` x ) e. ( Base ` R ) ) -> ( I ` ( G ` x ) ) e. ( Base ` R ) )
20 12 18 19 syl2anc 
 |-  ( ( ph /\ x e. V ) -> ( I ` ( G ` x ) ) e. ( Base ` R ) )
21 20 4 fmptd 
 |-  ( ph -> N : V --> ( Base ` R ) )
22 ringabl 
 |-  ( R e. Ring -> R e. Abel )
23 9 22 syl 
 |-  ( ph -> R e. Abel )
24 23 adantr 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> R e. Abel )
25 9 adantr 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> R e. Ring )
26 simpr1 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> k e. ( Base ` R ) )
27 6 adantr 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> W e. LMod )
28 7 adantr 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> G e. F )
29 simpr2 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> y e. V )
30 2 16 1 5 lflcl 
 |-  ( ( W e. LMod /\ G e. F /\ y e. V ) -> ( G ` y ) e. ( Base ` R ) )
31 27 28 29 30 syl3anc 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( G ` y ) e. ( Base ` R ) )
32 eqid 
 |-  ( .r ` R ) = ( .r ` R )
33 16 32 ringcl 
 |-  ( ( R e. Ring /\ k e. ( Base ` R ) /\ ( G ` y ) e. ( Base ` R ) ) -> ( k ( .r ` R ) ( G ` y ) ) e. ( Base ` R ) )
34 25 26 31 33 syl3anc 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( k ( .r ` R ) ( G ` y ) ) e. ( Base ` R ) )
35 simpr3 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> z e. V )
36 2 16 1 5 lflcl 
 |-  ( ( W e. LMod /\ G e. F /\ z e. V ) -> ( G ` z ) e. ( Base ` R ) )
37 27 28 35 36 syl3anc 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( G ` z ) e. ( Base ` R ) )
38 eqid 
 |-  ( +g ` R ) = ( +g ` R )
39 16 38 3 ablinvadd 
 |-  ( ( R e. Abel /\ ( k ( .r ` R ) ( G ` y ) ) e. ( Base ` R ) /\ ( G ` z ) e. ( Base ` R ) ) -> ( I ` ( ( k ( .r ` R ) ( G ` y ) ) ( +g ` R ) ( G ` z ) ) ) = ( ( I ` ( k ( .r ` R ) ( G ` y ) ) ) ( +g ` R ) ( I ` ( G ` z ) ) ) )
40 24 34 37 39 syl3anc 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( I ` ( ( k ( .r ` R ) ( G ` y ) ) ( +g ` R ) ( G ` z ) ) ) = ( ( I ` ( k ( .r ` R ) ( G ` y ) ) ) ( +g ` R ) ( I ` ( G ` z ) ) ) )
41 eqid 
 |-  ( +g ` W ) = ( +g ` W )
42 eqid 
 |-  ( .s ` W ) = ( .s ` W )
43 1 41 2 42 16 38 32 5 lfli 
 |-  ( ( W e. LMod /\ G e. F /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( G ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) = ( ( k ( .r ` R ) ( G ` y ) ) ( +g ` R ) ( G ` z ) ) )
44 27 28 26 29 35 43 syl113anc 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( G ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) = ( ( k ( .r ` R ) ( G ` y ) ) ( +g ` R ) ( G ` z ) ) )
45 44 fveq2d 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( I ` ( G ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) ) = ( I ` ( ( k ( .r ` R ) ( G ` y ) ) ( +g ` R ) ( G ` z ) ) ) )
46 16 32 3 25 26 31 ringmneg2 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( k ( .r ` R ) ( I ` ( G ` y ) ) ) = ( I ` ( k ( .r ` R ) ( G ` y ) ) ) )
47 46 oveq1d 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( ( k ( .r ` R ) ( I ` ( G ` y ) ) ) ( +g ` R ) ( I ` ( G ` z ) ) ) = ( ( I ` ( k ( .r ` R ) ( G ` y ) ) ) ( +g ` R ) ( I ` ( G ` z ) ) ) )
48 40 45 47 3eqtr4d 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( I ` ( G ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) ) = ( ( k ( .r ` R ) ( I ` ( G ` y ) ) ) ( +g ` R ) ( I ` ( G ` z ) ) ) )
49 1 2 42 16 lmodvscl 
 |-  ( ( W e. LMod /\ k e. ( Base ` R ) /\ y e. V ) -> ( k ( .s ` W ) y ) e. V )
50 27 26 29 49 syl3anc 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( k ( .s ` W ) y ) e. V )
51 1 41 lmodvacl 
 |-  ( ( W e. LMod /\ ( k ( .s ` W ) y ) e. V /\ z e. V ) -> ( ( k ( .s ` W ) y ) ( +g ` W ) z ) e. V )
52 27 50 35 51 syl3anc 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( ( k ( .s ` W ) y ) ( +g ` W ) z ) e. V )
53 2fveq3 
 |-  ( x = ( ( k ( .s ` W ) y ) ( +g ` W ) z ) -> ( I ` ( G ` x ) ) = ( I ` ( G ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) ) )
54 fvex 
 |-  ( I ` ( G ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) ) e. _V
55 53 4 54 fvmpt 
 |-  ( ( ( k ( .s ` W ) y ) ( +g ` W ) z ) e. V -> ( N ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) = ( I ` ( G ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) ) )
56 52 55 syl 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( N ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) = ( I ` ( G ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) ) )
57 2fveq3 
 |-  ( x = y -> ( I ` ( G ` x ) ) = ( I ` ( G ` y ) ) )
58 fvex 
 |-  ( I ` ( G ` y ) ) e. _V
59 57 4 58 fvmpt 
 |-  ( y e. V -> ( N ` y ) = ( I ` ( G ` y ) ) )
60 29 59 syl 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( N ` y ) = ( I ` ( G ` y ) ) )
61 60 oveq2d 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( k ( .r ` R ) ( N ` y ) ) = ( k ( .r ` R ) ( I ` ( G ` y ) ) ) )
62 2fveq3 
 |-  ( x = z -> ( I ` ( G ` x ) ) = ( I ` ( G ` z ) ) )
63 fvex 
 |-  ( I ` ( G ` z ) ) e. _V
64 62 4 63 fvmpt 
 |-  ( z e. V -> ( N ` z ) = ( I ` ( G ` z ) ) )
65 35 64 syl 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( N ` z ) = ( I ` ( G ` z ) ) )
66 61 65 oveq12d 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( ( k ( .r ` R ) ( N ` y ) ) ( +g ` R ) ( N ` z ) ) = ( ( k ( .r ` R ) ( I ` ( G ` y ) ) ) ( +g ` R ) ( I ` ( G ` z ) ) ) )
67 48 56 66 3eqtr4d 
 |-  ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( N ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) = ( ( k ( .r ` R ) ( N ` y ) ) ( +g ` R ) ( N ` z ) ) )
68 67 ralrimivvva 
 |-  ( ph -> A. k e. ( Base ` R ) A. y e. V A. z e. V ( N ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) = ( ( k ( .r ` R ) ( N ` y ) ) ( +g ` R ) ( N ` z ) ) )
69 1 41 2 42 16 38 32 5 islfl 
 |-  ( W e. LMod -> ( N e. F <-> ( N : V --> ( Base ` R ) /\ A. k e. ( Base ` R ) A. y e. V A. z e. V ( N ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) = ( ( k ( .r ` R ) ( N ` y ) ) ( +g ` R ) ( N ` z ) ) ) ) )
70 6 69 syl 
 |-  ( ph -> ( N e. F <-> ( N : V --> ( Base ` R ) /\ A. k e. ( Base ` R ) A. y e. V A. z e. V ( N ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) = ( ( k ( .r ` R ) ( N ` y ) ) ( +g ` R ) ( N ` z ) ) ) ) )
71 21 68 70 mpbir2and 
 |-  ( ph -> N e. F )