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 16911

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 5918	. . 3 ⊢ (𝜑 → 𝐹 ∈ V)
5		fngsum 13622	. . . . . . . 8 ⊢ Σ_g Fn (V × V)
6	5	a1i 9	. . . . . . 7 ⊢ (𝜑 → Σ_g Fn (V × V))
7	1	elexd 2829	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ V)
8		gfsumval.g	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴)
9		f1of 5616	. . . . . . . . . 10 ⊢ (𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝐺:(1...(♯‘𝐴))⟶𝐴)
10	8, 9	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:(1...(♯‘𝐴))⟶𝐴)
11		1zzd 9609	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℤ)
12		hashcl 11152	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ₀)
13	3, 12	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐴) ∈ ℕ₀)
14	13	nn0zd 9704	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝐴) ∈ ℤ)
15	11, 14	fzfigd 10800	. . . . . . . . 9 ⊢ (𝜑 → (1...(♯‘𝐴)) ∈ Fin)
16	10, 15	fexd 5918	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ V)
17		coexg 5309	. . . . . . . 8 ⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹 ∘ 𝐺) ∈ V)
18	4, 16, 17	syl2anc 411	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∘ 𝐺) ∈ V)
19		fnovex 6085	. . . . . . 7 ⊢ (( Σ_g Fn (V × V) ∧ 𝑊 ∈ V ∧ (𝐹 ∘ 𝐺) ∈ V) → (𝑊 Σ_g (𝐹 ∘ 𝐺)) ∈ V)
20	6, 7, 18, 19	syl3anc 1274	. . . . . 6 ⊢ (𝜑 → (𝑊 Σ_g (𝐹 ∘ 𝐺)) ∈ V)
21	2	fdmd 5517	. . . . . . . 8 ⊢ (𝜑 → dom 𝐹 = 𝐴)
22	21, 3	eqeltrd 2311	. . . . . . 7 ⊢ (𝜑 → dom 𝐹 ∈ Fin)
23		eqidd 2235	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 = 𝐺)
24	21	fveq2d 5676	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘dom 𝐹) = (♯‘𝐴))
25	24	oveq2d 6068	. . . . . . . . . . 11 ⊢ (𝜑 → (1...(♯‘dom 𝐹)) = (1...(♯‘𝐴)))
26	23, 25, 21	f1oeq123d 5610	. . . . . . . . . 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 2235	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 Σ_g (𝐹 ∘ 𝐺)) = (𝑊 Σ_g (𝐹 ∘ 𝐺)))
29	27, 28	jca 306	. . . . . . . 8 ⊢ (𝜑 → (𝐺:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σ_g (𝐹 ∘ 𝐺)) = (𝑊 Σ_g (𝐹 ∘ 𝐺))))
30		f1oeq1 5604	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ↔ 𝐺:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹))
31		coeq2 4915	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → (𝐹 ∘ 𝑔) = (𝐹 ∘ 𝐺))
32	31	oveq2d 6068	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (𝑊 Σ_g (𝐹 ∘ 𝑔)) = (𝑊 Σ_g (𝐹 ∘ 𝐺)))
33	32	eqeq2d 2246	. . . . . . . . 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 2964	. . . . . . 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 2241	. . . . . . . . 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 1874	. . . . . . 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 2964	. . . . 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 5604	. . . . . . . . . . . . 13 ⊢ (𝑔 = ℎ → (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ↔ ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹))
44		coeq2 4915	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = ℎ → (𝐹 ∘ 𝑔) = (𝐹 ∘ ℎ))
45	44	oveq2d 6068	. . . . . . . . . . . . . 14 ⊢ (𝑔 = ℎ → (𝑊 Σ_g (𝐹 ∘ 𝑔)) = (𝑊 Σ_g (𝐹 ∘ ℎ)))
46	45	eqeq2d 2246	. . . . . . . . . . . . 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 1970	. . . . . . . . . . 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 14046	. . . . . . . . . . . . . . . . . . . . . . . 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 2234	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (+_g‘𝑊) = (+_g‘𝑊)
56	54, 55	mndcl 13657	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑊 ∈ Mnd ∧ 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵) → (𝑝(+_g‘𝑊)𝑞) ∈ 𝐵)
57	51, 52, 53, 56	syl3anc 1274	. . . . . . . . . . . . . . . . . . . . . 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 14040	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑊 ∈ CMnd ∧ 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵) → (𝑝(+_g‘𝑊)𝑞) = (𝑞(+_g‘𝑊)𝑝))
60	58, 52, 53, 59	syl3anc 1274	. . . . . . . . . . . . . . . . . . . . . 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 13658	. . . . . . . . . . . . . . . . . . . . . . 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 9897	. . . . . . . . . . . . . . . . . . . . . . . 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 3261	. . . . . . . . . . . . . . . . . . . . . 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 13346	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (+_g = Slot (+_g‘ndx) ∧ (+_g‘ndx) ∈ ℕ)
70	69	slotex 13260	. . . . . . . . . . . . . . . . . . . . . . 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 5613	. . . . . . . . . . . . . . . . . . . . . . . . . 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 5629	. . . . . . . . . . . . . . . . . . . . . . . 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 5613	. . . . . . . . . . . . . . . . . . . . . . . . 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 5639	. . . . . . . . . . . . . . . . . . . . . . 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 5616	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5499	. . . . . . . . . . . . . . . . . . . . . . . . . 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 5529	. . . . . . . . . . . . . . . . . . . . . . . 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 5815	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑝 ∈ (1...(♯‘dom 𝐹))) → ((𝐹 ∘ 𝑔)‘𝑝) ∈ 𝐵)
95		f1of 5616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5750	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5676	. . . . . . . . . . . . . . . . . . . . . . . . 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 5815	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → (ℎ‘𝑠) ∈ 𝐴)
106		f1ocnvfv2 5953	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2267	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → (𝑔‘((^◡𝑔 ∘ ℎ)‘𝑠)) = (ℎ‘𝑠))
109	108	fveq2d 5676	. . . . . . . . . . . . . . . . . . . . . . 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 5629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 → ^◡𝑔:dom 𝐹–1-1-onto→(1...(♯‘dom 𝐹)))
112		f1of 5616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5498	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5815	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → (^◡𝑔‘(ℎ‘𝑠)) ∈ (1...(♯‘dom 𝐹)))
118	101, 117	eqeltrd 2311	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → ((^◡𝑔 ∘ ℎ)‘𝑠) ∈ (1...(♯‘dom 𝐹)))
119		fvco3 5750	. . . . . . . . . . . . . . . . . . . . . . . 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 5750	. . . . . . . . . . . . . . . . . . . . . . . 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 2278	. . . . . . . . . . . . . . . . . . . . . 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 2818	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑔 ∈ V
126		coexg 5309	. . . . . . . . . . . . . . . . . . . . . . . 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 2818	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℎ ∈ V
130		coexg 5309	. . . . . . . . . . . . . . . . . . . . . . . 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 10890	. . . . . . . . . . . . . . . . . . . . 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 5529	. . . . . . . . . . . . . . . . . . . . . . 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 13631	. . . . . . . . . . . . . . . . . . . . 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 5517	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → dom 𝐹 = 𝐴)
142	141	feq3d 5499	. . . . . . . . . . . . . . . . . . . . . . . 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 13631	. . . . . . . . . . . . . . . . . . . . 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 2277	. . . . . . . . . . . . . . . . . . . 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 2278	. . . . . . . . . . . . . . . . . . 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 11164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5499	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5561	. . . . . . . . . . . . . . . . . . . . . . . . . 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 4919	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝐹 ∘ ℎ) = (𝐹 ∘ ∅))
165		co02 5278	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∘ ∅) = ∅
166	164, 165	eqtrdi 2283	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝐹 ∘ ℎ) = ∅)
167	166	oveq2d 6068	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝑊 Σ_g (𝐹 ∘ ℎ)) = (𝑊 Σ_g ∅))
168		eqid 2234	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0_g‘𝑊) = (0_g‘𝑊)
169	168	gsum0g 13630	. . . . . . . . . . . . . . . . . . . . . . 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 2267	. . . . . . . . . . . . . . . . . . . 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 5499	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5561	. . . . . . . . . . . . . . . . . . . . . . . . . 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 4919	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝐹 ∘ 𝑔) = (𝐹 ∘ ∅))
183	182, 165	eqtrdi 2283	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝐹 ∘ 𝑔) = ∅)
184	183	oveq2d 6068	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝑊 Σ_g (𝐹 ∘ 𝑔)) = (𝑊 Σ_g ∅))
185	174, 184, 171	3eqtrd 2271	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑥 = (0_g‘𝑊))
186	172, 173, 185	3eqtr4rd 2278	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑥 = 𝑦)
187	24, 13	eqeltrd 2311	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (♯‘dom 𝐹) ∈ ℕ₀)
188		elnn0 9503	. . . . . . . . . . . . . . . . . . . . 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 806	. . . . . . . . . . . . . . . . . 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 1868	. . . . . . . . . . . . . . . 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 1868	. . . . . . . . . . 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 1924	. . . . 5 ⊢ (𝜑 → ∀𝑥∀𝑦(((dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))) → 𝑥 = 𝑦))
205		eqeq1 2241	. . . . . . . . 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 1874	. . . . . . 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 2145	. . . . 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 5331	. . . 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 6059	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (𝑤 Σ_g (𝑓 ∘ 𝑔)) = (𝑊 Σ_g (𝑓 ∘ 𝑔)))
214	213	eqeq2d 2246	. . . . . . . 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 1874	. . . . . 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 5337	. . . 4 ⊢ (𝑤 = 𝑊 → (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σ_g (𝑓 ∘ 𝑔))))) = (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑊 Σ_g (𝑓 ∘ 𝑔))))))
219		dmeq 4958	. . . . . . 7 ⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
220	219	eleq1d 2303	. . . . . 6 ⊢ (𝑓 = 𝐹 → (dom 𝑓 ∈ Fin ↔ dom 𝐹 ∈ Fin))
221		eqidd 2235	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → 𝑔 = 𝑔)
222	219	fveq2d 5676	. . . . . . . . . 10 ⊢ (𝑓 = 𝐹 → (♯‘dom 𝑓) = (♯‘dom 𝐹))
223	222	oveq2d 6068	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → (1...(♯‘dom 𝑓)) = (1...(♯‘dom 𝐹)))
224	221, 223, 219	f1oeq123d 5610	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → (𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ↔ 𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹))
225		coeq1 4914	. . . . . . . . . 10 ⊢ (𝑓 = 𝐹 → (𝑓 ∘ 𝑔) = (𝐹 ∘ 𝑔))
226	225	oveq2d 6068	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → (𝑊 Σ_g (𝑓 ∘ 𝑔)) = (𝑊 Σ_g (𝐹 ∘ 𝑔)))
227	226	eqeq2d 2246	. . . . . . . 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 1874	. . . . . 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 5337	. . . 4 ⊢ (𝑓 = 𝐹 → (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑊 Σ_g (𝑓 ∘ 𝑔))))) = (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))))
232		df-gfsum 16910	. . . 4 ⊢ Σ_gf = (𝑤 ∈ CMnd, 𝑓 ∈ V ↦ (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σ_g (𝑓 ∘ 𝑔))))))
233	218, 231, 232	ovmpog 6190	. . 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 1274	. 2 ⊢ (𝜑 → (𝑊 Σ_gf 𝐹) = (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))))
235	40	iota2 5344	. . . 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 2267	1 ⊢ (𝜑 → (𝑊 Σ_gf 𝐹) = (𝑊 Σ_g (𝐹 ∘ 𝐺)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 716 ∧ w3a 1005 ∀wal 1396 = wceq 1398 ∃wex 1541 ∃!weu 2082 ∈ wcel 2205 Vcvv 2815 ∅c0 3510 × cxp 4749 ^◡ccnv 4750 dom cdm 4751 ∘ ccom 4755 ℩cio 5312 Fn wfn 5349 ⟶wf 5350 –1-1-onto→wf1o 5353 ‘cfv 5354 (class class class)co 6052 Fincfn 6977 0cc0 8132 1c1 8133 ℕcn 9242 ℕ₀cn0 9501 ℤ_≥cuz 9859 ...cfz 10348 seqcseq 10816 ♯chash 11146 Basecbs 13233 +_gcplusg 13311 0_gc0g 13490 Σ_g cgsu 13491 Mndcmnd 13650 CMndccmn 14022 Σ_gf cgfsu 16909

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 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2207 ax-14 2208 ax-ext 2216 ax-coll 4227 ax-sep 4230 ax-nul 4238 ax-pow 4289 ax-pr 4324 ax-un 4556 ax-setind 4661 ax-iinf 4712 ax-cnex 8223 ax-resscn 8224 ax-1cn 8225 ax-1re 8226 ax-icn 8227 ax-addcl 8228 ax-addrcl 8229 ax-mulcl 8230 ax-mulrcl 8231 ax-addcom 8232 ax-mulcom 8233 ax-addass 8234 ax-mulass 8235 ax-distr 8236 ax-i2m1 8237 ax-0lt1 8238 ax-1rid 8239 ax-0id 8240 ax-rnegex 8241 ax-precex 8242 ax-cnre 8243 ax-pre-ltirr 8244 ax-pre-ltwlin 8245 ax-pre-lttrn 8246 ax-pre-apti 8247 ax-pre-ltadd 8248 ax-pre-mulgt0 8249

This theorem depends on definitions: df-bi 117 df-stab 839 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2085 df-mo 2086 df-clab 2221 df-cleq 2227 df-clel 2230 df-nfc 2375 df-ne 2415 df-nel 2510 df-ral 2527 df-rex 2528 df-reu 2529 df-rab 2531 df-v 2817 df-sbc 3045 df-csb 3141 df-dif 3215 df-un 3217 df-in 3219 df-ss 3226 df-nul 3511 df-if 3623 df-pw 3673 df-sn 3697 df-pr 3698 df-op 3700 df-uni 3917 df-int 3952 df-iun 3995 df-br 4112 df-opab 4174 df-mpt 4175 df-tr 4211 df-id 4416 df-iord 4489 df-on 4491 df-ilim 4492 df-suc 4494 df-iom 4715 df-xp 4757 df-rel 4758 df-cnv 4759 df-co 4760 df-dm 4761 df-rn 4762 df-res 4763 df-ima 4764 df-iota 5314 df-fun 5356 df-fn 5357 df-f 5358 df-f1 5359 df-fo 5360 df-f1o 5361 df-fv 5362 df-riota 6005 df-ov 6055 df-oprab 6056 df-mpo 6057 df-1st 6336 df-2nd 6337 df-recs 6538 df-frec 6624 df-1o 6649 df-er 6769 df-en 6978 df-dom 6979 df-fin 6980 df-pnf 8315 df-mnf 8316 df-xr 8317 df-ltxr 8318 df-le 8319 df-sub 8451 df-neg 8452 df-reap 8854 df-ap 8861 df-inn 9243 df-2 9301 df-n0 9502 df-z 9583 df-uz 9860 df-fz 10349 df-fzo 10484 df-seqfrec 10817 df-ihash 11147 df-ndx 13236 df-slot 13237 df-base 13239 df-plusg 13324 df-0g 13492 df-igsum 13493 df-mgm 13590 df-sgrp 13636 df-mnd 13651 df-cmn 14024 df-gfsum 16910

This theorem is referenced by: gsumgfsum1 16912 gsumgfsum 16915 gfsumsn 16916 gfsump1 16917

W3C validator