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