Theorem gsumpropd 17587

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 17631 etc. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Proof shortened by Mario Carneiro, 18-Sep-2015.)

Hypotheses

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

Assertion

Ref	Expression
gsumpropd	⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹))

Proof of Theorem gsumpropd

Dummy variables 𝑎 𝑏 𝑓 𝑚 𝑛 𝑠 𝑡 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gsumpropd.b	. . . . 5 ⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐻))
2		gsumpropd.p	. . . . . . . . 9 ⊢ (𝜑 → (+g‘𝐺) = (+g‘𝐻))
3	2	oveqd 6895	. . . . . . . 8 ⊢ (𝜑 → (𝑠(+g‘𝐺)𝑡) = (𝑠(+g‘𝐻)𝑡))
4	3	eqeq1d 2801	. . . . . . 7 ⊢ (𝜑 → ((𝑠(+g‘𝐺)𝑡) = 𝑡 ↔ (𝑠(+g‘𝐻)𝑡) = 𝑡))
5	2	oveqd 6895	. . . . . . . 8 ⊢ (𝜑 → (𝑡(+g‘𝐺)𝑠) = (𝑡(+g‘𝐻)𝑠))
6	5	eqeq1d 2801	. . . . . . 7 ⊢ (𝜑 → ((𝑡(+g‘𝐺)𝑠) = 𝑡 ↔ (𝑡(+g‘𝐻)𝑠) = 𝑡))
7	4, 6	anbi12d 625	. . . . . 6 ⊢ (𝜑 → (((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡) ↔ ((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)))
8	1, 7	raleqbidv 3335	. . . . 5 ⊢ (𝜑 → (∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡) ↔ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)))
9	1, 8	rabeqbidv 3379	. . . 4 ⊢ (𝜑 → {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)} = {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)})
10	9	sseq2d 3829	. . 3 ⊢ (𝜑 → (ran 𝐹 ⊆ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)} ↔ ran 𝐹 ⊆ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)}))
11		eqidd 2800	. . . 4 ⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐺))
12	2	oveqdr 6906	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺))) → (𝑎(+g‘𝐺)𝑏) = (𝑎(+g‘𝐻)𝑏))
13	11, 1, 12	grpidpropd 17576	. . 3 ⊢ (𝜑 → (0g‘𝐺) = (0g‘𝐻))
14	2	seqeq2d 13062	. . . . . . . . . 10 ⊢ (𝜑 → seq𝑚((+g‘𝐺), 𝐹) = seq𝑚((+g‘𝐻), 𝐹))
15	14	fveq1d 6413	. . . . . . . . 9 ⊢ (𝜑 → (seq𝑚((+g‘𝐺), 𝐹)‘𝑛) = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛))
16	15	eqeq2d 2809	. . . . . . . 8 ⊢ (𝜑 → (𝑥 = (seq𝑚((+g‘𝐺), 𝐹)‘𝑛) ↔ 𝑥 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛)))
17	16	anbi2d 623	. . . . . . 7 ⊢ (𝜑 → ((dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝐺), 𝐹)‘𝑛)) ↔ (dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛))))
18	17	rexbidv 3233	. . . . . 6 ⊢ (𝜑 → (∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝐺), 𝐹)‘𝑛)) ↔ ∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛))))
19	18	exbidv 2017	. . . . 5 ⊢ (𝜑 → (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝐺), 𝐹)‘𝑛)) ↔ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛))))
20	19	iotabidv 6085	. . . 4 ⊢ (𝜑 → (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝐺), 𝐹)‘𝑛))) = (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛))))
21	9	difeq2d 3926	. . . . . . . . . . . 12 ⊢ (𝜑 → (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)}) = (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)}))
22	21	imaeq2d 5683	. . . . . . . . . . 11 ⊢ (𝜑 → (◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)})) = (◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)})))
23	22	fveq2d 6415	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)}))) = (♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)}))))
24	23	oveq2d 6894	. . . . . . . . 9 ⊢ (𝜑 → (1...(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)})))) = (1...(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)})))))
25	24	f1oeq2d 6352	. . . . . . . 8 ⊢ (𝜑 → (𝑓:(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‘𝐺)𝑠) = 𝑡)}))))
26		f1oeq3 6347	. . . . . . . . 9 ⊢ ((◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)})) = (◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)})) → (𝑓:(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‘𝐻)𝑠) = 𝑡)}))))
27	22, 26	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑓:(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‘𝐻)𝑠) = 𝑡)}))))
28	25, 27	bitrd 271	. . . . . . 7 ⊢ (𝜑 → (𝑓:(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	2	seqeq2d 13062	. . . . . . . . 9 ⊢ (𝜑 → seq1((+g‘𝐺), (𝐹 ∘ 𝑓)) = seq1((+g‘𝐻), (𝐹 ∘ 𝑓)))
30	29, 23	fveq12d 6418	. . . . . . . 8 ⊢ (𝜑 → (seq1((+g‘𝐺), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)})))) = (seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)})))))
31	30	eqeq2d 2809	. . . . . . 7 ⊢ (𝜑 → (𝑥 = (seq1((+g‘𝐺), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)})))) ↔ 𝑥 = (seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)}))))))
32	28, 31	anbi12d 625	. . . . . 6 ⊢ (𝜑 → ((𝑓:(1...(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)}))))–1-1-onto→(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)})) ∧ 𝑥 = (seq1((+g‘𝐺), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)}))))) ↔ (𝑓:(1...(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)}))))–1-1-onto→(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)})) ∧ 𝑥 = (seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)})))))))
33	32	exbidv 2017	. . . . 5 ⊢ (𝜑 → (∃𝑓(𝑓:(1...(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)}))))–1-1-onto→(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)})) ∧ 𝑥 = (seq1((+g‘𝐺), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)}))))) ↔ ∃𝑓(𝑓:(1...(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)}))))–1-1-onto→(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)})) ∧ 𝑥 = (seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)})))))))
34	33	iotabidv 6085	. . . 4 ⊢ (𝜑 → (℩𝑥∃𝑓(𝑓:(1...(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)}))))–1-1-onto→(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)})) ∧ 𝑥 = (seq1((+g‘𝐺), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)})))))) = (℩𝑥∃𝑓(𝑓:(1...(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)}))))–1-1-onto→(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)})) ∧ 𝑥 = (seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)})))))))
35	20, 34	ifeq12d 4297	. . 3 ⊢ (𝜑 → if(dom 𝐹 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝐺), 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)}))))–1-1-onto→(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)})) ∧ 𝑥 = (seq1((+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‘𝐻)𝑠) = 𝑡)})) ∧ 𝑥 = (seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)}))))))))
36	10, 13, 35	ifbieq12d 4304	. 2 ⊢ (𝜑 → 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‘𝐺)𝑠) = 𝑡)})) ∧ 𝑥 = (seq1((+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‘𝐻)𝑠) = 𝑡)})) ∧ 𝑥 = (seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)})))))))))
37		eqid 2799	. . 3 ⊢ (Base‘𝐺) = (Base‘𝐺)
38		eqid 2799	. . 3 ⊢ (0g‘𝐺) = (0g‘𝐺)
39		eqid 2799	. . 3 ⊢ (+g‘𝐺) = (+g‘𝐺)
40		eqid 2799	. . 3 ⊢ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)} = {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)}
41		eqidd 2800	. . 3 ⊢ (𝜑 → (◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)})) = (◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)})))
42		gsumpropd.g	. . 3 ⊢ (𝜑 → 𝐺 ∈ 𝑊)
43		gsumpropd.f	. . 3 ⊢ (𝜑 → 𝐹 ∈ 𝑉)
44		eqidd 2800	. . 3 ⊢ (𝜑 → dom 𝐹 = dom 𝐹)
45	37, 38, 39, 40, 41, 42, 43, 44	gsumvalx 17585	. 2 ⊢ (𝜑 → (𝐺 Σ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‘𝐺)𝑠) = 𝑡)})) ∧ 𝑥 = (seq1((+g‘𝐺), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)})))))))))
46		eqid 2799	. . 3 ⊢ (Base‘𝐻) = (Base‘𝐻)
47		eqid 2799	. . 3 ⊢ (0g‘𝐻) = (0g‘𝐻)
48		eqid 2799	. . 3 ⊢ (+g‘𝐻) = (+g‘𝐻)
49		eqid 2799	. . 3 ⊢ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)} = {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)}
50		eqidd 2800	. . 3 ⊢ (𝜑 → (◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)})) = (◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)})))
51		gsumpropd.h	. . 3 ⊢ (𝜑 → 𝐻 ∈ 𝑋)
52	46, 47, 48, 49, 50, 51, 43, 44	gsumvalx 17585	. 2 ⊢ (𝜑 → (𝐻 Σ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‘𝐻)𝑠) = 𝑡)})) ∧ 𝑥 = (seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)})))))))))
53	36, 45, 52	3eqtr4d 2843	1 ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 385   = wceq 1653  ∃wex 1875   ∈ wcel 2157  ∀wral 3089  ∃wrex 3090  {crab 3093  Vcvv 3385   ∖ cdif 3766   ⊆ wss 3769  ifcif 4277  ^◡ccnv 5311  dom cdm 5312  ran crn 5313   “ cima 5315   ∘ ccom 5316  ℩cio 6062  –1-1-onto→wf1o 6100  ‘cfv 6101  (class class class)co 6878  1c1 10225  ℤ_≥cuz 11930  ...cfz 12580  seqcseq 13055  ♯chash 13370  Basecbs 16184  +_gcplusg 16267  0_gc0g 16415   Σ_g cgsu 16416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5097  ax-un 7183

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3387  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-pw 4351  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-br 4844  df-opab 4906  df-mpt 4923  df-id 5220  df-xp 5318  df-rel 5319  df-cnv 5320  df-co 5321  df-dm 5322  df-rn 5323  df-res 5324  df-ima 5325  df-pred 5898  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-ov 6881  df-oprab 6882  df-mpt2 6883  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-seq 13056  df-0g 16417  df-gsum 16418

This theorem is referenced by:  psropprmul  19930  ply1coe  19988  frlmgsum  20436  matgsum  20568  tsmspropd  22263