gfsumval - Mathbox for Jim Kingdon

	Mathbox for Jim Kingdon		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > Mathboxes > gfsumval		GIF version

Theorem gfsumval 16748

Description: Value of the finite group sum over an unordered finite set. (Contributed by Jim Kingdon, 24-Mar-2026.)

**Hypotheses**
Ref	Expression
gfsumval.b	⊢ 𝐵 = (Base‘𝑊)
gfsumval.w	⊢ (𝜑 → 𝑊 ∈ CMnd)
gfsumval.f	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
gfsumval.fi	⊢ (𝜑 → 𝐴 ∈ Fin)
gfsumval.g	⊢ (𝜑 → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴)

**Assertion**
Ref	Expression
gfsumval	⊢ (𝜑 → (𝑊 Σ_gf 𝐹) = (𝑊 Σ_g (𝐹 ∘ 𝐺)))

Proof of Theorem gfsumval Dummy variables 𝑝 𝑞 𝑟 𝑠 𝑓 𝑔 𝑤 𝑥 ℎ 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gfsumval.w	. . 3 ⊢ (𝜑 → 𝑊 ∈ CMnd)
2		gfsumval.f	. . . 4 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
3		gfsumval.fi	. . . 4 ⊢ (𝜑 → 𝐴 ∈ Fin)
4	2, 3	fexd 5889	. . 3 ⊢ (𝜑 → 𝐹 ∈ V)
5		fngsum 13494	. . . . . . . 8 ⊢ Σ_g Fn (V × V)
6	5	a1i 9	. . . . . . 7 ⊢ (𝜑 → Σ_g Fn (V × V))
7	1	elexd 2815	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ V)
8		gfsumval.g	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴)
9		f1of 5586	. . . . . . . . . 10 ⊢ (𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝐺:(1...(♯‘𝐴))⟶𝐴)
10	8, 9	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:(1...(♯‘𝐴))⟶𝐴)
11		1zzd 9511	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℤ)
12		hashcl 11049	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ₀)
13	3, 12	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐴) ∈ ℕ₀)
14	13	nn0zd 9605	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝐴) ∈ ℤ)
15	11, 14	fzfigd 10699	. . . . . . . . 9 ⊢ (𝜑 → (1...(♯‘𝐴)) ∈ Fin)
16	10, 15	fexd 5889	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ V)
17		coexg 5283	. . . . . . . 8 ⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹 ∘ 𝐺) ∈ V)
18	4, 16, 17	syl2anc 411	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∘ 𝐺) ∈ V)
19		fnovex 6056	. . . . . . 7 ⊢ (( Σ_g Fn (V × V) ∧ 𝑊 ∈ V ∧ (𝐹 ∘ 𝐺) ∈ V) → (𝑊 Σ_g (𝐹 ∘ 𝐺)) ∈ V)
20	6, 7, 18, 19	syl3anc 1273	. . . . . 6 ⊢ (𝜑 → (𝑊 Σ_g (𝐹 ∘ 𝐺)) ∈ V)
21	2	fdmd 5491	. . . . . . . 8 ⊢ (𝜑 → dom 𝐹 = 𝐴)
22	21, 3	eqeltrd 2307	. . . . . . 7 ⊢ (𝜑 → dom 𝐹 ∈ Fin)
23		eqidd 2231	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 = 𝐺)
24	21	fveq2d 5646	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘dom 𝐹) = (♯‘𝐴))
25	24	oveq2d 6039	. . . . . . . . . . 11 ⊢ (𝜑 → (1...(♯‘dom 𝐹)) = (1...(♯‘𝐴)))
26	23, 25, 21	f1oeq123d 5580	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ↔ 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴))
27	8, 26	mpbird 167	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹)
28		eqidd 2231	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 Σ_g (𝐹 ∘ 𝐺)) = (𝑊 Σ_g (𝐹 ∘ 𝐺)))
29	27, 28	jca 306	. . . . . . . 8 ⊢ (𝜑 → (𝐺:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σ_g (𝐹 ∘ 𝐺)) = (𝑊 Σ_g (𝐹 ∘ 𝐺))))
30		f1oeq1 5574	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ↔ 𝐺:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹))
31		coeq2 4890	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → (𝐹 ∘ 𝑔) = (𝐹 ∘ 𝐺))
32	31	oveq2d 6039	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (𝑊 Σ_g (𝐹 ∘ 𝑔)) = (𝑊 Σ_g (𝐹 ∘ 𝐺)))
33	32	eqeq2d 2242	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → ((𝑊 Σ_g (𝐹 ∘ 𝐺)) = (𝑊 Σ_g (𝐹 ∘ 𝑔)) ↔ (𝑊 Σ_g (𝐹 ∘ 𝐺)) = (𝑊 Σ_g (𝐹 ∘ 𝐺))))
34	30, 33	anbi12d 473	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σ_g (𝐹 ∘ 𝐺)) = (𝑊 Σ_g (𝐹 ∘ 𝑔))) ↔ (𝐺:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σ_g (𝐹 ∘ 𝐺)) = (𝑊 Σ_g (𝐹 ∘ 𝐺)))))
35	16, 29, 34	elabd 2950	. . . . . . 7 ⊢ (𝜑 → ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σ_g (𝐹 ∘ 𝐺)) = (𝑊 Σ_g (𝐹 ∘ 𝑔))))
36	22, 35	jca 306	. . . . . 6 ⊢ (𝜑 → (dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σ_g (𝐹 ∘ 𝐺)) = (𝑊 Σ_g (𝐹 ∘ 𝑔)))))
37		eqeq1 2237	. . . . . . . . 9 ⊢ (𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝐺)) → (𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)) ↔ (𝑊 Σ_g (𝐹 ∘ 𝐺)) = (𝑊 Σ_g (𝐹 ∘ 𝑔))))
38	37	anbi2d 464	. . . . . . . 8 ⊢ (𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝐺)) → ((𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))) ↔ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σ_g (𝐹 ∘ 𝐺)) = (𝑊 Σ_g (𝐹 ∘ 𝑔)))))
39	38	exbidv 1872	. . . . . . 7 ⊢ (𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝐺)) → (∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))) ↔ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σ_g (𝐹 ∘ 𝐺)) = (𝑊 Σ_g (𝐹 ∘ 𝑔)))))
40	39	anbi2d 464	. . . . . 6 ⊢ (𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝐺)) → ((dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ↔ (dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σ_g (𝐹 ∘ 𝐺)) = (𝑊 Σ_g (𝐹 ∘ 𝑔))))))
41	20, 36, 40	elabd 2950	. . . . 5 ⊢ (𝜑 → ∃𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))))
42		anandi 594	. . . . . . . 8 ⊢ ((dom 𝐹 ∈ Fin ∧ (∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))) ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))) ↔ ((dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))))
43		f1oeq1 5574	. . . . . . . . . . . . 13 ⊢ (𝑔 = ℎ → (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ↔ ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹))
44		coeq2 4890	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = ℎ → (𝐹 ∘ 𝑔) = (𝐹 ∘ ℎ))
45	44	oveq2d 6039	. . . . . . . . . . . . . 14 ⊢ (𝑔 = ℎ → (𝑊 Σ_g (𝐹 ∘ 𝑔)) = (𝑊 Σ_g (𝐹 ∘ ℎ)))
46	45	eqeq2d 2242	. . . . . . . . . . . . 13 ⊢ (𝑔 = ℎ → (𝑦 = (𝑊 Σ_g (𝐹 ∘ 𝑔)) ↔ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ))))
47	43, 46	anbi12d 473	. . . . . . . . . . . 12 ⊢ (𝑔 = ℎ → ((𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ 𝑔))) ↔ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))))
48	47	cbvexv 1966	. . . . . . . . . . 11 ⊢ (∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ 𝑔))) ↔ ∃ℎ(ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ))))
49	1	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → 𝑊 ∈ CMnd)
50	49	cmnmndd 13918	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → 𝑊 ∈ Mnd)
51	50	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → 𝑊 ∈ Mnd)
52		simprl 531	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → 𝑝 ∈ 𝐵)
53		simprr 533	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → 𝑞 ∈ 𝐵)
54		gfsumval.b	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐵 = (Base‘𝑊)
55		eqid 2230	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (+_g‘𝑊) = (+_g‘𝑊)
56	54, 55	mndcl 13529	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑊 ∈ Mnd ∧ 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵) → (𝑝(+_g‘𝑊)𝑞) ∈ 𝐵)
57	51, 52, 53, 56	syl3anc 1273	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (𝑝(+_g‘𝑊)𝑞) ∈ 𝐵)
58	49	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → 𝑊 ∈ CMnd)
59	54, 55	cmncom 13912	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑊 ∈ CMnd ∧ 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵) → (𝑝(+_g‘𝑊)𝑞) = (𝑞(+_g‘𝑊)𝑝))
60	58, 52, 53, 59	syl3anc 1273	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (𝑝(+_g‘𝑊)𝑞) = (𝑞(+_g‘𝑊)𝑝))
61	50	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → 𝑊 ∈ Mnd)
62	54, 55	mndass 13530	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑊 ∈ Mnd ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → ((𝑝(+_g‘𝑊)𝑞)(+_g‘𝑊)𝑟) = (𝑝(+_g‘𝑊)(𝑞(+_g‘𝑊)𝑟)))
63	61, 62	sylancom 420	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → ((𝑝(+_g‘𝑊)𝑞)(+_g‘𝑊)𝑟) = (𝑝(+_g‘𝑊)(𝑞(+_g‘𝑊)𝑟)))
64		elnnuz 9798	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((♯‘dom 𝐹) ∈ ℕ ↔ (♯‘dom 𝐹) ∈ (ℤ_≥‘1))
65	64	biimpi 120	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((♯‘dom 𝐹) ∈ ℕ → (♯‘dom 𝐹) ∈ (ℤ_≥‘1))
66	65	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (♯‘dom 𝐹) ∈ (ℤ_≥‘1))
67		ssidd 3247	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → 𝐵 ⊆ 𝐵)
68	1	ad3antrrr 492	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → 𝑊 ∈ CMnd)
69		plusgslid 13218	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (+_g = Slot (+_g‘ndx) ∧ (+_g‘ndx) ∈ ℕ)
70	69	slotex 13132	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑊 ∈ CMnd → (+_g‘𝑊) ∈ V)
71	68, 70	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (+_g‘𝑊) ∈ V)
72		simprl 531	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → 𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹)
73	21	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → dom 𝐹 = 𝐴)
74	73	f1oeq3d 5583	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ↔ 𝑔:(1...(♯‘dom 𝐹))–1-1-onto→𝐴))
75	72, 74	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → 𝑔:(1...(♯‘dom 𝐹))–1-1-onto→𝐴)
76	75	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → 𝑔:(1...(♯‘dom 𝐹))–1-1-onto→𝐴)
77		f1ocnv 5599	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→𝐴 → ^◡𝑔:𝐴–1-1-onto→(1...(♯‘dom 𝐹)))
78	76, 77	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → ^◡𝑔:𝐴–1-1-onto→(1...(♯‘dom 𝐹)))
79		simplrl 537	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹)
80	73	f1oeq3d 5583	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ↔ ℎ:(1...(♯‘dom 𝐹))–1-1-onto→𝐴))
81	79, 80	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → ℎ:(1...(♯‘dom 𝐹))–1-1-onto→𝐴)
82	81	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → ℎ:(1...(♯‘dom 𝐹))–1-1-onto→𝐴)
83		f1oco 5609	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((^◡𝑔:𝐴–1-1-onto→(1...(♯‘dom 𝐹)) ∧ ℎ:(1...(♯‘dom 𝐹))–1-1-onto→𝐴) → (^◡𝑔 ∘ ℎ):(1...(♯‘dom 𝐹))–1-1-onto→(1...(♯‘dom 𝐹)))
84	78, 82, 83	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (^◡𝑔 ∘ ℎ):(1...(♯‘dom 𝐹))–1-1-onto→(1...(♯‘dom 𝐹)))
85	2	ad4antr 494	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑝 ∈ (1...(♯‘dom 𝐹))) → 𝐹:𝐴⟶𝐵)
86		f1of 5586	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 → 𝑔:(1...(♯‘dom 𝐹))⟶dom 𝐹)
87	72, 86	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → 𝑔:(1...(♯‘dom 𝐹))⟶dom 𝐹)
88	73	feq3d 5473	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → (𝑔:(1...(♯‘dom 𝐹))⟶dom 𝐹 ↔ 𝑔:(1...(♯‘dom 𝐹))⟶𝐴))
89	87, 88	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → 𝑔:(1...(♯‘dom 𝐹))⟶𝐴)
90	89	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑝 ∈ (1...(♯‘dom 𝐹))) → 𝑔:(1...(♯‘dom 𝐹))⟶𝐴)
91		fco 5502	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑔:(1...(♯‘dom 𝐹))⟶𝐴) → (𝐹 ∘ 𝑔):(1...(♯‘dom 𝐹))⟶𝐵)
92	85, 90, 91	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑝 ∈ (1...(♯‘dom 𝐹))) → (𝐹 ∘ 𝑔):(1...(♯‘dom 𝐹))⟶𝐵)
93		simpr 110	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑝 ∈ (1...(♯‘dom 𝐹))) → 𝑝 ∈ (1...(♯‘dom 𝐹)))
94	92, 93	ffvelcdmd 5786	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑝 ∈ (1...(♯‘dom 𝐹))) → ((𝐹 ∘ 𝑔)‘𝑝) ∈ 𝐵)
95		f1of 5586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 → ℎ:(1...(♯‘dom 𝐹))⟶dom 𝐹)
96	79, 95	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → ℎ:(1...(♯‘dom 𝐹))⟶dom 𝐹)
97	73	feq3d 5473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → (ℎ:(1...(♯‘dom 𝐹))⟶dom 𝐹 ↔ ℎ:(1...(♯‘dom 𝐹))⟶𝐴))
98	96, 97	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → ℎ:(1...(♯‘dom 𝐹))⟶𝐴)
99	98	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → ℎ:(1...(♯‘dom 𝐹))⟶𝐴)
100		fvco3 5720	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ:(1...(♯‘dom 𝐹))⟶𝐴 ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → ((^◡𝑔 ∘ ℎ)‘𝑠) = (^◡𝑔‘(ℎ‘𝑠)))
101	99, 100	sylancom 420	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → ((^◡𝑔 ∘ ℎ)‘𝑠) = (^◡𝑔‘(ℎ‘𝑠)))
102	101	fveq2d 5646	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → (𝑔‘((^◡𝑔 ∘ ℎ)‘𝑠)) = (𝑔‘(^◡𝑔‘(ℎ‘𝑠))))
103	76	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → 𝑔:(1...(♯‘dom 𝐹))–1-1-onto→𝐴)
104		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → 𝑠 ∈ (1...(♯‘dom 𝐹)))
105	99, 104	ffvelcdmd 5786	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → (ℎ‘𝑠) ∈ 𝐴)
106		f1ocnvfv2 5924	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑔:(1...(♯‘dom 𝐹))–1-1-onto→𝐴 ∧ (ℎ‘𝑠) ∈ 𝐴) → (𝑔‘(^◡𝑔‘(ℎ‘𝑠))) = (ℎ‘𝑠))
107	103, 105, 106	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → (𝑔‘(^◡𝑔‘(ℎ‘𝑠))) = (ℎ‘𝑠))
108	102, 107	eqtrd 2263	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → (𝑔‘((^◡𝑔 ∘ ℎ)‘𝑠)) = (ℎ‘𝑠))
109	108	fveq2d 5646	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → (𝐹‘(𝑔‘((^◡𝑔 ∘ ℎ)‘𝑠))) = (𝐹‘(ℎ‘𝑠)))
110	89	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → 𝑔:(1...(♯‘dom 𝐹))⟶𝐴)
111		f1ocnv 5599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 → ^◡𝑔:dom 𝐹–1-1-onto→(1...(♯‘dom 𝐹)))
112		f1of 5586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (^◡𝑔:dom 𝐹–1-1-onto→(1...(♯‘dom 𝐹)) → ^◡𝑔:dom 𝐹⟶(1...(♯‘dom 𝐹)))
113	72, 111, 112	3syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → ^◡𝑔:dom 𝐹⟶(1...(♯‘dom 𝐹)))
114	73	feq2d 5472	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → (^◡𝑔:dom 𝐹⟶(1...(♯‘dom 𝐹)) ↔ ^◡𝑔:𝐴⟶(1...(♯‘dom 𝐹))))
115	113, 114	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → ^◡𝑔:𝐴⟶(1...(♯‘dom 𝐹)))
116	115	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → ^◡𝑔:𝐴⟶(1...(♯‘dom 𝐹)))
117	116, 105	ffvelcdmd 5786	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → (^◡𝑔‘(ℎ‘𝑠)) ∈ (1...(♯‘dom 𝐹)))
118	101, 117	eqeltrd 2307	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → ((^◡𝑔 ∘ ℎ)‘𝑠) ∈ (1...(♯‘dom 𝐹)))
119		fvco3 5720	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔:(1...(♯‘dom 𝐹))⟶𝐴 ∧ ((^◡𝑔 ∘ ℎ)‘𝑠) ∈ (1...(♯‘dom 𝐹))) → ((𝐹 ∘ 𝑔)‘((^◡𝑔 ∘ ℎ)‘𝑠)) = (𝐹‘(𝑔‘((^◡𝑔 ∘ ℎ)‘𝑠))))
120	110, 118, 119	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → ((𝐹 ∘ 𝑔)‘((^◡𝑔 ∘ ℎ)‘𝑠)) = (𝐹‘(𝑔‘((^◡𝑔 ∘ ℎ)‘𝑠))))
121		fvco3 5720	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ℎ:(1...(♯‘dom 𝐹))⟶𝐴 ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → ((𝐹 ∘ ℎ)‘𝑠) = (𝐹‘(ℎ‘𝑠)))
122	99, 121	sylancom 420	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → ((𝐹 ∘ ℎ)‘𝑠) = (𝐹‘(ℎ‘𝑠)))
123	109, 120, 122	3eqtr4rd 2274	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → ((𝐹 ∘ ℎ)‘𝑠) = ((𝐹 ∘ 𝑔)‘((^◡𝑔 ∘ ℎ)‘𝑠)))
124	4	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → 𝐹 ∈ V)
125		vex 2804	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑔 ∈ V
126		coexg 5283	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹 ∈ V ∧ 𝑔 ∈ V) → (𝐹 ∘ 𝑔) ∈ V)
127	124, 125, 126	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → (𝐹 ∘ 𝑔) ∈ V)
128	127	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (𝐹 ∘ 𝑔) ∈ V)
129		vex 2804	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℎ ∈ V
130		coexg 5283	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹 ∈ V ∧ ℎ ∈ V) → (𝐹 ∘ ℎ) ∈ V)
131	124, 129, 130	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → (𝐹 ∘ ℎ) ∈ V)
132	131	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (𝐹 ∘ ℎ) ∈ V)
133	57, 60, 63, 66, 67, 71, 84, 94, 123, 128, 132	seqf1og 10789	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (seq1((+_g‘𝑊), (𝐹 ∘ ℎ))‘(♯‘dom 𝐹)) = (seq1((+_g‘𝑊), (𝐹 ∘ 𝑔))‘(♯‘dom 𝐹)))
134	2	ad3antrrr 492	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → 𝐹:𝐴⟶𝐵)
135	98	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → ℎ:(1...(♯‘dom 𝐹))⟶𝐴)
136		fco 5502	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹:𝐴⟶𝐵 ∧ ℎ:(1...(♯‘dom 𝐹))⟶𝐴) → (𝐹 ∘ ℎ):(1...(♯‘dom 𝐹))⟶𝐵)
137	134, 135, 136	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (𝐹 ∘ ℎ):(1...(♯‘dom 𝐹))⟶𝐵)
138	54, 55, 68, 66, 137	gsumval2 13503	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (𝑊 Σ_g (𝐹 ∘ ℎ)) = (seq1((+_g‘𝑊), (𝐹 ∘ ℎ))‘(♯‘dom 𝐹)))
139		simplrl 537	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → 𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹)
140	139, 86	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → 𝑔:(1...(♯‘dom 𝐹))⟶dom 𝐹)
141	134	fdmd 5491	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → dom 𝐹 = 𝐴)
142	141	feq3d 5473	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (𝑔:(1...(♯‘dom 𝐹))⟶dom 𝐹 ↔ 𝑔:(1...(♯‘dom 𝐹))⟶𝐴))
143	140, 142	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → 𝑔:(1...(♯‘dom 𝐹))⟶𝐴)
144	134, 143, 91	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (𝐹 ∘ 𝑔):(1...(♯‘dom 𝐹))⟶𝐵)
145	54, 55, 68, 66, 144	gsumval2 13503	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (𝑊 Σ_g (𝐹 ∘ 𝑔)) = (seq1((+_g‘𝑊), (𝐹 ∘ 𝑔))‘(♯‘dom 𝐹)))
146	133, 138, 145	3eqtr4d 2273	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (𝑊 Σ_g (𝐹 ∘ ℎ)) = (𝑊 Σ_g (𝐹 ∘ 𝑔)))
147		simprr 533	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) → 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))
148	147	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))
149		simplrr 538	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))
150	146, 148, 149	3eqtr4rd 2274	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → 𝑥 = 𝑦)
151		simprl 531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) → ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹)
152	151	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹)
153	152, 95	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → ℎ:(1...(♯‘dom 𝐹))⟶dom 𝐹)
154		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (♯‘dom 𝐹) = 0)
155		fihasheq0 11061	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (dom 𝐹 ∈ Fin → ((♯‘dom 𝐹) = 0 ↔ dom 𝐹 = ∅))
156	22, 155	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ((♯‘dom 𝐹) = 0 ↔ dom 𝐹 = ∅))
157	156	ad3antrrr 492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → ((♯‘dom 𝐹) = 0 ↔ dom 𝐹 = ∅))
158	154, 157	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → dom 𝐹 = ∅)
159	158	feq3d 5473	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (ℎ:(1...(♯‘dom 𝐹))⟶dom 𝐹 ↔ ℎ:(1...(♯‘dom 𝐹))⟶∅))
160	153, 159	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → ℎ:(1...(♯‘dom 𝐹))⟶∅)
161		f00 5531	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ:(1...(♯‘dom 𝐹))⟶∅ ↔ (ℎ = ∅ ∧ (1...(♯‘dom 𝐹)) = ∅))
162	160, 161	sylib 122	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (ℎ = ∅ ∧ (1...(♯‘dom 𝐹)) = ∅))
163	162	simpld 112	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → ℎ = ∅)
164	163	coeq2d 4894	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝐹 ∘ ℎ) = (𝐹 ∘ ∅))
165		co02 5252	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∘ ∅) = ∅
166	164, 165	eqtrdi 2279	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝐹 ∘ ℎ) = ∅)
167	166	oveq2d 6039	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝑊 Σ_g (𝐹 ∘ ℎ)) = (𝑊 Σ_g ∅))
168		eqid 2230	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0_g‘𝑊) = (0_g‘𝑊)
169	168	gsum0g 13502	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑊 ∈ CMnd → (𝑊 Σ_g ∅) = (0_g‘𝑊))
170	1, 169	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑊 Σ_g ∅) = (0_g‘𝑊))
171	170	ad3antrrr 492	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝑊 Σ_g ∅) = (0_g‘𝑊))
172	167, 171	eqtrd 2263	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝑊 Σ_g (𝐹 ∘ ℎ)) = (0_g‘𝑊))
173	147	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))
174		simplrr 538	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))
175		simplrl 537	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹)
176	175, 86	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑔:(1...(♯‘dom 𝐹))⟶dom 𝐹)
177	158	feq3d 5473	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝑔:(1...(♯‘dom 𝐹))⟶dom 𝐹 ↔ 𝑔:(1...(♯‘dom 𝐹))⟶∅))
178	176, 177	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑔:(1...(♯‘dom 𝐹))⟶∅)
179		f00 5531	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑔:(1...(♯‘dom 𝐹))⟶∅ ↔ (𝑔 = ∅ ∧ (1...(♯‘dom 𝐹)) = ∅))
180	178, 179	sylib 122	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝑔 = ∅ ∧ (1...(♯‘dom 𝐹)) = ∅))
181	180	simpld 112	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑔 = ∅)
182	181	coeq2d 4894	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝐹 ∘ 𝑔) = (𝐹 ∘ ∅))
183	182, 165	eqtrdi 2279	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝐹 ∘ 𝑔) = ∅)
184	183	oveq2d 6039	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝑊 Σ_g (𝐹 ∘ 𝑔)) = (𝑊 Σ_g ∅))
185	174, 184, 171	3eqtrd 2267	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑥 = (0_g‘𝑊))
186	172, 173, 185	3eqtr4rd 2274	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑥 = 𝑦)
187	24, 13	eqeltrd 2307	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (♯‘dom 𝐹) ∈ ℕ₀)
188		elnn0 9409	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘dom 𝐹) ∈ ℕ₀ ↔ ((♯‘dom 𝐹) ∈ ℕ ∨ (♯‘dom 𝐹) = 0))
189	187, 188	sylib 122	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((♯‘dom 𝐹) ∈ ℕ ∨ (♯‘dom 𝐹) = 0))
190	189	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → ((♯‘dom 𝐹) ∈ ℕ ∨ (♯‘dom 𝐹) = 0))
191	150, 186, 190	mpjaodan 805	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → 𝑥 = 𝑦)
192	191	ex 115	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) → ((𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))) → 𝑥 = 𝑦))
193	192	exlimdv 1866	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) → (∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))) → 𝑥 = 𝑦))
194	193	ex 115	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ))) → (∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))) → 𝑥 = 𝑦)))
195	194	com23 78	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))) → ((ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ))) → 𝑥 = 𝑦)))
196	195	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ dom 𝐹 ∈ Fin) → (∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))) → ((ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ))) → 𝑥 = 𝑦)))
197	196	imp 124	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ dom 𝐹 ∈ Fin) ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → ((ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ))) → 𝑥 = 𝑦))
198	197	exlimdv 1866	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ dom 𝐹 ∈ Fin) ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → (∃ℎ(ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ))) → 𝑥 = 𝑦))
199	48, 198	biimtrid 152	. . . . . . . . . 10 ⊢ (((𝜑 ∧ dom 𝐹 ∈ Fin) ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → (∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ 𝑔))) → 𝑥 = 𝑦))
200	199	impr 379	. . . . . . . . 9 ⊢ (((𝜑 ∧ dom 𝐹 ∈ Fin) ∧ (∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))) ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))) → 𝑥 = 𝑦)
201	200	anasss 399	. . . . . . . 8 ⊢ ((𝜑 ∧ (dom 𝐹 ∈ Fin ∧ (∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))) ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))))) → 𝑥 = 𝑦)
202	42, 201	sylan2br 288	. . . . . . 7 ⊢ ((𝜑 ∧ ((dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))))) → 𝑥 = 𝑦)
203	202	ex 115	. . . . . 6 ⊢ (𝜑 → (((dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))) → 𝑥 = 𝑦))
204	203	alrimivv 1922	. . . . 5 ⊢ (𝜑 → ∀𝑥∀𝑦(((dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))) → 𝑥 = 𝑦))
205		eqeq1 2237	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)) ↔ 𝑦 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))
206	205	anbi2d 464	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))) ↔ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))))
207	206	exbidv 1872	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))) ↔ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))))
208	207	anbi2d 464	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ↔ (dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))))
209	208	eu4 2141	. . . . 5 ⊢ (∃!𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ↔ (∃𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ ∀𝑥∀𝑦(((dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))) → 𝑥 = 𝑦)))
210	41, 204, 209	sylanbrc 417	. . . 4 ⊢ (𝜑 → ∃!𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))))
211		euiotaex 5305	. . . 4 ⊢ (∃!𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))) ∈ V)
212	210, 211	syl 14	. . 3 ⊢ (𝜑 → (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))) ∈ V)
213		oveq1 6030	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (𝑤 Σ_g (𝑓 ∘ 𝑔)) = (𝑊 Σ_g (𝑓 ∘ 𝑔)))
214	213	eqeq2d 2242	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (𝑥 = (𝑤 Σ_g (𝑓 ∘ 𝑔)) ↔ 𝑥 = (𝑊 Σ_g (𝑓 ∘ 𝑔))))
215	214	anbi2d 464	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ((𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σ_g (𝑓 ∘ 𝑔))) ↔ (𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑊 Σ_g (𝑓 ∘ 𝑔)))))
216	215	exbidv 1872	. . . . . 6 ⊢ (𝑤 = 𝑊 → (∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σ_g (𝑓 ∘ 𝑔))) ↔ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑊 Σ_g (𝑓 ∘ 𝑔)))))
217	216	anbi2d 464	. . . . 5 ⊢ (𝑤 = 𝑊 → ((dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σ_g (𝑓 ∘ 𝑔)))) ↔ (dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑊 Σ_g (𝑓 ∘ 𝑔))))))
218	217	iotabidv 5311	. . . 4 ⊢ (𝑤 = 𝑊 → (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σ_g (𝑓 ∘ 𝑔))))) = (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑊 Σ_g (𝑓 ∘ 𝑔))))))
219		dmeq 4933	. . . . . . 7 ⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
220	219	eleq1d 2299	. . . . . 6 ⊢ (𝑓 = 𝐹 → (dom 𝑓 ∈ Fin ↔ dom 𝐹 ∈ Fin))
221		eqidd 2231	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → 𝑔 = 𝑔)
222	219	fveq2d 5646	. . . . . . . . . 10 ⊢ (𝑓 = 𝐹 → (♯‘dom 𝑓) = (♯‘dom 𝐹))
223	222	oveq2d 6039	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → (1...(♯‘dom 𝑓)) = (1...(♯‘dom 𝐹)))
224	221, 223, 219	f1oeq123d 5580	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → (𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ↔ 𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹))
225		coeq1 4889	. . . . . . . . . 10 ⊢ (𝑓 = 𝐹 → (𝑓 ∘ 𝑔) = (𝐹 ∘ 𝑔))
226	225	oveq2d 6039	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → (𝑊 Σ_g (𝑓 ∘ 𝑔)) = (𝑊 Σ_g (𝐹 ∘ 𝑔)))
227	226	eqeq2d 2242	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → (𝑥 = (𝑊 Σ_g (𝑓 ∘ 𝑔)) ↔ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))
228	224, 227	anbi12d 473	. . . . . . 7 ⊢ (𝑓 = 𝐹 → ((𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑊 Σ_g (𝑓 ∘ 𝑔))) ↔ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))))
229	228	exbidv 1872	. . . . . 6 ⊢ (𝑓 = 𝐹 → (∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑊 Σ_g (𝑓 ∘ 𝑔))) ↔ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))))
230	220, 229	anbi12d 473	. . . . 5 ⊢ (𝑓 = 𝐹 → ((dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑊 Σ_g (𝑓 ∘ 𝑔)))) ↔ (dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))))
231	230	iotabidv 5311	. . . 4 ⊢ (𝑓 = 𝐹 → (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑊 Σ_g (𝑓 ∘ 𝑔))))) = (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))))
232		df-gfsum 16747	. . . 4 ⊢ Σ_gf = (𝑤 ∈ CMnd, 𝑓 ∈ V ↦ (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σ_g (𝑓 ∘ 𝑔))))))
233	218, 231, 232	ovmpog 6161	. . 3 ⊢ ((𝑊 ∈ CMnd ∧ 𝐹 ∈ V ∧ (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))) ∈ V) → (𝑊 Σ_gf 𝐹) = (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))))
234	1, 4, 212, 233	syl3anc 1273	. 2 ⊢ (𝜑 → (𝑊 Σ_gf 𝐹) = (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))))
235	40	iota2 5318	. . . 4 ⊢ (((𝑊 Σ_g (𝐹 ∘ 𝐺)) ∈ V ∧ ∃!𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))) → ((dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σ_g (𝐹 ∘ 𝐺)) = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ↔ (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))) = (𝑊 Σ_g (𝐹 ∘ 𝐺))))
236	20, 210, 235	syl2anc 411	. . 3 ⊢ (𝜑 → ((dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σ_g (𝐹 ∘ 𝐺)) = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ↔ (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))) = (𝑊 Σ_g (𝐹 ∘ 𝐺))))
237	36, 236	mpbid 147	. 2 ⊢ (𝜑 → (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))) = (𝑊 Σ_g (𝐹 ∘ 𝐺)))
238	234, 237	eqtrd 2263	1 ⊢ (𝜑 → (𝑊 Σ_gf 𝐹) = (𝑊 Σ_g (𝐹 ∘ 𝐺)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 715 ∧ w3a 1004 ∀wal 1395 = wceq 1397 ∃wex 1540 ∃!weu 2078 ∈ wcel 2201 Vcvv 2801 ∅c0 3493 × cxp 4725 ^◡ccnv 4726 dom cdm 4727 ∘ ccom 4731 ℩cio 5286 Fn wfn 5323 ⟶wf 5324 –1-1-onto→wf1o 5327 ‘cfv 5328 (class class class)co 6023 Fincfn 6914 0cc0 8037 1c1 8038 ℕcn 9148 ℕ₀cn0 9407 ℤ_≥cuz 9760 ...cfz 10248 seqcseq 10715 ♯chash 11043 Basecbs 13105 +_gcplusg 13183 0_gc0g 13362 Σ_g cgsu 13363 Mndcmnd 13522 CMndccmn 13894 Σ_gf cgfsu 16746

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2203 ax-14 2204 ax-ext 2212 ax-coll 4205 ax-sep 4208 ax-nul 4216 ax-pow 4266 ax-pr 4301 ax-un 4532 ax-setind 4637 ax-iinf 4688 ax-cnex 8128 ax-resscn 8129 ax-1cn 8130 ax-1re 8131 ax-icn 8132 ax-addcl 8133 ax-addrcl 8134 ax-mulcl 8135 ax-mulrcl 8136 ax-addcom 8137 ax-mulcom 8138 ax-addass 8139 ax-mulass 8140 ax-distr 8141 ax-i2m1 8142 ax-0lt1 8143 ax-1rid 8144 ax-0id 8145 ax-rnegex 8146 ax-precex 8147 ax-cnre 8148 ax-pre-ltirr 8149 ax-pre-ltwlin 8150 ax-pre-lttrn 8151 ax-pre-apti 8152 ax-pre-ltadd 8153 ax-pre-mulgt0 8154

This theorem depends on definitions: df-bi 117 df-stab 838 df-dc 842 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1810 df-eu 2081 df-mo 2082 df-clab 2217 df-cleq 2223 df-clel 2226 df-nfc 2362 df-ne 2402 df-nel 2497 df-ral 2514 df-rex 2515 df-reu 2516 df-rab 2518 df-v 2803 df-sbc 3031 df-csb 3127 df-dif 3201 df-un 3203 df-in 3205 df-ss 3212 df-nul 3494 df-if 3605 df-pw 3655 df-sn 3676 df-pr 3677 df-op 3679 df-uni 3895 df-int 3930 df-iun 3973 df-br 4090 df-opab 4152 df-mpt 4153 df-tr 4189 df-id 4392 df-iord 4465 df-on 4467 df-ilim 4468 df-suc 4470 df-iom 4691 df-xp 4733 df-rel 4734 df-cnv 4735 df-co 4736 df-dm 4737 df-rn 4738 df-res 4739 df-ima 4740 df-iota 5288 df-fun 5330 df-fn 5331 df-f 5332 df-f1 5333 df-fo 5334 df-f1o 5335 df-fv 5336 df-riota 5976 df-ov 6026 df-oprab 6027 df-mpo 6028 df-1st 6308 df-2nd 6309 df-recs 6476 df-frec 6562 df-1o 6587 df-er 6707 df-en 6915 df-dom 6916 df-fin 6917 df-pnf 8221 df-mnf 8222 df-xr 8223 df-ltxr 8224 df-le 8225 df-sub 8357 df-neg 8358 df-reap 8760 df-ap 8767 df-inn 9149 df-2 9207 df-n0 9408 df-z 9485 df-uz 9761 df-fz 10249 df-fzo 10383 df-seqfrec 10716 df-ihash 11044 df-ndx 13108 df-slot 13109 df-base 13111 df-plusg 13196 df-0g 13364 df-igsum 13365 df-mgm 13462 df-sgrp 13508 df-mnd 13523 df-cmn 13896 df-gfsum 16747

This theorem is referenced by: gsumgfsum1 16749 gsumgfsum 16752 gfsumsn 16753 gfsump1 16754

W3C validator