Theorem ldualvsubval

Description: The value of the value of vector subtraction in the dual of a vector space. TODO: shorten with ldualvsub ? (Requires D to oppR conversion.) (Contributed by NM, 26-Feb-2015)

	Ref	Expression
Hypotheses	ldualvsubval.v	$$⊢V={\mathrm{Base}}_W$$
	ldualvsubval.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
	ldualvsubval.s	$$⊢S={-}_R$$
	ldualvsubval.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	ldualvsubval.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualvsubval.m	$$⊢\underset{\dot{}}{-}={-}_D$$
	ldualvsubval.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	ldualvsubval.g	$$⊢\phi \to G\in F$$
	ldualvsubval.h	$$⊢\phi \to H\in F$$
	ldualvsubval.x	$$⊢\phi \to X\in V$$
Assertion	ldualvsubval	$$⊢\phi \to \left(G\underset{\dot{}}{-}H\right)\left(X\right)=G\left(X\right)SH\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		ldualvsubval.v	$$⊢V={\mathrm{Base}}_W$$
2		ldualvsubval.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
3		ldualvsubval.s	$$⊢S={-}_R$$
4		ldualvsubval.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
5		ldualvsubval.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
6		ldualvsubval.m	$$⊢\underset{\dot{}}{-}={-}_D$$
7		ldualvsubval.w	$$⊢\phi \to W\in \mathrm{LMod}$$
8		ldualvsubval.g	$$⊢\phi \to G\in F$$
9		ldualvsubval.h	$$⊢\phi \to H\in F$$
10		ldualvsubval.x	$$⊢\phi \to X\in V$$
11	5 7	lduallmod	$$⊢\phi \to D\in \mathrm{LMod}$$
12		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
13	4 5 12 7 8	ldualelvbase	$$⊢\phi \to G\in {\mathrm{Base}}_D$$
14	4 5 12 7 9	ldualelvbase	$$⊢\phi \to H\in {\mathrm{Base}}_D$$
15		eqid	$$⊢{+}_D={+}_D$$
16		eqid	$$⊢\mathrm{Scalar}\left(D\right)=\mathrm{Scalar}\left(D\right)$$
17		eqid	$$⊢{\cdot }_D={\cdot }_D$$
18		eqid	$$⊢{inv}_g\left(\mathrm{Scalar}\left(D\right)\right)={inv}_g\left(\mathrm{Scalar}\left(D\right)\right)$$
19		eqid	$$⊢1_{\mathrm{Scalar}\left(D\right)}=1_{\mathrm{Scalar}\left(D\right)}$$
20	12 15 6 16 17 18 19	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{+}_D\left({inv}_g\left(\mathrm{Scalar}\left(D\right)\right)\left(1_{\mathrm{Scalar}\left(D\right)}\right){\cdot }_{D}H\right)$$
21	11 13 14 20	syl3anc	$$⊢\phi \to G\underset{\dot{}}{-}H=G{+}_D\left({inv}_g\left(\mathrm{Scalar}\left(D\right)\right)\left(1_{\mathrm{Scalar}\left(D\right)}\right){\cdot }_{D}H\right)$$
22	21	fveq1d	$$⊢\phi \to \left(G\underset{\dot{}}{-}H\right)\left(X\right)=\left(G{+}_D\left({inv}_g\left(\mathrm{Scalar}\left(D\right)\right)\left(1_{\mathrm{Scalar}\left(D\right)}\right){\cdot }_{D}H\right)\right)\left(X\right)$$
23		eqid	$$⊢{+}_R={+}_R$$
24		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
25	16	lmodfgrp	$$⊢D\in \mathrm{LMod}\to \mathrm{Scalar}\left(D\right)\in \mathrm{Grp}$$
26	11 25	syl	$$⊢\phi \to \mathrm{Scalar}\left(D\right)\in \mathrm{Grp}$$
27	16	lmodring	$$⊢D\in \mathrm{LMod}\to \mathrm{Scalar}\left(D\right)\in \mathrm{Ring}$$
28	11 27	syl	$$⊢\phi \to \mathrm{Scalar}\left(D\right)\in \mathrm{Ring}$$
29		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}$$
30	29 19	ringidcl	$$⊢\mathrm{Scalar}\left(D\right)\in \mathrm{Ring}\to 1_{\mathrm{Scalar}\left(D\right)}\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}$$
31	28 30	syl	$$⊢\phi \to 1_{\mathrm{Scalar}\left(D\right)}\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}$$
32	29 18	grpinvcl	$$⊢\left(\mathrm{Scalar}\left(D\right)\in \mathrm{Grp}\wedge 1_{\mathrm{Scalar}\left(D\right)}\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}\right)\to {inv}_g\left(\mathrm{Scalar}\left(D\right)\right)\left(1_{\mathrm{Scalar}\left(D\right)}\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}$$
33	26 31 32	syl2anc	$$⊢\phi \to {inv}_g\left(\mathrm{Scalar}\left(D\right)\right)\left(1_{\mathrm{Scalar}\left(D\right)}\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}$$
34	2 24 5 16 29 7	ldualsbase	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}={\mathrm{Base}}_R$$
35	33 34	eleqtrd	$$⊢\phi \to {inv}_g\left(\mathrm{Scalar}\left(D\right)\right)\left(1_{\mathrm{Scalar}\left(D\right)}\right)\in {\mathrm{Base}}_R$$
36	4 2 24 5 17 7 35 9	ldualvscl	$$⊢\phi \to {inv}_g\left(\mathrm{Scalar}\left(D\right)\right)\left(1_{\mathrm{Scalar}\left(D\right)}\right){\cdot }_{D}H\in F$$
37	1 2 23 4 5 15 7 8 36 10	ldualvaddval	$$⊢\phi \to \left(G{+}_D\left({inv}_g\left(\mathrm{Scalar}\left(D\right)\right)\left(1_{\mathrm{Scalar}\left(D\right)}\right){\cdot }_{D}H\right)\right)\left(X\right)=G\left(X\right){+}_R\left({inv}_g\left(\mathrm{Scalar}\left(D\right)\right)\left(1_{\mathrm{Scalar}\left(D\right)}\right){\cdot }_{D}H\right)\left(X\right)$$
38		eqid	$$⊢{inv}_g\left(R\right)={inv}_g\left(R\right)$$
39	2 38 5 16 18 7	ldualneg	$$⊢\phi \to {inv}_g\left(\mathrm{Scalar}\left(D\right)\right)={inv}_g\left(R\right)$$
40		eqid	$$⊢1_R=1_R$$
41	2 40 5 16 19 7	ldual1	$$⊢\phi \to 1_{\mathrm{Scalar}\left(D\right)}=1_R$$
42	39 41	fveq12d	$$⊢\phi \to {inv}_g\left(\mathrm{Scalar}\left(D\right)\right)\left(1_{\mathrm{Scalar}\left(D\right)}\right)={inv}_g\left(R\right)\left(1_R\right)$$
43	42	oveq1d	$$⊢\phi \to {inv}_g\left(\mathrm{Scalar}\left(D\right)\right)\left(1_{\mathrm{Scalar}\left(D\right)}\right){\cdot }_{D}H={inv}_g\left(R\right)\left(1_R\right){\cdot }_{D}H$$
44	43	fveq1d	$$⊢\phi \to \left({inv}_g\left(\mathrm{Scalar}\left(D\right)\right)\left(1_{\mathrm{Scalar}\left(D\right)}\right){\cdot }_{D}H\right)\left(X\right)=\left({inv}_g\left(R\right)\left(1_R\right){\cdot }_{D}H\right)\left(X\right)$$
45		eqid	$$⊢{\cdot }_R={\cdot }_R$$
46	2	lmodring	$$⊢W\in \mathrm{LMod}\to R\in \mathrm{Ring}$$
47	7 46	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
48		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
49	47 48	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
50	2 24 40	lmod1cl	$$⊢W\in \mathrm{LMod}\to 1_R\in {\mathrm{Base}}_R$$
51	7 50	syl	$$⊢\phi \to 1_R\in {\mathrm{Base}}_R$$
52	24 38	grpinvcl	$$⊢\left(R\in \mathrm{Grp}\wedge 1_R\in {\mathrm{Base}}_R\right)\to {inv}_g\left(R\right)\left(1_R\right)\in {\mathrm{Base}}_R$$
53	49 51 52	syl2anc	$$⊢\phi \to {inv}_g\left(R\right)\left(1_R\right)\in {\mathrm{Base}}_R$$
54	4 1 2 24 45 5 17 7 53 9 10	ldualvsval	$$⊢\phi \to \left({inv}_g\left(R\right)\left(1_R\right){\cdot }_{D}H\right)\left(X\right)=H\left(X\right){\cdot }_R{inv}_g\left(R\right)\left(1_R\right)$$
55	2 24 1 4	lflcl	$$⊢\left(W\in \mathrm{LMod}\wedge H\in F\wedge X\in V\right)\to H\left(X\right)\in {\mathrm{Base}}_R$$
56	7 9 10 55	syl3anc	$$⊢\phi \to H\left(X\right)\in {\mathrm{Base}}_R$$
57	24 45 40 38 47 56	rngnegr	$$⊢\phi \to H\left(X\right){\cdot }_R{inv}_g\left(R\right)\left(1_R\right)={inv}_g\left(R\right)\left(H\left(X\right)\right)$$
58	44 54 57	3eqtrd	$$⊢\phi \to \left({inv}_g\left(\mathrm{Scalar}\left(D\right)\right)\left(1_{\mathrm{Scalar}\left(D\right)}\right){\cdot }_{D}H\right)\left(X\right)={inv}_g\left(R\right)\left(H\left(X\right)\right)$$
59	58	oveq2d	$$⊢\phi \to G\left(X\right){+}_R\left({inv}_g\left(\mathrm{Scalar}\left(D\right)\right)\left(1_{\mathrm{Scalar}\left(D\right)}\right){\cdot }_{D}H\right)\left(X\right)=G\left(X\right){+}_R{inv}_g\left(R\right)\left(H\left(X\right)\right)$$
60	2 24 1 4	lflcl	$$⊢\left(W\in \mathrm{LMod}\wedge G\in F\wedge X\in V\right)\to G\left(X\right)\in {\mathrm{Base}}_R$$
61	7 8 10 60	syl3anc	$$⊢\phi \to G\left(X\right)\in {\mathrm{Base}}_R$$
62	24 23 38 3	grpsubval	$$⊢\left(G\left(X\right)\in {\mathrm{Base}}_R\wedge H\left(X\right)\in {\mathrm{Base}}_R\right)\to G\left(X\right)SH\left(X\right)=G\left(X\right){+}_R{inv}_g\left(R\right)\left(H\left(X\right)\right)$$
63	61 56 62	syl2anc	$$⊢\phi \to G\left(X\right)SH\left(X\right)=G\left(X\right){+}_R{inv}_g\left(R\right)\left(H\left(X\right)\right)$$
64	59 63	eqtr4d	$$⊢\phi \to G\left(X\right){+}_R\left({inv}_g\left(\mathrm{Scalar}\left(D\right)\right)\left(1_{\mathrm{Scalar}\left(D\right)}\right){\cdot }_{D}H\right)\left(X\right)=G\left(X\right)SH\left(X\right)$$
65	22 37 64	3eqtrd	$$⊢\phi \to \left(G\underset{\dot{}}{-}H\right)\left(X\right)=G\left(X\right)SH\left(X\right)$$