Metamath Proof Explorer


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 ( 𝑣𝑉 ↦ ( ( 𝑎𝑣 ) · 𝑣 ) ) ) ) ) )