Metamath Proof Explorer

Theorem ellspds

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

Ref Expression
Hypotheses ellspds.n 
|- N = ( LSpan ` M )
ellspds.v 
|- B = ( Base ` M )
ellspds.k 
|- K = ( Base ` S )
ellspds.s 
|- S = ( Scalar ` M )
ellspds.z 
|- .0. = ( 0g ` S )
ellspds.t 
|- .x. = ( .s ` M )
ellspds.m 
|- ( ph -> M e. LMod )
ellspds.1 
|- ( ph -> V C_ B )
Assertion ellspds 
|- ( ph -> ( X e. ( N ` V ) <-> E. a e. ( K ^m V ) ( a finSupp .0. /\ X = ( M gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ellspds.n 
 |-  N = ( LSpan ` M )
2 ellspds.v 
 |-  B = ( Base ` M )
3 ellspds.k 
 |-  K = ( Base ` S )
4 ellspds.s 
 |-  S = ( Scalar ` M )
5 ellspds.z 
 |-  .0. = ( 0g ` S )
6 ellspds.t 
 |-  .x. = ( .s ` M )
7 ellspds.m 
 |-  ( ph -> M e. LMod )
8 ellspds.1 
 |-  ( ph -> V C_ B )
9 f1oi 
 |-  ( _I |` V ) : V -1-1-onto-> V
10 f1of 
 |-  ( ( _I |` V ) : V -1-1-onto-> V -> ( _I |` V ) : V --> V )
11 9 10 mp1i 
 |-  ( ph -> ( _I |` V ) : V --> V )
12 11 8 fssd 
 |-  ( ph -> ( _I |` V ) : V --> B )
13 2 fvexi 
 |-  B e. _V
14 13 a1i 
 |-  ( ph -> B e. _V )
15 14 8 ssexd 
 |-  ( ph -> V e. _V )
16 1 2 3 4 5 6 12 7 15 ellspd 
 |-  ( ph -> ( X e. ( N ` ( ( _I |` V ) " V ) ) <-> E. a e. ( K ^m V ) ( a finSupp .0. /\ X = ( M gsum ( a oF .x. ( _I |` V ) ) ) ) ) )
17 ssid 
 |-  V C_ V
18 resiima 
 |-  ( V C_ V -> ( ( _I |` V ) " V ) = V )
19 17 18 mp1i 
 |-  ( ph -> ( ( _I |` V ) " V ) = V )
20 19 fveq2d 
 |-  ( ph -> ( N ` ( ( _I |` V ) " V ) ) = ( N ` V ) )
21 20 eleq2d 
 |-  ( ph -> ( X e. ( N ` ( ( _I |` V ) " V ) ) <-> X e. ( N ` V ) ) )
22 elmapfn 
 |-  ( a e. ( K ^m V ) -> a Fn V )
23 22 adantl 
 |-  ( ( ph /\ a e. ( K ^m V ) ) -> a Fn V )
24 9 10 mp1i 
 |-  ( ( ph /\ a e. ( K ^m V ) ) -> ( _I |` V ) : V --> V )
25 24 ffnd 
 |-  ( ( ph /\ a e. ( K ^m V ) ) -> ( _I |` V ) Fn V )
26 15 adantr 
 |-  ( ( ph /\ a e. ( K ^m V ) ) -> V e. _V )
27 inidm 
 |-  ( V i^i V ) = V
28 eqidd 
 |-  ( ( ( ph /\ a e. ( K ^m V ) ) /\ v e. V ) -> ( a ` v ) = ( a ` v ) )
29 fvresi 
 |-  ( v e. V -> ( ( _I |` V ) ` v ) = v )
30 29 adantl 
 |-  ( ( ( ph /\ a e. ( K ^m V ) ) /\ v e. V ) -> ( ( _I |` V ) ` v ) = v )
31 23 25 26 26 27 28 30 offval 
 |-  ( ( ph /\ a e. ( K ^m V ) ) -> ( a oF .x. ( _I |` V ) ) = ( v e. V |-> ( ( a ` v ) .x. v ) ) )
32 31 oveq2d 
 |-  ( ( ph /\ a e. ( K ^m V ) ) -> ( M gsum ( a oF .x. ( _I |` V ) ) ) = ( M gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) )
33 32 eqeq2d 
 |-  ( ( ph /\ a e. ( K ^m V ) ) -> ( X = ( M gsum ( a oF .x. ( _I |` V ) ) ) <-> X = ( M gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) ) )
34 33 anbi2d 
 |-  ( ( ph /\ a e. ( K ^m V ) ) -> ( ( a finSupp .0. /\ X = ( M gsum ( a oF .x. ( _I |` V ) ) ) ) <-> ( a finSupp .0. /\ X = ( M gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) ) ) )
35 34 rexbidva 
 |-  ( ph -> ( E. a e. ( K ^m V ) ( a finSupp .0. /\ X = ( M gsum ( a oF .x. ( _I |` V ) ) ) ) <-> E. a e. ( K ^m V ) ( a finSupp .0. /\ X = ( M gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) ) ) )
36 16 21 35 3bitr3d 
 |-  ( ph -> ( X e. ( N ` V ) <-> E. a e. ( K ^m V ) ( a finSupp .0. /\ X = ( M gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) ) ) )