Theorem lduallmodlem

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

	Ref	Expression
Hypotheses	lduallmod.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	lduallmod.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lduallmod.v	$$⊢V={\mathrm{Base}}_W$$
	lduallmod.p	$$⊢\underset{\dot{}}{+}={\circ }_f{+}_W$$
	lduallmod.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	lduallmod.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
	lduallmod.k	$$⊢K={\mathrm{Base}}_R$$
	lduallmod.t	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
	lduallmod.o	$$⊢O={opp}_r\left(R\right)$$
	lduallmod.s	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
Assertion	lduallmodlem	$$⊢\phi \to D\in \mathrm{LMod}$$

Proof

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