Metamath Proof Explorer

Theorem dprdf11

Description: Two group sums over a direct product that give the same value are equal as functions. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 14-Jul-2019)

Ref Expression
Hypotheses eldprdi.0 
|- .0. = ( 0g ` G )
eldprdi.w 
|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
eldprdi.1 
|- ( ph -> G dom DProd S )
eldprdi.2 
|- ( ph -> dom S = I )
eldprdi.3 
|- ( ph -> F e. W )
dprdf11.4 
|- ( ph -> H e. W )
Assertion dprdf11 
|- ( ph -> ( ( G gsum F ) = ( G gsum H ) <-> F = H ) )

Proof

Step Hyp Ref Expression
1 eldprdi.0 
 |-  .0. = ( 0g ` G )
2 eldprdi.w 
 |-  W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
3 eldprdi.1 
 |-  ( ph -> G dom DProd S )
4 eldprdi.2 
 |-  ( ph -> dom S = I )
5 eldprdi.3 
 |-  ( ph -> F e. W )
6 dprdf11.4 
 |-  ( ph -> H e. W )
7 eqid 
 |-  ( Base ` G ) = ( Base ` G )
8 2 3 4 5 7 dprdff 
 |-  ( ph -> F : I --> ( Base ` G ) )
9 8 ffnd 
 |-  ( ph -> F Fn I )
10 2 3 4 6 7 dprdff 
 |-  ( ph -> H : I --> ( Base ` G ) )
11 10 ffnd 
 |-  ( ph -> H Fn I )
12 eqfnfv 
 |-  ( ( F Fn I /\ H Fn I ) -> ( F = H <-> A. x e. I ( F ` x ) = ( H ` x ) ) )
13 9 11 12 syl2anc 
 |-  ( ph -> ( F = H <-> A. x e. I ( F ` x ) = ( H ` x ) ) )
14 eqid 
 |-  ( -g ` G ) = ( -g ` G )
15 1 2 3 4 5 6 14 dprdfsub 
 |-  ( ph -> ( ( F oF ( -g ` G ) H ) e. W /\ ( G gsum ( F oF ( -g ` G ) H ) ) = ( ( G gsum F ) ( -g ` G ) ( G gsum H ) ) ) )
16 15 simpld 
 |-  ( ph -> ( F oF ( -g ` G ) H ) e. W )
17 1 2 3 4 16 dprdfeq0 
 |-  ( ph -> ( ( G gsum ( F oF ( -g ` G ) H ) ) = .0. <-> ( F oF ( -g ` G ) H ) = ( x e. I |-> .0. ) ) )
18 15 simprd 
 |-  ( ph -> ( G gsum ( F oF ( -g ` G ) H ) ) = ( ( G gsum F ) ( -g ` G ) ( G gsum H ) ) )
19 18 eqeq1d 
 |-  ( ph -> ( ( G gsum ( F oF ( -g ` G ) H ) ) = .0. <-> ( ( G gsum F ) ( -g ` G ) ( G gsum H ) ) = .0. ) )
20 3 4 dprddomcld 
 |-  ( ph -> I e. _V )
21 fvexd 
 |-  ( ( ph /\ x e. I ) -> ( F ` x ) e. _V )
22 fvexd 
 |-  ( ( ph /\ x e. I ) -> ( H ` x ) e. _V )
23 8 feqmptd 
 |-  ( ph -> F = ( x e. I |-> ( F ` x ) ) )
24 10 feqmptd 
 |-  ( ph -> H = ( x e. I |-> ( H ` x ) ) )
25 20 21 22 23 24 offval2 
 |-  ( ph -> ( F oF ( -g ` G ) H ) = ( x e. I |-> ( ( F ` x ) ( -g ` G ) ( H ` x ) ) ) )
26 25 eqeq1d 
 |-  ( ph -> ( ( F oF ( -g ` G ) H ) = ( x e. I |-> .0. ) <-> ( x e. I |-> ( ( F ` x ) ( -g ` G ) ( H ` x ) ) ) = ( x e. I |-> .0. ) ) )
27 ovex 
 |-  ( ( F ` x ) ( -g ` G ) ( H ` x ) ) e. _V
28 27 rgenw 
 |-  A. x e. I ( ( F ` x ) ( -g ` G ) ( H ` x ) ) e. _V
29 mpteqb 
 |-  ( A. x e. I ( ( F ` x ) ( -g ` G ) ( H ` x ) ) e. _V -> ( ( x e. I |-> ( ( F ` x ) ( -g ` G ) ( H ` x ) ) ) = ( x e. I |-> .0. ) <-> A. x e. I ( ( F ` x ) ( -g ` G ) ( H ` x ) ) = .0. ) )
30 28 29 ax-mp 
 |-  ( ( x e. I |-> ( ( F ` x ) ( -g ` G ) ( H ` x ) ) ) = ( x e. I |-> .0. ) <-> A. x e. I ( ( F ` x ) ( -g ` G ) ( H ` x ) ) = .0. )
31 dprdgrp 
 |-  ( G dom DProd S -> G e. Grp )
32 3 31 syl 
 |-  ( ph -> G e. Grp )
33 32 adantr 
 |-  ( ( ph /\ x e. I ) -> G e. Grp )
34 8 ffvelcdmda 
 |-  ( ( ph /\ x e. I ) -> ( F ` x ) e. ( Base ` G ) )
35 10 ffvelcdmda 
 |-  ( ( ph /\ x e. I ) -> ( H ` x ) e. ( Base ` G ) )
36 7 1 14 grpsubeq0 
 |-  ( ( G e. Grp /\ ( F ` x ) e. ( Base ` G ) /\ ( H ` x ) e. ( Base ` G ) ) -> ( ( ( F ` x ) ( -g ` G ) ( H ` x ) ) = .0. <-> ( F ` x ) = ( H ` x ) ) )
37 33 34 35 36 syl3anc 
 |-  ( ( ph /\ x e. I ) -> ( ( ( F ` x ) ( -g ` G ) ( H ` x ) ) = .0. <-> ( F ` x ) = ( H ` x ) ) )
38 37 ralbidva 
 |-  ( ph -> ( A. x e. I ( ( F ` x ) ( -g ` G ) ( H ` x ) ) = .0. <-> A. x e. I ( F ` x ) = ( H ` x ) ) )
39 30 38 bitrid 
 |-  ( ph -> ( ( x e. I |-> ( ( F ` x ) ( -g ` G ) ( H ` x ) ) ) = ( x e. I |-> .0. ) <-> A. x e. I ( F ` x ) = ( H ` x ) ) )
40 26 39 bitrd 
 |-  ( ph -> ( ( F oF ( -g ` G ) H ) = ( x e. I |-> .0. ) <-> A. x e. I ( F ` x ) = ( H ` x ) ) )
41 17 19 40 3bitr3d 
 |-  ( ph -> ( ( ( G gsum F ) ( -g ` G ) ( G gsum H ) ) = .0. <-> A. x e. I ( F ` x ) = ( H ` x ) ) )
42 7 dprdssv 
 |-  ( G DProd S ) C_ ( Base ` G )
43 1 2 3 4 5 eldprdi 
 |-  ( ph -> ( G gsum F ) e. ( G DProd S ) )
44 42 43 sselid 
 |-  ( ph -> ( G gsum F ) e. ( Base ` G ) )
45 1 2 3 4 6 eldprdi 
 |-  ( ph -> ( G gsum H ) e. ( G DProd S ) )
46 42 45 sselid 
 |-  ( ph -> ( G gsum H ) e. ( Base ` G ) )
47 7 1 14 grpsubeq0 
 |-  ( ( G e. Grp /\ ( G gsum F ) e. ( Base ` G ) /\ ( G gsum H ) e. ( Base ` G ) ) -> ( ( ( G gsum F ) ( -g ` G ) ( G gsum H ) ) = .0. <-> ( G gsum F ) = ( G gsum H ) ) )
48 32 44 46 47 syl3anc 
 |-  ( ph -> ( ( ( G gsum F ) ( -g ` G ) ( G gsum H ) ) = .0. <-> ( G gsum F ) = ( G gsum H ) ) )
49 13 41 48 3bitr2rd 
 |-  ( ph -> ( ( G gsum F ) = ( G gsum H ) <-> F = H ) )