gsumval3eu - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > gsumval3eu		Structured version Visualization version GIF version

Theorem gsumval3eu 18128

Description: The group sum as defined in gsumval3a 18127 is uniquely defined. (Contributed by Mario Carneiro, 8-Dec-2014.)

**Hypotheses**
Ref	Expression
gsumval3.b	⊢ 𝐵 = (Base‘𝐺)
gsumval3.0	⊢ 0 = (0_g‘𝐺)
gsumval3.p	⊢ + = (+_g‘𝐺)
gsumval3.z	⊢ 𝑍 = (Cntz‘𝐺)
gsumval3.g	⊢ (𝜑 → 𝐺 ∈ Mnd)
gsumval3.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
gsumval3.f	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
gsumval3.c	⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
gsumval3a.t	⊢ (𝜑 → 𝑊 ∈ Fin)
gsumval3a.n	⊢ (𝜑 → 𝑊 ≠ ∅)
gsumval3a.s	⊢ (𝜑 → 𝑊 ⊆ 𝐴)

**Assertion**
Ref	Expression
gsumval3eu	⊢ (𝜑 → ∃!𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))))

Distinct variable groups: 𝑥,𝑓, + 𝐴,𝑓,𝑥 𝜑,𝑓,𝑥 𝑥, 0 𝑓,𝐺,𝑥 𝑥,𝑉 𝐵,𝑓,𝑥 𝑓,𝐹,𝑥 𝑓,𝑊,𝑥 Allowed substitution hints: 𝑉(𝑓) 0 (𝑓) 𝑍(𝑥,𝑓)

Proof of Theorem gsumval3eu Dummy variables 𝑔 𝑘 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gsumval3a.n	. . . . . 6 ⊢ (𝜑 → 𝑊 ≠ ∅)
2	1	neneqd 2787	. . . . 5 ⊢ (𝜑 → ¬ 𝑊 = ∅)
3		gsumval3a.t	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ Fin)
4		fz1f1o 14288	. . . . . . 7 ⊢ (𝑊 ∈ Fin → (𝑊 = ∅ ∨ ((#‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)))
5	3, 4	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑊 = ∅ ∨ ((#‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)))
6	5	ord 391	. . . . 5 ⊢ (𝜑 → (¬ 𝑊 = ∅ → ((#‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)))
7	2, 6	mpd 15	. . . 4 ⊢ (𝜑 → ((#‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊))
8	7	simprd 478	. . 3 ⊢ (𝜑 → ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)
9		excom 2029	. . . 4 ⊢ (∃𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))) ↔ ∃𝑓∃𝑥(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))))
10		exancom 1774	. . . . . 6 ⊢ (∃𝑥(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))) ↔ ∃𝑥(𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)) ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊))
11		fvex 6113	. . . . . . 7 ⊢ (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)) ∈ V
12		biidd 251	. . . . . . 7 ⊢ (𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)) → (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ↔ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊))
13	11, 12	ceqsexv 3215	. . . . . 6 ⊢ (∃𝑥(𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)) ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊) ↔ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)
14	10, 13	bitri 263	. . . . 5 ⊢ (∃𝑥(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))) ↔ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)
15	14	exbii 1764	. . . 4 ⊢ (∃𝑓∃𝑥(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))) ↔ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)
16	9, 15	bitri 263	. . 3 ⊢ (∃𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))) ↔ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)
17	8, 16	sylibr 223	. 2 ⊢ (𝜑 → ∃𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))))
18		eeanv 2170	. . . 4 ⊢ (∃𝑓∃𝑔((𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))) ∧ (𝑔:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑦 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘𝑊)))) ↔ (∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))) ∧ ∃𝑔(𝑔:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑦 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘𝑊)))))
19		an4 861	. . . . . 6 ⊢ (((𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊) ∧ (𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)) ∧ 𝑦 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘𝑊)))) ↔ ((𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))) ∧ (𝑔:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑦 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘𝑊)))))
20		gsumval3.g	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ Mnd)
21	20	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝐺 ∈ Mnd)
22		gsumval3.b	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘𝐺)
23		gsumval3.p	. . . . . . . . . . . 12 ⊢ + = (+_g‘𝐺)
24	22, 23	mndcl 17124	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
25	24	3expb 1258	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
26	21, 25	sylan 487	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
27		gsumval3.c	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
28	27	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
29	28	sselda 3568	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ ran 𝐹) → 𝑥 ∈ (𝑍‘ran 𝐹))
30	29	adantrr 749	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) → 𝑥 ∈ (𝑍‘ran 𝐹))
31		simprr 792	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) → 𝑦 ∈ ran 𝐹)
32		gsumval3.z	. . . . . . . . . . 11 ⊢ 𝑍 = (Cntz‘𝐺)
33	23, 32	cntzi 17585	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (𝑍‘ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
34	30, 31, 33	syl2anc 691	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
35	22, 23	mndass 17125	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
36	21, 35	sylan 487	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
37	7	simpld 474	. . . . . . . . . . 11 ⊢ (𝜑 → (#‘𝑊) ∈ ℕ)
38	37	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) → (#‘𝑊) ∈ ℕ)
39		nnuz 11599	. . . . . . . . . 10 ⊢ ℕ = (ℤ_≥‘1)
40	38, 39	syl6eleq 2698	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) → (#‘𝑊) ∈ (ℤ_≥‘1))
41		gsumval3.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
42	41	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝐹:𝐴⟶𝐵)
43		frn 5966	. . . . . . . . . 10 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
44	42, 43	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) → ran 𝐹 ⊆ 𝐵)
45		simprr 792	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)
46		f1ocnv 6062	. . . . . . . . . . 11 ⊢ (𝑔:(1...(#‘𝑊))–1-1-onto→𝑊 → ^◡𝑔:𝑊–1-1-onto→(1...(#‘𝑊)))
47	45, 46	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) → ^◡𝑔:𝑊–1-1-onto→(1...(#‘𝑊)))
48		simprl 790	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)
49		f1oco 6072	. . . . . . . . . 10 ⊢ ((^◡𝑔:𝑊–1-1-onto→(1...(#‘𝑊)) ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊) → (^◡𝑔 ∘ 𝑓):(1...(#‘𝑊))–1-1-onto→(1...(#‘𝑊)))
50	47, 48, 49	syl2anc 691	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) → (^◡𝑔 ∘ 𝑓):(1...(#‘𝑊))–1-1-onto→(1...(#‘𝑊)))
51		f1of 6050	. . . . . . . . . . . 12 ⊢ (𝑔:(1...(#‘𝑊))–1-1-onto→𝑊 → 𝑔:(1...(#‘𝑊))⟶𝑊)
52	45, 51	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝑔:(1...(#‘𝑊))⟶𝑊)
53		fvco3 6185	. . . . . . . . . . 11 ⊢ ((𝑔:(1...(#‘𝑊))⟶𝑊 ∧ 𝑥 ∈ (1...(#‘𝑊))) → ((𝐹 ∘ 𝑔)‘𝑥) = (𝐹‘(𝑔‘𝑥)))
54	52, 53	sylan 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (1...(#‘𝑊))) → ((𝐹 ∘ 𝑔)‘𝑥) = (𝐹‘(𝑔‘𝑥)))
55		ffn 5958	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
56	42, 55	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝐹 Fn 𝐴)
57	56	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (1...(#‘𝑊))) → 𝐹 Fn 𝐴)
58		gsumval3a.s	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑊 ⊆ 𝐴)
59	58	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝑊 ⊆ 𝐴)
60	52, 59	fssd 5970	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝑔:(1...(#‘𝑊))⟶𝐴)
61	60	ffvelrnda 6267	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (1...(#‘𝑊))) → (𝑔‘𝑥) ∈ 𝐴)
62		fnfvelrn 6264	. . . . . . . . . . 11 ⊢ ((𝐹 Fn 𝐴 ∧ (𝑔‘𝑥) ∈ 𝐴) → (𝐹‘(𝑔‘𝑥)) ∈ ran 𝐹)
63	57, 61, 62	syl2anc 691	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (1...(#‘𝑊))) → (𝐹‘(𝑔‘𝑥)) ∈ ran 𝐹)
64	54, 63	eqeltrd 2688	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (1...(#‘𝑊))) → ((𝐹 ∘ 𝑔)‘𝑥) ∈ ran 𝐹)
65		f1of 6050	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 → 𝑓:(1...(#‘𝑊))⟶𝑊)
66	48, 65	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝑓:(1...(#‘𝑊))⟶𝑊)
67		fvco3 6185	. . . . . . . . . . . . . 14 ⊢ ((𝑓:(1...(#‘𝑊))⟶𝑊 ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((^◡𝑔 ∘ 𝑓)‘𝑘) = (^◡𝑔‘(𝑓‘𝑘)))
68	66, 67	sylan 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((^◡𝑔 ∘ 𝑓)‘𝑘) = (^◡𝑔‘(𝑓‘𝑘)))
69	68	fveq2d 6107	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (𝑔‘((^◡𝑔 ∘ 𝑓)‘𝑘)) = (𝑔‘(^◡𝑔‘(𝑓‘𝑘))))
70	45	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)
71	66	ffvelrnda 6267	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (𝑓‘𝑘) ∈ 𝑊)
72		f1ocnvfv2 6433	. . . . . . . . . . . . 13 ⊢ ((𝑔:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ (𝑓‘𝑘) ∈ 𝑊) → (𝑔‘(^◡𝑔‘(𝑓‘𝑘))) = (𝑓‘𝑘))
73	70, 71, 72	syl2anc 691	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (𝑔‘(^◡𝑔‘(𝑓‘𝑘))) = (𝑓‘𝑘))
74	69, 73	eqtr2d 2645	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (𝑓‘𝑘) = (𝑔‘((^◡𝑔 ∘ 𝑓)‘𝑘)))
75	74	fveq2d 6107	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (𝐹‘(𝑓‘𝑘)) = (𝐹‘(𝑔‘((^◡𝑔 ∘ 𝑓)‘𝑘))))
76		fvco3 6185	. . . . . . . . . . 11 ⊢ ((𝑓:(1...(#‘𝑊))⟶𝑊 ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐹 ∘ 𝑓)‘𝑘) = (𝐹‘(𝑓‘𝑘)))
77	66, 76	sylan 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐹 ∘ 𝑓)‘𝑘) = (𝐹‘(𝑓‘𝑘)))
78		f1of 6050	. . . . . . . . . . . . 13 ⊢ ((^◡𝑔 ∘ 𝑓):(1...(#‘𝑊))–1-1-onto→(1...(#‘𝑊)) → (^◡𝑔 ∘ 𝑓):(1...(#‘𝑊))⟶(1...(#‘𝑊)))
79	50, 78	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) → (^◡𝑔 ∘ 𝑓):(1...(#‘𝑊))⟶(1...(#‘𝑊)))
80	79	ffvelrnda 6267	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((^◡𝑔 ∘ 𝑓)‘𝑘) ∈ (1...(#‘𝑊)))
81		fvco3 6185	. . . . . . . . . . . 12 ⊢ ((𝑔:(1...(#‘𝑊))⟶𝐴 ∧ ((^◡𝑔 ∘ 𝑓)‘𝑘) ∈ (1...(#‘𝑊))) → ((𝐹 ∘ 𝑔)‘((^◡𝑔 ∘ 𝑓)‘𝑘)) = (𝐹‘(𝑔‘((^◡𝑔 ∘ 𝑓)‘𝑘))))
82	60, 81	sylan 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ ((^◡𝑔 ∘ 𝑓)‘𝑘) ∈ (1...(#‘𝑊))) → ((𝐹 ∘ 𝑔)‘((^◡𝑔 ∘ 𝑓)‘𝑘)) = (𝐹‘(𝑔‘((^◡𝑔 ∘ 𝑓)‘𝑘))))
83	80, 82	syldan 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐹 ∘ 𝑔)‘((^◡𝑔 ∘ 𝑓)‘𝑘)) = (𝐹‘(𝑔‘((^◡𝑔 ∘ 𝑓)‘𝑘))))
84	75, 77, 83	3eqtr4d 2654	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐹 ∘ 𝑓)‘𝑘) = ((𝐹 ∘ 𝑔)‘((^◡𝑔 ∘ 𝑓)‘𝑘)))
85	26, 34, 36, 40, 44, 50, 64, 84	seqf1o 12704	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) → (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘𝑊)))
86		eqeq12 2623	. . . . . . . 8 ⊢ ((𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)) ∧ 𝑦 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘𝑊))) → (𝑥 = 𝑦 ↔ (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘𝑊))))
87	85, 86	syl5ibrcom 236	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊)) → ((𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)) ∧ 𝑦 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘𝑊))) → 𝑥 = 𝑦))
88	87	expimpd 627	. . . . . 6 ⊢ (𝜑 → (((𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊) ∧ (𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)) ∧ 𝑦 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘𝑊)))) → 𝑥 = 𝑦))
89	19, 88	syl5bir 232	. . . . 5 ⊢ (𝜑 → (((𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))) ∧ (𝑔:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑦 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘𝑊)))) → 𝑥 = 𝑦))
90	89	exlimdvv 1849	. . . 4 ⊢ (𝜑 → (∃𝑓∃𝑔((𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))) ∧ (𝑔:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑦 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘𝑊)))) → 𝑥 = 𝑦))
91	18, 90	syl5bir 232	. . 3 ⊢ (𝜑 → ((∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))) ∧ ∃𝑔(𝑔:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑦 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘𝑊)))) → 𝑥 = 𝑦))
92	91	alrimivv 1843	. 2 ⊢ (𝜑 → ∀𝑥∀𝑦((∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))) ∧ ∃𝑔(𝑔:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑦 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘𝑊)))) → 𝑥 = 𝑦))
93		eqeq1 2614	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)) ↔ 𝑦 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))))
94	93	anbi2d 736	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))) ↔ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑦 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)))))
95	94	exbidv 1837	. . . 4 ⊢ (𝑥 = 𝑦 → (∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))) ↔ ∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑦 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)))))
96		f1oeq1 6040	. . . . . 6 ⊢ (𝑓 = 𝑔 → (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ↔ 𝑔:(1...(#‘𝑊))–1-1-onto→𝑊))
97		coeq2 5202	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝐹 ∘ 𝑓) = (𝐹 ∘ 𝑔))
98	97	seqeq3d 12671	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → seq1( + , (𝐹 ∘ 𝑓)) = seq1( + , (𝐹 ∘ 𝑔)))
99	98	fveq1d 6105	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘𝑊)))
100	99	eqeq2d 2620	. . . . . 6 ⊢ (𝑓 = 𝑔 → (𝑦 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)) ↔ 𝑦 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘𝑊))))
101	96, 100	anbi12d 743	. . . . 5 ⊢ (𝑓 = 𝑔 → ((𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑦 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))) ↔ (𝑔:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑦 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘𝑊)))))
102	101	cbvexv 2263	. . . 4 ⊢ (∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑦 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))) ↔ ∃𝑔(𝑔:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑦 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘𝑊))))
103	95, 102	syl6bb 275	. . 3 ⊢ (𝑥 = 𝑦 → (∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))) ↔ ∃𝑔(𝑔:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑦 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘𝑊)))))
104	103	eu4 2506	. 2 ⊢ (∃!𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))) ↔ (∃𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))) ∧ ∀𝑥∀𝑦((∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))) ∧ ∃𝑔(𝑔:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑦 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘𝑊)))) → 𝑥 = 𝑦)))
105	17, 92, 104	sylanbrc 695	1 ⊢ (𝜑 → ∃!𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∨ wo 382 ∧ wa 383 ∧ w3a 1031 ∀wal 1473 = wceq 1475 ∃wex 1695 ∈ wcel 1977 ∃!weu 2458 ≠ wne 2780 ⊆ wss 3540 ∅c0 3874 ^◡ccnv 5037 ran crn 5039 ∘ ccom 5042 Fn wfn 5799 ⟶wf 5800 –1-1-onto→wf1o 5803 ‘cfv 5804 (class class class)co 6549 Fincfn 7841 1c1 9816 ℕcn 10897 ℤ_≥cuz 11563 ...cfz 12197 seqcseq 12663 #chash 12979 Basecbs 15695 +_gcplusg 15768 0_gc0g 15923 Mndcmnd 17117 Cntzccntz 17571

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-card 8648 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-n0 11170 df-z 11255 df-uz 11564 df-fz 12198 df-fzo 12335 df-seq 12664 df-hash 12980 df-mgm 17065 df-sgrp 17107 df-mnd 17118 df-cntz 17573

This theorem is referenced by: gsumval3lem2 18130

W3C validator