Theorem ellspds

Description: Variation on ellspd . (Contributed by Thierry Arnoux, 18-May-2023)

	Ref	Expression
Hypotheses	ellspds.n	⊢ 𝑁 = ( LSpan ‘ 𝑀 )
	ellspds.v	⊢ 𝐵 = ( Base ‘ 𝑀 )
	ellspds.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	ellspds.s	⊢ 𝑆 = ( Scalar ‘ 𝑀 )
	ellspds.z	⊢ 0 = ( 0g ‘ 𝑆 )
	ellspds.t	⊢ · = ( ·𝑠 ‘ 𝑀 )
	ellspds.m	⊢ ( 𝜑 → 𝑀 ∈ LMod )
	ellspds.1	⊢ ( 𝜑 → 𝑉 ⊆ 𝐵 )
Assertion	ellspds	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ 𝑉 ) ↔ ∃ 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ( 𝑎 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ellspds.n	⊢ 𝑁 = ( LSpan ‘ 𝑀 )
2		ellspds.v	⊢ 𝐵 = ( Base ‘ 𝑀 )
3		ellspds.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
4		ellspds.s	⊢ 𝑆 = ( Scalar ‘ 𝑀 )
5		ellspds.z	⊢ 0 = ( 0g ‘ 𝑆 )
6		ellspds.t	⊢ · = ( ·𝑠 ‘ 𝑀 )
7		ellspds.m	⊢ ( 𝜑 → 𝑀 ∈ LMod )
8		ellspds.1	⊢ ( 𝜑 → 𝑉 ⊆ 𝐵 )
9		f1oi	⊢ ( I ↾ 𝑉 ) : 𝑉 –1-1-onto→ 𝑉
10		f1of	⊢ ( ( I ↾ 𝑉 ) : 𝑉 –1-1-onto→ 𝑉 → ( I ↾ 𝑉 ) : 𝑉 ⟶ 𝑉 )
11	9 10	mp1i	⊢ ( 𝜑 → ( I ↾ 𝑉 ) : 𝑉 ⟶ 𝑉 )
12	11 8	fssd	⊢ ( 𝜑 → ( I ↾ 𝑉 ) : 𝑉 ⟶ 𝐵 )
13	2	fvexi	⊢ 𝐵 ∈ V
14	13	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
15	14 8	ssexd	⊢ ( 𝜑 → 𝑉 ∈ V )
16	1 2 3 4 5 6 12 7 15	ellspd	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ ( ( I ↾ 𝑉 ) “ 𝑉 ) ) ↔ ∃ 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ( 𝑎 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑎 ∘f · ( I ↾ 𝑉 ) ) ) ) ) )
17		ssid	⊢ 𝑉 ⊆ 𝑉
18		resiima	⊢ ( 𝑉 ⊆ 𝑉 → ( ( I ↾ 𝑉 ) “ 𝑉 ) = 𝑉 )
19	17 18	mp1i	⊢ ( 𝜑 → ( ( I ↾ 𝑉 ) “ 𝑉 ) = 𝑉 )
20	19	fveq2d	⊢ ( 𝜑 → ( 𝑁 ‘ ( ( I ↾ 𝑉 ) “ 𝑉 ) ) = ( 𝑁 ‘ 𝑉 ) )
21	20	eleq2d	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ ( ( I ↾ 𝑉 ) “ 𝑉 ) ) ↔ 𝑋 ∈ ( 𝑁 ‘ 𝑉 ) ) )
22		elmapfn	⊢ ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) → 𝑎 Fn 𝑉 )
23	22	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ) → 𝑎 Fn 𝑉 )
24	9 10	mp1i	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ) → ( I ↾ 𝑉 ) : 𝑉 ⟶ 𝑉 )
25	24	ffnd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ) → ( I ↾ 𝑉 ) Fn 𝑉 )
26	15	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ) → 𝑉 ∈ V )
27		inidm	⊢ ( 𝑉 ∩ 𝑉 ) = 𝑉
28		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑎 ‘ 𝑣 ) = ( 𝑎 ‘ 𝑣 ) )
29		fvresi	⊢ ( 𝑣 ∈ 𝑉 → ( ( I ↾ 𝑉 ) ‘ 𝑣 ) = 𝑣 )
30	29	adantl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( I ↾ 𝑉 ) ‘ 𝑣 ) = 𝑣 )
31	23 25 26 26 27 28 30	offval	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ) → ( 𝑎 ∘f · ( I ↾ 𝑉 ) ) = ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) )
32	31	oveq2d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ) → ( 𝑀 Σg ( 𝑎 ∘f · ( I ↾ 𝑉 ) ) ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) )
33	32	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ) → ( 𝑋 = ( 𝑀 Σg ( 𝑎 ∘f · ( I ↾ 𝑉 ) ) ) ↔ 𝑋 = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) ) )
34	33	anbi2d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ) → ( ( 𝑎 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑎 ∘f · ( I ↾ 𝑉 ) ) ) ) ↔ ( 𝑎 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) ) ) )
35	34	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ( 𝑎 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑎 ∘f · ( I ↾ 𝑉 ) ) ) ) ↔ ∃ 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ( 𝑎 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) ) ) )
36	16 21 35	3bitr3d	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ 𝑉 ) ↔ ∃ 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ( 𝑎 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) ) ) )