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 = ( LHyp ` K )
	hdmap11.u	|- U = ( ( DVecH ` K ) ` W )
	hdmap11.v	|- V = ( Base ` U )
	hdmap11.p	|- .+ = ( +g ` U )
	hdmap11.c	|- C = ( ( LCDual ` K ) ` W )
	hdmap11.a	|- .+b = ( +g ` C )
	hdmap11.s	|- S = ( ( HDMap ` K ) ` W )
	hdmap11.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hdmap11.x	|- ( ph -> X e. V )
	hdmap11.y	|- ( ph -> Y e. V )
Assertion	hdmapadd	|- ( ph -> ( S ` ( X .+ Y ) ) = ( ( S ` X ) .+b ( S ` Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		hdmap11.h	|- H = ( LHyp ` K )
2		hdmap11.u	|- U = ( ( DVecH ` K ) ` W )
3		hdmap11.v	|- V = ( Base ` U )
4		hdmap11.p	|- .+ = ( +g ` U )
5		hdmap11.c	|- C = ( ( LCDual ` K ) ` W )
6		hdmap11.a	|- .+b = ( +g ` C )
7		hdmap11.s	|- S = ( ( HDMap ` K ) ` W )
8		hdmap11.k	|- ( ph -> ( K e. HL /\ W e. H ) )
9		hdmap11.x	|- ( ph -> X e. V )
10		hdmap11.y	|- ( ph -> Y e. V )
11		eqid	|- <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
12		eqid	|- ( 0g ` U ) = ( 0g ` U )
13		eqid	|- ( LSpan ` U ) = ( LSpan ` U )
14		eqid	|- ( Base ` C ) = ( Base ` C )
15		eqid	|- ( LSpan ` C ) = ( LSpan ` C )
16		eqid	|- ( ( mapd ` K ) ` W ) = ( ( mapd ` K ) ` W )
17		eqid	|- ( ( HVMap ` K ) ` W ) = ( ( HVMap ` K ) ` W )
18		eqid	|- ( ( HDMap1 ` K ) ` W ) = ( ( HDMap1 ` K ) ` W )
19	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18	hdmap11lem2	|- ( ph -> ( S ` ( X .+ Y ) ) = ( ( S ` X ) .+b ( S ` Y ) ) )