Theorem gsumvalfi 14129

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

Hypotheses

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

Assertion

Ref	Expression
gsumvalfi	⊢ (𝜑 → (𝑊 Σg 𝐹) = (𝑊 Σgz (𝐹 ∘ 𝐺)))

Proof of Theorem gsumvalfi

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

Step	Hyp	Ref	Expression
1		gsumvalfi.w	. . 3 ⊢ (𝜑 → 𝑊 ∈ CMnd)
2		gsumvalfi.f	. . . 4 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
3		gsumvalfi.fi	. . . 4 ⊢ (𝜑 → 𝐴 ∈ Fin)
4	2, 3	fexd 5938	. . 3 ⊢ (𝜑 → 𝐹 ∈ V)
5		fngzsum 13685	. . . . . . 7 ⊢ Σgz Fn (V × V)
6	1	elexd 2835	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ V)
7		gsumvalfi.g	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴)
8		f1of 5634	. . . . . . . . . 10 ⊢ (𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝐺:(1...(♯‘𝐴))⟶𝐴)
9	7, 8	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:(1...(♯‘𝐴))⟶𝐴)
10		1zzd 9650	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℤ)
11		hashcl 11198	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)
12	3, 11	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐴) ∈ ℕ0)
13	12	nn0zd 9745	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝐴) ∈ ℤ)
14	10, 13	fzfigd 10846	. . . . . . . . 9 ⊢ (𝜑 → (1...(♯‘𝐴)) ∈ Fin)
15	9, 14	fexd 5938	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ V)
16		coexg 5327	. . . . . . . 8 ⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹 ∘ 𝐺) ∈ V)
17	4, 15, 16	syl2anc 415	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∘ 𝐺) ∈ V)
18		fnovex 6108	. . . . . . 7 ⊢ (( Σgz Fn (V × V) ∧ 𝑊 ∈ V ∧ (𝐹 ∘ 𝐺) ∈ V) → (𝑊 Σgz (𝐹 ∘ 𝐺)) ∈ V)
19	5, 6, 17, 18	mp3an2i 1383	. . . . . 6 ⊢ (𝜑 → (𝑊 Σgz (𝐹 ∘ 𝐺)) ∈ V)
20	2	fdmd 5535	. . . . . . . 8 ⊢ (𝜑 → dom 𝐹 = 𝐴)
21	20, 3	eqeltrd 2315	. . . . . . 7 ⊢ (𝜑 → dom 𝐹 ∈ Fin)
22		eqidd 2239	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 = 𝐺)
23	20	fveq2d 5694	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘dom 𝐹) = (♯‘𝐴))
24	23	oveq2d 6091	. . . . . . . . . . 11 ⊢ (𝜑 → (1...(♯‘dom 𝐹)) = (1...(♯‘𝐴)))
25	22, 24, 20	f1oeq123d 5628	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ↔ 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴))
26	7, 25	mpbird 167	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹)
27		eqidd 2239	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 Σgz (𝐹 ∘ 𝐺)) = (𝑊 Σgz (𝐹 ∘ 𝐺)))
28	26, 27	jca 306	. . . . . . . 8 ⊢ (𝜑 → (𝐺:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σgz (𝐹 ∘ 𝐺)) = (𝑊 Σgz (𝐹 ∘ 𝐺))))
29		f1oeq1 5622	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ↔ 𝐺:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹))
30		coeq2 4933	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → (𝐹 ∘ 𝑔) = (𝐹 ∘ 𝐺))
31	30	oveq2d 6091	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (𝑊 Σgz (𝐹 ∘ 𝑔)) = (𝑊 Σgz (𝐹 ∘ 𝐺)))
32	31	eqeq2d 2250	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → ((𝑊 Σgz (𝐹 ∘ 𝐺)) = (𝑊 Σgz (𝐹 ∘ 𝑔)) ↔ (𝑊 Σgz (𝐹 ∘ 𝐺)) = (𝑊 Σgz (𝐹 ∘ 𝐺))))
33	29, 32	anbi12d 477	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σgz (𝐹 ∘ 𝐺)) = (𝑊 Σgz (𝐹 ∘ 𝑔))) ↔ (𝐺:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σgz (𝐹 ∘ 𝐺)) = (𝑊 Σgz (𝐹 ∘ 𝐺)))))
34	15, 28, 33	elabd 2971	. . . . . . 7 ⊢ (𝜑 → ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σgz (𝐹 ∘ 𝐺)) = (𝑊 Σgz (𝐹 ∘ 𝑔))))
35	21, 34	jca 306	. . . . . 6 ⊢ (𝜑 → (dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σgz (𝐹 ∘ 𝐺)) = (𝑊 Σgz (𝐹 ∘ 𝑔)))))
36		eqeq1 2245	. . . . . . . . 9 ⊢ (𝑥 = (𝑊 Σgz (𝐹 ∘ 𝐺)) → (𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)) ↔ (𝑊 Σgz (𝐹 ∘ 𝐺)) = (𝑊 Σgz (𝐹 ∘ 𝑔))))
37	36	anbi2d 468	. . . . . . . 8 ⊢ (𝑥 = (𝑊 Σgz (𝐹 ∘ 𝐺)) → ((𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))) ↔ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σgz (𝐹 ∘ 𝐺)) = (𝑊 Σgz (𝐹 ∘ 𝑔)))))
38	37	exbidv 1878	. . . . . . 7 ⊢ (𝑥 = (𝑊 Σgz (𝐹 ∘ 𝐺)) → (∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))) ↔ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σgz (𝐹 ∘ 𝐺)) = (𝑊 Σgz (𝐹 ∘ 𝑔)))))
39	38	anbi2d 468	. . . . . 6 ⊢ (𝑥 = (𝑊 Σgz (𝐹 ∘ 𝐺)) → ((dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ↔ (dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σgz (𝐹 ∘ 𝐺)) = (𝑊 Σgz (𝐹 ∘ 𝑔))))))
40	19, 35, 39	elabd 2971	. . . . 5 ⊢ (𝜑 → ∃𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))))
41		anandi 598	. . . . . . . 8 ⊢ ((dom 𝐹 ∈ Fin ∧ (∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))) ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ 𝑔))))) ↔ ((dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ 𝑔))))))
42		f1oeq1 5622	. . . . . . . . . . . . 13 ⊢ (𝑔 = ℎ → (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ↔ ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹))
43		coeq2 4933	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = ℎ → (𝐹 ∘ 𝑔) = (𝐹 ∘ ℎ))
44	43	oveq2d 6091	. . . . . . . . . . . . . 14 ⊢ (𝑔 = ℎ → (𝑊 Σgz (𝐹 ∘ 𝑔)) = (𝑊 Σgz (𝐹 ∘ ℎ)))
45	44	eqeq2d 2250	. . . . . . . . . . . . 13 ⊢ (𝑔 = ℎ → (𝑦 = (𝑊 Σgz (𝐹 ∘ 𝑔)) ↔ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ))))
46	42, 45	anbi12d 477	. . . . . . . . . . . 12 ⊢ (𝑔 = ℎ → ((𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ 𝑔))) ↔ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))))
47	46	cbvexv 1974	. . . . . . . . . . 11 ⊢ (∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ 𝑔))) ↔ ∃ℎ(ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ))))
48	1	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → 𝑊 ∈ CMnd)
49	48	cmnmndd 14088	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → 𝑊 ∈ Mnd)
50	49	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → 𝑊 ∈ Mnd)
51		simprl 535	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → 𝑝 ∈ 𝐵)
52		simprr 537	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → 𝑞 ∈ 𝐵)
53		gsumvalfi.b	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐵 = (Base‘𝑊)
54		eqid 2238	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (+g‘𝑊) = (+g‘𝑊)
55	53, 54	mndcl 13713	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑊 ∈ Mnd ∧ 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵) → (𝑝(+g‘𝑊)𝑞) ∈ 𝐵)
56	50, 51, 52, 55	syl3anc 1278	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (𝑝(+g‘𝑊)𝑞) ∈ 𝐵)
57	48	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → 𝑊 ∈ CMnd)
58	53, 54	cmncom 14082	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑊 ∈ CMnd ∧ 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵) → (𝑝(+g‘𝑊)𝑞) = (𝑞(+g‘𝑊)𝑝))
59	57, 51, 52, 58	syl3anc 1278	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (𝑝(+g‘𝑊)𝑞) = (𝑞(+g‘𝑊)𝑝))
60	49	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → 𝑊 ∈ Mnd)
61	53, 54	mndass 13714	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑊 ∈ Mnd ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → ((𝑝(+g‘𝑊)𝑞)(+g‘𝑊)𝑟) = (𝑝(+g‘𝑊)(𝑞(+g‘𝑊)𝑟)))
62	60, 61	sylancom 424	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → ((𝑝(+g‘𝑊)𝑞)(+g‘𝑊)𝑟) = (𝑝(+g‘𝑊)(𝑞(+g‘𝑊)𝑟)))
63		elnnuz 9938	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((♯‘dom 𝐹) ∈ ℕ ↔ (♯‘dom 𝐹) ∈ (ℤ≥‘1))
64	63	biimpi 120	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((♯‘dom 𝐹) ∈ ℕ → (♯‘dom 𝐹) ∈ (ℤ≥‘1))
65	64	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (♯‘dom 𝐹) ∈ (ℤ≥‘1))
66		ssidd 3269	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → 𝐵 ⊆ 𝐵)
67	1	ad3antrrr 496	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → 𝑊 ∈ CMnd)
68		plusgslid 13443	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (+g = Slot (+g‘ndx) ∧ (+g‘ndx) ∈ ℕ)
69	68	slotex 13357	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑊 ∈ CMnd → (+g‘𝑊) ∈ V)
70	67, 69	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (+g‘𝑊) ∈ V)
71		simprl 535	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → 𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹)
72	20	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → dom 𝐹 = 𝐴)
73	72	f1oeq3d 5631	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ↔ 𝑔:(1...(♯‘dom 𝐹))–1-1-onto→𝐴))
74	71, 73	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → 𝑔:(1...(♯‘dom 𝐹))–1-1-onto→𝐴)
75	74	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → 𝑔:(1...(♯‘dom 𝐹))–1-1-onto→𝐴)
76		f1ocnv 5647	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→𝐴 → ◡𝑔:𝐴–1-1-onto→(1...(♯‘dom 𝐹)))
77	75, 76	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → ◡𝑔:𝐴–1-1-onto→(1...(♯‘dom 𝐹)))
78		simplrl 541	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹)
79	72	f1oeq3d 5631	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ↔ ℎ:(1...(♯‘dom 𝐹))–1-1-onto→𝐴))
80	78, 79	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → ℎ:(1...(♯‘dom 𝐹))–1-1-onto→𝐴)
81	80	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → ℎ:(1...(♯‘dom 𝐹))–1-1-onto→𝐴)
82		f1oco 5657	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((◡𝑔:𝐴–1-1-onto→(1...(♯‘dom 𝐹)) ∧ ℎ:(1...(♯‘dom 𝐹))–1-1-onto→𝐴) → (◡𝑔 ∘ ℎ):(1...(♯‘dom 𝐹))–1-1-onto→(1...(♯‘dom 𝐹)))
83	77, 81, 82	syl2anc 415	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (◡𝑔 ∘ ℎ):(1...(♯‘dom 𝐹))–1-1-onto→(1...(♯‘dom 𝐹)))
84	2	ad4antr 498	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑝 ∈ (1...(♯‘dom 𝐹))) → 𝐹:𝐴⟶𝐵)
85		f1of 5634	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 → 𝑔:(1...(♯‘dom 𝐹))⟶dom 𝐹)
86	71, 85	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → 𝑔:(1...(♯‘dom 𝐹))⟶dom 𝐹)
87	72	feq3d 5517	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → (𝑔:(1...(♯‘dom 𝐹))⟶dom 𝐹 ↔ 𝑔:(1...(♯‘dom 𝐹))⟶𝐴))
88	86, 87	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → 𝑔:(1...(♯‘dom 𝐹))⟶𝐴)
89	88	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑝 ∈ (1...(♯‘dom 𝐹))) → 𝑔:(1...(♯‘dom 𝐹))⟶𝐴)
90	84, 89	fcod 5548	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑝 ∈ (1...(♯‘dom 𝐹))) → (𝐹 ∘ 𝑔):(1...(♯‘dom 𝐹))⟶𝐵)
91		simpr 110	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑝 ∈ (1...(♯‘dom 𝐹))) → 𝑝 ∈ (1...(♯‘dom 𝐹)))
92	90, 91	ffvelcdmd 5835	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑝 ∈ (1...(♯‘dom 𝐹))) → ((𝐹 ∘ 𝑔)‘𝑝) ∈ 𝐵)
93		f1of 5634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 → ℎ:(1...(♯‘dom 𝐹))⟶dom 𝐹)
94	78, 93	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → ℎ:(1...(♯‘dom 𝐹))⟶dom 𝐹)
95	72	feq3d 5517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → (ℎ:(1...(♯‘dom 𝐹))⟶dom 𝐹 ↔ ℎ:(1...(♯‘dom 𝐹))⟶𝐴))
96	94, 95	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → ℎ:(1...(♯‘dom 𝐹))⟶𝐴)
97	96	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → ℎ:(1...(♯‘dom 𝐹))⟶𝐴)
98		fvco3 5770	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ:(1...(♯‘dom 𝐹))⟶𝐴 ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → ((◡𝑔 ∘ ℎ)‘𝑠) = (◡𝑔‘(ℎ‘𝑠)))
99	97, 98	sylancom 424	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → ((◡𝑔 ∘ ℎ)‘𝑠) = (◡𝑔‘(ℎ‘𝑠)))
100	99	fveq2d 5694	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → (𝑔‘((◡𝑔 ∘ ℎ)‘𝑠)) = (𝑔‘(◡𝑔‘(ℎ‘𝑠))))
101	75	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → 𝑔:(1...(♯‘dom 𝐹))–1-1-onto→𝐴)
102		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → 𝑠 ∈ (1...(♯‘dom 𝐹)))
103	97, 102	ffvelcdmd 5835	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → (ℎ‘𝑠) ∈ 𝐴)
104		f1ocnvfv2 5974	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑔:(1...(♯‘dom 𝐹))–1-1-onto→𝐴 ∧ (ℎ‘𝑠) ∈ 𝐴) → (𝑔‘(◡𝑔‘(ℎ‘𝑠))) = (ℎ‘𝑠))
105	101, 103, 104	syl2anc 415	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → (𝑔‘(◡𝑔‘(ℎ‘𝑠))) = (ℎ‘𝑠))
106	100, 105	eqtrd 2271	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → (𝑔‘((◡𝑔 ∘ ℎ)‘𝑠)) = (ℎ‘𝑠))
107	106	fveq2d 5694	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → (𝐹‘(𝑔‘((◡𝑔 ∘ ℎ)‘𝑠))) = (𝐹‘(ℎ‘𝑠)))
108	88	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → 𝑔:(1...(♯‘dom 𝐹))⟶𝐴)
109		f1ocnv 5647	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 → ◡𝑔:dom 𝐹–1-1-onto→(1...(♯‘dom 𝐹)))
110		f1of 5634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (◡𝑔:dom 𝐹–1-1-onto→(1...(♯‘dom 𝐹)) → ◡𝑔:dom 𝐹⟶(1...(♯‘dom 𝐹)))
111	71, 109, 110	3syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → ◡𝑔:dom 𝐹⟶(1...(♯‘dom 𝐹)))
112	72	feq2d 5516	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → (◡𝑔:dom 𝐹⟶(1...(♯‘dom 𝐹)) ↔ ◡𝑔:𝐴⟶(1...(♯‘dom 𝐹))))
113	111, 112	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → ◡𝑔:𝐴⟶(1...(♯‘dom 𝐹)))
114	113	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → ◡𝑔:𝐴⟶(1...(♯‘dom 𝐹)))
115	114, 103	ffvelcdmd 5835	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → (◡𝑔‘(ℎ‘𝑠)) ∈ (1...(♯‘dom 𝐹)))
116	99, 115	eqeltrd 2315	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → ((◡𝑔 ∘ ℎ)‘𝑠) ∈ (1...(♯‘dom 𝐹)))
117		fvco3 5770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔:(1...(♯‘dom 𝐹))⟶𝐴 ∧ ((◡𝑔 ∘ ℎ)‘𝑠) ∈ (1...(♯‘dom 𝐹))) → ((𝐹 ∘ 𝑔)‘((◡𝑔 ∘ ℎ)‘𝑠)) = (𝐹‘(𝑔‘((◡𝑔 ∘ ℎ)‘𝑠))))
118	108, 116, 117	syl2anc 415	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → ((𝐹 ∘ 𝑔)‘((◡𝑔 ∘ ℎ)‘𝑠)) = (𝐹‘(𝑔‘((◡𝑔 ∘ ℎ)‘𝑠))))
119		fvco3 5770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ℎ:(1...(♯‘dom 𝐹))⟶𝐴 ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → ((𝐹 ∘ ℎ)‘𝑠) = (𝐹‘(ℎ‘𝑠)))
120	97, 119	sylancom 424	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → ((𝐹 ∘ ℎ)‘𝑠) = (𝐹‘(ℎ‘𝑠)))
121	107, 118, 120	3eqtr4rd 2282	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → ((𝐹 ∘ ℎ)‘𝑠) = ((𝐹 ∘ 𝑔)‘((◡𝑔 ∘ ℎ)‘𝑠)))
122	4	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → 𝐹 ∈ V)
123		vex 2824	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑔 ∈ V
124		coexg 5327	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹 ∈ V ∧ 𝑔 ∈ V) → (𝐹 ∘ 𝑔) ∈ V)
125	122, 123, 124	sylancl 417	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → (𝐹 ∘ 𝑔) ∈ V)
126	125	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (𝐹 ∘ 𝑔) ∈ V)
127		vex 2824	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℎ ∈ V
128		coexg 5327	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹 ∈ V ∧ ℎ ∈ V) → (𝐹 ∘ ℎ) ∈ V)
129	122, 127, 128	sylancl 417	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → (𝐹 ∘ ℎ) ∈ V)
130	129	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (𝐹 ∘ ℎ) ∈ V)
131	56, 59, 62, 65, 66, 70, 83, 92, 121, 126, 130	seqf1og 10936	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (seq1((+g‘𝑊), (𝐹 ∘ ℎ))‘(♯‘dom 𝐹)) = (seq1((+g‘𝑊), (𝐹 ∘ 𝑔))‘(♯‘dom 𝐹)))
132	2	ad3antrrr 496	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → 𝐹:𝐴⟶𝐵)
133	96	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → ℎ:(1...(♯‘dom 𝐹))⟶𝐴)
134	132, 133	fcod 5548	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (𝐹 ∘ ℎ):(1...(♯‘dom 𝐹))⟶𝐵)
135	53, 54, 67, 65, 134	gzsumval2 13691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (𝑊 Σgz (𝐹 ∘ ℎ)) = (seq1((+g‘𝑊), (𝐹 ∘ ℎ))‘(♯‘dom 𝐹)))
136		simplrl 541	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → 𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹)
137	136, 85	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → 𝑔:(1...(♯‘dom 𝐹))⟶dom 𝐹)
138	132	fdmd 5535	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → dom 𝐹 = 𝐴)
139	138	feq3d 5517	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (𝑔:(1...(♯‘dom 𝐹))⟶dom 𝐹 ↔ 𝑔:(1...(♯‘dom 𝐹))⟶𝐴))
140	137, 139	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → 𝑔:(1...(♯‘dom 𝐹))⟶𝐴)
141	132, 140	fcod 5548	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (𝐹 ∘ 𝑔):(1...(♯‘dom 𝐹))⟶𝐵)
142	53, 54, 67, 65, 141	gzsumval2 13691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (𝑊 Σgz (𝐹 ∘ 𝑔)) = (seq1((+g‘𝑊), (𝐹 ∘ 𝑔))‘(♯‘dom 𝐹)))
143	131, 135, 142	3eqtr4d 2281	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (𝑊 Σgz (𝐹 ∘ ℎ)) = (𝑊 Σgz (𝐹 ∘ 𝑔)))
144		simprr 537	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) → 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))
145	144	ad2antrr 492	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))
146		simplrr 542	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))
147	143, 145, 146	3eqtr4rd 2282	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → 𝑥 = 𝑦)
148		simprl 535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) → ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹)
149	148	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹)
150	149, 93	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → ℎ:(1...(♯‘dom 𝐹))⟶dom 𝐹)
151		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (♯‘dom 𝐹) = 0)
152		fihasheq0 11210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (dom 𝐹 ∈ Fin → ((♯‘dom 𝐹) = 0 ↔ dom 𝐹 = ∅))
153	21, 152	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ((♯‘dom 𝐹) = 0 ↔ dom 𝐹 = ∅))
154	153	ad3antrrr 496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → ((♯‘dom 𝐹) = 0 ↔ dom 𝐹 = ∅))
155	151, 154	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → dom 𝐹 = ∅)
156	155	feq3d 5517	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (ℎ:(1...(♯‘dom 𝐹))⟶dom 𝐹 ↔ ℎ:(1...(♯‘dom 𝐹))⟶∅))
157	150, 156	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → ℎ:(1...(♯‘dom 𝐹))⟶∅)
158		f00 5579	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ:(1...(♯‘dom 𝐹))⟶∅ ↔ (ℎ = ∅ ∧ (1...(♯‘dom 𝐹)) = ∅))
159	157, 158	sylib 122	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (ℎ = ∅ ∧ (1...(♯‘dom 𝐹)) = ∅))
160	159	simpld 112	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → ℎ = ∅)
161	160	coeq2d 4937	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝐹 ∘ ℎ) = (𝐹 ∘ ∅))
162		co02 5296	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∘ ∅) = ∅
163	161, 162	eqtrdi 2287	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝐹 ∘ ℎ) = ∅)
164	163	oveq2d 6091	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝑊 Σgz (𝐹 ∘ ℎ)) = (𝑊 Σgz ∅))
165		eqid 2238	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0g‘𝑊) = (0g‘𝑊)
166	165	gzsum0 13690	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑊 ∈ CMnd → (𝑊 Σgz ∅) = (0g‘𝑊))
167	1, 166	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑊 Σgz ∅) = (0g‘𝑊))
168	167	ad3antrrr 496	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝑊 Σgz ∅) = (0g‘𝑊))
169	164, 168	eqtrd 2271	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝑊 Σgz (𝐹 ∘ ℎ)) = (0g‘𝑊))
170	144	ad2antrr 492	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))
171		simplrr 542	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))
172		simplrl 541	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹)
173	172, 85	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑔:(1...(♯‘dom 𝐹))⟶dom 𝐹)
174	155	feq3d 5517	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝑔:(1...(♯‘dom 𝐹))⟶dom 𝐹 ↔ 𝑔:(1...(♯‘dom 𝐹))⟶∅))
175	173, 174	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑔:(1...(♯‘dom 𝐹))⟶∅)
176		f00 5579	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑔:(1...(♯‘dom 𝐹))⟶∅ ↔ (𝑔 = ∅ ∧ (1...(♯‘dom 𝐹)) = ∅))
177	175, 176	sylib 122	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝑔 = ∅ ∧ (1...(♯‘dom 𝐹)) = ∅))
178	177	simpld 112	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑔 = ∅)
179	178	coeq2d 4937	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝐹 ∘ 𝑔) = (𝐹 ∘ ∅))
180	179, 162	eqtrdi 2287	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝐹 ∘ 𝑔) = ∅)
181	180	oveq2d 6091	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝑊 Σgz (𝐹 ∘ 𝑔)) = (𝑊 Σgz ∅))
182	171, 181, 168	3eqtrd 2275	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑥 = (0g‘𝑊))
183	169, 170, 182	3eqtr4rd 2282	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑥 = 𝑦)
184	23, 12	eqeltrd 2315	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (♯‘dom 𝐹) ∈ ℕ0)
185		elnn0 9544	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘dom 𝐹) ∈ ℕ0 ↔ ((♯‘dom 𝐹) ∈ ℕ ∨ (♯‘dom 𝐹) = 0))
186	184, 185	sylib 122	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((♯‘dom 𝐹) ∈ ℕ ∨ (♯‘dom 𝐹) = 0))
187	186	ad2antrr 492	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → ((♯‘dom 𝐹) ∈ ℕ ∨ (♯‘dom 𝐹) = 0))
188	147, 183, 187	mpjaodan 810	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → 𝑥 = 𝑦)
189	188	ex 115	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) → ((𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))) → 𝑥 = 𝑦))
190	189	exlimdv 1872	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ)))) → (∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))) → 𝑥 = 𝑦))
191	190	ex 115	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ))) → (∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))) → 𝑥 = 𝑦)))
192	191	com23 78	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))) → ((ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ))) → 𝑥 = 𝑦)))
193	192	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ dom 𝐹 ∈ Fin) → (∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))) → ((ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ))) → 𝑥 = 𝑦)))
194	193	imp 124	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ dom 𝐹 ∈ Fin) ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → ((ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ))) → 𝑥 = 𝑦))
195	194	exlimdv 1872	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ dom 𝐹 ∈ Fin) ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → (∃ℎ(ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ ℎ))) → 𝑥 = 𝑦))
196	47, 195	biimtrid 152	. . . . . . . . . 10 ⊢ (((𝜑 ∧ dom 𝐹 ∈ Fin) ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → (∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ 𝑔))) → 𝑥 = 𝑦))
197	196	impr 379	. . . . . . . . 9 ⊢ (((𝜑 ∧ dom 𝐹 ∈ Fin) ∧ (∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))) ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ 𝑔))))) → 𝑥 = 𝑦)
198	197	anasss 403	. . . . . . . 8 ⊢ ((𝜑 ∧ (dom 𝐹 ∈ Fin ∧ (∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))) ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ 𝑔)))))) → 𝑥 = 𝑦)
199	41, 198	sylan2br 288	. . . . . . 7 ⊢ ((𝜑 ∧ ((dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ 𝑔)))))) → 𝑥 = 𝑦)
200	199	ex 115	. . . . . 6 ⊢ (𝜑 → (((dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ 𝑔))))) → 𝑥 = 𝑦))
201	200	alrimivv 1928	. . . . 5 ⊢ (𝜑 → ∀𝑥∀𝑦(((dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ 𝑔))))) → 𝑥 = 𝑦))
202		eqeq1 2245	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)) ↔ 𝑦 = (𝑊 Σgz (𝐹 ∘ 𝑔))))
203	202	anbi2d 468	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))) ↔ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ 𝑔)))))
204	203	exbidv 1878	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))) ↔ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ 𝑔)))))
205	204	anbi2d 468	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ↔ (dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ 𝑔))))))
206	205	eu4 2149	. . . . 5 ⊢ (∃!𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ↔ (∃𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ ∀𝑥∀𝑦(((dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ∧ (dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σgz (𝐹 ∘ 𝑔))))) → 𝑥 = 𝑦)))
207	40, 201, 206	sylanbrc 421	. . . 4 ⊢ (𝜑 → ∃!𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))))
208		euiotaex 5349	. . . 4 ⊢ (∃!𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))) → (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))))) ∈ V)
209	207, 208	syl 14	. . 3 ⊢ (𝜑 → (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))))) ∈ V)
210		oveq1 6082	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (𝑤 Σgz (𝑓 ∘ 𝑔)) = (𝑊 Σgz (𝑓 ∘ 𝑔)))
211	210	eqeq2d 2250	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (𝑥 = (𝑤 Σgz (𝑓 ∘ 𝑔)) ↔ 𝑥 = (𝑊 Σgz (𝑓 ∘ 𝑔))))
212	211	anbi2d 468	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ((𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σgz (𝑓 ∘ 𝑔))) ↔ (𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑊 Σgz (𝑓 ∘ 𝑔)))))
213	212	exbidv 1878	. . . . . 6 ⊢ (𝑤 = 𝑊 → (∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σgz (𝑓 ∘ 𝑔))) ↔ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑊 Σgz (𝑓 ∘ 𝑔)))))
214	213	anbi2d 468	. . . . 5 ⊢ (𝑤 = 𝑊 → ((dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σgz (𝑓 ∘ 𝑔)))) ↔ (dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑊 Σgz (𝑓 ∘ 𝑔))))))
215	214	iotabidv 5355	. . . 4 ⊢ (𝑤 = 𝑊 → (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σgz (𝑓 ∘ 𝑔))))) = (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑊 Σgz (𝑓 ∘ 𝑔))))))
216		dmeq 4976	. . . . . . 7 ⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
217	216	eleq1d 2307	. . . . . 6 ⊢ (𝑓 = 𝐹 → (dom 𝑓 ∈ Fin ↔ dom 𝐹 ∈ Fin))
218		eqidd 2239	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → 𝑔 = 𝑔)
219	216	fveq2d 5694	. . . . . . . . . 10 ⊢ (𝑓 = 𝐹 → (♯‘dom 𝑓) = (♯‘dom 𝐹))
220	219	oveq2d 6091	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → (1...(♯‘dom 𝑓)) = (1...(♯‘dom 𝐹)))
221	218, 220, 216	f1oeq123d 5628	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → (𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ↔ 𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹))
222		coeq1 4932	. . . . . . . . . 10 ⊢ (𝑓 = 𝐹 → (𝑓 ∘ 𝑔) = (𝐹 ∘ 𝑔))
223	222	oveq2d 6091	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → (𝑊 Σgz (𝑓 ∘ 𝑔)) = (𝑊 Σgz (𝐹 ∘ 𝑔)))
224	223	eqeq2d 2250	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → (𝑥 = (𝑊 Σgz (𝑓 ∘ 𝑔)) ↔ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))))
225	221, 224	anbi12d 477	. . . . . . 7 ⊢ (𝑓 = 𝐹 → ((𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑊 Σgz (𝑓 ∘ 𝑔))) ↔ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))))
226	225	exbidv 1878	. . . . . 6 ⊢ (𝑓 = 𝐹 → (∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑊 Σgz (𝑓 ∘ 𝑔))) ↔ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔)))))
227	217, 226	anbi12d 477	. . . . 5 ⊢ (𝑓 = 𝐹 → ((dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑊 Σgz (𝑓 ∘ 𝑔)))) ↔ (dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))))))
228	227	iotabidv 5355	. . . 4 ⊢ (𝑓 = 𝐹 → (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑊 Σgz (𝑓 ∘ 𝑔))))) = (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))))))
229		df-gsumfi 14128	. . . 4 ⊢ Σg = (𝑤 ∈ CMnd, 𝑓 ∈ V ↦ (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σgz (𝑓 ∘ 𝑔))))))
230	215, 228, 229	ovmpog 6213	. . 3 ⊢ ((𝑊 ∈ CMnd ∧ 𝐹 ∈ V ∧ (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))))) ∈ V) → (𝑊 Σg 𝐹) = (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))))))
231	1, 4, 209, 230	syl3anc 1278	. 2 ⊢ (𝜑 → (𝑊 Σg 𝐹) = (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))))))
232	39	iota2 5362	. . . 4 ⊢ (((𝑊 Σgz (𝐹 ∘ 𝐺)) ∈ V ∧ ∃!𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))))) → ((dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σgz (𝐹 ∘ 𝐺)) = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ↔ (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))))) = (𝑊 Σgz (𝐹 ∘ 𝐺))))
233	19, 207, 232	syl2anc 415	. . 3 ⊢ (𝜑 → ((dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σgz (𝐹 ∘ 𝐺)) = (𝑊 Σgz (𝐹 ∘ 𝑔)))) ↔ (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))))) = (𝑊 Σgz (𝐹 ∘ 𝐺))))
234	35, 233	mpbid 147	. 2 ⊢ (𝜑 → (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σgz (𝐹 ∘ 𝑔))))) = (𝑊 Σgz (𝐹 ∘ 𝐺)))
235	231, 234	eqtrd 2271	1 ⊢ (𝜑 → (𝑊 Σg 𝐹) = (𝑊 Σgz (𝐹 ∘ 𝐺)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 720   ∧ w3a 1009  ∀wal 1400   = wceq 1402  ∃wex 1545  ∃!weu 2086   ∈ wcel 2209  Vcvv 2821  ∅c0 3520   × cxp 4767  ^◡ccnv 4768  dom cdm 4769   ∘ ccom 4773  ℩cio 5330   Fn wfn 5367  ⟶wf 5368  –1-1-onto→wf1o 5371  ‘cfv 5372  (class class class)co 6075  Fincfn 7012  0cc0 8169  1c1 8170  ℕcn 9283  ℕ₀cn0 9542  ℤ_≥cuz 9900  ...cfz 10390  seqcseq 10862  ♯chash 11192  Basecbs 13330  +_gcplusg 13408  0_gc0g 13587   Σ_gz cgzsu 13588  Mndcmnd 13706  CMndccmn 14064   Σ_g cgsu 14127

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 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4241  ax-sep 4244  ax-nul 4254  ax-pow 4306  ax-pr 4341  ax-un 4573  ax-setind 4679  ax-iinf 4730  ax-cnex 8260  ax-resscn 8261  ax-1cn 8262  ax-1re 8263  ax-icn 8264  ax-addcl 8265  ax-addrcl 8266  ax-mulcl 8267  ax-mulrcl 8268  ax-addcom 8269  ax-mulcom 8270  ax-addass 8271  ax-mulass 8272  ax-distr 8273  ax-i2m1 8274  ax-0lt1 8275  ax-1rid 8276  ax-0id 8277  ax-rnegex 8278  ax-precex 8279  ax-cnre 8280  ax-pre-ltirr 8281  ax-pre-ltwlin 8282  ax-pre-lttrn 8283  ax-pre-apti 8284  ax-pre-ltadd 8285  ax-pre-mulgt0 8286

This theorem depends on definitions:  df-bi 117  df-stab 843  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-if 3636  df-pw 3687  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-int 3966  df-iun 4009  df-br 4126  df-opab 4188  df-mpt 4189  df-tr 4225  df-id 4433  df-iord 4506  df-on 4508  df-ilim 4509  df-suc 4511  df-iom 4733  df-xp 4775  df-rel 4776  df-cnv 4777  df-co 4778  df-dm 4779  df-rn 4780  df-res 4781  df-ima 4782  df-iota 5332  df-fun 5374  df-fn 5375  df-f 5376  df-f1 5377  df-fo 5378  df-f1o 5379  df-fv 5380  df-riota 6028  df-ov 6078  df-oprab 6079  df-mpo 6080  df-1st 6364  df-2nd 6365  df-recs 6566  df-frec 6652  df-1o 6677  df-er 6797  df-en 7013  df-dom 7014  df-fin 7015  df-pnf 8352  df-mnf 8353  df-xr 8354  df-ltxr 8355  df-le 8356  df-sub 8489  df-neg 8490  df-reap 8893  df-ap 8900  df-inn 9284  df-2 9342  df-n0 9543  df-z 9624  df-uz 9901  df-fz 10391  df-fzo 10528  df-seqfrec 10863  df-ihash 11193  df-ndx 13333  df-slot 13334  df-base 13336  df-plusg 13421  df-0g 13589  df-gzsum 13590  df-mgm 13653  df-sgrp 13694  df-mnd 13707  df-cmn 14066  df-gsumfi 14128

This theorem is referenced by:  gzsumgsum1  14130  gzsumgsum  14132  gsumsncmn  14133  gsump1  14134  gsumf1ofi  14137  gsummhmfi  14141  gsumressfi  14144