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

Theorem gsumval3eu 18351
 Description: The group sum as defined in gsumval3a 18350 is uniquely defined. (Contributed by Mario Carneiro, 8-Dec-2014.)
Hypotheses
Ref Expression
gsumval3.b 𝐵 = (Base‘𝐺)
gsumval3.0 0 = (0g𝐺)
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.
StepHypRef Expression
1 gsumval3a.n . . . . . 6 (𝜑𝑊 ≠ ∅)
21neneqd 2828 . . . . 5 (𝜑 → ¬ 𝑊 = ∅)
3 gsumval3a.t . . . . . . 7 (𝜑𝑊 ∈ Fin)
4 fz1f1o 14485 . . . . . . 7 (𝑊 ∈ Fin → (𝑊 = ∅ ∨ ((#‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)))
53, 4syl 17 . . . . . 6 (𝜑 → (𝑊 = ∅ ∨ ((#‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)))
65ord 391 . . . . 5 (𝜑 → (¬ 𝑊 = ∅ → ((#‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)))
72, 6mpd 15 . . . 4 (𝜑 → ((#‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto𝑊))
87simprd 478 . . 3 (𝜑 → ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)
9 excom 2082 . . . 4 (∃𝑥𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))) ↔ ∃𝑓𝑥(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))))
10 exancom 1827 . . . . . 6 (∃𝑥(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))) ↔ ∃𝑥(𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)) ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊))
11 fvex 6239 . . . . . . 7 (seq1( + , (𝐹𝑓))‘(#‘𝑊)) ∈ V
12 biidd 252 . . . . . . 7 (𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)) → (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑓:(1...(#‘𝑊))–1-1-onto𝑊))
1311, 12ceqsexv 3273 . . . . . 6 (∃𝑥(𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)) ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊) ↔ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)
1410, 13bitri 264 . . . . 5 (∃𝑥(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))) ↔ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)
1514exbii 1814 . . . 4 (∃𝑓𝑥(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))) ↔ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)
169, 15bitri 264 . . 3 (∃𝑥𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))) ↔ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)
178, 16sylibr 224 . 2 (𝜑 → ∃𝑥𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))))
18 eeanv 2218 . . . 4 (∃𝑓𝑔((𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))) ∧ (𝑔:(1...(#‘𝑊))–1-1-onto𝑊𝑦 = (seq1( + , (𝐹𝑔))‘(#‘𝑊)))) ↔ (∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))) ∧ ∃𝑔(𝑔:(1...(#‘𝑊))–1-1-onto𝑊𝑦 = (seq1( + , (𝐹𝑔))‘(#‘𝑊)))))
19 an4 882 . . . . . 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)
2120adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝐺 ∈ Mnd)
22 gsumval3.b . . . . . . . . . . . 12 𝐵 = (Base‘𝐺)
23 gsumval3.p . . . . . . . . . . . 12 + = (+g𝐺)
2422, 23mndcl 17348 . . . . . . . . . . 11 ((𝐺 ∈ Mnd ∧ 𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
25243expb 1285 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
2621, 25sylan 487 . . . . . . . . 9 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
27 gsumval3.c . . . . . . . . . . . . 13 (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
2827adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
2928sselda 3636 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ ran 𝐹) → 𝑥 ∈ (𝑍‘ran 𝐹))
3029adantrr 753 . . . . . . . . . 10 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ (𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐹)) → 𝑥 ∈ (𝑍‘ran 𝐹))
31 simprr 811 . . . . . . . . . 10 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ (𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐹)) → 𝑦 ∈ ran 𝐹)
32 gsumval3.z . . . . . . . . . . 11 𝑍 = (Cntz‘𝐺)
3323, 32cntzi 17808 . . . . . . . . . 10 ((𝑥 ∈ (𝑍‘ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
3430, 31, 33syl2anc 694 . . . . . . . . 9 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ (𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐹)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
3522, 23mndass 17349 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
3621, 35sylan 487 . . . . . . . . 9 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
377simpld 474 . . . . . . . . . . 11 (𝜑 → (#‘𝑊) ∈ ℕ)
3837adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) → (#‘𝑊) ∈ ℕ)
39 nnuz 11761 . . . . . . . . . 10 ℕ = (ℤ‘1)
4038, 39syl6eleq 2740 . . . . . . . . 9 ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) → (#‘𝑊) ∈ (ℤ‘1))
41 gsumval3.f . . . . . . . . . . 11 (𝜑𝐹:𝐴𝐵)
4241adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝐹:𝐴𝐵)
43 frn 6091 . . . . . . . . . 10 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
4442, 43syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) → ran 𝐹𝐵)
45 simprr 811 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝑔:(1...(#‘𝑊))–1-1-onto𝑊)
46 f1ocnv 6187 . . . . . . . . . . 11 (𝑔:(1...(#‘𝑊))–1-1-onto𝑊𝑔:𝑊1-1-onto→(1...(#‘𝑊)))
4745, 46syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝑔:𝑊1-1-onto→(1...(#‘𝑊)))
48 simprl 809 . . . . . . . . . 10 ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)
49 f1oco 6197 . . . . . . . . . 10 ((𝑔:𝑊1-1-onto→(1...(#‘𝑊)) ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊) → (𝑔𝑓):(1...(#‘𝑊))–1-1-onto→(1...(#‘𝑊)))
5047, 48, 49syl2anc 694 . . . . . . . . 9 ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝑔𝑓):(1...(#‘𝑊))–1-1-onto→(1...(#‘𝑊)))
51 f1of 6175 . . . . . . . . . . . 12 (𝑔:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))⟶𝑊)
5245, 51syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝑔:(1...(#‘𝑊))⟶𝑊)
53 fvco3 6314 . . . . . . . . . . 11 ((𝑔:(1...(#‘𝑊))⟶𝑊𝑥 ∈ (1...(#‘𝑊))) → ((𝐹𝑔)‘𝑥) = (𝐹‘(𝑔𝑥)))
5452, 53sylan 487 . . . . . . . . . 10 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (1...(#‘𝑊))) → ((𝐹𝑔)‘𝑥) = (𝐹‘(𝑔𝑥)))
55 ffn 6083 . . . . . . . . . . . . 13 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
5642, 55syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝐹 Fn 𝐴)
5756adantr 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (1...(#‘𝑊))) → 𝐹 Fn 𝐴)
58 gsumval3a.s . . . . . . . . . . . . . 14 (𝜑𝑊𝐴)
5958adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝑊𝐴)
6052, 59fssd 6095 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝑔:(1...(#‘𝑊))⟶𝐴)
6160ffvelrnda 6399 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (1...(#‘𝑊))) → (𝑔𝑥) ∈ 𝐴)
62 fnfvelrn 6396 . . . . . . . . . . 11 ((𝐹 Fn 𝐴 ∧ (𝑔𝑥) ∈ 𝐴) → (𝐹‘(𝑔𝑥)) ∈ ran 𝐹)
6357, 61, 62syl2anc 694 . . . . . . . . . 10 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (1...(#‘𝑊))) → (𝐹‘(𝑔𝑥)) ∈ ran 𝐹)
6454, 63eqeltrd 2730 . . . . . . . . 9 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (1...(#‘𝑊))) → ((𝐹𝑔)‘𝑥) ∈ ran 𝐹)
65 f1of 6175 . . . . . . . . . . . . . . 15 (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑓:(1...(#‘𝑊))⟶𝑊)
6648, 65syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝑓:(1...(#‘𝑊))⟶𝑊)
67 fvco3 6314 . . . . . . . . . . . . . 14 ((𝑓:(1...(#‘𝑊))⟶𝑊𝑘 ∈ (1...(#‘𝑊))) → ((𝑔𝑓)‘𝑘) = (𝑔‘(𝑓𝑘)))
6866, 67sylan 487 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝑔𝑓)‘𝑘) = (𝑔‘(𝑓𝑘)))
6968fveq2d 6233 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (𝑔‘((𝑔𝑓)‘𝑘)) = (𝑔‘(𝑔‘(𝑓𝑘))))
7045adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → 𝑔:(1...(#‘𝑊))–1-1-onto𝑊)
7166ffvelrnda 6399 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (𝑓𝑘) ∈ 𝑊)
72 f1ocnvfv2 6573 . . . . . . . . . . . . 13 ((𝑔:(1...(#‘𝑊))–1-1-onto𝑊 ∧ (𝑓𝑘) ∈ 𝑊) → (𝑔‘(𝑔‘(𝑓𝑘))) = (𝑓𝑘))
7370, 71, 72syl2anc 694 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (𝑔‘(𝑔‘(𝑓𝑘))) = (𝑓𝑘))
7469, 73eqtr2d 2686 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (𝑓𝑘) = (𝑔‘((𝑔𝑓)‘𝑘)))
7574fveq2d 6233 . . . . . . . . . 10 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (𝐹‘(𝑓𝑘)) = (𝐹‘(𝑔‘((𝑔𝑓)‘𝑘))))
76 fvco3 6314 . . . . . . . . . . 11 ((𝑓:(1...(#‘𝑊))⟶𝑊𝑘 ∈ (1...(#‘𝑊))) → ((𝐹𝑓)‘𝑘) = (𝐹‘(𝑓𝑘)))
7766, 76sylan 487 . . . . . . . . . 10 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐹𝑓)‘𝑘) = (𝐹‘(𝑓𝑘)))
78 f1of 6175 . . . . . . . . . . . . 13 ((𝑔𝑓):(1...(#‘𝑊))–1-1-onto→(1...(#‘𝑊)) → (𝑔𝑓):(1...(#‘𝑊))⟶(1...(#‘𝑊)))
7950, 78syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝑔𝑓):(1...(#‘𝑊))⟶(1...(#‘𝑊)))
8079ffvelrnda 6399 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝑔𝑓)‘𝑘) ∈ (1...(#‘𝑊)))
81 fvco3 6314 . . . . . . . . . . . 12 ((𝑔:(1...(#‘𝑊))⟶𝐴 ∧ ((𝑔𝑓)‘𝑘) ∈ (1...(#‘𝑊))) → ((𝐹𝑔)‘((𝑔𝑓)‘𝑘)) = (𝐹‘(𝑔‘((𝑔𝑓)‘𝑘))))
8260, 81sylan 487 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ ((𝑔𝑓)‘𝑘) ∈ (1...(#‘𝑊))) → ((𝐹𝑔)‘((𝑔𝑓)‘𝑘)) = (𝐹‘(𝑔‘((𝑔𝑓)‘𝑘))))
8380, 82syldan 486 . . . . . . . . . 10 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐹𝑔)‘((𝑔𝑓)‘𝑘)) = (𝐹‘(𝑔‘((𝑔𝑓)‘𝑘))))
8475, 77, 833eqtr4d 2695 . . . . . . . . 9 (((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐹𝑓)‘𝑘) = ((𝐹𝑔)‘((𝑔𝑓)‘𝑘)))
8526, 34, 36, 40, 44, 50, 64, 84seqf1o 12882 . . . . . . . 8 ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) → (seq1( + , (𝐹𝑓))‘(#‘𝑊)) = (seq1( + , (𝐹𝑔))‘(#‘𝑊)))
86 eqeq12 2664 . . . . . . . 8 ((𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)) ∧ 𝑦 = (seq1( + , (𝐹𝑔))‘(#‘𝑊))) → (𝑥 = 𝑦 ↔ (seq1( + , (𝐹𝑓))‘(#‘𝑊)) = (seq1( + , (𝐹𝑔))‘(#‘𝑊))))
8785, 86syl5ibrcom 237 . . . . . . 7 ((𝜑 ∧ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊)) → ((𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)) ∧ 𝑦 = (seq1( + , (𝐹𝑔))‘(#‘𝑊))) → 𝑥 = 𝑦))
8887expimpd 628 . . . . . 6 (𝜑 → (((𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊) ∧ (𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)) ∧ 𝑦 = (seq1( + , (𝐹𝑔))‘(#‘𝑊)))) → 𝑥 = 𝑦))
8919, 88syl5bir 233 . . . . 5 (𝜑 → (((𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))) ∧ (𝑔:(1...(#‘𝑊))–1-1-onto𝑊𝑦 = (seq1( + , (𝐹𝑔))‘(#‘𝑊)))) → 𝑥 = 𝑦))
9089exlimdvv 1902 . . . 4 (𝜑 → (∃𝑓𝑔((𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))) ∧ (𝑔:(1...(#‘𝑊))–1-1-onto𝑊𝑦 = (seq1( + , (𝐹𝑔))‘(#‘𝑊)))) → 𝑥 = 𝑦))
9118, 90syl5bir 233 . . 3 (𝜑 → ((∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))) ∧ ∃𝑔(𝑔:(1...(#‘𝑊))–1-1-onto𝑊𝑦 = (seq1( + , (𝐹𝑔))‘(#‘𝑊)))) → 𝑥 = 𝑦))
9291alrimivv 1896 . 2 (𝜑 → ∀𝑥𝑦((∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))) ∧ ∃𝑔(𝑔:(1...(#‘𝑊))–1-1-onto𝑊𝑦 = (seq1( + , (𝐹𝑔))‘(#‘𝑊)))) → 𝑥 = 𝑦))
93 eqeq1 2655 . . . . . 6 (𝑥 = 𝑦 → (𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)) ↔ 𝑦 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))))
9493anbi2d 740 . . . . 5 (𝑥 = 𝑦 → ((𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))) ↔ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑦 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))))
9594exbidv 1890 . . . 4 (𝑥 = 𝑦 → (∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))) ↔ ∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑦 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))))
96 f1oeq1 6165 . . . . . 6 (𝑓 = 𝑔 → (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑔:(1...(#‘𝑊))–1-1-onto𝑊))
97 coeq2 5313 . . . . . . . . 9 (𝑓 = 𝑔 → (𝐹𝑓) = (𝐹𝑔))
9897seqeq3d 12849 . . . . . . . 8 (𝑓 = 𝑔 → seq1( + , (𝐹𝑓)) = seq1( + , (𝐹𝑔)))
9998fveq1d 6231 . . . . . . 7 (𝑓 = 𝑔 → (seq1( + , (𝐹𝑓))‘(#‘𝑊)) = (seq1( + , (𝐹𝑔))‘(#‘𝑊)))
10099eqeq2d 2661 . . . . . 6 (𝑓 = 𝑔 → (𝑦 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)) ↔ 𝑦 = (seq1( + , (𝐹𝑔))‘(#‘𝑊))))
10196, 100anbi12d 747 . . . . 5 (𝑓 = 𝑔 → ((𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑦 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))) ↔ (𝑔:(1...(#‘𝑊))–1-1-onto𝑊𝑦 = (seq1( + , (𝐹𝑔))‘(#‘𝑊)))))
102101cbvexv 2311 . . . 4 (∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑦 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))) ↔ ∃𝑔(𝑔:(1...(#‘𝑊))–1-1-onto𝑊𝑦 = (seq1( + , (𝐹𝑔))‘(#‘𝑊))))
10395, 102syl6bb 276 . . 3 (𝑥 = 𝑦 → (∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))) ↔ ∃𝑔(𝑔:(1...(#‘𝑊))–1-1-onto𝑊𝑦 = (seq1( + , (𝐹𝑔))‘(#‘𝑊)))))
104103eu4 2547 . 2 (∃!𝑥𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))) ↔ (∃𝑥𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))) ∧ ∀𝑥𝑦((∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))) ∧ ∃𝑔(𝑔:(1...(#‘𝑊))–1-1-onto𝑊𝑦 = (seq1( + , (𝐹𝑔))‘(#‘𝑊)))) → 𝑥 = 𝑦)))
10517, 92, 104sylanbrc 699 1 (𝜑 → ∃!𝑥𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 382   ∧ wa 383   ∧ w3a 1054  ∀wal 1521   = wceq 1523  ∃wex 1744   ∈ wcel 2030  ∃!weu 2498   ≠ wne 2823   ⊆ wss 3607  ∅c0 3948  ◡ccnv 5142  ran crn 5144   ∘ ccom 5147   Fn wfn 5921  ⟶wf 5922  –1-1-onto→wf1o 5925  ‘cfv 5926  (class class class)co 6690  Fincfn 7997  1c1 9975  ℕcn 11058  ℤ≥cuz 11725  ...cfz 12364  seqcseq 12841  #chash 13157  Basecbs 15904  +gcplusg 15988  0gc0g 16147  Mndcmnd 17341  Cntzccntz 17794 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-fzo 12505  df-seq 12842  df-hash 13158  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-cntz 17796 This theorem is referenced by:  gsumval3lem2  18353
 Copyright terms: Public domain W3C validator