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	⊢ ( 𝜑 → ( 0_g ‘ 𝐺 ) = ( 0_g ‘ 𝐻 ) )
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 ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } , ( 0_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 ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) ) ) = if ( ran 𝐹 ⊆ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +_g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +_g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } , ( 0_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 ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) ) ) )
39		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
40		eqid	⊢ ( 0_g ‘ 𝐺 ) = ( 0_g ‘ 𝐺 )
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 ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } , ( 0_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 ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) ) ) )
46		eqid	⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
47		eqid	⊢ ( 0_g ‘ 𝐻 ) = ( 0_g ‘ 𝐻 )
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 ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } , ( 0_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 ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) ) ) )
52	38 45 51	3eqtr4d	⊢ ( 𝜑 → ( 𝐺 Σ_g 𝐹 ) = ( 𝐻 Σ_g 𝐹 ) )

Metamath Proof Explorer

Theorem gsumpropd

Proof