Metamath Proof Explorer

Theorem ldualvsubcl

Description: Closure of vector subtraction in the dual of a vector space. (Contributed by NM, 27-Feb-2015)

Ref Expression
Hypotheses ldualvsubcl.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
ldualvsubcl.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
ldualvsubcl.m ⊢ − = ( -g ‘ 𝐷 )
ldualvsubcl.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
ldualvsubcl.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
ldualvsubcl.h ⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
Assertion ldualvsubcl ( 𝜑 → ( 𝐺 − 𝐻 ) ∈ 𝐹 )

Proof

Step Hyp Ref Expression
1 ldualvsubcl.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
2 ldualvsubcl.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
3 ldualvsubcl.m ⊢ − = ( -g ‘ 𝐷 )
4 ldualvsubcl.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
5 ldualvsubcl.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
6 ldualvsubcl.h ⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
7 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
8 eqid ⊢ ( invg ‘ ( Scalar ‘ 𝑊 ) ) = ( invg ‘ ( Scalar ‘ 𝑊 ) )
9 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) )
10 eqid ⊢ ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 )
11 eqid ⊢ ( ·𝑠 ‘ 𝐷 ) = ( ·𝑠 ‘ 𝐷 )
12 7 8 9 1 2 10 11 3 4 5 6 ldualvsub ⊢ ( 𝜑 → ( 𝐺 − 𝐻 ) = ( 𝐺 ( +g ‘ 𝐷 ) ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) )
13 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
14 7 lmodring ⊢ ( 𝑊 ∈ LMod → ( Scalar ‘ 𝑊 ) ∈ Ring )
15 4 14 syl ⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) ∈ Ring )
16 ringgrp ⊢ ( ( Scalar ‘ 𝑊 ) ∈ Ring → ( Scalar ‘ 𝑊 ) ∈ Grp )
17 15 16 syl ⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) ∈ Grp )
18 13 9 ringidcl ⊢ ( ( Scalar ‘ 𝑊 ) ∈ Ring → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
19 15 18 syl ⊢ ( 𝜑 → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
20 13 8 grpinvcl ⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ Grp ∧ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
21 17 19 20 syl2anc ⊢ ( 𝜑 → ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
22 1 7 13 2 11 4 21 6 ldualvscl ⊢ ( 𝜑 → ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ∈ 𝐹 )
23 1 2 10 4 5 22 ldualvaddcl ⊢ ( 𝜑 → ( 𝐺 ( +g ‘ 𝐷 ) ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) ∈ 𝐹 )
24 12 23 eqeltrd ⊢ ( 𝜑 → ( 𝐺 − 𝐻 ) ∈ 𝐹 )