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 16630

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 5879	. . 3 ⊢ (𝜑 → 𝐹 ∈ V)
5		fngsum 13464	. . . . . . . 8 ⊢ Σ_g Fn (V × V)
6	5	a1i 9	. . . . . . 7 ⊢ (𝜑 → Σ_g Fn (V × V))
7	1	elexd 2814	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ V)
8		gfsumval.g	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴)
9		f1of 5580	. . . . . . . . . 10 ⊢ (𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝐺:(1...(♯‘𝐴))⟶𝐴)
10	8, 9	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:(1...(♯‘𝐴))⟶𝐴)
11		1zzd 9499	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℤ)
12		hashcl 11036	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ₀)
13	3, 12	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐴) ∈ ℕ₀)
14	13	nn0zd 9593	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝐴) ∈ ℤ)
15	11, 14	fzfigd 10686	. . . . . . . . 9 ⊢ (𝜑 → (1...(♯‘𝐴)) ∈ Fin)
16	10, 15	fexd 5879	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ V)
17		coexg 5279	. . . . . . . 8 ⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹 ∘ 𝐺) ∈ V)
18	4, 16, 17	syl2anc 411	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∘ 𝐺) ∈ V)
19		fnovex 6046	. . . . . . 7 ⊢ (( Σ_g Fn (V × V) ∧ 𝑊 ∈ V ∧ (𝐹 ∘ 𝐺) ∈ V) → (𝑊 Σ_g (𝐹 ∘ 𝐺)) ∈ V)
20	6, 7, 18, 19	syl3anc 1271	. . . . . 6 ⊢ (𝜑 → (𝑊 Σ_g (𝐹 ∘ 𝐺)) ∈ V)
21	2	fdmd 5486	. . . . . . . 8 ⊢ (𝜑 → dom 𝐹 = 𝐴)
22	21, 3	eqeltrd 2306	. . . . . . 7 ⊢ (𝜑 → dom 𝐹 ∈ Fin)
23		eqidd 2230	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 = 𝐺)
24	21	fveq2d 5639	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘dom 𝐹) = (♯‘𝐴))
25	24	oveq2d 6029	. . . . . . . . . . 11 ⊢ (𝜑 → (1...(♯‘dom 𝐹)) = (1...(♯‘𝐴)))
26	23, 25, 21	f1oeq123d 5574	. . . . . . . . . 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 2230	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 Σ_g (𝐹 ∘ 𝐺)) = (𝑊 Σ_g (𝐹 ∘ 𝐺)))
29	27, 28	jca 306	. . . . . . . 8 ⊢ (𝜑 → (𝐺:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ (𝑊 Σ_g (𝐹 ∘ 𝐺)) = (𝑊 Σ_g (𝐹 ∘ 𝐺))))
30		f1oeq1 5568	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ↔ 𝐺:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹))
31		coeq2 4886	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → (𝐹 ∘ 𝑔) = (𝐹 ∘ 𝐺))
32	31	oveq2d 6029	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (𝑊 Σ_g (𝐹 ∘ 𝑔)) = (𝑊 Σ_g (𝐹 ∘ 𝐺)))
33	32	eqeq2d 2241	. . . . . . . . 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 2949	. . . . . . 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 2236	. . . . . . . . 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 1871	. . . . . . 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 2949	. . . . 5 ⊢ (𝜑 → ∃𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))))
42		anandi 592	. . . . . . . 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 5568	. . . . . . . . . . . . 13 ⊢ (𝑔 = ℎ → (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ↔ ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹))
44		coeq2 4886	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = ℎ → (𝐹 ∘ 𝑔) = (𝐹 ∘ ℎ))
45	44	oveq2d 6029	. . . . . . . . . . . . . 14 ⊢ (𝑔 = ℎ → (𝑊 Σ_g (𝐹 ∘ 𝑔)) = (𝑊 Σ_g (𝐹 ∘ ℎ)))
46	45	eqeq2d 2241	. . . . . . . . . . . . 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 1965	. . . . . . . . . . 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 13888	. . . . . . . . . . . . . . . . . . . . . . . 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 529	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → 𝑝 ∈ 𝐵)
53		simprr 531	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → 𝑞 ∈ 𝐵)
54		gfsumval.b	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐵 = (Base‘𝑊)
55		eqid 2229	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (+_g‘𝑊) = (+_g‘𝑊)
56	54, 55	mndcl 13499	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑊 ∈ Mnd ∧ 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵) → (𝑝(+_g‘𝑊)𝑞) ∈ 𝐵)
57	51, 52, 53, 56	syl3anc 1271	. . . . . . . . . . . . . . . . . . . . . 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 13882	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑊 ∈ CMnd ∧ 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵) → (𝑝(+_g‘𝑊)𝑞) = (𝑞(+_g‘𝑊)𝑝))
60	58, 52, 53, 59	syl3anc 1271	. . . . . . . . . . . . . . . . . . . . . 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 13500	. . . . . . . . . . . . . . . . . . . . . . 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 9786	. . . . . . . . . . . . . . . . . . . . . . . 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 3246	. . . . . . . . . . . . . . . . . . . . . 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 13188	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (+_g = Slot (+_g‘ndx) ∧ (+_g‘ndx) ∈ ℕ)
70	69	slotex 13102	. . . . . . . . . . . . . . . . . . . . . . 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 529	. . . . . . . . . . . . . . . . . . . . . . . . . 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 5577	. . . . . . . . . . . . . . . . . . . . . . . . . 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 5593	. . . . . . . . . . . . . . . . . . . . . . . 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 535	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) → ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹)
80	73	f1oeq3d 5577	. . . . . . . . . . . . . . . . . . . . . . . . 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 5603	. . . . . . . . . . . . . . . . . . . . . . 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 5580	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5468	. . . . . . . . . . . . . . . . . . . . . . . . . 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 5497	. . . . . . . . . . . . . . . . . . . . . . . 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 5779	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑝 ∈ (1...(♯‘dom 𝐹))) → ((𝐹 ∘ 𝑔)‘𝑝) ∈ 𝐵)
95		f1of 5580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5713	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5639	. . . . . . . . . . . . . . . . . . . . . . . . 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 5779	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → (ℎ‘𝑠) ∈ 𝐴)
106		f1ocnvfv2 5914	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2262	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → (𝑔‘((^◡𝑔 ∘ ℎ)‘𝑠)) = (ℎ‘𝑠))
109	108	fveq2d 5639	. . . . . . . . . . . . . . . . . . . . . . 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 5593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 → ^◡𝑔:dom 𝐹–1-1-onto→(1...(♯‘dom 𝐹)))
112		f1of 5580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5779	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → (^◡𝑔‘(ℎ‘𝑠)) ∈ (1...(♯‘dom 𝐹)))
118	101, 117	eqeltrd 2306	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) ∧ 𝑠 ∈ (1...(♯‘dom 𝐹))) → ((^◡𝑔 ∘ ℎ)‘𝑠) ∈ (1...(♯‘dom 𝐹)))
119		fvco3 5713	. . . . . . . . . . . . . . . . . . . . . . . 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 5713	. . . . . . . . . . . . . . . . . . . . . . . 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 2273	. . . . . . . . . . . . . . . . . . . . . 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 2803	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑔 ∈ V
126		coexg 5279	. . . . . . . . . . . . . . . . . . . . . . . 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 2803	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℎ ∈ V
130		coexg 5279	. . . . . . . . . . . . . . . . . . . . . . . 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 10776	. . . . . . . . . . . . . . . . . . . . 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 5497	. . . . . . . . . . . . . . . . . . . . . . 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 13473	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (𝑊 Σ_g (𝐹 ∘ ℎ)) = (seq1((+_g‘𝑊), (𝐹 ∘ ℎ))‘(♯‘dom 𝐹)))
139		simplrl 535	. . . . . . . . . . . . . . . . . . . . . . . . 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 5486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → dom 𝐹 = 𝐴)
142	141	feq3d 5468	. . . . . . . . . . . . . . . . . . . . . . . 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 13473	. . . . . . . . . . . . . . . . . . . . 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 2272	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → (𝑊 Σ_g (𝐹 ∘ ℎ)) = (𝑊 Σ_g (𝐹 ∘ 𝑔)))
147		simprr 531	. . . . . . . . . . . . . . . . . . . . 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 536	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))
150	146, 148, 149	3eqtr4rd 2273	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) ∈ ℕ) → 𝑥 = 𝑦)
151		simprl 529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5468	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5525	. . . . . . . . . . . . . . . . . . . . . . . . . 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 4890	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝐹 ∘ ℎ) = (𝐹 ∘ ∅))
165		co02 5248	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∘ ∅) = ∅
166	164, 165	eqtrdi 2278	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝐹 ∘ ℎ) = ∅)
167	166	oveq2d 6029	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝑊 Σ_g (𝐹 ∘ ℎ)) = (𝑊 Σ_g ∅))
168		eqid 2229	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0_g‘𝑊) = (0_g‘𝑊)
169	168	gsum0g 13472	. . . . . . . . . . . . . . . . . . . . . . 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 2262	. . . . . . . . . . . . . . . . . . . 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 536	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))
175		simplrl 535	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5468	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5525	. . . . . . . . . . . . . . . . . . . . . . . . . 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 4890	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝐹 ∘ 𝑔) = (𝐹 ∘ ∅))
183	182, 165	eqtrdi 2278	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝐹 ∘ 𝑔) = ∅)
184	183	oveq2d 6029	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → (𝑊 Σ_g (𝐹 ∘ 𝑔)) = (𝑊 Σ_g ∅))
185	174, 184, 171	3eqtrd 2266	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑥 = (0_g‘𝑊))
186	172, 173, 185	3eqtr4rd 2273	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (ℎ:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ ℎ)))) ∧ (𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (♯‘dom 𝐹) = 0) → 𝑥 = 𝑦)
187	24, 13	eqeltrd 2306	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (♯‘dom 𝐹) ∈ ℕ₀)
188		elnn0 9397	. . . . . . . . . . . . . . . . . . . . 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 803	. . . . . . . . . . . . . . . . . 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 1865	. . . . . . . . . . . . . . . 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 1865	. . . . . . . . . . 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 1921	. . . . 5 ⊢ (𝜑 → ∀𝑥∀𝑦(((dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔)))) ∧ (dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑦 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))) → 𝑥 = 𝑦))
205		eqeq1 2236	. . . . . . . . 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 1871	. . . . . . 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 2140	. . . . 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 5301	. . . 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 6020	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (𝑤 Σ_g (𝑓 ∘ 𝑔)) = (𝑊 Σ_g (𝑓 ∘ 𝑔)))
214	213	eqeq2d 2241	. . . . . . . 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 1871	. . . . . 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 5307	. . . 4 ⊢ (𝑤 = 𝑊 → (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σ_g (𝑓 ∘ 𝑔))))) = (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑊 Σ_g (𝑓 ∘ 𝑔))))))
219		dmeq 4929	. . . . . . 7 ⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
220	219	eleq1d 2298	. . . . . 6 ⊢ (𝑓 = 𝐹 → (dom 𝑓 ∈ Fin ↔ dom 𝐹 ∈ Fin))
221		eqidd 2230	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → 𝑔 = 𝑔)
222	219	fveq2d 5639	. . . . . . . . . 10 ⊢ (𝑓 = 𝐹 → (♯‘dom 𝑓) = (♯‘dom 𝐹))
223	222	oveq2d 6029	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → (1...(♯‘dom 𝑓)) = (1...(♯‘dom 𝐹)))
224	221, 223, 219	f1oeq123d 5574	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → (𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ↔ 𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹))
225		coeq1 4885	. . . . . . . . . 10 ⊢ (𝑓 = 𝐹 → (𝑓 ∘ 𝑔) = (𝐹 ∘ 𝑔))
226	225	oveq2d 6029	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → (𝑊 Σ_g (𝑓 ∘ 𝑔)) = (𝑊 Σ_g (𝐹 ∘ 𝑔)))
227	226	eqeq2d 2241	. . . . . . . 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 1871	. . . . . 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 5307	. . . 4 ⊢ (𝑓 = 𝐹 → (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑊 Σ_g (𝑓 ∘ 𝑔))))) = (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))))
232		df-gfsum 16629	. . . 4 ⊢ Σ_gf = (𝑤 ∈ CMnd, 𝑓 ∈ V ↦ (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σ_g (𝑓 ∘ 𝑔))))))
233	218, 231, 232	ovmpog 6151	. . 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 1271	. 2 ⊢ (𝜑 → (𝑊 Σ_gf 𝐹) = (℩𝑥(dom 𝐹 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝐹))–1-1-onto→dom 𝐹 ∧ 𝑥 = (𝑊 Σ_g (𝐹 ∘ 𝑔))))))
235	40	iota2 5314	. . . 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 2262	1 ⊢ (𝜑 → (𝑊 Σ_gf 𝐹) = (𝑊 Σ_g (𝐹 ∘ 𝐺)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 713 ∧ w3a 1002 ∀wal 1393 = wceq 1395 ∃wex 1538 ∃!weu 2077 ∈ wcel 2200 Vcvv 2800 ∅c0 3492 × cxp 4721 ^◡ccnv 4722 dom cdm 4723 ∘ ccom 4727 ℩cio 5282 Fn wfn 5319 ⟶wf 5320 –1-1-onto→wf1o 5323 ‘cfv 5324 (class class class)co 6013 Fincfn 6904 0cc0 8025 1c1 8026 ℕcn 9136 ℕ₀cn0 9395 ℤ_≥cuz 9748 ...cfz 10236 seqcseq 10702 ♯chash 11030 Basecbs 13075 +_gcplusg 13153 0_gc0g 13332 Σ_g cgsu 13333 Mndcmnd 13492 CMndccmn 13864 Σ_gf cgfsu 16628

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4202 ax-sep 4205 ax-nul 4213 ax-pow 4262 ax-pr 4297 ax-un 4528 ax-setind 4633 ax-iinf 4684 ax-cnex 8116 ax-resscn 8117 ax-1cn 8118 ax-1re 8119 ax-icn 8120 ax-addcl 8121 ax-addrcl 8122 ax-mulcl 8123 ax-mulrcl 8124 ax-addcom 8125 ax-mulcom 8126 ax-addass 8127 ax-mulass 8128 ax-distr 8129 ax-i2m1 8130 ax-0lt1 8131 ax-1rid 8132 ax-0id 8133 ax-rnegex 8134 ax-precex 8135 ax-cnre 8136 ax-pre-ltirr 8137 ax-pre-ltwlin 8138 ax-pre-lttrn 8139 ax-pre-apti 8140 ax-pre-ltadd 8141 ax-pre-mulgt0 8142

This theorem depends on definitions: df-bi 117 df-stab 836 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rab 2517 df-v 2802 df-sbc 3030 df-csb 3126 df-dif 3200 df-un 3202 df-in 3204 df-ss 3211 df-nul 3493 df-if 3604 df-pw 3652 df-sn 3673 df-pr 3674 df-op 3676 df-uni 3892 df-int 3927 df-iun 3970 df-br 4087 df-opab 4149 df-mpt 4150 df-tr 4186 df-id 4388 df-iord 4461 df-on 4463 df-ilim 4464 df-suc 4466 df-iom 4687 df-xp 4729 df-rel 4730 df-cnv 4731 df-co 4732 df-dm 4733 df-rn 4734 df-res 4735 df-ima 4736 df-iota 5284 df-fun 5326 df-fn 5327 df-f 5328 df-f1 5329 df-fo 5330 df-f1o 5331 df-fv 5332 df-riota 5966 df-ov 6016 df-oprab 6017 df-mpo 6018 df-1st 6298 df-2nd 6299 df-recs 6466 df-frec 6552 df-1o 6577 df-er 6697 df-en 6905 df-dom 6906 df-fin 6907 df-pnf 8209 df-mnf 8210 df-xr 8211 df-ltxr 8212 df-le 8213 df-sub 8345 df-neg 8346 df-reap 8748 df-ap 8755 df-inn 9137 df-2 9195 df-n0 9396 df-z 9473 df-uz 9749 df-fz 10237 df-fzo 10371 df-seqfrec 10703 df-ihash 11031 df-ndx 13078 df-slot 13079 df-base 13081 df-plusg 13166 df-0g 13334 df-igsum 13335 df-mgm 13432 df-sgrp 13478 df-mnd 13493 df-cmn 13866 df-gfsum 16629

This theorem is referenced by: gsumgfsum1 16631 gsumgfsum 16634

W3C validator