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	bitrid	⊢ ( 𝜑 → ( 𝑋 ∈ { 𝑎 ∣ ∃ 𝑓 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) 𝑎 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) } ↔ ∃ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) ( 𝑓 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ) ) )
40	22 39	bitrd	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ ( 𝐹 “ 𝐼 ) ) ↔ ∃ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) ( 𝑓 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ) ) )