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 ⊢ 𝐷 = ( LDual ‘ 𝑊 )
ldualgrp.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
Assertion ldualgrp ( 𝜑 → 𝐷 ∈ Grp )

Proof

Step Hyp Ref Expression
1 ldualgrp.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
2 ldualgrp.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
3 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
4 eqid ⊢ ∘f ( +g ‘ 𝑊 ) = ∘f ( +g ‘ 𝑊 )
5 eqid ⊢ ( LFnl ‘ 𝑊 ) = ( LFnl ‘ 𝑊 )
6 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
7 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
8 eqid ⊢ ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ ( Scalar ‘ 𝑊 ) )
9 eqid ⊢ ( oppr ‘ ( Scalar ‘ 𝑊 ) ) = ( oppr ‘ ( Scalar ‘ 𝑊 ) )
10 eqid ⊢ ( ·𝑠 ‘ 𝐷 ) = ( ·𝑠 ‘ 𝐷 )
11 1 2 3 4 5 6 7 8 9 10 ldualgrplem ⊢ ( 𝜑 → 𝐷 ∈ Grp )