Theorem lspf

Description: The span operator on a left module maps subsets to subsets. (Contributed by Stefan O'Rear, 12-Dec-2014)

	Ref	Expression
Hypotheses	lspval.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lspval.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lspval.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion	lspf	⊢ ( 𝑊 ∈ LMod → 𝑁 : 𝒫 𝑉 ⟶ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		lspval.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspval.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3		lspval.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4	1 2 3	lspfval	⊢ ( 𝑊 ∈ LMod → 𝑁 = ( 𝑠 ∈ 𝒫 𝑉 ↦ ∩ { 𝑝 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑝 } ) )
5		simpl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑠 ∈ 𝒫 𝑉 ) → 𝑊 ∈ LMod )
6		ssrab2	⊢ { 𝑝 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑝 } ⊆ 𝑆
7	6	a1i	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑠 ∈ 𝒫 𝑉 ) → { 𝑝 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑝 } ⊆ 𝑆 )
8	1 2	lss1	⊢ ( 𝑊 ∈ LMod → 𝑉 ∈ 𝑆 )
9		elpwi	⊢ ( 𝑠 ∈ 𝒫 𝑉 → 𝑠 ⊆ 𝑉 )
10		sseq2	⊢ ( 𝑝 = 𝑉 → ( 𝑠 ⊆ 𝑝 ↔ 𝑠 ⊆ 𝑉 ) )
11	10	rspcev	⊢ ( ( 𝑉 ∈ 𝑆 ∧ 𝑠 ⊆ 𝑉 ) → ∃ 𝑝 ∈ 𝑆 𝑠 ⊆ 𝑝 )
12	8 9 11	syl2an	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑠 ∈ 𝒫 𝑉 ) → ∃ 𝑝 ∈ 𝑆 𝑠 ⊆ 𝑝 )
13		rabn0	⊢ ( { 𝑝 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑝 } ≠ ∅ ↔ ∃ 𝑝 ∈ 𝑆 𝑠 ⊆ 𝑝 )
14	12 13	sylibr	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑠 ∈ 𝒫 𝑉 ) → { 𝑝 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑝 } ≠ ∅ )
15	2	lssintcl	⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑝 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑝 } ⊆ 𝑆 ∧ { 𝑝 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑝 } ≠ ∅ ) → ∩ { 𝑝 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑝 } ∈ 𝑆 )
16	5 7 14 15	syl3anc	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑠 ∈ 𝒫 𝑉 ) → ∩ { 𝑝 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑝 } ∈ 𝑆 )
17	4 16	fmpt3d	⊢ ( 𝑊 ∈ LMod → 𝑁 : 𝒫 𝑉 ⟶ 𝑆 )