Metamath Proof Explorer


Theorem lduallmodlem

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

Ref Expression
Hypotheses lduallmod.d D=LDualW
lduallmod.w φWLMod
lduallmod.v V=BaseW
lduallmod.p +˙=f+W
lduallmod.f F=LFnlW
lduallmod.r R=ScalarW
lduallmod.k K=BaseR
lduallmod.t ×˙=R
lduallmod.o O=opprR
lduallmod.s ·˙=D
Assertion lduallmodlem φDLMod

Proof

Step Hyp Ref Expression
1 lduallmod.d D=LDualW
2 lduallmod.w φWLMod
3 lduallmod.v V=BaseW
4 lduallmod.p +˙=f+W
5 lduallmod.f F=LFnlW
6 lduallmod.r R=ScalarW
7 lduallmod.k K=BaseR
8 lduallmod.t ×˙=R
9 lduallmod.o O=opprR
10 lduallmod.s ·˙=D
11 eqid BaseD=BaseD
12 5 1 11 2 ldualvbase φBaseD=F
13 12 eqcomd φF=BaseD
14 eqidd φ+D=+D
15 eqid ScalarD=ScalarD
16 6 9 1 15 2 ldualsca φScalarD=O
17 16 eqcomd φO=ScalarD
18 10 a1i φ·˙=D
19 9 7 opprbas K=BaseO
20 19 a1i φK=BaseO
21 eqid +R=+R
22 9 21 oppradd +R=+O
23 22 a1i φ+R=+O
24 16 fveq2d φScalarD=O
25 eqid 1R=1R
26 9 25 oppr1 1R=1O
27 26 a1i φ1R=1O
28 6 lmodring WLModRRing
29 9 opprring RRingORing
30 2 28 29 3syl φORing
31 1 2 ldualgrp φDGrp
32 2 3ad2ant1 φxKyFWLMod
33 simp2 φxKyFxK
34 simp3 φxKyFyF
35 5 6 7 1 10 32 33 34 ldualvscl φxKyFx·˙yF
36 eqid +D=+D
37 2 adantr φxKyFzFWLMod
38 simpr1 φxKyFzFxK
39 simpr2 φxKyFzFyF
40 simpr3 φxKyFzFzF
41 5 6 7 1 36 10 37 38 39 40 ldualvsdi1 φxKyFzFx·˙y+Dz=x·˙y+Dx·˙z
42 2 adantr φxKyKzFWLMod
43 simpr1 φxKyKzFxK
44 simpr2 φxKyKzFyK
45 simpr3 φxKyKzFzF
46 5 6 21 7 1 36 10 42 43 44 45 ldualvsdi2 φxKyKzFx+Ry·˙z=x·˙z+Dy·˙z
47 eqid ScalarD=ScalarD
48 5 6 7 1 15 47 10 42 43 44 45 ldualvsass2 φxKyKzFxScalarDy·˙z=x·˙y·˙z
49 2 adantr φxFWLMod
50 7 25 ringidcl RRing1RK
51 2 28 50 3syl φ1RK
52 51 adantr φxF1RK
53 simpr φxFxF
54 5 3 6 7 8 1 10 49 52 53 ldualvs φxF1R·˙x=x×˙fV×1R
55 3 6 5 7 8 25 49 53 lfl1sc φxFx×˙fV×1R=x
56 54 55 eqtrd φxF1R·˙x=x
57 13 14 17 18 20 23 24 27 30 31 35 41 46 48 56 islmodd φDLMod