Metamath Proof Explorer

Theorem ldualgrp

Description: The dual of a vector space is a group. (Contributed by NM, 21-Oct-2014)

Ref Expression
Hypotheses ldualgrp.d ${⊢}{D}=\mathrm{LDual}\left({W}\right)$
ldualgrp.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
Assertion ldualgrp ${⊢}{\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 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
4 eqid ${⊢}{\circ }_{f}{+}_{{W}}={\circ }_{f}{+}_{{W}}$
5 eqid ${⊢}\mathrm{LFnl}\left({W}\right)=\mathrm{LFnl}\left({W}\right)$
6 eqid ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
7 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
8 eqid ${⊢}{\cdot }_{\mathrm{Scalar}\left({W}\right)}={\cdot }_{\mathrm{Scalar}\left({W}\right)}$
9 eqid ${⊢}{opp}_{r}\left(\mathrm{Scalar}\left({W}\right)\right)={opp}_{r}\left(\mathrm{Scalar}\left({W}\right)\right)$
10 eqid ${⊢}{\cdot }_{{D}}={\cdot }_{{D}}$
11 1 2 3 4 5 6 7 8 9 10 ldualgrplem ${⊢}{\phi }\to {D}\in \mathrm{Grp}$