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 16701

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 5884	. . 3 ⊢ (𝜑 → 𝐹 ∈ V)
5		fngsum 13473	. . . . . . . 8 ⊢ Σ_g Fn (V × V)
6	5	a1i 9	. . . . . . 7 ⊢ (𝜑 → Σ_g Fn (V × V))
7	1	elexd 2816	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ V)
8		gfsumval.g	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴)
9		f1of 5583	. . . . . . . . . 10 ⊢ (𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝐺:(1...(♯‘𝐴))⟶𝐴)
10	8, 9	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:(1...(♯‘𝐴))⟶𝐴)
11		1zzd 9506	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℤ)
12		hashcl 11044	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ₀)
13	3, 12	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐴) ∈ ℕ₀)
14	13	nn0zd 9600	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝐴) ∈ ℤ)
15	11, 14	fzfigd 10694	. . . . . . . . 9 ⊢ (𝜑 → (1...(♯‘𝐴)) ∈ Fin)
16	10, 15	fexd 5884	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ V)
17		coexg 5281	. . . . . . . 8 ⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹 ∘ 𝐺) ∈ V)
18	4, 16, 17	syl2anc 411	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∘ 𝐺) ∈ V)
19		fnovex 6051	. . . . . . 7 ⊢ (( Σ_g Fn (V × V) ∧ 𝑊 ∈ V ∧ (𝐹 ∘ 𝐺) ∈ V) → (𝑊 Σ_g (𝐹 ∘ 𝐺)) ∈ V)
20	6, 7, 18, 19	syl3anc 1273	. . . . . 6 ⊢ (𝜑 → (𝑊 Σ_g (𝐹 ∘ 𝐺)) ∈ V)
21	2	fdmd 5489	. . . . . . . 8 ⊢ (𝜑 → dom 𝐹 = 𝐴)
22	21, 3	eqeltrd 2308	. . . . . . 7 ⊢ (𝜑 → dom 𝐹 ∈ Fin)
23		eqidd 2232	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 = 𝐺)
24	21	fveq2d 5643	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘dom 𝐹) = (♯‘𝐴))
25	24	oveq2d 6034	. . . . . . . . . . 11 ⊢ (𝜑 → (1...(♯‘dom 𝐹)) = (1...(♯‘𝐴)))
26	23, 25, 21	f1oeq123d 5577	. . . . . . . . . 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 2232	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 Σ_g (𝐹 ∘ 𝐺)) = (𝑊 Σ_g (𝐹 ∘ 𝐺)))
29	27, 28	jca 306	. . . . . . . 8 ⊢ (𝜑 → (𝐺:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σ_g (𝐹 ∘ 𝐺)) = (𝑊 Σ_g (𝐹 ∘ 𝐺))))
30		f1oeq1 5571	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ↔ 𝐺:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹))
31		coeq2 4888	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → (𝐹 ∘ 𝑔) = (𝐹 ∘ 𝐺))
32	31	oveq2d 6034	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (𝑊 Σ_g (𝐹 ∘ 𝑔)) = (𝑊 Σ_g (𝐹 ∘ 𝐺)))
33	32	eqeq2d 2243	. . . . . . . . 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 2951	. . . . . . 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 2238	. . . . . . . . 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 1873	. . . . . . 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 2951	. . . . 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 5571	. . . . . . . . . . . . 13 ⊢ (𝑔 = ℎ → (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ↔ ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹))
44		coeq2 4888	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = ℎ → (𝐹 ∘ 𝑔) = (𝐹 ∘ ℎ))
45	44	oveq2d 6034	. . . . . . . . . . . . . 14 ⊢ (𝑔 = ℎ → (𝑊 Σ_g (𝐹 ∘ 𝑔)) = (𝑊 Σ_g (𝐹 ∘ ℎ)))
46	45	eqeq2d 2243	. . . . . . . . . . . . 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 1967	. . . . . . . . . . 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 13897	. . . . . . . . . . . . . . . . . . . . . . . 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 2231	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (+_g‘𝑊) = (+_g‘𝑊)
56	54, 55	mndcl 13508	. . . . . . . . . . . . . . . . . . . . . . 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 13891	. . . . . . . . . . . . . . . . . . . . . . 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 13509	. . . . . . . . . . . . . . . . . . . . . . 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 9793	. . . . . . . . . . . . . . . . . . . . . . . 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 3248	. . . . . . . . . . . . . . . . . . . . . 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 13197	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (+_g = Slot (+_g‘ndx) ∧ (+_g‘ndx) ∈ ℕ)
70	69	slotex 13111	. . . . . . . . . . . . . . . . . . . . . . 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 5580	. . . . . . . . . . . . . . . . . . . . . . . . . 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 5596	. . . . . . . . . . . . . . . . . . . . . . . 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 5580	. . . . . . . . . . . . . . . . . . . . . . . . 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 5606	. . . . . . . . . . . . . . . . . . . . . . 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 5583	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5471	. . . . . . . . . . . . . . . . . . . . . . . . . 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 5500	. . . . . . . . . . . . . . . . . . . . . . . 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 5783	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑝 ∈ (1...(♯‘dom 𝐹))) → ((𝐹 ∘ 𝑔)‘𝑝) ∈ 𝐵)
95		f1of 5583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5717	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5643	. . . . . . . . . . . . . . . . . . . . . . . . 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 5783	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → (ℎ‘𝑠) ∈ 𝐴)
106		f1ocnvfv2 5919	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2264	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → (𝑔‘((^◡𝑔 ∘ ℎ)‘𝑠)) = (ℎ‘𝑠))
109	108	fveq2d 5643	. . . . . . . . . . . . . . . . . . . . . . 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 5596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 → ^◡𝑔:dom 𝐹–1-1-onto→(1...(♯‘dom 𝐹)))
112		f1of 5583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5470	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5783	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → (^◡𝑔‘(ℎ‘𝑠)) ∈ (1...(♯‘dom 𝐹)))
118	101, 117	eqeltrd 2308	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → ((^◡𝑔 ∘ ℎ)‘𝑠) ∈ (1...(♯‘dom 𝐹)))
119		fvco3 5717	. . . . . . . . . . . . . . . . . . . . . . . 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 5717	. . . . . . . . . . . . . . . . . . . . . . . 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 2275	. . . . . . . . . . . . . . . . . . . . . 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 2805	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑔 ∈ V
126		coexg 5281	. . . . . . . . . . . . . . . . . . . . . . . 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 2805	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℎ ∈ V
130		coexg 5281	. . . . . . . . . . . . . . . . . . . . . . . 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 10784	. . . . . . . . . . . . . . . . . . . . 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 5500	. . . . . . . . . . . . . . . . . . . . . . 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 13482	. . . . . . . . . . . . . . . . . . . . 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 5489	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → dom 𝐹 = 𝐴)
142	141	feq3d 5471	. . . . . . . . . . . . . . . . . . . . . . . 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 13482	. . . . . . . . . . . . . . . . . . . . 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 2274	. . . . . . . . . . . . . . . . . . . 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 2275	. . . . . . . . . . . . . . . . . . 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 11056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5471	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5528	. . . . . . . . . . . . . . . . . . . . . . . . . 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 4892	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝐹 ∘ ℎ) = (𝐹 ∘ ∅))
165		co02 5250	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∘ ∅) = ∅
166	164, 165	eqtrdi 2280	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝐹 ∘ ℎ) = ∅)
167	166	oveq2d 6034	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝑊 Σ_g (𝐹 ∘ ℎ)) = (𝑊 Σ_g ∅))
168		eqid 2231	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0_g‘𝑊) = (0_g‘𝑊)
169	168	gsum0g 13481	. . . . . . . . . . . . . . . . . . . . . . 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 2264	. . . . . . . . . . . . . . . . . . . 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 5471	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5528	. . . . . . . . . . . . . . . . . . . . . . . . . 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 4892	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝐹 ∘ 𝑔) = (𝐹 ∘ ∅))
183	182, 165	eqtrdi 2280	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝐹 ∘ 𝑔) = ∅)
184	183	oveq2d 6034	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝑊 Σ_g (𝐹 ∘ 𝑔)) = (𝑊 Σ_g ∅))
185	174, 184, 171	3eqtrd 2268	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑥 = (0_g‘𝑊))
186	172, 173, 185	3eqtr4rd 2275	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑥 = 𝑦)
187	24, 13	eqeltrd 2308	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (♯‘dom 𝐹) ∈ ℕ₀)
188		elnn0 9404	. . . . . . . . . . . . . . . . . . . . 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 1867	. . . . . . . . . . . . . . . 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 1867	. . . . . . . . . . 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 1923	. . . . 5 ⊢ (𝜑 → ∀𝑥∀𝑦(((dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))) → 𝑥 = 𝑦))
205		eqeq1 2238	. . . . . . . . 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 1873	. . . . . . 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 2142	. . . . 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 5303	. . . 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 6025	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (𝑤 Σ_g (𝑓 ∘ 𝑔)) = (𝑊 Σ_g (𝑓 ∘ 𝑔)))
214	213	eqeq2d 2243	. . . . . . . 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 1873	. . . . . 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 5309	. . . 4 ⊢ (𝑤 = 𝑊 → (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σ_g (𝑓 ∘ 𝑔))))) = (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑊 Σ_g (𝑓 ∘ 𝑔))))))
219		dmeq 4931	. . . . . . 7 ⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
220	219	eleq1d 2300	. . . . . 6 ⊢ (𝑓 = 𝐹 → (dom 𝑓 ∈ Fin ↔ dom 𝐹 ∈ Fin))
221		eqidd 2232	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → 𝑔 = 𝑔)
222	219	fveq2d 5643	. . . . . . . . . 10 ⊢ (𝑓 = 𝐹 → (♯‘dom 𝑓) = (♯‘dom 𝐹))
223	222	oveq2d 6034	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → (1...(♯‘dom 𝑓)) = (1...(♯‘dom 𝐹)))
224	221, 223, 219	f1oeq123d 5577	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → (𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ↔ 𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹))
225		coeq1 4887	. . . . . . . . . 10 ⊢ (𝑓 = 𝐹 → (𝑓 ∘ 𝑔) = (𝐹 ∘ 𝑔))
226	225	oveq2d 6034	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → (𝑊 Σ_g (𝑓 ∘ 𝑔)) = (𝑊 Σ_g (𝐹 ∘ 𝑔)))
227	226	eqeq2d 2243	. . . . . . . 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 1873	. . . . . 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 5309	. . . 4 ⊢ (𝑓 = 𝐹 → (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑊 Σ_g (𝑓 ∘ 𝑔))))) = (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))))
232		df-gfsum 16700	. . . 4 ⊢ Σ_gf = (𝑤 ∈ CMnd, 𝑓 ∈ V ↦ (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σ_g (𝑓 ∘ 𝑔))))))
233	218, 231, 232	ovmpog 6156	. . 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 5316	. . . 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 2264	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 2079 ∈ wcel 2202 Vcvv 2802 ∅c0 3494 × cxp 4723 ^◡ccnv 4724 dom cdm 4725 ∘ ccom 4729 ℩cio 5284 Fn wfn 5321 ⟶wf 5322 –1-1-onto→wf1o 5325 ‘cfv 5326 (class class class)co 6018 Fincfn 6909 0cc0 8032 1c1 8033 ℕcn 9143 ℕ₀cn0 9402 ℤ_≥cuz 9755 ...cfz 10243 seqcseq 10710 ♯chash 11038 Basecbs 13084 +_gcplusg 13162 0_gc0g 13341 Σ_g cgsu 13342 Mndcmnd 13501 CMndccmn 13873 Σ_gf cgfsu 16699

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 2204 ax-14 2205 ax-ext 2213 ax-coll 4204 ax-sep 4207 ax-nul 4215 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-setind 4635 ax-iinf 4686 ax-cnex 8123 ax-resscn 8124 ax-1cn 8125 ax-1re 8126 ax-icn 8127 ax-addcl 8128 ax-addrcl 8129 ax-mulcl 8130 ax-mulrcl 8131 ax-addcom 8132 ax-mulcom 8133 ax-addass 8134 ax-mulass 8135 ax-distr 8136 ax-i2m1 8137 ax-0lt1 8138 ax-1rid 8139 ax-0id 8140 ax-rnegex 8141 ax-precex 8142 ax-cnre 8143 ax-pre-ltirr 8144 ax-pre-ltwlin 8145 ax-pre-lttrn 8146 ax-pre-apti 8147 ax-pre-ltadd 8148 ax-pre-mulgt0 8149

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 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-nel 2498 df-ral 2515 df-rex 2516 df-reu 2517 df-rab 2519 df-v 2804 df-sbc 3032 df-csb 3128 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-nul 3495 df-if 3606 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-int 3929 df-iun 3972 df-br 4089 df-opab 4151 df-mpt 4152 df-tr 4188 df-id 4390 df-iord 4463 df-on 4465 df-ilim 4466 df-suc 4468 df-iom 4689 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-rn 4736 df-res 4737 df-ima 4738 df-iota 5286 df-fun 5328 df-fn 5329 df-f 5330 df-f1 5331 df-fo 5332 df-f1o 5333 df-fv 5334 df-riota 5971 df-ov 6021 df-oprab 6022 df-mpo 6023 df-1st 6303 df-2nd 6304 df-recs 6471 df-frec 6557 df-1o 6582 df-er 6702 df-en 6910 df-dom 6911 df-fin 6912 df-pnf 8216 df-mnf 8217 df-xr 8218 df-ltxr 8219 df-le 8220 df-sub 8352 df-neg 8353 df-reap 8755 df-ap 8762 df-inn 9144 df-2 9202 df-n0 9403 df-z 9480 df-uz 9756 df-fz 10244 df-fzo 10378 df-seqfrec 10711 df-ihash 11039 df-ndx 13087 df-slot 13088 df-base 13090 df-plusg 13175 df-0g 13343 df-igsum 13344 df-mgm 13441 df-sgrp 13487 df-mnd 13502 df-cmn 13875 df-gfsum 16700

This theorem is referenced by: gsumgfsum1 16702 gsumgfsum 16705 gfsumsn 16706 gfsump1 16707

W3C validator