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	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	ldualvsubcl.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualvsubcl.m	$$⊢\underset{\dot{}}{-}={-}_D$$
	ldualvsubcl.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	ldualvsubcl.g	$$⊢\phi \to G\in F$$
	ldualvsubcl.h	$$⊢\phi \to H\in F$$
Assertion	ldualvsubcl	$$⊢\phi \to G\underset{\dot{}}{-}H\in F$$

Proof

Step	Hyp	Ref	Expression
1		ldualvsubcl.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
2		ldualvsubcl.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
3		ldualvsubcl.m	$$⊢\underset{\dot{}}{-}={-}_D$$
4		ldualvsubcl.w	$$⊢\phi \to W\in \mathrm{LMod}$$
5		ldualvsubcl.g	$$⊢\phi \to G\in F$$
6		ldualvsubcl.h	$$⊢\phi \to H\in F$$
7		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
8		eqid	$$⊢{inv}_g\left(\mathrm{Scalar}\left(W\right)\right)={inv}_g\left(\mathrm{Scalar}\left(W\right)\right)$$
9		eqid	$$⊢1_{\mathrm{Scalar}\left(W\right)}=1_{\mathrm{Scalar}\left(W\right)}$$
10		eqid	$$⊢{+}_D={+}_D$$
11		eqid	$$⊢{\cdot }_D={\cdot }_D$$
12	7 8 9 1 2 10 11 3 4 5 6	ldualvsub	$$⊢\phi \to G\underset{\dot{}}{-}H=G{+}_D\left({inv}_g\left(\mathrm{Scalar}\left(W\right)\right)\left(1_{\mathrm{Scalar}\left(W\right)}\right){\cdot }_{D}H\right)$$
13		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
14	7	lmodring	$$⊢W\in \mathrm{LMod}\to \mathrm{Scalar}\left(W\right)\in \mathrm{Ring}$$
15	4 14	syl	$$⊢\phi \to \mathrm{Scalar}\left(W\right)\in \mathrm{Ring}$$
16		ringgrp	$$⊢\mathrm{Scalar}\left(W\right)\in \mathrm{Ring}\to \mathrm{Scalar}\left(W\right)\in \mathrm{Grp}$$
17	15 16	syl	$$⊢\phi \to \mathrm{Scalar}\left(W\right)\in \mathrm{Grp}$$
18	13 9	ringidcl	$$⊢\mathrm{Scalar}\left(W\right)\in \mathrm{Ring}\to 1_{\mathrm{Scalar}\left(W\right)}\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
19	15 18	syl	$$⊢\phi \to 1_{\mathrm{Scalar}\left(W\right)}\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
20	13 8	grpinvcl	$$⊢\left(\mathrm{Scalar}\left(W\right)\in \mathrm{Grp}\wedge 1_{\mathrm{Scalar}\left(W\right)}\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\right)\to {inv}_g\left(\mathrm{Scalar}\left(W\right)\right)\left(1_{\mathrm{Scalar}\left(W\right)}\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
21	17 19 20	syl2anc	$$⊢\phi \to {inv}_g\left(\mathrm{Scalar}\left(W\right)\right)\left(1_{\mathrm{Scalar}\left(W\right)}\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
22	1 7 13 2 11 4 21 6	ldualvscl	$$⊢\phi \to {inv}_g\left(\mathrm{Scalar}\left(W\right)\right)\left(1_{\mathrm{Scalar}\left(W\right)}\right){\cdot }_{D}H\in F$$
23	1 2 10 4 5 22	ldualvaddcl	$$⊢\phi \to G{+}_D\left({inv}_g\left(\mathrm{Scalar}\left(W\right)\right)\left(1_{\mathrm{Scalar}\left(W\right)}\right){\cdot }_{D}H\right)\in F$$
24	12 23	eqeltrd	$$⊢\phi \to G\underset{\dot{}}{-}H\in F$$