Theorem summolem3 15755

Description: Lemma for summo 15758. (Contributed by Mario Carneiro, 29-Mar-2014.)

Hypotheses

Ref	Expression
summo.1	⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))
summo.2	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
summo.3	⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)
summolem3.4	⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ⦋(𝐾‘𝑛) / 𝑘⦌𝐵)
summolem3.5	⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ))
summolem3.6	⊢ (𝜑 → 𝑓:(1...𝑀)–1-1-onto→𝐴)
summolem3.7	⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴)

Assertion

Ref	Expression
summolem3	⊢ (𝜑 → (seq1( + , 𝐺)‘𝑀) = (seq1( + , 𝐻)‘𝑁))

Distinct variable groups:   𝑓,𝑘,𝑛,𝐴   𝑓,𝐹,𝑘,𝑛   𝑘,𝐺,𝑛   𝑘,𝐾,𝑛   𝑘,𝑁,𝑛   𝜑,𝑘,𝑛   𝐵,𝑓,𝑛   𝑘,𝑀,𝑛

Allowed substitution hints:   𝜑(𝑓)   𝐵(𝑘)   𝐺(𝑓)   𝐻(𝑓,𝑘,𝑛)   𝐾(𝑓)   𝑀(𝑓)   𝑁(𝑓)

Proof of Theorem summolem3

Dummy variables 𝑖 𝑗 𝑚 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		addcl 11170	. . . 4 ⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑚 + 𝑗) ∈ ℂ)
2	1	adantl 486	. . 3 ⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ)) → (𝑚 + 𝑗) ∈ ℂ)
3		addcom 11384	. . . 4 ⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑚 + 𝑗) = (𝑗 + 𝑚))
4	3	adantl 486	. . 3 ⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ)) → (𝑚 + 𝑗) = (𝑗 + 𝑚))
5		addass 11175	. . . 4 ⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑚 + 𝑗) + 𝑦) = (𝑚 + (𝑗 + 𝑦)))
6	5	adantl 486	. . 3 ⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → ((𝑚 + 𝑗) + 𝑦) = (𝑚 + (𝑗 + 𝑦)))
7		summolem3.5	. . . . 5 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ))
8	7	simpld 499	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℕ)
9		nnuz 12892	. . . 4 ⊢ ℕ = (ℤ≥‘1)
10	8, 9	eleqtrdi 2875	. . 3 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘1))
11		ssidd 3962	. . 3 ⊢ (𝜑 → ℂ ⊆ ℂ)
12		summolem3.6	. . . . . 6 ⊢ (𝜑 → 𝑓:(1...𝑀)–1-1-onto→𝐴)
13		f1ocnv 6823	. . . . . 6 ⊢ (𝑓:(1...𝑀)–1-1-onto→𝐴 → ◡𝑓:𝐴–1-1-onto→(1...𝑀))
14	12, 13	syl 18	. . . . 5 ⊢ (𝜑 → ◡𝑓:𝐴–1-1-onto→(1...𝑀))
15		summolem3.7	. . . . 5 ⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴)
16		f1oco 6834	. . . . 5 ⊢ ((◡𝑓:𝐴–1-1-onto→(1...𝑀) ∧ 𝐾:(1...𝑁)–1-1-onto→𝐴) → (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀))
17	14, 15, 16	syl2anc 595	. . . 4 ⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀))
18		ovex 7433	. . . . . . . . . 10 ⊢ (1...𝑁) ∈ V
19	18	f1oen 8957	. . . . . . . . 9 ⊢ ((◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀) → (1...𝑁) ≈ (1...𝑀))
20	17, 19	syl 18	. . . . . . . 8 ⊢ (𝜑 → (1...𝑁) ≈ (1...𝑀))
21		fzfi 13999	. . . . . . . . 9 ⊢ (1...𝑁) ∈ Fin
22		fzfi 13999	. . . . . . . . 9 ⊢ (1...𝑀) ∈ Fin
23		hashen 14374	. . . . . . . . 9 ⊢ (((1...𝑁) ∈ Fin ∧ (1...𝑀) ∈ Fin) → ((♯‘(1...𝑁)) = (♯‘(1...𝑀)) ↔ (1...𝑁) ≈ (1...𝑀)))
24	21, 22, 23	mp2an 704	. . . . . . . 8 ⊢ ((♯‘(1...𝑁)) = (♯‘(1...𝑀)) ↔ (1...𝑁) ≈ (1...𝑀))
25	20, 24	sylibr 237	. . . . . . 7 ⊢ (𝜑 → (♯‘(1...𝑁)) = (♯‘(1...𝑀)))
26	7	simprd 500	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ)
27		nnnn0 12502	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
28		hashfz1 14373	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁)
29	26, 27, 28	3syl 19	. . . . . . 7 ⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁)
30		nnnn0 12502	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ0)
31		hashfz1 14373	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ0 → (♯‘(1...𝑀)) = 𝑀)
32	8, 30, 31	3syl 19	. . . . . . 7 ⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀)
33	25, 29, 32	3eqtr3rd 2809	. . . . . 6 ⊢ (𝜑 → 𝑀 = 𝑁)
34	33	oveq2d 7416	. . . . 5 ⊢ (𝜑 → (1...𝑀) = (1...𝑁))
35	34	f1oeq2d 6806	. . . 4 ⊢ (𝜑 → ((◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀) ↔ (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀)))
36	17, 35	mpbird 260	. . 3 ⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀))
37		summo.3	. . . . 5 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)
38		fveq2 6871	. . . . . 6 ⊢ (𝑛 = 𝑚 → (𝑓‘𝑛) = (𝑓‘𝑚))
39	38	csbeq1d 3859	. . . . 5 ⊢ (𝑛 = 𝑚 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵)
40		elfznn 13572	. . . . . 6 ⊢ (𝑚 ∈ (1...𝑀) → 𝑚 ∈ ℕ)
41	40	adantl 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → 𝑚 ∈ ℕ)
42		f1of 6810	. . . . . . . 8 ⊢ (𝑓:(1...𝑀)–1-1-onto→𝐴 → 𝑓:(1...𝑀)⟶𝐴)
43	12, 42	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑓:(1...𝑀)⟶𝐴)
44	43	ffvelcdmda 7069	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → (𝑓‘𝑚) ∈ 𝐴)
45		summo.2	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
46	45	ralrimiva 3157	. . . . . . 7 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
47	46	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
48		nfcsb1v 3879	. . . . . . . 8 ⊢ Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵
49	48	nfel1 2943	. . . . . . 7 ⊢ Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ
50		csbeq1a 3869	. . . . . . . 8 ⊢ (𝑘 = (𝑓‘𝑚) → 𝐵 = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵)
51	50	eleq1d 2850	. . . . . . 7 ⊢ (𝑘 = (𝑓‘𝑚) → (𝐵 ∈ ℂ ↔ ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ))
52	49, 51	rspc 3572	. . . . . 6 ⊢ ((𝑓‘𝑚) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ))
53	44, 47, 52	sylc 66	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)
54	37, 39, 41, 53	fvmptd3 7003	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → (𝐺‘𝑚) = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵)
55	54, 53	eqeltrd 2865	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → (𝐺‘𝑚) ∈ ℂ)
56	34	f1oeq2d 6806	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐾:(1...𝑁)–1-1-onto→𝐴))
57	15, 56	mpbird 260	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾:(1...𝑀)–1-1-onto→𝐴)
58		f1of 6810	. . . . . . . . . 10 ⊢ (𝐾:(1...𝑀)–1-1-onto→𝐴 → 𝐾:(1...𝑀)⟶𝐴)
59	57, 58	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐾:(1...𝑀)⟶𝐴)
60		fvco3 6971	. . . . . . . . 9 ⊢ ((𝐾:(1...𝑀)⟶𝐴 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) = (◡𝑓‘(𝐾‘𝑖)))
61	59, 60	sylan 591	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) = (◡𝑓‘(𝐾‘𝑖)))
62	61	fveq2d 6875	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) = (𝑓‘(◡𝑓‘(𝐾‘𝑖))))
63	12	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑓:(1...𝑀)–1-1-onto→𝐴)
64	59	ffvelcdmda 7069	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐾‘𝑖) ∈ 𝐴)
65		f1ocnvfv2 7265	. . . . . . . 8 ⊢ ((𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (𝐾‘𝑖) ∈ 𝐴) → (𝑓‘(◡𝑓‘(𝐾‘𝑖))) = (𝐾‘𝑖))
66	63, 64, 65	syl2anc 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑓‘(◡𝑓‘(𝐾‘𝑖))) = (𝐾‘𝑖))
67	62, 66	eqtr2d 2801	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐾‘𝑖) = (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)))
68	67	csbeq1d 3859	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ⦋(𝐾‘𝑖) / 𝑘⦌𝐵 = ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵)
69	68	fveq2d 6875	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ( I ‘⦋(𝐾‘𝑖) / 𝑘⦌𝐵) = ( I ‘⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵))
70		elfznn 13572	. . . . . 6 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℕ)
71	70	adantl 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ ℕ)
72		fveq2 6871	. . . . . . 7 ⊢ (𝑛 = 𝑖 → (𝐾‘𝑛) = (𝐾‘𝑖))
73	72	csbeq1d 3859	. . . . . 6 ⊢ (𝑛 = 𝑖 → ⦋(𝐾‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑖) / 𝑘⦌𝐵)
74		summolem3.4	. . . . . 6 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ⦋(𝐾‘𝑛) / 𝑘⦌𝐵)
75	73, 74	fvmpti 6978	. . . . 5 ⊢ (𝑖 ∈ ℕ → (𝐻‘𝑖) = ( I ‘⦋(𝐾‘𝑖) / 𝑘⦌𝐵))
76	71, 75	syl 18	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘𝑖) = ( I ‘⦋(𝐾‘𝑖) / 𝑘⦌𝐵))
77		f1of 6810	. . . . . . 7 ⊢ ((◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀) → (◡𝑓 ∘ 𝐾):(1...𝑀)⟶(1...𝑀))
78	36, 77	syl 18	. . . . . 6 ⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑀)⟶(1...𝑀))
79	78	ffvelcdmda 7069	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) ∈ (1...𝑀))
80		elfznn 13572	. . . . 5 ⊢ (((◡𝑓 ∘ 𝐾)‘𝑖) ∈ (1...𝑀) → ((◡𝑓 ∘ 𝐾)‘𝑖) ∈ ℕ)
81		fveq2 6871	. . . . . . 7 ⊢ (𝑛 = ((◡𝑓 ∘ 𝐾)‘𝑖) → (𝑓‘𝑛) = (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)))
82	81	csbeq1d 3859	. . . . . 6 ⊢ (𝑛 = ((◡𝑓 ∘ 𝐾)‘𝑖) → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵)
83	82, 37	fvmpti 6978	. . . . 5 ⊢ (((◡𝑓 ∘ 𝐾)‘𝑖) ∈ ℕ → (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖)) = ( I ‘⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵))
84	79, 80, 83	3syl 19	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖)) = ( I ‘⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵))
85	69, 76, 84	3eqtr4d 2810	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘𝑖) = (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖)))
86	2, 4, 6, 10, 11, 36, 55, 85	seqf1o 14070	. 2 ⊢ (𝜑 → (seq1( + , 𝐻)‘𝑀) = (seq1( + , 𝐺)‘𝑀))
87	33	fveq2d 6875	. 2 ⊢ (𝜑 → (seq1( + , 𝐻)‘𝑀) = (seq1( + , 𝐻)‘𝑁))
88	86, 87	eqtr3d 2802	1 ⊢ (𝜑 → (seq1( + , 𝐺)‘𝑀) = (seq1( + , 𝐻)‘𝑁))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145  ∀wral 3079  ⦋csb 3855  ifcif 4483   class class class wbr 5105   ↦ cmpt 5186   I cid 5546  ^◡ccnv 5651   ∘ ccom 5656  ⟶wf 6521  –1-1-onto→wf1o 6524  ‘cfv 6525  (class class class)co 7400   ≈ cen 8928  Fincfn 8931  ℂcc 11086  0cc0 11088  1c1 11089   + caddc 11091  ℕcn 12224  ℕ₀cn0 12495  ℤcz 12582  ℤ_≥cuz 12853  ...cfz 13526  seqcseq 14028  ♯chash 14357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5232  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-cnex 11144  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164  ax-pre-mulgt0 11165

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-int 4909  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-om 7851  df-1st 7974  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-1o 8441  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-fin 8935  df-card 9913  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-sub 11431  df-neg 11432  df-nn 12225  df-n0 12496  df-z 12583  df-uz 12854  df-fz 13527  df-fzo 13674  df-seq 14029  df-hash 14358

This theorem is referenced by:  summolem2a  15756  summo  15758