This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lspf

Description: The span function on a left module maps subsets to subspaces. (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 → 𝑁 : 𝒫 𝑉 ⟶ 𝑆 )