Theorem lcdsadd

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

	Ref	Expression
Hypotheses	lcdsadd.h	|- H = ( LHyp ` K )
	lcdsadd.u	|- U = ( ( DVecH ` K ) ` W )
	lcdsadd.f	|- F = ( Scalar ` U )
	lcdsadd.p	|- .+ = ( +g ` F )
	lcdsadd.c	|- C = ( ( LCDual ` K ) ` W )
	lcdsadd.s	|- S = ( Scalar ` C )
	lcdsadd.a	|- .+b = ( +g ` S )
	lcdsadd.k	|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion	lcdsadd	|- ( ph -> .+b = .+ )

Proof

Step	Hyp	Ref	Expression
1		lcdsadd.h	|- H = ( LHyp ` K )
2		lcdsadd.u	|- U = ( ( DVecH ` K ) ` W )
3		lcdsadd.f	|- F = ( Scalar ` U )
4		lcdsadd.p	|- .+ = ( +g ` F )
5		lcdsadd.c	|- C = ( ( LCDual ` K ) ` W )
6		lcdsadd.s	|- S = ( Scalar ` C )
7		lcdsadd.a	|- .+b = ( +g ` S )
8		lcdsadd.k	|- ( ph -> ( K e. HL /\ W e. H ) )
9		eqid	|- ( oppR ` F ) = ( oppR ` F )
10	1 2 3 9 5 6 8	lcdsca	|- ( ph -> S = ( oppR ` F ) )
11	10	fveq2d	|- ( ph -> ( +g ` S ) = ( +g ` ( oppR ` F ) ) )
12	9 4	oppradd	|- .+ = ( +g ` ( oppR ` F ) )
13	11 7 12	3eqtr4g	|- ( ph -> .+b = .+ )