# Metamath Proof Explorer

## 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
ldualgrp.f ${⊢}{F}=\mathrm{LFnl}\left({W}\right)$
ldualgrp.r ${⊢}{R}=\mathrm{Scalar}\left({W}\right)$
ldualgrp.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
ldualgrp.t
ldualgrp.o ${⊢}{O}={opp}_{r}\left({R}\right)$
ldualgrp.s
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
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
9 ldualgrp.o ${⊢}{O}={opp}_{r}\left({R}\right)$
10 ldualgrp.s
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}×\left\{{0}_{{R}}\right\}\in {F}$
38 2 37 syl ${⊢}{\phi }\to {V}×\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}×\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}×\left\{{0}_{{R}}\right\}\right){+}_{{D}}{x}=\left({V}×\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}×\left\{{0}_{{R}}\right\}\right){{+}_{{R}}}_{f}{x}={x}$
44 42 43 eqtrd ${⊢}\left({\phi }\wedge {x}\in {F}\right)\to \left({V}×\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}×\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}×\left\{{0}_{{R}}\right\}$
51 13 14 19 35 38 44 47 50 isgrpd ${⊢}{\phi }\to {D}\in \mathrm{Grp}$