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	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	mapdlsmcl.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
	mapdlsmcl.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	mapdlsmcl.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	mapdlsmcl.p	⊢ ⊕ = ( LSSum ‘ 𝐶 )
	mapdlsmcl.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	mapdlsmcl.x	⊢ ( 𝜑 → 𝑋 ∈ ran 𝑀 )
	mapdlsmcl.y	⊢ ( 𝜑 → 𝑌 ∈ ran 𝑀 )
Assertion	mapdlsmcl	⊢ ( 𝜑 → ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		mapdlsmcl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		mapdlsmcl.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
3		mapdlsmcl.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		mapdlsmcl.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
5		mapdlsmcl.p	⊢ ⊕ = ( LSSum ‘ 𝐶 )
6		mapdlsmcl.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7		mapdlsmcl.x	⊢ ( 𝜑 → 𝑋 ∈ ran 𝑀 )
8		mapdlsmcl.y	⊢ ( 𝜑 → 𝑌 ∈ ran 𝑀 )
9	1 4 6	lcdlmod	⊢ ( 𝜑 → 𝐶 ∈ LMod )
10		eqid	⊢ ( LSubSp ‘ 𝐶 ) = ( LSubSp ‘ 𝐶 )
11	1 2 4 10 6	mapdrn2	⊢ ( 𝜑 → ran 𝑀 = ( LSubSp ‘ 𝐶 ) )
12	7 11	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( LSubSp ‘ 𝐶 ) )
13	8 11	eleqtrd	⊢ ( 𝜑 → 𝑌 ∈ ( LSubSp ‘ 𝐶 ) )
14	10 5	lsmcl	⊢ ( ( 𝐶 ∈ LMod ∧ 𝑋 ∈ ( LSubSp ‘ 𝐶 ) ∧ 𝑌 ∈ ( LSubSp ‘ 𝐶 ) ) → ( 𝑋 ⊕ 𝑌 ) ∈ ( LSubSp ‘ 𝐶 ) )
15	9 12 13 14	syl3anc	⊢ ( 𝜑 → ( 𝑋 ⊕ 𝑌 ) ∈ ( LSubSp ‘ 𝐶 ) )
16	15 11	eleqtrrd	⊢ ( 𝜑 → ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝑀 )