Metamath Proof Explorer


Theorem gsumpropd

Description: The group sum depends only on the base set and additive operation. Note that for entirely unrestricted functions, there can be dependency on out-of-domain values of the operation, so this is somewhat weaker than mndpropd etc. (Contributed by Stefan O'Rear, 1-Feb-2015) (Proof shortened by Mario Carneiro, 18-Sep-2015)

Ref Expression
Hypotheses gsumpropd.f ( 𝜑𝐹𝑉 )
gsumpropd.g ( 𝜑𝐺𝑊 )
gsumpropd.h ( 𝜑𝐻𝑋 )
gsumpropd.b ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐻 ) )
gsumpropd.p ( 𝜑 → ( +g𝐺 ) = ( +g𝐻 ) )
Assertion gsumpropd ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐻 Σg 𝐹 ) )

Proof

Step Hyp Ref Expression
1 gsumpropd.f ( 𝜑𝐹𝑉 )
2 gsumpropd.g ( 𝜑𝐺𝑊 )
3 gsumpropd.h ( 𝜑𝐻𝑋 )
4 gsumpropd.b ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐻 ) )
5 gsumpropd.p ( 𝜑 → ( +g𝐺 ) = ( +g𝐻 ) )
6 5 oveqd ( 𝜑 → ( 𝑠 ( +g𝐺 ) 𝑡 ) = ( 𝑠 ( +g𝐻 ) 𝑡 ) )
7 6 eqeq1d ( 𝜑 → ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ↔ ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ) )
8 5 oveqd ( 𝜑 → ( 𝑡 ( +g𝐺 ) 𝑠 ) = ( 𝑡 ( +g𝐻 ) 𝑠 ) )
9 8 eqeq1d ( 𝜑 → ( ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ↔ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) )
10 7 9 anbi12d ( 𝜑 → ( ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) ↔ ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) ) )
11 4 10 raleqbidv ( 𝜑 → ( ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) ↔ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) ) )
12 4 11 rabeqbidv ( 𝜑 → { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } = { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } )
13 12 sseq2d ( 𝜑 → ( ran 𝐹 ⊆ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ↔ ran 𝐹 ⊆ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) )
14 eqidd ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
15 5 oveqdr ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑎 ( +g𝐺 ) 𝑏 ) = ( 𝑎 ( +g𝐻 ) 𝑏 ) )
16 14 4 15 grpidpropd ( 𝜑 → ( 0g𝐺 ) = ( 0g𝐻 ) )
17 5 seqeq2d ( 𝜑 → seq 𝑚 ( ( +g𝐺 ) , 𝐹 ) = seq 𝑚 ( ( +g𝐻 ) , 𝐹 ) )
18 17 fveq1d ( 𝜑 → ( seq 𝑚 ( ( +g𝐺 ) , 𝐹 ) ‘ 𝑛 ) = ( seq 𝑚 ( ( +g𝐻 ) , 𝐹 ) ‘ 𝑛 ) )
19 18 eqeq2d ( 𝜑 → ( 𝑥 = ( seq 𝑚 ( ( +g𝐺 ) , 𝐹 ) ‘ 𝑛 ) ↔ 𝑥 = ( seq 𝑚 ( ( +g𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) )
20 19 anbi2d ( 𝜑 → ( ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g𝐺 ) , 𝐹 ) ‘ 𝑛 ) ) ↔ ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) )
21 20 rexbidv ( 𝜑 → ( ∃ 𝑛 ∈ ( ℤ𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g𝐺 ) , 𝐹 ) ‘ 𝑛 ) ) ↔ ∃ 𝑛 ∈ ( ℤ𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) )
22 21 exbidv ( 𝜑 → ( ∃ 𝑚𝑛 ∈ ( ℤ𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g𝐺 ) , 𝐹 ) ‘ 𝑛 ) ) ↔ ∃ 𝑚𝑛 ∈ ( ℤ𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) )
23 22 iotabidv ( 𝜑 → ( ℩ 𝑥𝑚𝑛 ∈ ( ℤ𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g𝐺 ) , 𝐹 ) ‘ 𝑛 ) ) ) = ( ℩ 𝑥𝑚𝑛 ∈ ( ℤ𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) )
24 12 difeq2d ( 𝜑 → ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) = ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) )
25 24 imaeq2d ( 𝜑 → ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) = ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) )
26 25 fveq2d ( 𝜑 → ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) = ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) )
27 26 oveq2d ( 𝜑 → ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) = ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) )
28 27 f1oeq2d ( 𝜑 → ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ↔ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) )
29 25 f1oeq3d ( 𝜑 → ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ↔ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) )
30 28 29 bitrd ( 𝜑 → ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ↔ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) )
31 5 seqeq2d ( 𝜑 → seq 1 ( ( +g𝐺 ) , ( 𝐹𝑓 ) ) = seq 1 ( ( +g𝐻 ) , ( 𝐹𝑓 ) ) )
32 31 26 fveq12d ( 𝜑 → ( seq 1 ( ( +g𝐺 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) = ( seq 1 ( ( +g𝐻 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) )
33 32 eqeq2d ( 𝜑 → ( 𝑥 = ( seq 1 ( ( +g𝐺 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ↔ 𝑥 = ( seq 1 ( ( +g𝐻 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) )
34 30 33 anbi12d ( 𝜑 → ( ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g𝐺 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ↔ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g𝐻 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) )
35 34 exbidv ( 𝜑 → ( ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g𝐺 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g𝐻 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) )
36 35 iotabidv ( 𝜑 → ( ℩ 𝑥𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g𝐺 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) = ( ℩ 𝑥𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g𝐻 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) )
37 23 36 ifeq12d ( 𝜑 → if ( dom 𝐹 ∈ ran ... , ( ℩ 𝑥𝑚𝑛 ∈ ( ℤ𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g𝐺 ) , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g𝐺 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) ) = if ( dom 𝐹 ∈ ran ... , ( ℩ 𝑥𝑚𝑛 ∈ ( ℤ𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g𝐻 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) ) )
38 13 16 37 ifbieq12d ( 𝜑 → if ( ran 𝐹 ⊆ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } , ( 0g𝐺 ) , if ( dom 𝐹 ∈ ran ... , ( ℩ 𝑥𝑚𝑛 ∈ ( ℤ𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g𝐺 ) , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g𝐺 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) ) ) = if ( ran 𝐹 ⊆ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } , ( 0g𝐻 ) , if ( dom 𝐹 ∈ ran ... , ( ℩ 𝑥𝑚𝑛 ∈ ( ℤ𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g𝐻 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) ) ) )
39 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
40 eqid ( 0g𝐺 ) = ( 0g𝐺 )
41 eqid ( +g𝐺 ) = ( +g𝐺 )
42 eqid { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } = { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) }
43 eqidd ( 𝜑 → ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) = ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) )
44 eqidd ( 𝜑 → dom 𝐹 = dom 𝐹 )
45 39 40 41 42 43 2 1 44 gsumvalx ( 𝜑 → ( 𝐺 Σg 𝐹 ) = if ( ran 𝐹 ⊆ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } , ( 0g𝐺 ) , if ( dom 𝐹 ∈ ran ... , ( ℩ 𝑥𝑚𝑛 ∈ ( ℤ𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g𝐺 ) , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g𝐺 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) ) ) )
46 eqid ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
47 eqid ( 0g𝐻 ) = ( 0g𝐻 )
48 eqid ( +g𝐻 ) = ( +g𝐻 )
49 eqid { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } = { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) }
50 eqidd ( 𝜑 → ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) = ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) )
51 46 47 48 49 50 3 1 44 gsumvalx ( 𝜑 → ( 𝐻 Σg 𝐹 ) = if ( ran 𝐹 ⊆ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } , ( 0g𝐻 ) , if ( dom 𝐹 ∈ ran ... , ( ℩ 𝑥𝑚𝑛 ∈ ( ℤ𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g𝐻 ) , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) ) ) )
52 38 45 51 3eqtr4d ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐻 Σg 𝐹 ) )