Metamath Proof Explorer

Theorem gsumlsscl

Description: Closure of a group sum in a linear subspace: A (finitely supported) sum of scalar multiplications of vectors of a subset of a linear subspace is also contained in the linear subspace. (Contributed by AV, 20-Apr-2019) (Revised by AV, 28-Jul-2019)

Ref Expression
Hypotheses gsumlsscl.s 
|- S = ( LSubSp ` M )
gsumlsscl.r 
|- R = ( Scalar ` M )
gsumlsscl.b 
|- B = ( Base ` R )
Assertion gsumlsscl 
|- ( ( M e. LMod /\ Z e. S /\ V C_ Z ) -> ( ( F e. ( B ^m V ) /\ F finSupp ( 0g ` R ) ) -> ( M gsum ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) ) e. Z ) )

Proof

Step Hyp Ref Expression
1 gsumlsscl.s 
 |-  S = ( LSubSp ` M )
2 gsumlsscl.r 
 |-  R = ( Scalar ` M )
3 gsumlsscl.b 
 |-  B = ( Base ` R )
4 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
5 lmodabl 
 |-  ( M e. LMod -> M e. Abel )
6 5 3ad2ant1 
 |-  ( ( M e. LMod /\ Z e. S /\ V C_ Z ) -> M e. Abel )
7 6 adantr 
 |-  ( ( ( M e. LMod /\ Z e. S /\ V C_ Z ) /\ ( F e. ( B ^m V ) /\ F finSupp ( 0g ` R ) ) ) -> M e. Abel )
8 ssexg 
 |-  ( ( V C_ Z /\ Z e. S ) -> V e. _V )
9 8 ancoms 
 |-  ( ( Z e. S /\ V C_ Z ) -> V e. _V )
10 9 3adant1 
 |-  ( ( M e. LMod /\ Z e. S /\ V C_ Z ) -> V e. _V )
11 10 adantr 
 |-  ( ( ( M e. LMod /\ Z e. S /\ V C_ Z ) /\ ( F e. ( B ^m V ) /\ F finSupp ( 0g ` R ) ) ) -> V e. _V )
12 3simpa 
 |-  ( ( M e. LMod /\ Z e. S /\ V C_ Z ) -> ( M e. LMod /\ Z e. S ) )
13 1 lsssubg 
 |-  ( ( M e. LMod /\ Z e. S ) -> Z e. ( SubGrp ` M ) )
14 12 13 syl 
 |-  ( ( M e. LMod /\ Z e. S /\ V C_ Z ) -> Z e. ( SubGrp ` M ) )
15 14 adantr 
 |-  ( ( ( M e. LMod /\ Z e. S /\ V C_ Z ) /\ ( F e. ( B ^m V ) /\ F finSupp ( 0g ` R ) ) ) -> Z e. ( SubGrp ` M ) )
16 12 adantr 
 |-  ( ( ( M e. LMod /\ Z e. S /\ V C_ Z ) /\ ( F e. ( B ^m V ) /\ F finSupp ( 0g ` R ) ) ) -> ( M e. LMod /\ Z e. S ) )
17 16 adantr 
 |-  ( ( ( ( M e. LMod /\ Z e. S /\ V C_ Z ) /\ ( F e. ( B ^m V ) /\ F finSupp ( 0g ` R ) ) ) /\ v e. V ) -> ( M e. LMod /\ Z e. S ) )
18 elmapi 
 |-  ( F e. ( B ^m V ) -> F : V --> B )
19 ffvelrn 
 |-  ( ( F : V --> B /\ v e. V ) -> ( F ` v ) e. B )
20 19 ex 
 |-  ( F : V --> B -> ( v e. V -> ( F ` v ) e. B ) )
21 18 20 syl 
 |-  ( F e. ( B ^m V ) -> ( v e. V -> ( F ` v ) e. B ) )
22 21 ad2antrl 
 |-  ( ( ( M e. LMod /\ Z e. S /\ V C_ Z ) /\ ( F e. ( B ^m V ) /\ F finSupp ( 0g ` R ) ) ) -> ( v e. V -> ( F ` v ) e. B ) )
23 22 imp 
 |-  ( ( ( ( M e. LMod /\ Z e. S /\ V C_ Z ) /\ ( F e. ( B ^m V ) /\ F finSupp ( 0g ` R ) ) ) /\ v e. V ) -> ( F ` v ) e. B )
24 ssel 
 |-  ( V C_ Z -> ( v e. V -> v e. Z ) )
25 24 3ad2ant3 
 |-  ( ( M e. LMod /\ Z e. S /\ V C_ Z ) -> ( v e. V -> v e. Z ) )
26 25 adantr 
 |-  ( ( ( M e. LMod /\ Z e. S /\ V C_ Z ) /\ ( F e. ( B ^m V ) /\ F finSupp ( 0g ` R ) ) ) -> ( v e. V -> v e. Z ) )
27 26 imp 
 |-  ( ( ( ( M e. LMod /\ Z e. S /\ V C_ Z ) /\ ( F e. ( B ^m V ) /\ F finSupp ( 0g ` R ) ) ) /\ v e. V ) -> v e. Z )
28 eqid 
 |-  ( .s ` M ) = ( .s ` M )
29 2 28 3 1 lssvscl 
 |-  ( ( ( M e. LMod /\ Z e. S ) /\ ( ( F ` v ) e. B /\ v e. Z ) ) -> ( ( F ` v ) ( .s ` M ) v ) e. Z )
30 17 23 27 29 syl12anc 
 |-  ( ( ( ( M e. LMod /\ Z e. S /\ V C_ Z ) /\ ( F e. ( B ^m V ) /\ F finSupp ( 0g ` R ) ) ) /\ v e. V ) -> ( ( F ` v ) ( .s ` M ) v ) e. Z )
31 30 fmpttd 
 |-  ( ( ( M e. LMod /\ Z e. S /\ V C_ Z ) /\ ( F e. ( B ^m V ) /\ F finSupp ( 0g ` R ) ) ) -> ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) : V --> Z )
32 simp1 
 |-  ( ( M e. LMod /\ Z e. S /\ V C_ Z ) -> M e. LMod )
33 eqid 
 |-  ( Base ` M ) = ( Base ` M )
34 33 1 lssss 
 |-  ( Z e. S -> Z C_ ( Base ` M ) )
35 sstr 
 |-  ( ( V C_ Z /\ Z C_ ( Base ` M ) ) -> V C_ ( Base ` M ) )
36 35 expcom 
 |-  ( Z C_ ( Base ` M ) -> ( V C_ Z -> V C_ ( Base ` M ) ) )
37 34 36 syl 
 |-  ( Z e. S -> ( V C_ Z -> V C_ ( Base ` M ) ) )
38 37 a1i 
 |-  ( M e. LMod -> ( Z e. S -> ( V C_ Z -> V C_ ( Base ` M ) ) ) )
39 38 3imp 
 |-  ( ( M e. LMod /\ Z e. S /\ V C_ Z ) -> V C_ ( Base ` M ) )
40 elpwg 
 |-  ( V e. _V -> ( V e. ~P ( Base ` M ) <-> V C_ ( Base ` M ) ) )
41 10 40 syl 
 |-  ( ( M e. LMod /\ Z e. S /\ V C_ Z ) -> ( V e. ~P ( Base ` M ) <-> V C_ ( Base ` M ) ) )
42 39 41 mpbird 
 |-  ( ( M e. LMod /\ Z e. S /\ V C_ Z ) -> V e. ~P ( Base ` M ) )
43 32 42 jca 
 |-  ( ( M e. LMod /\ Z e. S /\ V C_ Z ) -> ( M e. LMod /\ V e. ~P ( Base ` M ) ) )
44 43 adantr 
 |-  ( ( ( M e. LMod /\ Z e. S /\ V C_ Z ) /\ ( F e. ( B ^m V ) /\ F finSupp ( 0g ` R ) ) ) -> ( M e. LMod /\ V e. ~P ( Base ` M ) ) )
45 simprl 
 |-  ( ( ( M e. LMod /\ Z e. S /\ V C_ Z ) /\ ( F e. ( B ^m V ) /\ F finSupp ( 0g ` R ) ) ) -> F e. ( B ^m V ) )
46 simprr 
 |-  ( ( ( M e. LMod /\ Z e. S /\ V C_ Z ) /\ ( F e. ( B ^m V ) /\ F finSupp ( 0g ` R ) ) ) -> F finSupp ( 0g ` R ) )
47 2 3 scmfsupp 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ F e. ( B ^m V ) /\ F finSupp ( 0g ` R ) ) -> ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) finSupp ( 0g ` M ) )
48 44 45 46 47 syl3anc 
 |-  ( ( ( M e. LMod /\ Z e. S /\ V C_ Z ) /\ ( F e. ( B ^m V ) /\ F finSupp ( 0g ` R ) ) ) -> ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) finSupp ( 0g ` M ) )
49 4 7 11 15 31 48 gsumsubgcl 
 |-  ( ( ( M e. LMod /\ Z e. S /\ V C_ Z ) /\ ( F e. ( B ^m V ) /\ F finSupp ( 0g ` R ) ) ) -> ( M gsum ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) ) e. Z )
50 49 ex 
 |-  ( ( M e. LMod /\ Z e. S /\ V C_ Z ) -> ( ( F e. ( B ^m V ) /\ F finSupp ( 0g ` R ) ) -> ( M gsum ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) ) e. Z ) )