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 𝐹 ) )