Metamath Proof Explorer

Theorem lduallmodlem

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

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

Proof

Step Hyp Ref Expression
1 lduallmod.d 
 |-  D = ( LDual ` W )
2 lduallmod.w 
 |-  ( ph -> W e. LMod )
3 lduallmod.v 
 |-  V = ( Base ` W )
4 lduallmod.p 
 |-  .+ = oF ( +g ` W )
5 lduallmod.f 
 |-  F = ( LFnl ` W )
6 lduallmod.r 
 |-  R = ( Scalar ` W )
7 lduallmod.k 
 |-  K = ( Base ` R )
8 lduallmod.t 
 |-  .X. = ( .r ` R )
9 lduallmod.o 
 |-  O = ( oppR ` R )
10 lduallmod.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 
 |-  ( Scalar ` D ) = ( Scalar ` D )
16 6 9 1 15 2 ldualsca 
 |-  ( ph -> ( Scalar ` D ) = O )
17 16 eqcomd 
 |-  ( ph -> O = ( Scalar ` D ) )
18 10 a1i 
 |-  ( ph -> .x. = ( .s ` D ) )
19 9 7 opprbas 
 |-  K = ( Base ` O )
20 19 a1i 
 |-  ( ph -> K = ( Base ` O ) )
21 eqid 
 |-  ( +g ` R ) = ( +g ` R )
22 9 21 oppradd 
 |-  ( +g ` R ) = ( +g ` O )
23 22 a1i 
 |-  ( ph -> ( +g ` R ) = ( +g ` O ) )
24 16 fveq2d 
 |-  ( ph -> ( .r ` ( Scalar ` D ) ) = ( .r ` O ) )
25 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
26 9 25 oppr1 
 |-  ( 1r ` R ) = ( 1r ` O )
27 26 a1i 
 |-  ( ph -> ( 1r ` R ) = ( 1r ` O ) )
28 6 lmodring 
 |-  ( W e. LMod -> R e. Ring )
29 9 opprring 
 |-  ( R e. Ring -> O e. Ring )
30 2 28 29 3syl 
 |-  ( ph -> O e. Ring )
31 1 2 ldualgrp 
 |-  ( ph -> D e. Grp )
32 2 3ad2ant1 
 |-  ( ( ph /\ x e. K /\ y e. F ) -> W e. LMod )
33 simp2 
 |-  ( ( ph /\ x e. K /\ y e. F ) -> x e. K )
34 simp3 
 |-  ( ( ph /\ x e. K /\ y e. F ) -> y e. F )
35 5 6 7 1 10 32 33 34 ldualvscl 
 |-  ( ( ph /\ x e. K /\ y e. F ) -> ( x .x. y ) e. F )
36 eqid 
 |-  ( +g ` D ) = ( +g ` D )
37 2 adantr 
 |-  ( ( ph /\ ( x e. K /\ y e. F /\ z e. F ) ) -> W e. LMod )
38 simpr1 
 |-  ( ( ph /\ ( x e. K /\ y e. F /\ z e. F ) ) -> x e. K )
39 simpr2 
 |-  ( ( ph /\ ( x e. K /\ y e. F /\ z e. F ) ) -> y e. F )
40 simpr3 
 |-  ( ( ph /\ ( x e. K /\ y e. F /\ z e. F ) ) -> z e. F )
41 5 6 7 1 36 10 37 38 39 40 ldualvsdi1 
 |-  ( ( ph /\ ( x e. K /\ y e. F /\ z e. F ) ) -> ( x .x. ( y ( +g ` D ) z ) ) = ( ( x .x. y ) ( +g ` D ) ( x .x. z ) ) )
42 2 adantr 
 |-  ( ( ph /\ ( x e. K /\ y e. K /\ z e. F ) ) -> W e. LMod )
43 simpr1 
 |-  ( ( ph /\ ( x e. K /\ y e. K /\ z e. F ) ) -> x e. K )
44 simpr2 
 |-  ( ( ph /\ ( x e. K /\ y e. K /\ z e. F ) ) -> y e. K )
45 simpr3 
 |-  ( ( ph /\ ( x e. K /\ y e. K /\ z e. F ) ) -> z e. F )
46 5 6 21 7 1 36 10 42 43 44 45 ldualvsdi2 
 |-  ( ( ph /\ ( x e. K /\ y e. K /\ z e. F ) ) -> ( ( x ( +g ` R ) y ) .x. z ) = ( ( x .x. z ) ( +g ` D ) ( y .x. z ) ) )
47 eqid 
 |-  ( .r ` ( Scalar ` D ) ) = ( .r ` ( Scalar ` D ) )
48 5 6 7 1 15 47 10 42 43 44 45 ldualvsass2 
 |-  ( ( ph /\ ( x e. K /\ y e. K /\ z e. F ) ) -> ( ( x ( .r ` ( Scalar ` D ) ) y ) .x. z ) = ( x .x. ( y .x. z ) ) )
49 2 adantr 
 |-  ( ( ph /\ x e. F ) -> W e. LMod )
50 7 25 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. K )
51 2 28 50 3syl 
 |-  ( ph -> ( 1r ` R ) e. K )
52 51 adantr 
 |-  ( ( ph /\ x e. F ) -> ( 1r ` R ) e. K )
53 simpr 
 |-  ( ( ph /\ x e. F ) -> x e. F )
54 5 3 6 7 8 1 10 49 52 53 ldualvs 
 |-  ( ( ph /\ x e. F ) -> ( ( 1r ` R ) .x. x ) = ( x oF .X. ( V X. { ( 1r ` R ) } ) ) )
55 3 6 5 7 8 25 49 53 lfl1sc 
 |-  ( ( ph /\ x e. F ) -> ( x oF .X. ( V X. { ( 1r ` R ) } ) ) = x )
56 54 55 eqtrd 
 |-  ( ( ph /\ x e. F ) -> ( ( 1r ` R ) .x. x ) = x )
57 13 14 17 18 20 23 24 27 30 31 35 41 46 48 56 islmodd 
 |-  ( ph -> D e. LMod )