Theorem lcdvsub

Description: The value of vector subtraction in the closed kernel dual space. (Contributed by NM, 22-Mar-2015)

	Ref	Expression
Hypotheses	lcdvsub.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcdvsub.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcdvsub.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
	lcdvsub.n	$$⊢N={inv}_g\left(S\right)$$
	lcdvsub.e	$$⊢\underset{\dot{}}{1}=1_S$$
	lcdvsub.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	lcdvsub.v	$$⊢V={\mathrm{Base}}_C$$
	lcdvsub.p	$$⊢\underset{\dot{}}{+}={+}_C$$
	lcdvsub.t	$$⊢\underset{\dot{}}{·}={\cdot }_C$$
	lcdvsub.m	$$⊢\underset{\dot{}}{-}={-}_C$$
	lcdvsub.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lcdvsub.f	$$⊢\phi \to F\in V$$
	lcdvsub.g	$$⊢\phi \to G\in V$$
Assertion	lcdvsub	$$⊢\phi \to F\underset{\dot{}}{-}G=F\underset{\dot{}}{+}\left(N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}G\right)$$

Proof

Step	Hyp	Ref	Expression
1		lcdvsub.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcdvsub.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		lcdvsub.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
4		lcdvsub.n	$$⊢N={inv}_g\left(S\right)$$
5		lcdvsub.e	$$⊢\underset{\dot{}}{1}=1_S$$
6		lcdvsub.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
7		lcdvsub.v	$$⊢V={\mathrm{Base}}_C$$
8		lcdvsub.p	$$⊢\underset{\dot{}}{+}={+}_C$$
9		lcdvsub.t	$$⊢\underset{\dot{}}{·}={\cdot }_C$$
10		lcdvsub.m	$$⊢\underset{\dot{}}{-}={-}_C$$
11		lcdvsub.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
12		lcdvsub.f	$$⊢\phi \to F\in V$$
13		lcdvsub.g	$$⊢\phi \to G\in V$$
14	1 6 11	lcdlmod	$$⊢\phi \to C\in \mathrm{LMod}$$
15		eqid	$$⊢\mathrm{Scalar}\left(C\right)=\mathrm{Scalar}\left(C\right)$$
16		eqid	$$⊢{inv}_g\left(\mathrm{Scalar}\left(C\right)\right)={inv}_g\left(\mathrm{Scalar}\left(C\right)\right)$$
17		eqid	$$⊢1_{\mathrm{Scalar}\left(C\right)}=1_{\mathrm{Scalar}\left(C\right)}$$
18	7 8 10 15 9 16 17	lmodvsubval2	$$⊢\left(C\in \mathrm{LMod}\wedge F\in V\wedge G\in V\right)\to F\underset{\dot{}}{-}G=F\underset{\dot{}}{+}\left({inv}_g\left(\mathrm{Scalar}\left(C\right)\right)\left(1_{\mathrm{Scalar}\left(C\right)}\right)\underset{\dot{}}{·}G\right)$$
19	14 12 13 18	syl3anc	$$⊢\phi \to F\underset{\dot{}}{-}G=F\underset{\dot{}}{+}\left({inv}_g\left(\mathrm{Scalar}\left(C\right)\right)\left(1_{\mathrm{Scalar}\left(C\right)}\right)\underset{\dot{}}{·}G\right)$$
20		eqid	$$⊢{opp}_r\left(S\right)={opp}_r\left(S\right)$$
21	1 2 3 20 6 15 11	lcdsca	$$⊢\phi \to \mathrm{Scalar}\left(C\right)={opp}_r\left(S\right)$$
22	21	fveq2d	$$⊢\phi \to {inv}_g\left(\mathrm{Scalar}\left(C\right)\right)={inv}_g\left({opp}_r\left(S\right)\right)$$
23	20 4	opprneg	$$⊢N={inv}_g\left({opp}_r\left(S\right)\right)$$
24	22 23	syl6reqr	$$⊢\phi \to N={inv}_g\left(\mathrm{Scalar}\left(C\right)\right)$$
25	21	fveq2d	$$⊢\phi \to 1_{\mathrm{Scalar}\left(C\right)}=1_{{opp}_r\left(S\right)}$$
26	20 5	oppr1	$$⊢\underset{\dot{}}{1}=1_{{opp}_r\left(S\right)}$$
27	25 26	syl6reqr	$$⊢\phi \to \underset{\dot{}}{1}=1_{\mathrm{Scalar}\left(C\right)}$$
28	24 27	fveq12d	$$⊢\phi \to N\left(\underset{\dot{}}{1}\right)={inv}_g\left(\mathrm{Scalar}\left(C\right)\right)\left(1_{\mathrm{Scalar}\left(C\right)}\right)$$
29	28	oveq1d	$$⊢\phi \to N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}G={inv}_g\left(\mathrm{Scalar}\left(C\right)\right)\left(1_{\mathrm{Scalar}\left(C\right)}\right)\underset{\dot{}}{·}G$$
30	29	oveq2d	$$⊢\phi \to F\underset{\dot{}}{+}\left(N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}G\right)=F\underset{\dot{}}{+}\left({inv}_g\left(\mathrm{Scalar}\left(C\right)\right)\left(1_{\mathrm{Scalar}\left(C\right)}\right)\underset{\dot{}}{·}G\right)$$
31	19 30	eqtr4d	$$⊢\phi \to F\underset{\dot{}}{-}G=F\underset{\dot{}}{+}\left(N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}G\right)$$