| 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 ) |