Theorem ldualvsub

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

	Ref	Expression
Hypotheses	ldualvsub.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
	ldualvsub.n	$$⊢N={inv}_g\left(R\right)$$
	ldualvsub.u	$$⊢\underset{\dot{}}{1}=1_R$$
	ldualvsub.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	ldualvsub.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualvsub.p	$$⊢\underset{\dot{}}{+}={+}_D$$
	ldualvsub.t	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
	ldualvsub.m	$$⊢\underset{\dot{}}{-}={-}_D$$
	ldualvsub.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	ldualvsub.g	$$⊢\phi \to G\in F$$
	ldualvsub.h	$$⊢\phi \to H\in F$$
Assertion	ldualvsub	$$⊢\phi \to G\underset{\dot{}}{-}H=G\underset{\dot{}}{+}\left(N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}H\right)$$

Proof

Step	Hyp	Ref	Expression
1		ldualvsub.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
2		ldualvsub.n	$$⊢N={inv}_g\left(R\right)$$
3		ldualvsub.u	$$⊢\underset{\dot{}}{1}=1_R$$
4		ldualvsub.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
5		ldualvsub.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
6		ldualvsub.p	$$⊢\underset{\dot{}}{+}={+}_D$$
7		ldualvsub.t	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
8		ldualvsub.m	$$⊢\underset{\dot{}}{-}={-}_D$$
9		ldualvsub.w	$$⊢\phi \to W\in \mathrm{LMod}$$
10		ldualvsub.g	$$⊢\phi \to G\in F$$
11		ldualvsub.h	$$⊢\phi \to H\in F$$
12	5 9	lduallmod	$$⊢\phi \to D\in \mathrm{LMod}$$
13		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
14	4 5 13 9 10	ldualelvbase	$$⊢\phi \to G\in {\mathrm{Base}}_D$$
15	4 5 13 9 11	ldualelvbase	$$⊢\phi \to H\in {\mathrm{Base}}_D$$
16		eqid	$$⊢\mathrm{Scalar}\left(D\right)=\mathrm{Scalar}\left(D\right)$$
17		eqid	$$⊢{inv}_g\left(\mathrm{Scalar}\left(D\right)\right)={inv}_g\left(\mathrm{Scalar}\left(D\right)\right)$$
18		eqid	$$⊢1_{\mathrm{Scalar}\left(D\right)}=1_{\mathrm{Scalar}\left(D\right)}$$
19	13 6 8 16 7 17 18	lmodvsubval2	$$⊢\left(D\in \mathrm{LMod}\wedge G\in {\mathrm{Base}}_D\wedge H\in {\mathrm{Base}}_D\right)\to G\underset{\dot{}}{-}H=G\underset{\dot{}}{+}\left({inv}_g\left(\mathrm{Scalar}\left(D\right)\right)\left(1_{\mathrm{Scalar}\left(D\right)}\right)\underset{\dot{}}{·}H\right)$$
20	12 14 15 19	syl3anc	$$⊢\phi \to G\underset{\dot{}}{-}H=G\underset{\dot{}}{+}\left({inv}_g\left(\mathrm{Scalar}\left(D\right)\right)\left(1_{\mathrm{Scalar}\left(D\right)}\right)\underset{\dot{}}{·}H\right)$$
21		eqid	$$⊢{opp}_r\left(R\right)={opp}_r\left(R\right)$$
22	21 2	opprneg	$$⊢N={inv}_g\left({opp}_r\left(R\right)\right)$$
23	1 21 5 16 9	ldualsca	$$⊢\phi \to \mathrm{Scalar}\left(D\right)={opp}_r\left(R\right)$$
24	23	fveq2d	$$⊢\phi \to {inv}_g\left(\mathrm{Scalar}\left(D\right)\right)={inv}_g\left({opp}_r\left(R\right)\right)$$
25	22 24	eqtr4id	$$⊢\phi \to N={inv}_g\left(\mathrm{Scalar}\left(D\right)\right)$$
26	21 3	oppr1	$$⊢\underset{\dot{}}{1}=1_{{opp}_r\left(R\right)}$$
27	23	fveq2d	$$⊢\phi \to 1_{\mathrm{Scalar}\left(D\right)}=1_{{opp}_r\left(R\right)}$$
28	26 27	eqtr4id	$$⊢\phi \to \underset{\dot{}}{1}=1_{\mathrm{Scalar}\left(D\right)}$$
29	25 28	fveq12d	$$⊢\phi \to N\left(\underset{\dot{}}{1}\right)={inv}_g\left(\mathrm{Scalar}\left(D\right)\right)\left(1_{\mathrm{Scalar}\left(D\right)}\right)$$
30	29	oveq1d	$$⊢\phi \to N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}H={inv}_g\left(\mathrm{Scalar}\left(D\right)\right)\left(1_{\mathrm{Scalar}\left(D\right)}\right)\underset{\dot{}}{·}H$$
31	30	oveq2d	$$⊢\phi \to G\underset{\dot{}}{+}\left(N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}H\right)=G\underset{\dot{}}{+}\left({inv}_g\left(\mathrm{Scalar}\left(D\right)\right)\left(1_{\mathrm{Scalar}\left(D\right)}\right)\underset{\dot{}}{·}H\right)$$
32	20 31	eqtr4d	$$⊢\phi \to G\underset{\dot{}}{-}H=G\underset{\dot{}}{+}\left(N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}H\right)$$