This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = LDual ⁡ W
ldualgrp.w ⊢ φ → W ∈ LMod
Assertion ldualgrp ⊢ φ → D ∈ Grp

Proof

Step Hyp Ref Expression
1 ldualgrp.d ⊢ D = LDual ⁡ W
2 ldualgrp.w ⊢ φ → W ∈ LMod
3 eqid ⊢ Base W = Base W
4 eqid ⊢ ∘ f ⁡ + W = ∘ f ⁡ + W
5 eqid ⊢ LFnl ⁡ W = LFnl ⁡ W
6 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
7 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
8 eqid ⊢ ⋅ Scalar ⁡ W = ⋅ Scalar ⁡ W
9 eqid ⊢ opp r ⁡ Scalar ⁡ W = opp r ⁡ Scalar ⁡ W
10 eqid ⊢ ⋅ D = ⋅ D
11 1 2 3 4 5 6 7 8 9 10 ldualgrplem ⊢ φ → D ∈ Grp