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 𝐵 = ( Base ‘ 𝐺 )
gsumress.o + = ( +g𝐺 )
gsumress.h 𝐻 = ( 𝐺s 𝑆 )
gsumress.g ( 𝜑𝐺𝑉 )
gsumress.a ( 𝜑𝐴𝑋 )
gsumress.s ( 𝜑𝑆𝐵 )
gsumress.f ( 𝜑𝐹 : 𝐴𝑆 )
gsumress.z ( 𝜑0𝑆 )
gsumress.c ( ( 𝜑𝑥𝐵 ) → ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) )
Assertion gsumress ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐻 Σg 𝐹 ) )

Proof

Step Hyp Ref Expression
1 gsumress.b 𝐵 = ( Base ‘ 𝐺 )
2 gsumress.o + = ( +g𝐺 )
3 gsumress.h 𝐻 = ( 𝐺s 𝑆 )
4 gsumress.g ( 𝜑𝐺𝑉 )
5 gsumress.a ( 𝜑𝐴𝑋 )
6 gsumress.s ( 𝜑𝑆𝐵 )
7 gsumress.f ( 𝜑𝐹 : 𝐴𝑆 )
8 gsumress.z ( 𝜑0𝑆 )
9 gsumress.c ( ( 𝜑𝑥𝐵 ) → ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) )
10 oveq1 ( 𝑦 = 0 → ( 𝑦 + 𝑥 ) = ( 0 + 𝑥 ) )
11 10 eqeq1d ( 𝑦 = 0 → ( ( 𝑦 + 𝑥 ) = 𝑥 ↔ ( 0 + 𝑥 ) = 𝑥 ) )
12 11 ovanraleqv ( 𝑦 = 0 → ( ∀ 𝑥𝐵 ( ( 𝑦 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑦 ) = 𝑥 ) ↔ ∀ 𝑥𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) )
13 6 8 sseldd ( 𝜑0𝐵 )
14 9 ralrimiva ( 𝜑 → ∀ 𝑥𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) )
15 12 13 14 elrabd ( 𝜑0 ∈ { 𝑦𝐵 ∣ ∀ 𝑥𝐵 ( ( 𝑦 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑦 ) = 𝑥 ) } )
16 15 snssd ( 𝜑 → { 0 } ⊆ { 𝑦𝐵 ∣ ∀ 𝑥𝐵 ( ( 𝑦 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑦 ) = 𝑥 ) } )
17 eqid ( 0g𝐺 ) = ( 0g𝐺 )
18 eqid { 𝑦𝐵 ∣ ∀ 𝑥𝐵 ( ( 𝑦 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑦 ) = 𝑥 ) } = { 𝑦𝐵 ∣ ∀ 𝑥𝐵 ( ( 𝑦 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑦 ) = 𝑥 ) }
19 1 17 2 18 mgmidsssn0 ( 𝐺𝑉 → { 𝑦𝐵 ∣ ∀ 𝑥𝐵 ( ( 𝑦 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑦 ) = 𝑥 ) } ⊆ { ( 0g𝐺 ) } )
20 4 19 syl ( 𝜑 → { 𝑦𝐵 ∣ ∀ 𝑥𝐵 ( ( 𝑦 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑦 ) = 𝑥 ) } ⊆ { ( 0g𝐺 ) } )
21 20 15 sseldd ( 𝜑0 ∈ { ( 0g𝐺 ) } )
22 elsni ( 0 ∈ { ( 0g𝐺 ) } → 0 = ( 0g𝐺 ) )
23 21 22 syl ( 𝜑0 = ( 0g𝐺 ) )
24 23 sneqd ( 𝜑 → { 0 } = { ( 0g𝐺 ) } )
25 20 24 sseqtrrd ( 𝜑 → { 𝑦𝐵 ∣ ∀ 𝑥𝐵 ( ( 𝑦 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑦 ) = 𝑥 ) } ⊆ { 0 } )
26 16 25 eqssd ( 𝜑 → { 0 } = { 𝑦𝐵 ∣ ∀ 𝑥𝐵 ( ( 𝑦 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑦 ) = 𝑥 ) } )
27 11 ovanraleqv ( 𝑦 = 0 → ( ∀ 𝑥𝑆 ( ( 𝑦 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑦 ) = 𝑥 ) ↔ ∀ 𝑥𝑆 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) )
28 6 sselda ( ( 𝜑𝑥𝑆 ) → 𝑥𝐵 )
29 28 9 syldan ( ( 𝜑𝑥𝑆 ) → ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) )
30 29 ralrimiva ( 𝜑 → ∀ 𝑥𝑆 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) )
31 27 8 30 elrabd ( 𝜑0 ∈ { 𝑦𝑆 ∣ ∀ 𝑥𝑆 ( ( 𝑦 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑦 ) = 𝑥 ) } )
32 3 1 ressbas2 ( 𝑆𝐵𝑆 = ( Base ‘ 𝐻 ) )
33 6 32 syl ( 𝜑𝑆 = ( Base ‘ 𝐻 ) )
34 fvex ( Base ‘ 𝐻 ) ∈ V
35 33 34 eqeltrdi ( 𝜑𝑆 ∈ V )
36 3 2 ressplusg ( 𝑆 ∈ V → + = ( +g𝐻 ) )
37 35 36 syl ( 𝜑+ = ( +g𝐻 ) )
38 37 oveqd ( 𝜑 → ( 𝑦 + 𝑥 ) = ( 𝑦 ( +g𝐻 ) 𝑥 ) )
39 38 eqeq1d ( 𝜑 → ( ( 𝑦 + 𝑥 ) = 𝑥 ↔ ( 𝑦 ( +g𝐻 ) 𝑥 ) = 𝑥 ) )
40 37 oveqd ( 𝜑 → ( 𝑥 + 𝑦 ) = ( 𝑥 ( +g𝐻 ) 𝑦 ) )
41 40 eqeq1d ( 𝜑 → ( ( 𝑥 + 𝑦 ) = 𝑥 ↔ ( 𝑥 ( +g𝐻 ) 𝑦 ) = 𝑥 ) )
42 39 41 anbi12d ( 𝜑 → ( ( ( 𝑦 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑦 ) = 𝑥 ) ↔ ( ( 𝑦 ( +g𝐻 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝐻 ) 𝑦 ) = 𝑥 ) ) )
43 33 42 raleqbidv ( 𝜑 → ( ∀ 𝑥𝑆 ( ( 𝑦 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑦 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g𝐻 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝐻 ) 𝑦 ) = 𝑥 ) ) )
44 33 43 rabeqbidv ( 𝜑 → { 𝑦𝑆 ∣ ∀ 𝑥𝑆 ( ( 𝑦 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑦 ) = 𝑥 ) } = { 𝑦 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g𝐻 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝐻 ) 𝑦 ) = 𝑥 ) } )
45 31 44 eleqtrd ( 𝜑0 ∈ { 𝑦 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g𝐻 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝐻 ) 𝑦 ) = 𝑥 ) } )
46 45 snssd ( 𝜑 → { 0 } ⊆ { 𝑦 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g𝐻 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝐻 ) 𝑦 ) = 𝑥 ) } )
47 3 ovexi 𝐻 ∈ V
48 47 a1i ( 𝜑𝐻 ∈ V )
49 eqid ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
50 eqid ( 0g𝐻 ) = ( 0g𝐻 )
51 eqid ( +g𝐻 ) = ( +g𝐻 )
52 eqid { 𝑦 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g𝐻 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝐻 ) 𝑦 ) = 𝑥 ) } = { 𝑦 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g𝐻 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝐻 ) 𝑦 ) = 𝑥 ) }
53 49 50 51 52 mgmidsssn0 ( 𝐻 ∈ V → { 𝑦 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g𝐻 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝐻 ) 𝑦 ) = 𝑥 ) } ⊆ { ( 0g𝐻 ) } )
54 48 53 syl ( 𝜑 → { 𝑦 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g𝐻 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝐻 ) 𝑦 ) = 𝑥 ) } ⊆ { ( 0g𝐻 ) } )
55 54 45 sseldd ( 𝜑0 ∈ { ( 0g𝐻 ) } )
56 elsni ( 0 ∈ { ( 0g𝐻 ) } → 0 = ( 0g𝐻 ) )
57 55 56 syl ( 𝜑0 = ( 0g𝐻 ) )
58 57 sneqd ( 𝜑 → { 0 } = { ( 0g𝐻 ) } )
59 54 58 sseqtrrd ( 𝜑 → { 𝑦 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g𝐻 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝐻 ) 𝑦 ) = 𝑥 ) } ⊆ { 0 } )
60 46 59 eqssd ( 𝜑 → { 0 } = { 𝑦 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g𝐻 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝐻 ) 𝑦 ) = 𝑥 ) } )
61 26 60 eqtr3d ( 𝜑 → { 𝑦𝐵 ∣ ∀ 𝑥𝐵 ( ( 𝑦 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑦 ) = 𝑥 ) } = { 𝑦 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g𝐻 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝐻 ) 𝑦 ) = 𝑥 ) } )
62 61 sseq2d ( 𝜑 → ( ran 𝐹 ⊆ { 𝑦𝐵 ∣ ∀ 𝑥𝐵 ( ( 𝑦 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑦 ) = 𝑥 ) } ↔ ran 𝐹 ⊆ { 𝑦 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g𝐻 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝐻 ) 𝑦 ) = 𝑥 ) } ) )
63 23 57 eqtr3d ( 𝜑 → ( 0g𝐺 ) = ( 0g𝐻 ) )
64 37 seqeq2d ( 𝜑 → seq 𝑚 ( + , 𝐹 ) = seq 𝑚 ( ( +g𝐻 ) , 𝐹 ) )
65 64 fveq1d ( 𝜑 → ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq 𝑚 ( ( +g𝐻 ) , 𝐹 ) ‘ 𝑛 ) )
66 65 eqeq2d ( 𝜑 → ( 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ↔ 𝑧 = ( seq 𝑚 ( ( +g𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) )
67 66 anbi2d ( 𝜑 → ( ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ↔ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( ( +g𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) )
68 67 rexbidv ( 𝜑 → ( ∃ 𝑛 ∈ ( ℤ𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ↔ ∃ 𝑛 ∈ ( ℤ𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( ( +g𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) )
69 68 exbidv ( 𝜑 → ( ∃ 𝑚𝑛 ∈ ( ℤ𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ↔ ∃ 𝑚𝑛 ∈ ( ℤ𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( ( +g𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) )
70 69 iotabidv ( 𝜑 → ( ℩ 𝑧𝑚𝑛 ∈ ( ℤ𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) = ( ℩ 𝑧𝑚𝑛 ∈ ( ℤ𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( ( +g𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) )
71 37 seqeq2d ( 𝜑 → seq 1 ( + , ( 𝐹𝑓 ) ) = seq 1 ( ( +g𝐻 ) , ( 𝐹𝑓 ) ) )
72 71 fveq1d ( 𝜑 → ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) = ( seq 1 ( ( +g𝐻 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) )
73 72 eqeq2d ( 𝜑 → ( 𝑧 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) ↔ 𝑧 = ( seq 1 ( ( +g𝐻 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) ) )
74 73 anbi2d ( 𝜑 → ( ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 0 } ) ) ∧ 𝑧 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) ) ↔ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 0 } ) ) ∧ 𝑧 = ( seq 1 ( ( +g𝐻 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) ) ) )
75 74 exbidv ( 𝜑 → ( ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 0 } ) ) ∧ 𝑧 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 0 } ) ) ∧ 𝑧 = ( seq 1 ( ( +g𝐻 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) ) ) )
76 75 iotabidv ( 𝜑 → ( ℩ 𝑧𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 0 } ) ) ∧ 𝑧 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) ) ) = ( ℩ 𝑧𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 0 } ) ) ∧ 𝑧 = ( seq 1 ( ( +g𝐻 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) ) ) )
77 70 76 ifeq12d ( 𝜑 → if ( 𝐴 ∈ ran ... , ( ℩ 𝑧𝑚𝑛 ∈ ( ℤ𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑧𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 0 } ) ) ∧ 𝑧 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) ) ) ) = if ( 𝐴 ∈ ran ... , ( ℩ 𝑧𝑚𝑛 ∈ ( ℤ𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( ( +g𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑧𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 0 } ) ) ∧ 𝑧 = ( seq 1 ( ( +g𝐻 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) ) ) ) )
78 62 63 77 ifbieq12d ( 𝜑 → if ( ran 𝐹 ⊆ { 𝑦𝐵 ∣ ∀ 𝑥𝐵 ( ( 𝑦 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑦 ) = 𝑥 ) } , ( 0g𝐺 ) , if ( 𝐴 ∈ ran ... , ( ℩ 𝑧𝑚𝑛 ∈ ( ℤ𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑧𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 0 } ) ) ∧ 𝑧 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) ) ) ) ) = if ( ran 𝐹 ⊆ { 𝑦 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g𝐻 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝐻 ) 𝑦 ) = 𝑥 ) } , ( 0g𝐻 ) , if ( 𝐴 ∈ ran ... , ( ℩ 𝑧𝑚𝑛 ∈ ( ℤ𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( ( +g𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑧𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 0 } ) ) ∧ 𝑧 = ( seq 1 ( ( +g𝐻 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) ) ) ) ) )
79 26 difeq2d ( 𝜑 → ( V ∖ { 0 } ) = ( V ∖ { 𝑦𝐵 ∣ ∀ 𝑥𝐵 ( ( 𝑦 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑦 ) = 𝑥 ) } ) )
80 79 imaeq2d ( 𝜑 → ( 𝐹 “ ( V ∖ { 0 } ) ) = ( 𝐹 “ ( V ∖ { 𝑦𝐵 ∣ ∀ 𝑥𝐵 ( ( 𝑦 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑦 ) = 𝑥 ) } ) ) )
81 7 6 fssd ( 𝜑𝐹 : 𝐴𝐵 )
82 1 17 2 18 80 4 5 81 gsumval ( 𝜑 → ( 𝐺 Σg 𝐹 ) = if ( ran 𝐹 ⊆ { 𝑦𝐵 ∣ ∀ 𝑥𝐵 ( ( 𝑦 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑦 ) = 𝑥 ) } , ( 0g𝐺 ) , if ( 𝐴 ∈ ran ... , ( ℩ 𝑧𝑚𝑛 ∈ ( ℤ𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑧𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 0 } ) ) ∧ 𝑧 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) ) ) ) ) )
83 60 difeq2d ( 𝜑 → ( V ∖ { 0 } ) = ( V ∖ { 𝑦 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g𝐻 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝐻 ) 𝑦 ) = 𝑥 ) } ) )
84 83 imaeq2d ( 𝜑 → ( 𝐹 “ ( V ∖ { 0 } ) ) = ( 𝐹 “ ( V ∖ { 𝑦 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g𝐻 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝐻 ) 𝑦 ) = 𝑥 ) } ) ) )
85 33 feq3d ( 𝜑 → ( 𝐹 : 𝐴𝑆𝐹 : 𝐴 ⟶ ( Base ‘ 𝐻 ) ) )
86 7 85 mpbid ( 𝜑𝐹 : 𝐴 ⟶ ( Base ‘ 𝐻 ) )
87 49 50 51 52 84 48 5 86 gsumval ( 𝜑 → ( 𝐻 Σg 𝐹 ) = if ( ran 𝐹 ⊆ { 𝑦 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g𝐻 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝐻 ) 𝑦 ) = 𝑥 ) } , ( 0g𝐻 ) , if ( 𝐴 ∈ ran ... , ( ℩ 𝑧𝑚𝑛 ∈ ( ℤ𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( ( +g𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑧𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 0 } ) ) ∧ 𝑧 = ( seq 1 ( ( +g𝐻 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 0 } ) ) ) ) ) ) ) ) )
88 78 82 87 3eqtr4d ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐻 Σg 𝐹 ) )