Theorem hdmapadd

Description: Part 11 in Baer p. 48 line 35, (a+b)S = aS+bS in their notation (S = sigma). (Contributed by NM, 22-May-2015)

	Ref	Expression
Hypotheses	hdmap11.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmap11.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmap11.v	$$⊢V={\mathrm{Base}}_U$$
	hdmap11.p	$$⊢\underset{\dot{}}{+}={+}_U$$
	hdmap11.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmap11.a	$$⊢\underset{\dot{}}{✚}={+}_C$$
	hdmap11.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmap11.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmap11.x	$$⊢\phi \to X\in V$$
	hdmap11.y	$$⊢\phi \to Y\in V$$
Assertion	hdmapadd	$$⊢\phi \to S\left(X\underset{\dot{}}{+}Y\right)=S\left(X\right)\underset{\dot{}}{✚}S\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmap11.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmap11.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmap11.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmap11.p	$$⊢\underset{\dot{}}{+}={+}_U$$
5		hdmap11.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
6		hdmap11.a	$$⊢\underset{\dot{}}{✚}={+}_C$$
7		hdmap11.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
8		hdmap11.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		hdmap11.x	$$⊢\phi \to X\in V$$
10		hdmap11.y	$$⊢\phi \to Y\in V$$
11		eqid	$$⊢⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩$$
12		eqid	$$⊢0_U=0_U$$
13		eqid	$$⊢\mathrm{LSpan}\left(U\right)=\mathrm{LSpan}\left(U\right)$$
14		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
15		eqid	$$⊢\mathrm{LSpan}\left(C\right)=\mathrm{LSpan}\left(C\right)$$
16		eqid	$$⊢\mathrm{mapd}\left(K\right)\left(W\right)=\mathrm{mapd}\left(K\right)\left(W\right)$$
17		eqid	$$⊢\mathrm{HVMap}\left(K\right)\left(W\right)=\mathrm{HVMap}\left(K\right)\left(W\right)$$
18		eqid	$$⊢\mathrm{HDMap1}\left(K\right)\left(W\right)=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
19	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18	hdmap11lem2	$$⊢\phi \to S\left(X\underset{\dot{}}{+}Y\right)=S\left(X\right)\underset{\dot{}}{✚}S\left(Y\right)$$