This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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