dihsmatrn

Description: The subspace sum of a closed subspace and an atom is closed. TODO: see if proof at https://math.stackexchange.com/a/1233211/50776 and Mon, 13 Apr 2015 20:44:07 -0400 email could be used instead of this and dihjat2 . (Contributed by NM, 15-Jan-2015)

	Ref	Expression
Hypotheses	dihsmatrn.h	\|- H = ( LHyp ` K )
	dihsmatrn.i	\|- I = ( ( DIsoH ` K ) ` W )
	dihsmatrn.u	\|- U = ( ( DVecH ` K ) ` W )
	dihsmatrn.p	\|- .(+) = ( LSSum ` U )
	dihsmatrn.a	\|- A = ( LSAtoms ` U )
	dihsmatrn.k	\|- ( ph -> ( K e. HL /\ W e. H ) )
	dihsmatrn.x	\|- ( ph -> X e. ran I )
	dihsmatrn.q	\|- ( ph -> Q e. A )
Assertion	dihsmatrn	\|- ( ph -> ( X .(+) Q ) e. ran I )

Proof

Step	Hyp	Ref	Expression
1		dihsmatrn.h	\|- H = ( LHyp ` K )
2		dihsmatrn.i	\|- I = ( ( DIsoH ` K ) ` W )
3		dihsmatrn.u	\|- U = ( ( DVecH ` K ) ` W )
4		dihsmatrn.p	\|- .(+) = ( LSSum ` U )
5		dihsmatrn.a	\|- A = ( LSAtoms ` U )
6		dihsmatrn.k	\|- ( ph -> ( K e. HL /\ W e. H ) )
7		dihsmatrn.x	\|- ( ph -> X e. ran I )
8		dihsmatrn.q	\|- ( ph -> Q e. A )
9		eqid	\|- ( ( joinH ` K ) ` W ) = ( ( joinH ` K ) ` W )
10	1 2 9 3 4 5 6 7 8	dihjat2	\|- ( ph -> ( X ( ( joinH ` K ) ` W ) Q ) = ( X .(+) Q ) )
11	10	eqcomd	\|- ( ph -> ( X .(+) Q ) = ( X ( ( joinH ` K ) ` W ) Q ) )
12		eqid	\|- ( Base ` U ) = ( Base ` U )
13		eqid	\|- ( LSubSp ` U ) = ( LSubSp ` U )
14	1 3 2 13	dihrnlss	\|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> X e. ( LSubSp ` U ) )
15	6 7 14	syl2anc	\|- ( ph -> X e. ( LSubSp ` U ) )
16	1 3 6	dvhlmod	\|- ( ph -> U e. LMod )
17	13 5 16 8	lsatlssel	\|- ( ph -> Q e. ( LSubSp ` U ) )
18	1 3 12 13 4 2 9 6 15 17	djhlsmcl	\|- ( ph -> ( ( X .(+) Q ) e. ran I <-> ( X .(+) Q ) = ( X ( ( joinH ` K ) ` W ) Q ) ) )
19	11 18	mpbird	\|- ( ph -> ( X .(+) Q ) e. ran I )

Metamath Proof Explorer

Theorem dihsmatrn

Proof