Metamath Proof Explorer

Theorem gsum2dlem1

Description: Lemma 1 for gsum2d . (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by AV, 8-Jun-2019)

Ref Expression
Hypotheses gsum2d.b 
|- B = ( Base ` G )
gsum2d.z 
|- .0. = ( 0g ` G )
gsum2d.g 
|- ( ph -> G e. CMnd )
gsum2d.a 
|- ( ph -> A e. V )
gsum2d.r 
|- ( ph -> Rel A )
gsum2d.d 
|- ( ph -> D e. W )
gsum2d.s 
|- ( ph -> dom A C_ D )
gsum2d.f 
|- ( ph -> F : A --> B )
gsum2d.w 
|- ( ph -> F finSupp .0. )
Assertion gsum2dlem1 
|- ( ph -> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) e. B )

Proof

Step Hyp Ref Expression
1 gsum2d.b 
 |-  B = ( Base ` G )
2 gsum2d.z 
 |-  .0. = ( 0g ` G )
3 gsum2d.g 
 |-  ( ph -> G e. CMnd )
4 gsum2d.a 
 |-  ( ph -> A e. V )
5 gsum2d.r 
 |-  ( ph -> Rel A )
6 gsum2d.d 
 |-  ( ph -> D e. W )
7 gsum2d.s 
 |-  ( ph -> dom A C_ D )
8 gsum2d.f 
 |-  ( ph -> F : A --> B )
9 gsum2d.w 
 |-  ( ph -> F finSupp .0. )
10 imaexg 
 |-  ( A e. V -> ( A " { j } ) e. _V )
11 4 10 syl 
 |-  ( ph -> ( A " { j } ) e. _V )
12 vex 
 |-  j e. _V
13 vex 
 |-  k e. _V
14 12 13 elimasn 
 |-  ( k e. ( A " { j } ) <-> <. j , k >. e. A )
15 df-ov 
 |-  ( j F k ) = ( F ` <. j , k >. )
16 8 ffvelcdmda 
 |-  ( ( ph /\ <. j , k >. e. A ) -> ( F ` <. j , k >. ) e. B )
17 15 16 eqeltrid 
 |-  ( ( ph /\ <. j , k >. e. A ) -> ( j F k ) e. B )
18 14 17 sylan2b 
 |-  ( ( ph /\ k e. ( A " { j } ) ) -> ( j F k ) e. B )
19 18 fmpttd 
 |-  ( ph -> ( k e. ( A " { j } ) |-> ( j F k ) ) : ( A " { j } ) --> B )
20 9 fsuppimpd 
 |-  ( ph -> ( F supp .0. ) e. Fin )
21 rnfi 
 |-  ( ( F supp .0. ) e. Fin -> ran ( F supp .0. ) e. Fin )
22 20 21 syl 
 |-  ( ph -> ran ( F supp .0. ) e. Fin )
23 14 biimpi 
 |-  ( k e. ( A " { j } ) -> <. j , k >. e. A )
24 12 13 opelrn 
 |-  ( <. j , k >. e. ( F supp .0. ) -> k e. ran ( F supp .0. ) )
25 24 con3i 
 |-  ( -. k e. ran ( F supp .0. ) -> -. <. j , k >. e. ( F supp .0. ) )
26 23 25 anim12i 
 |-  ( ( k e. ( A " { j } ) /\ -. k e. ran ( F supp .0. ) ) -> ( <. j , k >. e. A /\ -. <. j , k >. e. ( F supp .0. ) ) )
27 eldif 
 |-  ( k e. ( ( A " { j } ) \ ran ( F supp .0. ) ) <-> ( k e. ( A " { j } ) /\ -. k e. ran ( F supp .0. ) ) )
28 eldif 
 |-  ( <. j , k >. e. ( A \ ( F supp .0. ) ) <-> ( <. j , k >. e. A /\ -. <. j , k >. e. ( F supp .0. ) ) )
29 26 27 28 3imtr4i 
 |-  ( k e. ( ( A " { j } ) \ ran ( F supp .0. ) ) -> <. j , k >. e. ( A \ ( F supp .0. ) ) )
30 ssidd 
 |-  ( ph -> ( F supp .0. ) C_ ( F supp .0. ) )
31 2 fvexi 
 |-  .0. e. _V
32 31 a1i 
 |-  ( ph -> .0. e. _V )
33 8 30 4 32 suppssr 
 |-  ( ( ph /\ <. j , k >. e. ( A \ ( F supp .0. ) ) ) -> ( F ` <. j , k >. ) = .0. )
34 15 33 eqtrid 
 |-  ( ( ph /\ <. j , k >. e. ( A \ ( F supp .0. ) ) ) -> ( j F k ) = .0. )
35 29 34 sylan2 
 |-  ( ( ph /\ k e. ( ( A " { j } ) \ ran ( F supp .0. ) ) ) -> ( j F k ) = .0. )
36 35 11 suppss2 
 |-  ( ph -> ( ( k e. ( A " { j } ) |-> ( j F k ) ) supp .0. ) C_ ran ( F supp .0. ) )
37 22 36 ssfid 
 |-  ( ph -> ( ( k e. ( A " { j } ) |-> ( j F k ) ) supp .0. ) e. Fin )
38 1 2 3 11 19 37 gsumcl2 
 |-  ( ph -> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) e. B )