Theorem mapdlsmcl

Description: Closure of dual subspace sum for the map defined by df-mapd . (Contributed by NM, 13-Mar-2015)

	Ref	Expression
Hypotheses	mapdlsmcl.h	|- H = ( LHyp ` K )
	mapdlsmcl.m	|- M = ( ( mapd ` K ) ` W )
	mapdlsmcl.u	|- U = ( ( DVecH ` K ) ` W )
	mapdlsmcl.c	|- C = ( ( LCDual ` K ) ` W )
	mapdlsmcl.p	|- .(+) = ( LSSum ` C )
	mapdlsmcl.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	mapdlsmcl.x	|- ( ph -> X e. ran M )
	mapdlsmcl.y	|- ( ph -> Y e. ran M )
Assertion	mapdlsmcl	|- ( ph -> ( X .(+) Y ) e. ran M )

Proof

Step	Hyp	Ref	Expression
1		mapdlsmcl.h	|- H = ( LHyp ` K )
2		mapdlsmcl.m	|- M = ( ( mapd ` K ) ` W )
3		mapdlsmcl.u	|- U = ( ( DVecH ` K ) ` W )
4		mapdlsmcl.c	|- C = ( ( LCDual ` K ) ` W )
5		mapdlsmcl.p	|- .(+) = ( LSSum ` C )
6		mapdlsmcl.k	|- ( ph -> ( K e. HL /\ W e. H ) )
7		mapdlsmcl.x	|- ( ph -> X e. ran M )
8		mapdlsmcl.y	|- ( ph -> Y e. ran M )
9	1 4 6	lcdlmod	|- ( ph -> C e. LMod )
10		eqid	|- ( LSubSp ` C ) = ( LSubSp ` C )
11	1 2 4 10 6	mapdrn2	|- ( ph -> ran M = ( LSubSp ` C ) )
12	7 11	eleqtrd	|- ( ph -> X e. ( LSubSp ` C ) )
13	8 11	eleqtrd	|- ( ph -> Y e. ( LSubSp ` C ) )
14	10 5	lsmcl	|- ( ( C e. LMod /\ X e. ( LSubSp ` C ) /\ Y e. ( LSubSp ` C ) ) -> ( X .(+) Y ) e. ( LSubSp ` C ) )
15	9 12 13 14	syl3anc	|- ( ph -> ( X .(+) Y ) e. ( LSubSp ` C ) )
16	15 11	eleqtrrd	|- ( ph -> ( X .(+) Y ) e. ran M )