Theorem lcdvadd

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

	Ref	Expression
Hypotheses	lcdvadd.h	|- H = ( LHyp ` K )
	lcdvadd.u	|- U = ( ( DVecH ` K ) ` W )
	lcdvadd.d	|- D = ( LDual ` U )
	lcdvadd.a	|- .+ = ( +g ` D )
	lcdvadd.c	|- C = ( ( LCDual ` K ) ` W )
	lcdvadd.p	|- .+b = ( +g ` C )
	lcdvadd.k	|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion	lcdvadd	|- ( ph -> .+b = .+ )

Proof

Step	Hyp	Ref	Expression
1		lcdvadd.h	|- H = ( LHyp ` K )
2		lcdvadd.u	|- U = ( ( DVecH ` K ) ` W )
3		lcdvadd.d	|- D = ( LDual ` U )
4		lcdvadd.a	|- .+ = ( +g ` D )
5		lcdvadd.c	|- C = ( ( LCDual ` K ) ` W )
6		lcdvadd.p	|- .+b = ( +g ` C )
7		lcdvadd.k	|- ( ph -> ( K e. HL /\ W e. H ) )
8		eqid	|- ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
9		eqid	|- ( LFnl ` U ) = ( LFnl ` U )
10		eqid	|- ( LKer ` U ) = ( LKer ` U )
11	1 8 5 2 9 10 3 7	lcdval	|- ( ph -> C = ( D |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) )
12	11	fveq2d	|- ( ph -> ( +g ` C ) = ( +g ` ( D |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) ) )
13		fvex	|- ( LFnl ` U ) e. _V
14	13	rabex	|- { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } e. _V
15		eqid	|- ( D |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) = ( D |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } )
16	15 4	ressplusg	|- ( { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } e. _V -> .+ = ( +g ` ( D |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) ) )
17	14 16	ax-mp	|- .+ = ( +g ` ( D |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) )
18	12 6 17	3eqtr4g	|- ( ph -> .+b = .+ )