Theorem lcfrlem7

Description: Lemma for lcfr . Closure of vector sum when one vector is zero. TODO: share hypotheses with others. (Contributed by NM, 11-Mar-2015)

	Ref	Expression
Hypotheses	lcfrlem7.h	|- H = ( LHyp ` K )
	lcfrlem7.o	|- ._|_ = ( ( ocH ` K ) ` W )
	lcfrlem7.u	|- U = ( ( DVecH ` K ) ` W )
	lcfrlem7.p	|- .+ = ( +g ` U )
	lcfrlem7.l	|- L = ( LKer ` U )
	lcfrlem7.d	|- D = ( LDual ` U )
	lcfrlem7.q	|- Q = ( LSubSp ` D )
	lcfrlem7.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	lcfrlem7.g	|- ( ph -> G e. Q )
	lcfrlem7.e	|- E = U_ g e. G ( ._|_ ` ( L ` g ) )
	lcfrlem7.x	|- ( ph -> X e. E )
	lcfrlem7.z	|- .0. = ( 0g ` U )
	lcfrlem7.y	|- ( ph -> Y = .0. )
Assertion	lcfrlem7	|- ( ph -> ( X .+ Y ) e. E )

Proof

Step	Hyp	Ref	Expression
1		lcfrlem7.h	|- H = ( LHyp ` K )
2		lcfrlem7.o	|- ._|_ = ( ( ocH ` K ) ` W )
3		lcfrlem7.u	|- U = ( ( DVecH ` K ) ` W )
4		lcfrlem7.p	|- .+ = ( +g ` U )
5		lcfrlem7.l	|- L = ( LKer ` U )
6		lcfrlem7.d	|- D = ( LDual ` U )
7		lcfrlem7.q	|- Q = ( LSubSp ` D )
8		lcfrlem7.k	|- ( ph -> ( K e. HL /\ W e. H ) )
9		lcfrlem7.g	|- ( ph -> G e. Q )
10		lcfrlem7.e	|- E = U_ g e. G ( ._|_ ` ( L ` g ) )
11		lcfrlem7.x	|- ( ph -> X e. E )
12		lcfrlem7.z	|- .0. = ( 0g ` U )
13		lcfrlem7.y	|- ( ph -> Y = .0. )
14	13	oveq2d	|- ( ph -> ( X .+ Y ) = ( X .+ .0. ) )
15	1 3 8	dvhlmod	|- ( ph -> U e. LMod )
16		eqid	|- ( Base ` U ) = ( Base ` U )
17	1 2 3 16 5 6 7 10 8 9 11	lcfrlem4	|- ( ph -> X e. ( Base ` U ) )
18	16 4 12	lmod0vrid	|- ( ( U e. LMod /\ X e. ( Base ` U ) ) -> ( X .+ .0. ) = X )
19	15 17 18	syl2anc	|- ( ph -> ( X .+ .0. ) = X )
20	14 19	eqtrd	|- ( ph -> ( X .+ Y ) = X )
21	20 11	eqeltrd	|- ( ph -> ( X .+ Y ) e. E )