Metamath Proof Explorer

Theorem lsatset

Description: The set of all 1-dim subspaces (atoms) of a left module or left vector space. (Contributed by NM, 9-Apr-2014) (Revised by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses lsatset.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lsatset.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lsatset.z ⊢ 0 = ( 0g ‘ 𝑊 )
lsatset.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
Assertion lsatset ( 𝑊 ∈ 𝑋 → 𝐴 = ran ( 𝑣 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑁 ‘ { 𝑣 } ) ) )

Proof

Step Hyp Ref Expression
1 lsatset.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lsatset.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3 lsatset.z ⊢ 0 = ( 0g ‘ 𝑊 )
4 lsatset.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
5 elex ⊢ ( 𝑊 ∈ 𝑋 → 𝑊 ∈ V )
6 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
7 6 1 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝑉 )
8 fveq2 ⊢ ( 𝑤 = 𝑊 → ( 0g ‘ 𝑤 ) = ( 0g ‘ 𝑊 ) )
9 8 3 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( 0g ‘ 𝑤 ) = 0 )
10 9 sneqd ⊢ ( 𝑤 = 𝑊 → { ( 0g ‘ 𝑤 ) } = { 0 } )
11 7 10 difeq12d ⊢ ( 𝑤 = 𝑊 → ( ( Base ‘ 𝑤 ) ∖ { ( 0g ‘ 𝑤 ) } ) = ( 𝑉 ∖ { 0 } ) )
12 fveq2 ⊢ ( 𝑤 = 𝑊 → ( LSpan ‘ 𝑤 ) = ( LSpan ‘ 𝑊 ) )
13 12 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( LSpan ‘ 𝑤 ) = 𝑁 )
14 13 fveq1d ⊢ ( 𝑤 = 𝑊 → ( ( LSpan ‘ 𝑤 ) ‘ { 𝑣 } ) = ( 𝑁 ‘ { 𝑣 } ) )
15 11 14 mpteq12dv ⊢ ( 𝑤 = 𝑊 → ( 𝑣 ∈ ( ( Base ‘ 𝑤 ) ∖ { ( 0g ‘ 𝑤 ) } ) ↦ ( ( LSpan ‘ 𝑤 ) ‘ { 𝑣 } ) ) = ( 𝑣 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑁 ‘ { 𝑣 } ) ) )
16 15 rneqd ⊢ ( 𝑤 = 𝑊 → ran ( 𝑣 ∈ ( ( Base ‘ 𝑤 ) ∖ { ( 0g ‘ 𝑤 ) } ) ↦ ( ( LSpan ‘ 𝑤 ) ‘ { 𝑣 } ) ) = ran ( 𝑣 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑁 ‘ { 𝑣 } ) ) )
17 df-lsatoms ⊢ LSAtoms = ( 𝑤 ∈ V ↦ ran ( 𝑣 ∈ ( ( Base ‘ 𝑤 ) ∖ { ( 0g ‘ 𝑤 ) } ) ↦ ( ( LSpan ‘ 𝑤 ) ‘ { 𝑣 } ) ) )
18 2 fvexi ⊢ 𝑁 ∈ V
19 18 rnex ⊢ ran 𝑁 ∈ V
20 p0ex ⊢ { ∅ } ∈ V
21 19 20 unex ⊢ ( ran 𝑁 ∪ { ∅ } ) ∈ V
22 eqid ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝑣 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑁 ‘ { 𝑣 } ) )
23 fvrn0 ⊢ ( 𝑁 ‘ { 𝑣 } ) ∈ ( ran 𝑁 ∪ { ∅ } )
24 23 a1i ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 0 } ) → ( 𝑁 ‘ { 𝑣 } ) ∈ ( ran 𝑁 ∪ { ∅ } ) )
25 22 24 fmpti ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑁 ‘ { 𝑣 } ) ) : ( 𝑉 ∖ { 0 } ) ⟶ ( ran 𝑁 ∪ { ∅ } )
26 frn ⊢ ( ( 𝑣 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑁 ‘ { 𝑣 } ) ) : ( 𝑉 ∖ { 0 } ) ⟶ ( ran 𝑁 ∪ { ∅ } ) → ran ( 𝑣 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑁 ‘ { 𝑣 } ) ) ⊆ ( ran 𝑁 ∪ { ∅ } ) )
27 25 26 ax-mp ⊢ ran ( 𝑣 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑁 ‘ { 𝑣 } ) ) ⊆ ( ran 𝑁 ∪ { ∅ } )
28 21 27 ssexi ⊢ ran ( 𝑣 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑁 ‘ { 𝑣 } ) ) ∈ V
29 16 17 28 fvmpt ⊢ ( 𝑊 ∈ V → ( LSAtoms ‘ 𝑊 ) = ran ( 𝑣 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑁 ‘ { 𝑣 } ) ) )
30 5 29 syl ⊢ ( 𝑊 ∈ 𝑋 → ( LSAtoms ‘ 𝑊 ) = ran ( 𝑣 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑁 ‘ { 𝑣 } ) ) )
31 4 30 syl5eq ⊢ ( 𝑊 ∈ 𝑋 → 𝐴 = ran ( 𝑣 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑁 ‘ { 𝑣 } ) ) )