Theorem dihsmsprn

Description: Subspace sum of a closed subspace and the span of a singleton. (Contributed by NM, 17-Jan-2015)

	Ref	Expression
Hypotheses	dihsmsprn.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dihsmsprn.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dihsmsprn.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	dihsmsprn.p	⊢ ⊕ = ( LSSum ‘ 𝑈 )
	dihsmsprn.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	dihsmsprn.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
	dihsmsprn.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dihsmsprn.x	⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
	dihsmsprn.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
Assertion	dihsmsprn	⊢ ( 𝜑 → ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) ∈ ran 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		dihsmsprn.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dihsmsprn.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		dihsmsprn.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		dihsmsprn.p	⊢ ⊕ = ( LSSum ‘ 𝑈 )
5		dihsmsprn.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
6		dihsmsprn.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
7		dihsmsprn.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8		dihsmsprn.x	⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
9		dihsmsprn.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
10		eqid	⊢ ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
11	1 2 3 4 5 6 10 7 8 9	dihjat1	⊢ ( 𝜑 → ( 𝑋 ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) )
12	1 2 6 3	dihrnss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝑋 ⊆ 𝑉 )
13	7 8 12	syl2anc	⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
14	1 2 7	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
15	9	snssd	⊢ ( 𝜑 → { 𝑇 } ⊆ 𝑉 )
16	3 5	lspssv	⊢ ( ( 𝑈 ∈ LMod ∧ { 𝑇 } ⊆ 𝑉 ) → ( 𝑁 ‘ { 𝑇 } ) ⊆ 𝑉 )
17	14 15 16	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑇 } ) ⊆ 𝑉 )
18	1 6 2 3 10	djhcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑉 ∧ ( 𝑁 ‘ { 𝑇 } ) ⊆ 𝑉 ) ) → ( 𝑋 ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑁 ‘ { 𝑇 } ) ) ∈ ran 𝐼 )
19	7 13 17 18	syl12anc	⊢ ( 𝜑 → ( 𝑋 ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑁 ‘ { 𝑇 } ) ) ∈ ran 𝐼 )
20	11 19	eqeltrrd	⊢ ( 𝜑 → ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) ∈ ran 𝐼 )