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 φ W LMod
lduallmod.v V = Base W
lduallmod.p + ˙ = f + W
lduallmod.f F = LFnl W
lduallmod.r R = Scalar W
lduallmod.k K = Base R
lduallmod.t × ˙ = R
lduallmod.o O = opp r R
lduallmod.s · ˙ = D
Assertion lduallmodlem φ D LMod

Proof

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