Theorem 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	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dihsmatrn.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
	dihsmatrn.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dihsmatrn.p	⊢ ⊕ = ( LSSum ‘ 𝑈 )
	dihsmatrn.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
	dihsmatrn.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dihsmatrn.x	⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
	dihsmatrn.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
Assertion	dihsmatrn	⊢ ( 𝜑 → ( 𝑋 ⊕ 𝑄 ) ∈ ran 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		dihsmatrn.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dihsmatrn.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3		dihsmatrn.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		dihsmatrn.p	⊢ ⊕ = ( LSSum ‘ 𝑈 )
5		dihsmatrn.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
6		dihsmatrn.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7		dihsmatrn.x	⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
8		dihsmatrn.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
9		eqid	⊢ ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
10	1 2 9 3 4 5 6 7 8	dihjat2	⊢ ( 𝜑 → ( 𝑋 ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) 𝑄 ) = ( 𝑋 ⊕ 𝑄 ) )
11	10	eqcomd	⊢ ( 𝜑 → ( 𝑋 ⊕ 𝑄 ) = ( 𝑋 ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) 𝑄 ) )
12		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
13		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
14	1 3 2 13	dihrnlss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝑋 ∈ ( LSubSp ‘ 𝑈 ) )
15	6 7 14	syl2anc	⊢ ( 𝜑 → 𝑋 ∈ ( LSubSp ‘ 𝑈 ) )
16	1 3 6	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
17	13 5 16 8	lsatlssel	⊢ ( 𝜑 → 𝑄 ∈ ( LSubSp ‘ 𝑈 ) )
18	1 3 12 13 4 2 9 6 15 17	djhlsmcl	⊢ ( 𝜑 → ( ( 𝑋 ⊕ 𝑄 ) ∈ ran 𝐼 ↔ ( 𝑋 ⊕ 𝑄 ) = ( 𝑋 ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) 𝑄 ) ) )
19	11 18	mpbird	⊢ ( 𝜑 → ( 𝑋 ⊕ 𝑄 ) ∈ ran 𝐼 )