Theorem hdmapsub

Description: Part of proof of part 12 in Baer p. 49 line 5, (a-b)S = aS-bS in their notation (S = sigma). (Contributed by NM, 26-May-2015)

	Ref	Expression
Hypotheses	hdmap12c.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmap12c.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmap12c.v	$$⊢V={\mathrm{Base}}_U$$
	hdmap12c.m	$$⊢\underset{\dot{}}{-}={-}_U$$
	hdmap12c.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmap12c.n	$$⊢N={-}_C$$
	hdmap12c.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmap12c.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmap12c.x	$$⊢\phi \to X\in V$$
	hdmap12c.y	$$⊢\phi \to Y\in V$$
Assertion	hdmapsub	$$⊢\phi \to S\left(X\underset{\dot{}}{-}Y\right)=S\left(X\right)NS\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmap12c.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmap12c.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmap12c.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmap12c.m	$$⊢\underset{\dot{}}{-}={-}_U$$
5		hdmap12c.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
6		hdmap12c.n	$$⊢N={-}_C$$
7		hdmap12c.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
8		hdmap12c.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		hdmap12c.x	$$⊢\phi \to X\in V$$
10		hdmap12c.y	$$⊢\phi \to Y\in V$$
11		eqid	$$⊢{+}_U={+}_U$$
12		eqid	$$⊢{inv}_g\left(U\right)={inv}_g\left(U\right)$$
13	3 11 12 4	grpsubval	$$⊢\left(X\in V\wedge Y\in V\right)\to X\underset{\dot{}}{-}Y=X{+}_U{inv}_g\left(U\right)\left(Y\right)$$
14	9 10 13	syl2anc	$$⊢\phi \to X\underset{\dot{}}{-}Y=X{+}_U{inv}_g\left(U\right)\left(Y\right)$$
15	14	fveq2d	$$⊢\phi \to S\left(X\underset{\dot{}}{-}Y\right)=S\left(X{+}_U{inv}_g\left(U\right)\left(Y\right)\right)$$
16		eqid	$$⊢{+}_C={+}_C$$
17	1 2 8	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
18	3 12	lmodvnegcl	$$⊢\left(U\in \mathrm{LMod}\wedge Y\in V\right)\to {inv}_g\left(U\right)\left(Y\right)\in V$$
19	17 10 18	syl2anc	$$⊢\phi \to {inv}_g\left(U\right)\left(Y\right)\in V$$
20	1 2 3 11 5 16 7 8 9 19	hdmapadd	$$⊢\phi \to S\left(X{+}_U{inv}_g\left(U\right)\left(Y\right)\right)=S\left(X\right){+}_{C}S\left({inv}_g\left(U\right)\left(Y\right)\right)$$
21		eqid	$$⊢{inv}_g\left(C\right)={inv}_g\left(C\right)$$
22	1 2 3 12 5 21 7 8 10	hdmapneg	$$⊢\phi \to S\left({inv}_g\left(U\right)\left(Y\right)\right)={inv}_g\left(C\right)\left(S\left(Y\right)\right)$$
23	22	oveq2d	$$⊢\phi \to S\left(X\right){+}_{C}S\left({inv}_g\left(U\right)\left(Y\right)\right)=S\left(X\right){+}_C{inv}_g\left(C\right)\left(S\left(Y\right)\right)$$
24	15 20 23	3eqtrd	$$⊢\phi \to S\left(X\underset{\dot{}}{-}Y\right)=S\left(X\right){+}_C{inv}_g\left(C\right)\left(S\left(Y\right)\right)$$
25		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
26	1 2 3 5 25 7 8 9	hdmapcl	$$⊢\phi \to S\left(X\right)\in {\mathrm{Base}}_C$$
27	1 2 3 5 25 7 8 10	hdmapcl	$$⊢\phi \to S\left(Y\right)\in {\mathrm{Base}}_C$$
28	25 16 21 6	grpsubval	$$⊢\left(S\left(X\right)\in {\mathrm{Base}}_C\wedge S\left(Y\right)\in {\mathrm{Base}}_C\right)\to S\left(X\right)NS\left(Y\right)=S\left(X\right){+}_C{inv}_g\left(C\right)\left(S\left(Y\right)\right)$$
29	26 27 28	syl2anc	$$⊢\phi \to S\left(X\right)NS\left(Y\right)=S\left(X\right){+}_C{inv}_g\left(C\right)\left(S\left(Y\right)\right)$$
30	24 29	eqtr4d	$$⊢\phi \to S\left(X\underset{\dot{}}{-}Y\right)=S\left(X\right)NS\left(Y\right)$$