Metamath Proof Explorer

Theorem ldualgrplem

Description: Lemma for ldualgrp . (Contributed by NM, 22-Oct-2014)

Ref Expression
Hypotheses ldualgrp.d 
|- D = ( LDual ` W )
ldualgrp.w 
|- ( ph -> W e. LMod )
ldualgrp.v 
|- V = ( Base ` W )
ldualgrp.p 
|- .+ = oF ( +g ` W )
ldualgrp.f 
|- F = ( LFnl ` W )
ldualgrp.r 
|- R = ( Scalar ` W )
ldualgrp.k 
|- K = ( Base ` R )
ldualgrp.t 
|- .X. = ( .r ` R )
ldualgrp.o 
|- O = ( oppR ` R )
ldualgrp.s 
|- .x. = ( .s ` D )
Assertion ldualgrplem 
|- ( ph -> D e. Grp )

Proof

Step Hyp Ref Expression
1 ldualgrp.d 
 |-  D = ( LDual ` W )
2 ldualgrp.w 
 |-  ( ph -> W e. LMod )
3 ldualgrp.v 
 |-  V = ( Base ` W )
4 ldualgrp.p 
 |-  .+ = oF ( +g ` W )
5 ldualgrp.f 
 |-  F = ( LFnl ` W )
6 ldualgrp.r 
 |-  R = ( Scalar ` W )
7 ldualgrp.k 
 |-  K = ( Base ` R )
8 ldualgrp.t 
 |-  .X. = ( .r ` R )
9 ldualgrp.o 
 |-  O = ( oppR ` R )
10 ldualgrp.s 
 |-  .x. = ( .s ` D )
11 eqid 
 |-  ( Base ` D ) = ( Base ` D )
12 5 1 11 2 ldualvbase 
 |-  ( ph -> ( Base ` D ) = F )
13 12 eqcomd 
 |-  ( ph -> F = ( Base ` D ) )
14 eqidd 
 |-  ( ph -> ( +g ` D ) = ( +g ` D ) )
15 eqid 
 |-  ( +g ` D ) = ( +g ` D )
16 2 3ad2ant1 
 |-  ( ( ph /\ x e. F /\ y e. F ) -> W e. LMod )
17 simp2 
 |-  ( ( ph /\ x e. F /\ y e. F ) -> x e. F )
18 simp3 
 |-  ( ( ph /\ x e. F /\ y e. F ) -> y e. F )
19 5 1 15 16 17 18 ldualvaddcl 
 |-  ( ( ph /\ x e. F /\ y e. F ) -> ( x ( +g ` D ) y ) e. F )
20 eqid 
 |-  ( +g ` R ) = ( +g ` R )
21 2 adantr 
 |-  ( ( ph /\ ( x e. F /\ y e. F /\ z e. F ) ) -> W e. LMod )
22 simpr2 
 |-  ( ( ph /\ ( x e. F /\ y e. F /\ z e. F ) ) -> y e. F )
23 simpr3 
 |-  ( ( ph /\ ( x e. F /\ y e. F /\ z e. F ) ) -> z e. F )
24 5 6 20 1 15 21 22 23 ldualvadd 
 |-  ( ( ph /\ ( x e. F /\ y e. F /\ z e. F ) ) -> ( y ( +g ` D ) z ) = ( y oF ( +g ` R ) z ) )
25 24 oveq2d 
 |-  ( ( ph /\ ( x e. F /\ y e. F /\ z e. F ) ) -> ( x oF ( +g ` R ) ( y ( +g ` D ) z ) ) = ( x oF ( +g ` R ) ( y oF ( +g ` R ) z ) ) )
26 simpr1 
 |-  ( ( ph /\ ( x e. F /\ y e. F /\ z e. F ) ) -> x e. F )
27 5 1 15 21 22 23 ldualvaddcl 
 |-  ( ( ph /\ ( x e. F /\ y e. F /\ z e. F ) ) -> ( y ( +g ` D ) z ) e. F )
28 5 6 20 1 15 21 26 27 ldualvadd 
 |-  ( ( ph /\ ( x e. F /\ y e. F /\ z e. F ) ) -> ( x ( +g ` D ) ( y ( +g ` D ) z ) ) = ( x oF ( +g ` R ) ( y ( +g ` D ) z ) ) )
29 5 1 15 21 26 22 ldualvaddcl 
 |-  ( ( ph /\ ( x e. F /\ y e. F /\ z e. F ) ) -> ( x ( +g ` D ) y ) e. F )
30 5 6 20 1 15 21 29 23 ldualvadd 
 |-  ( ( ph /\ ( x e. F /\ y e. F /\ z e. F ) ) -> ( ( x ( +g ` D ) y ) ( +g ` D ) z ) = ( ( x ( +g ` D ) y ) oF ( +g ` R ) z ) )
31 5 6 20 1 15 21 26 22 ldualvadd 
 |-  ( ( ph /\ ( x e. F /\ y e. F /\ z e. F ) ) -> ( x ( +g ` D ) y ) = ( x oF ( +g ` R ) y ) )
32 31 oveq1d 
 |-  ( ( ph /\ ( x e. F /\ y e. F /\ z e. F ) ) -> ( ( x ( +g ` D ) y ) oF ( +g ` R ) z ) = ( ( x oF ( +g ` R ) y ) oF ( +g ` R ) z ) )
33 6 20 5 21 26 22 23 lfladdass 
 |-  ( ( ph /\ ( x e. F /\ y e. F /\ z e. F ) ) -> ( ( x oF ( +g ` R ) y ) oF ( +g ` R ) z ) = ( x oF ( +g ` R ) ( y oF ( +g ` R ) z ) ) )
34 30 32 33 3eqtrd 
 |-  ( ( ph /\ ( x e. F /\ y e. F /\ z e. F ) ) -> ( ( x ( +g ` D ) y ) ( +g ` D ) z ) = ( x oF ( +g ` R ) ( y oF ( +g ` R ) z ) ) )
35 25 28 34 3eqtr4rd 
 |-  ( ( ph /\ ( x e. F /\ y e. F /\ z e. F ) ) -> ( ( x ( +g ` D ) y ) ( +g ` D ) z ) = ( x ( +g ` D ) ( y ( +g ` D ) z ) ) )
36 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
37 6 36 3 5 lfl0f 
 |-  ( W e. LMod -> ( V X. { ( 0g ` R ) } ) e. F )
38 2 37 syl 
 |-  ( ph -> ( V X. { ( 0g ` R ) } ) e. F )
39 2 adantr 
 |-  ( ( ph /\ x e. F ) -> W e. LMod )
40 38 adantr 
 |-  ( ( ph /\ x e. F ) -> ( V X. { ( 0g ` R ) } ) e. F )
41 simpr 
 |-  ( ( ph /\ x e. F ) -> x e. F )
42 5 6 20 1 15 39 40 41 ldualvadd 
 |-  ( ( ph /\ x e. F ) -> ( ( V X. { ( 0g ` R ) } ) ( +g ` D ) x ) = ( ( V X. { ( 0g ` R ) } ) oF ( +g ` R ) x ) )
43 3 6 20 36 5 39 41 lfladd0l 
 |-  ( ( ph /\ x e. F ) -> ( ( V X. { ( 0g ` R ) } ) oF ( +g ` R ) x ) = x )
44 42 43 eqtrd 
 |-  ( ( ph /\ x e. F ) -> ( ( V X. { ( 0g ` R ) } ) ( +g ` D ) x ) = x )
45 eqid 
 |-  ( invg ` R ) = ( invg ` R )
46 eqid 
 |-  ( z e. V |-> ( ( invg ` R ) ` ( x ` z ) ) ) = ( z e. V |-> ( ( invg ` R ) ` ( x ` z ) ) )
47 3 6 45 46 5 39 41 lflnegcl 
 |-  ( ( ph /\ x e. F ) -> ( z e. V |-> ( ( invg ` R ) ` ( x ` z ) ) ) e. F )
48 5 6 20 1 15 39 47 41 ldualvadd 
 |-  ( ( ph /\ x e. F ) -> ( ( z e. V |-> ( ( invg ` R ) ` ( x ` z ) ) ) ( +g ` D ) x ) = ( ( z e. V |-> ( ( invg ` R ) ` ( x ` z ) ) ) oF ( +g ` R ) x ) )
49 3 6 45 46 5 39 41 20 36 lflnegl 
 |-  ( ( ph /\ x e. F ) -> ( ( z e. V |-> ( ( invg ` R ) ` ( x ` z ) ) ) oF ( +g ` R ) x ) = ( V X. { ( 0g ` R ) } ) )
50 48 49 eqtrd 
 |-  ( ( ph /\ x e. F ) -> ( ( z e. V |-> ( ( invg ` R ) ` ( x ` z ) ) ) ( +g ` D ) x ) = ( V X. { ( 0g ` R ) } ) )
51 13 14 19 35 38 44 47 50 isgrpd 
 |-  ( ph -> D e. Grp )