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	⊢ ( 𝜑 → ( 𝐺 − 𝐻 ) ∈ 𝐹 )