Theorem ldualgrplem

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

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

Proof

Step	Hyp	Ref	Expression
1		ldualgrp.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
2		ldualgrp.w	$$⊢\phi \to W\in \mathrm{LMod}$$
3		ldualgrp.v	$$⊢V={\mathrm{Base}}_W$$
4		ldualgrp.p	$$⊢\underset{\dot{}}{+}={\circ }_f{+}_W$$
5		ldualgrp.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
6		ldualgrp.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
7		ldualgrp.k	$$⊢K={\mathrm{Base}}_R$$
8		ldualgrp.t	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
9		ldualgrp.o	$$⊢O={opp}_r\left(R\right)$$
10		ldualgrp.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	$$⊢{+}_D={+}_D$$
16	2	3ad2ant1	$$⊢\left(\phi \wedge x\in F\wedge y\in F\right)\to W\in \mathrm{LMod}$$
17		simp2	$$⊢\left(\phi \wedge x\in F\wedge y\in F\right)\to x\in F$$
18		simp3	$$⊢\left(\phi \wedge x\in F\wedge y\in F\right)\to y\in F$$
19	5 1 15 16 17 18	ldualvaddcl	$$⊢\left(\phi \wedge x\in F\wedge y\in F\right)\to x{+}_{D}y\in F$$
20		eqid	$$⊢{+}_R={+}_R$$
21	2	adantr	$$⊢\left(\phi \wedge \left(x\in F\wedge y\in F\wedge z\in F\right)\right)\to W\in \mathrm{LMod}$$
22		simpr2	$$⊢\left(\phi \wedge \left(x\in F\wedge y\in F\wedge z\in F\right)\right)\to y\in F$$
23		simpr3	$$⊢\left(\phi \wedge \left(x\in F\wedge y\in F\wedge z\in F\right)\right)\to z\in F$$
24	5 6 20 1 15 21 22 23	ldualvadd	$$⊢\left(\phi \wedge \left(x\in F\wedge y\in F\wedge z\in F\right)\right)\to y{+}_{D}z=y{{+}_R}_{f}z$$
25	24	oveq2d	$$⊢\left(\phi \wedge \left(x\in F\wedge y\in F\wedge z\in F\right)\right)\to x{{+}_R}_f\left(y{+}_{D}z\right)=x{{+}_R}_f\left(y{{+}_R}_{f}z\right)$$
26		simpr1	$$⊢\left(\phi \wedge \left(x\in F\wedge y\in F\wedge z\in F\right)\right)\to x\in F$$
27	5 1 15 21 22 23	ldualvaddcl	$$⊢\left(\phi \wedge \left(x\in F\wedge y\in F\wedge z\in F\right)\right)\to y{+}_{D}z\in F$$
28	5 6 20 1 15 21 26 27	ldualvadd	$$⊢\left(\phi \wedge \left(x\in F\wedge y\in F\wedge z\in F\right)\right)\to x{+}_D\left(y{+}_{D}z\right)=x{{+}_R}_f\left(y{+}_{D}z\right)$$
29	5 1 15 21 26 22	ldualvaddcl	$$⊢\left(\phi \wedge \left(x\in F\wedge y\in F\wedge z\in F\right)\right)\to x{+}_{D}y\in F$$
30	5 6 20 1 15 21 29 23	ldualvadd	$$⊢\left(\phi \wedge \left(x\in F\wedge y\in F\wedge z\in F\right)\right)\to \left(x{+}_{D}y\right){+}_{D}z=\left(x{+}_{D}y\right){{+}_R}_{f}z$$
31	5 6 20 1 15 21 26 22	ldualvadd	$$⊢\left(\phi \wedge \left(x\in F\wedge y\in F\wedge z\in F\right)\right)\to x{+}_{D}y=x{{+}_R}_{f}y$$
32	31	oveq1d	$$⊢\left(\phi \wedge \left(x\in F\wedge y\in F\wedge z\in F\right)\right)\to \left(x{+}_{D}y\right){{+}_R}_{f}z=\left(x{{+}_R}_{f}y\right){{+}_R}_{f}z$$
33	6 20 5 21 26 22 23	lfladdass	$$⊢\left(\phi \wedge \left(x\in F\wedge y\in F\wedge z\in F\right)\right)\to \left(x{{+}_R}_{f}y\right){{+}_R}_{f}z=x{{+}_R}_f\left(y{{+}_R}_{f}z\right)$$
34	30 32 33	3eqtrd	$$⊢\left(\phi \wedge \left(x\in F\wedge y\in F\wedge z\in F\right)\right)\to \left(x{+}_{D}y\right){+}_{D}z=x{{+}_R}_f\left(y{{+}_R}_{f}z\right)$$
35	25 28 34	3eqtr4rd	$$⊢\left(\phi \wedge \left(x\in F\wedge y\in F\wedge z\in F\right)\right)\to \left(x{+}_{D}y\right){+}_{D}z=x{+}_D\left(y{+}_{D}z\right)$$
36		eqid	$$⊢0_R=0_R$$
37	6 36 3 5	lfl0f	$$⊢W\in \mathrm{LMod}\to V\times \left\{0_R\right\}\in F$$
38	2 37	syl	$$⊢\phi \to V\times \left\{0_R\right\}\in F$$
39	2	adantr	$$⊢\left(\phi \wedge x\in F\right)\to W\in \mathrm{LMod}$$
40	38	adantr	$$⊢\left(\phi \wedge x\in F\right)\to V\times \left\{0_R\right\}\in F$$
41		simpr	$$⊢\left(\phi \wedge x\in F\right)\to x\in F$$
42	5 6 20 1 15 39 40 41	ldualvadd	$$⊢\left(\phi \wedge x\in F\right)\to \left(V\times \left\{0_R\right\}\right){+}_{D}x=\left(V\times \left\{0_R\right\}\right){{+}_R}_{f}x$$
43	3 6 20 36 5 39 41	lfladd0l	$$⊢\left(\phi \wedge x\in F\right)\to \left(V\times \left\{0_R\right\}\right){{+}_R}_{f}x=x$$
44	42 43	eqtrd	$$⊢\left(\phi \wedge x\in F\right)\to \left(V\times \left\{0_R\right\}\right){+}_{D}x=x$$
45		eqid	$$⊢{inv}_g\left(R\right)={inv}_g\left(R\right)$$
46		eqid	$$⊢\left(z\in V⟼{inv}_g\left(R\right)\left(x\left(z\right)\right)\right)=\left(z\in V⟼{inv}_g\left(R\right)\left(x\left(z\right)\right)\right)$$
47	3 6 45 46 5 39 41	lflnegcl	$$⊢\left(\phi \wedge x\in F\right)\to \left(z\in V⟼{inv}_g\left(R\right)\left(x\left(z\right)\right)\right)\in F$$
48	5 6 20 1 15 39 47 41	ldualvadd	$$⊢\left(\phi \wedge x\in F\right)\to \left(z\in V⟼{inv}_g\left(R\right)\left(x\left(z\right)\right)\right){+}_{D}x=\left(z\in V⟼{inv}_g\left(R\right)\left(x\left(z\right)\right)\right){{+}_R}_{f}x$$
49	3 6 45 46 5 39 41 20 36	lflnegl	$$⊢\left(\phi \wedge x\in F\right)\to \left(z\in V⟼{inv}_g\left(R\right)\left(x\left(z\right)\right)\right){{+}_R}_{f}x=V\times \left\{0_R\right\}$$
50	48 49	eqtrd	$$⊢\left(\phi \wedge x\in F\right)\to \left(z\in V⟼{inv}_g\left(R\right)\left(x\left(z\right)\right)\right){+}_{D}x=V\times \left\{0_R\right\}$$
51	13 14 19 35 38 44 47 50	isgrpd	$$⊢\phi \to D\in \mathrm{Grp}$$