Metamath Proof Explorer

Theorem elrsp

Description: Write the elements of a ring span as finite linear combinations. (Contributed by Thierry Arnoux, 1-Jun-2024)

Ref Expression
Hypotheses elrsp.n 
|- N = ( RSpan ` R )
elrsp.b 
|- B = ( Base ` R )
elrsp.1 
|- .0. = ( 0g ` R )
elrsp.x 
|- .x. = ( .r ` R )
elrsp.r 
|- ( ph -> R e. Ring )
elrsp.i 
|- ( ph -> I C_ B )
Assertion elrsp 
|- ( ph -> ( X e. ( N ` I ) <-> E. a e. ( B ^m I ) ( a finSupp .0. /\ X = ( R gsum ( i e. I |-> ( ( a ` i ) .x. i ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elrsp.n 
 |-  N = ( RSpan ` R )
2 elrsp.b 
 |-  B = ( Base ` R )
3 elrsp.1 
 |-  .0. = ( 0g ` R )
4 elrsp.x 
 |-  .x. = ( .r ` R )
5 elrsp.r 
 |-  ( ph -> R e. Ring )
6 elrsp.i 
 |-  ( ph -> I C_ B )
7 rspval 
 |-  ( RSpan ` R ) = ( LSpan ` ( ringLMod ` R ) )
8 1 7 eqtri 
 |-  N = ( LSpan ` ( ringLMod ` R ) )
9 rlmbas 
 |-  ( Base ` R ) = ( Base ` ( ringLMod ` R ) )
10 2 9 eqtri 
 |-  B = ( Base ` ( ringLMod ` R ) )
11 eqid 
 |-  ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) = ( Base ` ( Scalar ` ( ringLMod ` R ) ) )
12 eqid 
 |-  ( Scalar ` ( ringLMod ` R ) ) = ( Scalar ` ( ringLMod ` R ) )
13 eqid 
 |-  ( 0g ` ( Scalar ` ( ringLMod ` R ) ) ) = ( 0g ` ( Scalar ` ( ringLMod ` R ) ) )
14 rlmvsca 
 |-  ( .r ` R ) = ( .s ` ( ringLMod ` R ) )
15 4 14 eqtri 
 |-  .x. = ( .s ` ( ringLMod ` R ) )
16 rlmlmod 
 |-  ( R e. Ring -> ( ringLMod ` R ) e. LMod )
17 5 16 syl 
 |-  ( ph -> ( ringLMod ` R ) e. LMod )
18 8 10 11 12 13 15 17 6 ellspds 
 |-  ( ph -> ( X e. ( N ` I ) <-> E. a e. ( ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) ^m I ) ( a finSupp ( 0g ` ( Scalar ` ( ringLMod ` R ) ) ) /\ X = ( ( ringLMod ` R ) gsum ( i e. I |-> ( ( a ` i ) .x. i ) ) ) ) ) )
19 rlmsca 
 |-  ( R e. Ring -> R = ( Scalar ` ( ringLMod ` R ) ) )
20 5 19 syl 
 |-  ( ph -> R = ( Scalar ` ( ringLMod ` R ) ) )
21 20 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) )
22 2 21 eqtrid 
 |-  ( ph -> B = ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) )
23 22 oveq1d 
 |-  ( ph -> ( B ^m I ) = ( ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) ^m I ) )
24 20 fveq2d 
 |-  ( ph -> ( 0g ` R ) = ( 0g ` ( Scalar ` ( ringLMod ` R ) ) ) )
25 3 24 eqtrid 
 |-  ( ph -> .0. = ( 0g ` ( Scalar ` ( ringLMod ` R ) ) ) )
26 25 breq2d 
 |-  ( ph -> ( a finSupp .0. <-> a finSupp ( 0g ` ( Scalar ` ( ringLMod ` R ) ) ) ) )
27 2 fvexi 
 |-  B e. _V
28 27 a1i 
 |-  ( ph -> B e. _V )
29 28 6 ssexd 
 |-  ( ph -> I e. _V )
30 29 mptexd 
 |-  ( ph -> ( i e. I |-> ( ( a ` i ) .x. i ) ) e. _V )
31 9 a1i 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( ringLMod ` R ) ) )
32 rlmplusg 
 |-  ( +g ` R ) = ( +g ` ( ringLMod ` R ) )
33 32 a1i 
 |-  ( ph -> ( +g ` R ) = ( +g ` ( ringLMod ` R ) ) )
34 30 5 17 31 33 gsumpropd 
 |-  ( ph -> ( R gsum ( i e. I |-> ( ( a ` i ) .x. i ) ) ) = ( ( ringLMod ` R ) gsum ( i e. I |-> ( ( a ` i ) .x. i ) ) ) )
35 34 eqeq2d 
 |-  ( ph -> ( X = ( R gsum ( i e. I |-> ( ( a ` i ) .x. i ) ) ) <-> X = ( ( ringLMod ` R ) gsum ( i e. I |-> ( ( a ` i ) .x. i ) ) ) ) )
36 26 35 anbi12d 
 |-  ( ph -> ( ( a finSupp .0. /\ X = ( R gsum ( i e. I |-> ( ( a ` i ) .x. i ) ) ) ) <-> ( a finSupp ( 0g ` ( Scalar ` ( ringLMod ` R ) ) ) /\ X = ( ( ringLMod ` R ) gsum ( i e. I |-> ( ( a ` i ) .x. i ) ) ) ) ) )
37 23 36 rexeqbidv 
 |-  ( ph -> ( E. a e. ( B ^m I ) ( a finSupp .0. /\ X = ( R gsum ( i e. I |-> ( ( a ` i ) .x. i ) ) ) ) <-> E. a e. ( ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) ^m I ) ( a finSupp ( 0g ` ( Scalar ` ( ringLMod ` R ) ) ) /\ X = ( ( ringLMod ` R ) gsum ( i e. I |-> ( ( a ` i ) .x. i ) ) ) ) ) )
38 18 37 bitr4d 
 |-  ( ph -> ( X e. ( N ` I ) <-> E. a e. ( B ^m I ) ( a finSupp .0. /\ X = ( R gsum ( i e. I |-> ( ( a ` i ) .x. i ) ) ) ) ) )