Theorem gsumpropd 18661

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 18742 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 7427	. . . . . . . 8 ⊢ (𝜑 → (𝑠(+g‘𝐺)𝑡) = (𝑠(+g‘𝐻)𝑡))
4	3	eqeq1d 2738	. . . . . . 7 ⊢ (𝜑 → ((𝑠(+g‘𝐺)𝑡) = 𝑡 ↔ (𝑠(+g‘𝐻)𝑡) = 𝑡))
5	2	oveqd 7427	. . . . . . . 8 ⊢ (𝜑 → (𝑡(+g‘𝐺)𝑠) = (𝑡(+g‘𝐻)𝑠))
6	5	eqeq1d 2738	. . . . . . 7 ⊢ (𝜑 → ((𝑡(+g‘𝐺)𝑠) = 𝑡 ↔ (𝑡(+g‘𝐻)𝑠) = 𝑡))
7	4, 6	anbi12d 632	. . . . . 6 ⊢ (𝜑 → (((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡) ↔ ((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)))
8	1, 7	raleqbidv 3329	. . . . 5 ⊢ (𝜑 → (∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡) ↔ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)))
9	1, 8	rabeqbidv 3439	. . . 4 ⊢ (𝜑 → {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)} = {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)})
10	9	sseq2d 3996	. . 3 ⊢ (𝜑 → (ran 𝐹 ⊆ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)} ↔ ran 𝐹 ⊆ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)}))
11		eqidd 2737	. . . 4 ⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐺))
12	2	oveqdr 7438	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺))) → (𝑎(+g‘𝐺)𝑏) = (𝑎(+g‘𝐻)𝑏))
13	11, 1, 12	grpidpropd 18645	. . 3 ⊢ (𝜑 → (0g‘𝐺) = (0g‘𝐻))
14	2	seqeq2d 14031	. . . . . . . . . 10 ⊢ (𝜑 → seq𝑚((+g‘𝐺), 𝐹) = seq𝑚((+g‘𝐻), 𝐹))
15	14	fveq1d 6883	. . . . . . . . 9 ⊢ (𝜑 → (seq𝑚((+g‘𝐺), 𝐹)‘𝑛) = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛))
16	15	eqeq2d 2747	. . . . . . . 8 ⊢ (𝜑 → (𝑥 = (seq𝑚((+g‘𝐺), 𝐹)‘𝑛) ↔ 𝑥 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛)))
17	16	anbi2d 630	. . . . . . 7 ⊢ (𝜑 → ((dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝐺), 𝐹)‘𝑛)) ↔ (dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛))))
18	17	rexbidv 3165	. . . . . 6 ⊢ (𝜑 → (∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝐺), 𝐹)‘𝑛)) ↔ ∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛))))
19	18	exbidv 1921	. . . . 5 ⊢ (𝜑 → (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝐺), 𝐹)‘𝑛)) ↔ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛))))
20	19	iotabidv 6520	. . . 4 ⊢ (𝜑 → (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝐺), 𝐹)‘𝑛))) = (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛))))
21	9	difeq2d 4106	. . . . . . . . . . . 12 ⊢ (𝜑 → (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)}) = (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)}))
22	21	imaeq2d 6052	. . . . . . . . . . 11 ⊢ (𝜑 → (◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)})) = (◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)})))
23	22	fveq2d 6885	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)}))) = (♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)}))))
24	23	oveq2d 7426	. . . . . . . . 9 ⊢ (𝜑 → (1...(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)})))) = (1...(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)})))))
25	24	f1oeq2d 6819	. . . . . . . 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	22	f1oeq3d 6820	. . . . . . . 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‘𝐻)𝑠) = 𝑡)}))))
27	25, 26	bitrd 279	. . . . . . 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‘𝐻)𝑠) = 𝑡)}))))
28	2	seqeq2d 14031	. . . . . . . . 9 ⊢ (𝜑 → seq1((+g‘𝐺), (𝐹 ∘ 𝑓)) = seq1((+g‘𝐻), (𝐹 ∘ 𝑓)))
29	28, 23	fveq12d 6888	. . . . . . . 8 ⊢ (𝜑 → (seq1((+g‘𝐺), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)})))) = (seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)})))))
30	29	eqeq2d 2747	. . . . . . 7 ⊢ (𝜑 → (𝑥 = (seq1((+g‘𝐺), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)})))) ↔ 𝑥 = (seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)}))))))
31	27, 30	anbi12d 632	. . . . . 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‘𝐻)𝑠) = 𝑡)})))))))
32	31	exbidv 1921	. . . . 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‘𝐻)𝑠) = 𝑡)})))))))
33	32	iotabidv 6520	. . . 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‘𝐻)𝑠) = 𝑡)})))))))
34	20, 33	ifeq12d 4527	. . 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‘𝐻)𝑠) = 𝑡)}))))))))
35	10, 13, 34	ifbieq12d 4534	. 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‘𝐻)𝑠) = 𝑡)})))))))))
36		eqid 2736	. . 3 ⊢ (Base‘𝐺) = (Base‘𝐺)
37		eqid 2736	. . 3 ⊢ (0g‘𝐺) = (0g‘𝐺)
38		eqid 2736	. . 3 ⊢ (+g‘𝐺) = (+g‘𝐺)
39		eqid 2736	. . 3 ⊢ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)} = {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)}
40		eqidd 2737	. . 3 ⊢ (𝜑 → (◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)})) = (◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)})))
41		gsumpropd.g	. . 3 ⊢ (𝜑 → 𝐺 ∈ 𝑊)
42		gsumpropd.f	. . 3 ⊢ (𝜑 → 𝐹 ∈ 𝑉)
43		eqidd 2737	. . 3 ⊢ (𝜑 → dom 𝐹 = dom 𝐹)
44	36, 37, 38, 39, 40, 41, 42, 43	gsumvalx 18659	. 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‘𝐺)𝑠) = 𝑡)})))))))))
45		eqid 2736	. . 3 ⊢ (Base‘𝐻) = (Base‘𝐻)
46		eqid 2736	. . 3 ⊢ (0g‘𝐻) = (0g‘𝐻)
47		eqid 2736	. . 3 ⊢ (+g‘𝐻) = (+g‘𝐻)
48		eqid 2736	. . 3 ⊢ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)} = {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)}
49		eqidd 2737	. . 3 ⊢ (𝜑 → (◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)})) = (◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)})))
50		gsumpropd.h	. . 3 ⊢ (𝜑 → 𝐻 ∈ 𝑋)
51	45, 46, 47, 48, 49, 50, 42, 43	gsumvalx 18659	. 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‘𝐻)𝑠) = 𝑡)})))))))))
52	35, 44, 51	3eqtr4d 2781	1 ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∀wral 3052  ∃wrex 3061  {crab 3420  Vcvv 3464   ∖ cdif 3928   ⊆ wss 3931  ifcif 4505  ^◡ccnv 5658  dom cdm 5659  ran crn 5660   “ cima 5662   ∘ ccom 5663  ℩cio 6487  –1-1-onto→wf1o 6535  ‘cfv 6536  (class class class)co 7410  1c1 11135  ℤ_≥cuz 12857  ...cfz 13529  seqcseq 14024  ♯chash 14353  Basecbs 17233  +_gcplusg 17276  0_gc0g 17458   Σ_g cgsu 17459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-seq 14025  df-0g 17460  df-gsum 17461

This theorem is referenced by:  frlmgsum  21737  psropprmul  22178  ply1coe  22241  matgsum  22380  tsmspropd  24075  gsumsra  33046  elrsp  33392  mnringmulrd  44214