Theorem lcdsadd

Description: Scalar addition for the closed kernel vector space dual. (Contributed by NM, 6-Jun-2015)

	Ref	Expression
Hypotheses	lcdsadd.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcdsadd.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcdsadd.f	$$⊢F=\mathrm{Scalar}\left(U\right)$$
	lcdsadd.p	$$⊢\underset{\dot{}}{+}={+}_F$$
	lcdsadd.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	lcdsadd.s	$$⊢S=\mathrm{Scalar}\left(C\right)$$
	lcdsadd.a	$$⊢\underset{\dot{}}{✚}={+}_S$$
	lcdsadd.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	lcdsadd	$$⊢\phi \to \underset{\dot{}}{✚}=\underset{\dot{}}{+}$$

Proof

Step	Hyp	Ref	Expression
1		lcdsadd.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcdsadd.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		lcdsadd.f	$$⊢F=\mathrm{Scalar}\left(U\right)$$
4		lcdsadd.p	$$⊢\underset{\dot{}}{+}={+}_F$$
5		lcdsadd.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
6		lcdsadd.s	$$⊢S=\mathrm{Scalar}\left(C\right)$$
7		lcdsadd.a	$$⊢\underset{\dot{}}{✚}={+}_S$$
8		lcdsadd.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		eqid	$$⊢{opp}_r\left(F\right)={opp}_r\left(F\right)$$
10	1 2 3 9 5 6 8	lcdsca	$$⊢\phi \to S={opp}_r\left(F\right)$$
11	10	fveq2d	$$⊢\phi \to {+}_S={+}_{{opp}_r\left(F\right)}$$
12	9 4	oppradd	$$⊢\underset{\dot{}}{+}={+}_{{opp}_r\left(F\right)}$$
13	11 7 12	3eqtr4g	$$⊢\phi \to \underset{\dot{}}{✚}=\underset{\dot{}}{+}$$