Metamath Proof Explorer

Theorem gsumress

Description: The group sum in a substructure is the same as the group sum in the original structure. The only requirement on the substructure is that it contain the identity element; neither G nor H need be groups. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypotheses gsumress.b 
|- B = ( Base ` G )
gsumress.o 
|- .+ = ( +g ` G )
gsumress.h 
|- H = ( G |`s S )
gsumress.g 
|- ( ph -> G e. V )
gsumress.a 
|- ( ph -> A e. X )
gsumress.s 
|- ( ph -> S C_ B )
gsumress.f 
|- ( ph -> F : A --> S )
gsumress.z 
|- ( ph -> .0. e. S )
gsumress.c 
|- ( ( ph /\ x e. B ) -> ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) )
Assertion gsumress 
|- ( ph -> ( G gsum F ) = ( H gsum F ) )

Proof

Step Hyp Ref Expression
1 gsumress.b 
 |-  B = ( Base ` G )
2 gsumress.o 
 |-  .+ = ( +g ` G )
3 gsumress.h 
 |-  H = ( G |`s S )
4 gsumress.g 
 |-  ( ph -> G e. V )
5 gsumress.a 
 |-  ( ph -> A e. X )
6 gsumress.s 
 |-  ( ph -> S C_ B )
7 gsumress.f 
 |-  ( ph -> F : A --> S )
8 gsumress.z 
 |-  ( ph -> .0. e. S )
9 gsumress.c 
 |-  ( ( ph /\ x e. B ) -> ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) )
10 oveq1 
 |-  ( y = .0. -> ( y .+ x ) = ( .0. .+ x ) )
11 10 eqeq1d 
 |-  ( y = .0. -> ( ( y .+ x ) = x <-> ( .0. .+ x ) = x ) )
12 11 ovanraleqv 
 |-  ( y = .0. -> ( A. x e. B ( ( y .+ x ) = x /\ ( x .+ y ) = x ) <-> A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) )
13 6 8 sseldd 
 |-  ( ph -> .0. e. B )
14 9 ralrimiva 
 |-  ( ph -> A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) )
15 12 13 14 elrabd 
 |-  ( ph -> .0. e. { y e. B | A. x e. B ( ( y .+ x ) = x /\ ( x .+ y ) = x ) } )
16 15 snssd 
 |-  ( ph -> { .0. } C_ { y e. B | A. x e. B ( ( y .+ x ) = x /\ ( x .+ y ) = x ) } )
17 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
18 eqid 
 |-  { y e. B | A. x e. B ( ( y .+ x ) = x /\ ( x .+ y ) = x ) } = { y e. B | A. x e. B ( ( y .+ x ) = x /\ ( x .+ y ) = x ) }
19 1 17 2 18 mgmidsssn0 
 |-  ( G e. V -> { y e. B | A. x e. B ( ( y .+ x ) = x /\ ( x .+ y ) = x ) } C_ { ( 0g ` G ) } )
20 4 19 syl 
 |-  ( ph -> { y e. B | A. x e. B ( ( y .+ x ) = x /\ ( x .+ y ) = x ) } C_ { ( 0g ` G ) } )
21 20 15 sseldd 
 |-  ( ph -> .0. e. { ( 0g ` G ) } )
22 elsni 
 |-  ( .0. e. { ( 0g ` G ) } -> .0. = ( 0g ` G ) )
23 21 22 syl 
 |-  ( ph -> .0. = ( 0g ` G ) )
24 23 sneqd 
 |-  ( ph -> { .0. } = { ( 0g ` G ) } )
25 20 24 sseqtrrd 
 |-  ( ph -> { y e. B | A. x e. B ( ( y .+ x ) = x /\ ( x .+ y ) = x ) } C_ { .0. } )
26 16 25 eqssd 
 |-  ( ph -> { .0. } = { y e. B | A. x e. B ( ( y .+ x ) = x /\ ( x .+ y ) = x ) } )
27 11 ovanraleqv 
 |-  ( y = .0. -> ( A. x e. S ( ( y .+ x ) = x /\ ( x .+ y ) = x ) <-> A. x e. S ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) )
28 6 sselda 
 |-  ( ( ph /\ x e. S ) -> x e. B )
29 28 9 syldan 
 |-  ( ( ph /\ x e. S ) -> ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) )
30 29 ralrimiva 
 |-  ( ph -> A. x e. S ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) )
31 27 8 30 elrabd 
 |-  ( ph -> .0. e. { y e. S | A. x e. S ( ( y .+ x ) = x /\ ( x .+ y ) = x ) } )
32 3 1 ressbas2 
 |-  ( S C_ B -> S = ( Base ` H ) )
33 6 32 syl 
 |-  ( ph -> S = ( Base ` H ) )
34 fvex 
 |-  ( Base ` H ) e. _V
35 33 34 eqeltrdi 
 |-  ( ph -> S e. _V )
36 3 2 ressplusg 
 |-  ( S e. _V -> .+ = ( +g ` H ) )
37 35 36 syl 
 |-  ( ph -> .+ = ( +g ` H ) )
38 37 oveqd 
 |-  ( ph -> ( y .+ x ) = ( y ( +g ` H ) x ) )
39 38 eqeq1d 
 |-  ( ph -> ( ( y .+ x ) = x <-> ( y ( +g ` H ) x ) = x ) )
40 37 oveqd 
 |-  ( ph -> ( x .+ y ) = ( x ( +g ` H ) y ) )
41 40 eqeq1d 
 |-  ( ph -> ( ( x .+ y ) = x <-> ( x ( +g ` H ) y ) = x ) )
42 39 41 anbi12d 
 |-  ( ph -> ( ( ( y .+ x ) = x /\ ( x .+ y ) = x ) <-> ( ( y ( +g ` H ) x ) = x /\ ( x ( +g ` H ) y ) = x ) ) )
43 33 42 raleqbidv 
 |-  ( ph -> ( A. x e. S ( ( y .+ x ) = x /\ ( x .+ y ) = x ) <-> A. x e. ( Base ` H ) ( ( y ( +g ` H ) x ) = x /\ ( x ( +g ` H ) y ) = x ) ) )
44 33 43 rabeqbidv 
 |-  ( ph -> { y e. S | A. x e. S ( ( y .+ x ) = x /\ ( x .+ y ) = x ) } = { y e. ( Base ` H ) | A. x e. ( Base ` H ) ( ( y ( +g ` H ) x ) = x /\ ( x ( +g ` H ) y ) = x ) } )
45 31 44 eleqtrd 
 |-  ( ph -> .0. e. { y e. ( Base ` H ) | A. x e. ( Base ` H ) ( ( y ( +g ` H ) x ) = x /\ ( x ( +g ` H ) y ) = x ) } )
46 45 snssd 
 |-  ( ph -> { .0. } C_ { y e. ( Base ` H ) | A. x e. ( Base ` H ) ( ( y ( +g ` H ) x ) = x /\ ( x ( +g ` H ) y ) = x ) } )
47 3 ovexi 
 |-  H e. _V
48 47 a1i 
 |-  ( ph -> H e. _V )
49 eqid 
 |-  ( Base ` H ) = ( Base ` H )
50 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
51 eqid 
 |-  ( +g ` H ) = ( +g ` H )
52 eqid 
 |-  { y e. ( Base ` H ) | A. x e. ( Base ` H ) ( ( y ( +g ` H ) x ) = x /\ ( x ( +g ` H ) y ) = x ) } = { y e. ( Base ` H ) | A. x e. ( Base ` H ) ( ( y ( +g ` H ) x ) = x /\ ( x ( +g ` H ) y ) = x ) }
53 49 50 51 52 mgmidsssn0 
 |-  ( H e. _V -> { y e. ( Base ` H ) | A. x e. ( Base ` H ) ( ( y ( +g ` H ) x ) = x /\ ( x ( +g ` H ) y ) = x ) } C_ { ( 0g ` H ) } )
54 48 53 syl 
 |-  ( ph -> { y e. ( Base ` H ) | A. x e. ( Base ` H ) ( ( y ( +g ` H ) x ) = x /\ ( x ( +g ` H ) y ) = x ) } C_ { ( 0g ` H ) } )
55 54 45 sseldd 
 |-  ( ph -> .0. e. { ( 0g ` H ) } )
56 elsni 
 |-  ( .0. e. { ( 0g ` H ) } -> .0. = ( 0g ` H ) )
57 55 56 syl 
 |-  ( ph -> .0. = ( 0g ` H ) )
58 57 sneqd 
 |-  ( ph -> { .0. } = { ( 0g ` H ) } )
59 54 58 sseqtrrd 
 |-  ( ph -> { y e. ( Base ` H ) | A. x e. ( Base ` H ) ( ( y ( +g ` H ) x ) = x /\ ( x ( +g ` H ) y ) = x ) } C_ { .0. } )
60 46 59 eqssd 
 |-  ( ph -> { .0. } = { y e. ( Base ` H ) | A. x e. ( Base ` H ) ( ( y ( +g ` H ) x ) = x /\ ( x ( +g ` H ) y ) = x ) } )
61 26 60 eqtr3d 
 |-  ( ph -> { y e. B | A. x e. B ( ( y .+ x ) = x /\ ( x .+ y ) = x ) } = { y e. ( Base ` H ) | A. x e. ( Base ` H ) ( ( y ( +g ` H ) x ) = x /\ ( x ( +g ` H ) y ) = x ) } )
62 61 sseq2d 
 |-  ( ph -> ( ran F C_ { y e. B | A. x e. B ( ( y .+ x ) = x /\ ( x .+ y ) = x ) } <-> ran F C_ { y e. ( Base ` H ) | A. x e. ( Base ` H ) ( ( y ( +g ` H ) x ) = x /\ ( x ( +g ` H ) y ) = x ) } ) )
63 23 57 eqtr3d 
 |-  ( ph -> ( 0g ` G ) = ( 0g ` H ) )
64 37 seqeq2d 
 |-  ( ph -> seq m ( .+ , F ) = seq m ( ( +g ` H ) , F ) )
65 64 fveq1d 
 |-  ( ph -> ( seq m ( .+ , F ) ` n ) = ( seq m ( ( +g ` H ) , F ) ` n ) )
66 65 eqeq2d 
 |-  ( ph -> ( z = ( seq m ( .+ , F ) ` n ) <-> z = ( seq m ( ( +g ` H ) , F ) ` n ) ) )
67 66 anbi2d 
 |-  ( ph -> ( ( A = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) <-> ( A = ( m ... n ) /\ z = ( seq m ( ( +g ` H ) , F ) ` n ) ) ) )
68 67 rexbidv 
 |-  ( ph -> ( E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) <-> E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ z = ( seq m ( ( +g ` H ) , F ) ` n ) ) ) )
69 68 exbidv 
 |-  ( ph -> ( E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) <-> E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ z = ( seq m ( ( +g ` H ) , F ) ` n ) ) ) )
70 69 iotabidv 
 |-  ( ph -> ( iota z E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) ) = ( iota z E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ z = ( seq m ( ( +g ` H ) , F ) ` n ) ) ) )
71 37 seqeq2d 
 |-  ( ph -> seq 1 ( .+ , ( F o. f ) ) = seq 1 ( ( +g ` H ) , ( F o. f ) ) )
72 71 fveq1d 
 |-  ( ph -> ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) )
73 72 eqeq2d 
 |-  ( ph -> ( z = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) <-> z = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) )
74 73 anbi2d 
 |-  ( ph -> ( ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) /\ z = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) <-> ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) /\ z = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) ) )
75 74 exbidv 
 |-  ( ph -> ( E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) /\ z = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) <-> E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) /\ z = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) ) )
76 75 iotabidv 
 |-  ( ph -> ( iota z E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) /\ z = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) ) = ( iota z E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) /\ z = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) ) )
77 70 76 ifeq12d 
 |-  ( ph -> if ( A e. ran ... , ( iota z E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) ) , ( iota z E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) /\ z = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) ) ) = if ( A e. ran ... , ( iota z E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ z = ( seq m ( ( +g ` H ) , F ) ` n ) ) ) , ( iota z E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) /\ z = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) ) ) )
78 62 63 77 ifbieq12d 
 |-  ( ph -> if ( ran F C_ { y e. B | A. x e. B ( ( y .+ x ) = x /\ ( x .+ y ) = x ) } , ( 0g ` G ) , if ( A e. ran ... , ( iota z E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) ) , ( iota z E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) /\ z = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) ) ) ) = if ( ran F C_ { y e. ( Base ` H ) | A. x e. ( Base ` H ) ( ( y ( +g ` H ) x ) = x /\ ( x ( +g ` H ) y ) = x ) } , ( 0g ` H ) , if ( A e. ran ... , ( iota z E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ z = ( seq m ( ( +g ` H ) , F ) ` n ) ) ) , ( iota z E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) /\ z = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) ) ) ) )
79 26 difeq2d 
 |-  ( ph -> ( _V \ { .0. } ) = ( _V \ { y e. B | A. x e. B ( ( y .+ x ) = x /\ ( x .+ y ) = x ) } ) )
80 79 imaeq2d 
 |-  ( ph -> ( `' F " ( _V \ { .0. } ) ) = ( `' F " ( _V \ { y e. B | A. x e. B ( ( y .+ x ) = x /\ ( x .+ y ) = x ) } ) ) )
81 7 6 fssd 
 |-  ( ph -> F : A --> B )
82 1 17 2 18 80 4 5 81 gsumval 
 |-  ( ph -> ( G gsum F ) = if ( ran F C_ { y e. B | A. x e. B ( ( y .+ x ) = x /\ ( x .+ y ) = x ) } , ( 0g ` G ) , if ( A e. ran ... , ( iota z E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ z = ( seq m ( .+ , F ) ` n ) ) ) , ( iota z E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) /\ z = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) ) ) ) )
83 60 difeq2d 
 |-  ( ph -> ( _V \ { .0. } ) = ( _V \ { y e. ( Base ` H ) | A. x e. ( Base ` H ) ( ( y ( +g ` H ) x ) = x /\ ( x ( +g ` H ) y ) = x ) } ) )
84 83 imaeq2d 
 |-  ( ph -> ( `' F " ( _V \ { .0. } ) ) = ( `' F " ( _V \ { y e. ( Base ` H ) | A. x e. ( Base ` H ) ( ( y ( +g ` H ) x ) = x /\ ( x ( +g ` H ) y ) = x ) } ) ) )
85 33 feq3d 
 |-  ( ph -> ( F : A --> S <-> F : A --> ( Base ` H ) ) )
86 7 85 mpbid 
 |-  ( ph -> F : A --> ( Base ` H ) )
87 49 50 51 52 84 48 5 86 gsumval 
 |-  ( ph -> ( H gsum F ) = if ( ran F C_ { y e. ( Base ` H ) | A. x e. ( Base ` H ) ( ( y ( +g ` H ) x ) = x /\ ( x ( +g ` H ) y ) = x ) } , ( 0g ` H ) , if ( A e. ran ... , ( iota z E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ z = ( seq m ( ( +g ` H ) , F ) ` n ) ) ) , ( iota z E. f ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) /\ z = ( seq 1 ( ( +g ` H ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) ) ) ) )
88 78 82 87 3eqtr4d 
 |-  ( ph -> ( G gsum F ) = ( H gsum F ) )