Metamath Proof Explorer

Theorem ellspd

Description: The elements of the span of an indexed collection of basic vectors are those vectors which can be written as finite linear combinations of basic vectors. (Contributed by Stefan O'Rear, 7-Feb-2015) (Revised by AV, 24-Jun-2019) (Revised by AV, 11-Apr-2024)

Ref Expression
Hypotheses ellspd.n ⊢ 𝑁 = ( LSpan ‘ 𝑀 )
ellspd.v ⊢ 𝐵 = ( Base ‘ 𝑀 )
ellspd.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
ellspd.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
ellspd.z ⊢ 0 = ( 0g ‘ 𝑆 )
ellspd.t ⊢ · = ( ·𝑠 ‘ 𝑀 )
ellspd.f ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )
ellspd.m ⊢ ( 𝜑 → 𝑀 ∈ LMod )
ellspd.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
Assertion ellspd ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ ( 𝐹 “ 𝐼 ) ) ↔ ∃ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) ( 𝑓 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ellspd.n ⊢ 𝑁 = ( LSpan ‘ 𝑀 )
2 ellspd.v ⊢ 𝐵 = ( Base ‘ 𝑀 )
3 ellspd.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
4 ellspd.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
5 ellspd.z ⊢ 0 = ( 0g ‘ 𝑆 )
6 ellspd.t ⊢ · = ( ·𝑠 ‘ 𝑀 )
7 ellspd.f ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )
8 ellspd.m ⊢ ( 𝜑 → 𝑀 ∈ LMod )
9 ellspd.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
10 ffn ⊢ ( 𝐹 : 𝐼 ⟶ 𝐵 → 𝐹 Fn 𝐼 )
11 fnima ⊢ ( 𝐹 Fn 𝐼 → ( 𝐹 “ 𝐼 ) = ran 𝐹 )
12 7 10 11 3syl ⊢ ( 𝜑 → ( 𝐹 “ 𝐼 ) = ran 𝐹 )
13 12 fveq2d ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝐹 “ 𝐼 ) ) = ( 𝑁 ‘ ran 𝐹 ) )
14 eqid ⊢ ( 𝑓 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) ↦ ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ) = ( 𝑓 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) ↦ ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) )
15 14 rnmpt ⊢ ran ( 𝑓 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) ↦ ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ) = { 𝑎 ∣ ∃ 𝑓 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) 𝑎 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) }
16 eqid ⊢ ( 𝑆 freeLMod 𝐼 ) = ( 𝑆 freeLMod 𝐼 )
17 eqid ⊢ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) = ( Base ‘ ( 𝑆 freeLMod 𝐼 ) )
18 4 a1i ⊢ ( 𝜑 → 𝑆 = ( Scalar ‘ 𝑀 ) )
19 16 17 2 6 14 8 9 18 7 1 frlmup3 ⊢ ( 𝜑 → ran ( 𝑓 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) ↦ ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ) = ( 𝑁 ‘ ran 𝐹 ) )
20 15 19 eqtr3id ⊢ ( 𝜑 → { 𝑎 ∣ ∃ 𝑓 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) 𝑎 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) } = ( 𝑁 ‘ ran 𝐹 ) )
21 13 20 eqtr4d ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝐹 “ 𝐼 ) ) = { 𝑎 ∣ ∃ 𝑓 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) 𝑎 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) } )
22 21 eleq2d ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ ( 𝐹 “ 𝐼 ) ) ↔ 𝑋 ∈ { 𝑎 ∣ ∃ 𝑓 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) 𝑎 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) } ) )
23 ovex ⊢ ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ∈ V
24 eleq1 ⊢ ( 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) → ( 𝑋 ∈ V ↔ ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ∈ V ) )
25 23 24 mpbiri ⊢ ( 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) → 𝑋 ∈ V )
26 25 rexlimivw ⊢ ( ∃ 𝑓 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) → 𝑋 ∈ V )
27 eqeq1 ⊢ ( 𝑎 = 𝑋 → ( 𝑎 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ↔ 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ) )
28 27 rexbidv ⊢ ( 𝑎 = 𝑋 → ( ∃ 𝑓 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) 𝑎 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ↔ ∃ 𝑓 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ) )
29 26 28 elab3 ⊢ ( 𝑋 ∈ { 𝑎 ∣ ∃ 𝑓 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) 𝑎 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) } ↔ ∃ 𝑓 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) )
30 4 fvexi ⊢ 𝑆 ∈ V
31 eqid ⊢ { 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ∣ 𝑎 finSupp 0 } = { 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ∣ 𝑎 finSupp 0 }
32 16 3 5 31 frlmbas ⊢ ( ( 𝑆 ∈ V ∧ 𝐼 ∈ 𝑉 ) → { 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ∣ 𝑎 finSupp 0 } = ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) )
33 30 9 32 sylancr ⊢ ( 𝜑 → { 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ∣ 𝑎 finSupp 0 } = ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) )
34 33 eqcomd ⊢ ( 𝜑 → ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) = { 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ∣ 𝑎 finSupp 0 } )
35 34 rexeqdv ⊢ ( 𝜑 → ( ∃ 𝑓 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ↔ ∃ 𝑓 ∈ { 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ∣ 𝑎 finSupp 0 } 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ) )
36 breq1 ⊢ ( 𝑎 = 𝑓 → ( 𝑎 finSupp 0 ↔ 𝑓 finSupp 0 ) )
37 36 rexrab ⊢ ( ∃ 𝑓 ∈ { 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ∣ 𝑎 finSupp 0 } 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ↔ ∃ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) ( 𝑓 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ) )
38 35 37 bitrdi ⊢ ( 𝜑 → ( ∃ 𝑓 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ↔ ∃ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) ( 𝑓 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ) ) )
39 29 38 syl5bb ⊢ ( 𝜑 → ( 𝑋 ∈ { 𝑎 ∣ ∃ 𝑓 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) 𝑎 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) } ↔ ∃ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) ( 𝑓 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ) ) )
40 22 39 bitrd ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ ( 𝐹 “ 𝐼 ) ) ↔ ∃ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) ( 𝑓 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ) ) )