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}$$