Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvnprodlem1 Structured version   Visualization version   GIF version

Theorem dvnprodlem1 42111
Description: 𝐷 is bijective. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
dvnprodlem1.c 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
dvnprodlem1.j (𝜑𝐽 ∈ ℕ0)
dvnprodlem1.d 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
dvnprodlem1.t (𝜑𝑇 ∈ Fin)
dvnprodlem1.z (𝜑𝑍𝑇)
dvnprodlem1.zr (𝜑 → ¬ 𝑍𝑅)
dvnprodlem1.rzt (𝜑 → (𝑅 ∪ {𝑍}) ⊆ 𝑇)
Assertion
Ref Expression
dvnprodlem1 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
Distinct variable groups:   𝐶,𝑐,𝑘   𝐷,𝑐,𝑡   𝐽,𝑐,𝑘,𝑛,𝑡   𝑅,𝑐,𝑘,𝑛,𝑡   𝑅,𝑠,𝑐,𝑛,𝑡   𝑡,𝑇,𝑠   𝑍,𝑐,𝑘,𝑛,𝑡   𝑍,𝑠   𝜑,𝑐,𝑛,𝑡,𝑘   𝜑,𝑠
Allowed substitution hints:   𝐶(𝑡,𝑛,𝑠)   𝐷(𝑘,𝑛,𝑠)   𝑇(𝑘,𝑛,𝑐)   𝐽(𝑠)

Proof of Theorem dvnprodlem1
Dummy variables 𝑑 𝑒 𝑚 𝑝 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqidd 2822 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
2 0zd 11982 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ∈ ℤ)
3 dvnprodlem1.j . . . . . . . . . . . . . . 15 (𝜑𝐽 ∈ ℕ0)
43nn0zd 12074 . . . . . . . . . . . . . 14 (𝜑𝐽 ∈ ℤ)
54adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℤ)
6 fzssz 12899 . . . . . . . . . . . . . . . 16 (0...𝐽) ⊆ ℤ
76a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ ℤ)
8 dvnprodlem1.c . . . . . . . . . . . . . . . . . . . . . 22 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
9 oveq2 7153 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 = (𝑅 ∪ {𝑍}) → ((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m (𝑅 ∪ {𝑍})))
10 rabeq 3484 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
119, 10syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
12 sumeq1 15035 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 = (𝑅 ∪ {𝑍}) → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡))
1312eqeq1d 2823 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 = (𝑅 ∪ {𝑍}) → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛))
1413rabbidv 3481 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
1511, 14eqtrd 2856 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
1615mpteq2dv 5154 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝑅 ∪ {𝑍}) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
17 dvnprodlem1.rzt . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑅 ∪ {𝑍}) ⊆ 𝑇)
18 dvnprodlem1.t . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑇 ∈ Fin)
19 ssexg 5219 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 ∪ {𝑍}) ⊆ 𝑇𝑇 ∈ Fin) → (𝑅 ∪ {𝑍}) ∈ V)
2017, 18, 19syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑅 ∪ {𝑍}) ∈ V)
21 elpwg 4543 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 ∪ {𝑍}) ∈ V → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
2220, 21syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
2317, 22mpbird 258 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇)
24 nn0ex 11892 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ V
2524mptex 6978 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}) ∈ V
2625a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}) ∈ V)
278, 16, 23, 26fvmptd3 6784 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐶‘(𝑅 ∪ {𝑍})) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
28 oveq2 7153 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝐽 → (0...𝑛) = (0...𝐽))
2928oveq1d 7160 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝐽 → ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
30 rabeq 3484 . . . . . . . . . . . . . . . . . . . . . . . 24 (((0...𝑛) ↑m (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
3129, 30syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
32 eqeq2 2833 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝐽 → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽))
3332rabbidv 3481 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
3431, 33eqtrd 2856 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
3534adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 = 𝐽) → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
36 ovex 7178 . . . . . . . . . . . . . . . . . . . . . . 23 ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∈ V
3736rabex 5227 . . . . . . . . . . . . . . . . . . . . . 22 {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ V
3837a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ V)
3927, 35, 3, 38fvmptd 6768 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
40 ssrab2 4055 . . . . . . . . . . . . . . . . . . . . 21 {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑m (𝑅 ∪ {𝑍}))
4140a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
4239, 41eqsstrd 4004 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ⊆ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
4342adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ⊆ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
44 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
4543, 44sseldd 3967 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
46 elmapi 8418 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
4745, 46syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
48 dvnprodlem1.z . . . . . . . . . . . . . . . . . . 19 (𝜑𝑍𝑇)
49 snidg 4591 . . . . . . . . . . . . . . . . . . 19 (𝑍𝑇𝑍 ∈ {𝑍})
5048, 49syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑍 ∈ {𝑍})
51 elun2 4152 . . . . . . . . . . . . . . . . . 18 (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑅 ∪ {𝑍}))
5250, 51syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑍 ∈ (𝑅 ∪ {𝑍}))
5352adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
5447, 53ffvelrnd 6845 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ (0...𝐽))
557, 54sseldd 3967 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℤ)
565, 55zsubcld 12081 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ ℤ)
572, 5, 563jca 1120 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ))
58 elfzle2 12901 . . . . . . . . . . . . . 14 ((𝑐𝑍) ∈ (0...𝐽) → (𝑐𝑍) ≤ 𝐽)
5954, 58syl 17 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ≤ 𝐽)
605zred 12076 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℝ)
6155zred 12076 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℝ)
6260, 61subge0d 11219 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ≤ (𝐽 − (𝑐𝑍)) ↔ (𝑐𝑍) ≤ 𝐽))
6359, 62mpbird 258 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ≤ (𝐽 − (𝑐𝑍)))
64 elfzle1 12900 . . . . . . . . . . . . . 14 ((𝑐𝑍) ∈ (0...𝐽) → 0 ≤ (𝑐𝑍))
6554, 64syl 17 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ≤ (𝑐𝑍))
6660, 61subge02d 11221 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ≤ (𝑐𝑍) ↔ (𝐽 − (𝑐𝑍)) ≤ 𝐽))
6765, 66mpbid 233 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ≤ 𝐽)
6857, 63, 67jca32 516 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ) ∧ (0 ≤ (𝐽 − (𝑐𝑍)) ∧ (𝐽 − (𝑐𝑍)) ≤ 𝐽)))
69 elfz2 12889 . . . . . . . . . . 11 ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ↔ ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ) ∧ (0 ≤ (𝐽 − (𝑐𝑍)) ∧ (𝐽 − (𝑐𝑍)) ≤ 𝐽)))
7068, 69sylibr 235 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ (0...𝐽))
71 elmapfn 8419 . . . . . . . . . . . . . . . . . 18 (𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) → 𝑐 Fn (𝑅 ∪ {𝑍}))
7245, 71syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 Fn (𝑅 ∪ {𝑍}))
73 ssun1 4147 . . . . . . . . . . . . . . . . . 18 𝑅 ⊆ (𝑅 ∪ {𝑍})
7473a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ⊆ (𝑅 ∪ {𝑍}))
75 fnssres 6464 . . . . . . . . . . . . . . . . 17 ((𝑐 Fn (𝑅 ∪ {𝑍}) ∧ 𝑅 ⊆ (𝑅 ∪ {𝑍})) → (𝑐𝑅) Fn 𝑅)
7672, 74, 75syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) Fn 𝑅)
77 nfv 1906 . . . . . . . . . . . . . . . . . 18 𝑡𝜑
78 nfcv 2977 . . . . . . . . . . . . . . . . . . 19 𝑡𝑐
79 nfcv 2977 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡𝒫 𝑇
80 nfcv 2977 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡0
81 nfcv 2977 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑡𝑠
8281nfsum1 15036 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡Σ𝑡𝑠 (𝑐𝑡)
83 nfcv 2977 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡𝑛
8482, 83nfeq 2991 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡Σ𝑡𝑠 (𝑐𝑡) = 𝑛
85 nfcv 2977 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡((0...𝑛) ↑m 𝑠)
8684, 85nfrab 3387 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡{𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}
8780, 86nfmpt 5155 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
8879, 87nfmpt 5155 . . . . . . . . . . . . . . . . . . . . . 22 𝑡(𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
898, 88nfcxfr 2975 . . . . . . . . . . . . . . . . . . . . 21 𝑡𝐶
90 nfcv 2977 . . . . . . . . . . . . . . . . . . . . 21 𝑡(𝑅 ∪ {𝑍})
9189, 90nffv 6674 . . . . . . . . . . . . . . . . . . . 20 𝑡(𝐶‘(𝑅 ∪ {𝑍}))
92 nfcv 2977 . . . . . . . . . . . . . . . . . . . 20 𝑡𝐽
9391, 92nffv 6674 . . . . . . . . . . . . . . . . . . 19 𝑡((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
9478, 93nfel 2992 . . . . . . . . . . . . . . . . . 18 𝑡 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
9577, 94nfan 1891 . . . . . . . . . . . . . . . . 17 𝑡(𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
96 fvres 6683 . . . . . . . . . . . . . . . . . . . 20 (𝑡𝑅 → ((𝑐𝑅)‘𝑡) = (𝑐𝑡))
9796adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((𝑐𝑅)‘𝑡) = (𝑐𝑡))
982adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 0 ∈ ℤ)
9956adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝐽 − (𝑐𝑍)) ∈ ℤ)
1006a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (0...𝐽) ⊆ ℤ)
10147adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
10274sselda 3966 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
103101, 102ffvelrnd 6845 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝐽))
104100, 103sseldd 3967 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ ℤ)
10598, 99, 1043jca 1120 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (0 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ ∧ (𝑐𝑡) ∈ ℤ))
106 elfzle1 12900 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑐𝑡) ∈ (0...𝐽) → 0 ≤ (𝑐𝑡))
107103, 106syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 0 ≤ (𝑐𝑡))
10817unssad 4162 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑅𝑇)
109 ssfi 8727 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑇 ∈ Fin ∧ 𝑅𝑇) → 𝑅 ∈ Fin)
11018, 108, 109syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑅 ∈ Fin)
111110ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑅 ∈ Fin)
112 zssre 11977 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℤ ⊆ ℝ
1136, 112sstri 3975 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0...𝐽) ⊆ ℝ
114113a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → (0...𝐽) ⊆ ℝ)
11547adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
11674sselda 3966 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → 𝑟 ∈ (𝑅 ∪ {𝑍}))
117115, 116ffvelrnd 6845 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → (𝑐𝑟) ∈ (0...𝐽))
118114, 117sseldd 3967 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → (𝑐𝑟) ∈ ℝ)
119118adantlr 711 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) ∧ 𝑟𝑅) → (𝑐𝑟) ∈ ℝ)
120 elfzle1 12900 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑐𝑟) ∈ (0...𝐽) → 0 ≤ (𝑐𝑟))
121117, 120syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → 0 ≤ (𝑐𝑟))
122121adantlr 711 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) ∧ 𝑟𝑅) → 0 ≤ (𝑐𝑟))
123 fveq2 6664 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑟 = 𝑡 → (𝑐𝑟) = (𝑐𝑡))
124 simpr 485 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑡𝑅)
125111, 119, 122, 123, 124fsumge1 15142 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ≤ Σ𝑟𝑅 (𝑐𝑟))
126110adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ Fin)
127118recnd 10658 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → (𝑐𝑟) ∈ ℂ)
128126, 127fsumcl 15080 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟𝑅 (𝑐𝑟) ∈ ℂ)
12961recnd 10658 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℂ)
130128, 129pncand 10987 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((Σ𝑟𝑅 (𝑐𝑟) + (𝑐𝑍)) − (𝑐𝑍)) = Σ𝑟𝑅 (𝑐𝑟))
131 nfv 1906 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑟(𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
132 nfcv 2977 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑟(𝑐𝑍)
13348adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍𝑇)
134 dvnprodlem1.zr . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ¬ 𝑍𝑅)
135134adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ¬ 𝑍𝑅)
136 fveq2 6664 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑟 = 𝑍 → (𝑐𝑟) = (𝑐𝑍))
137131, 132, 126, 133, 135, 127, 136, 129fsumsplitsn 15090 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐𝑟) = (Σ𝑟𝑅 (𝑐𝑟) + (𝑐𝑍)))
138137eqcomd 2827 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (Σ𝑟𝑅 (𝑐𝑟) + (𝑐𝑍)) = Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐𝑟))
139123cbvsumv 15043 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐𝑟) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡)
140139a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐𝑟) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡))
14139adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
14244, 141eleqtrd 2915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
143 rabid 3379 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ↔ (𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽))
144142, 143sylib 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽))
145144simprd 496 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽)
146140, 145eqtrd 2856 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐𝑟) = 𝐽)
147138, 146eqtrd 2856 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (Σ𝑟𝑅 (𝑐𝑟) + (𝑐𝑍)) = 𝐽)
148147oveq1d 7160 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((Σ𝑟𝑅 (𝑐𝑟) + (𝑐𝑍)) − (𝑐𝑍)) = (𝐽 − (𝑐𝑍)))
149130, 148eqtr3d 2858 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟𝑅 (𝑐𝑟) = (𝐽 − (𝑐𝑍)))
150149adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → Σ𝑟𝑅 (𝑐𝑟) = (𝐽 − (𝑐𝑍)))
151125, 150breqtrd 5084 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ≤ (𝐽 − (𝑐𝑍)))
152105, 107, 151jca32 516 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((0 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ ∧ (𝑐𝑡) ∈ ℤ) ∧ (0 ≤ (𝑐𝑡) ∧ (𝑐𝑡) ≤ (𝐽 − (𝑐𝑍)))))
153 elfz2 12889 . . . . . . . . . . . . . . . . . . . 20 ((𝑐𝑡) ∈ (0...(𝐽 − (𝑐𝑍))) ↔ ((0 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ ∧ (𝑐𝑡) ∈ ℤ) ∧ (0 ≤ (𝑐𝑡) ∧ (𝑐𝑡) ≤ (𝐽 − (𝑐𝑍)))))
154152, 153sylibr 235 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...(𝐽 − (𝑐𝑍))))
15597, 154eqeltrd 2913 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍))))
156155ex 413 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑡𝑅 → ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍)))))
15795, 156ralrimi 3216 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∀𝑡𝑅 ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍))))
15876, 157jca 512 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐𝑅) Fn 𝑅 ∧ ∀𝑡𝑅 ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍)))))
159 ffnfv 6875 . . . . . . . . . . . . . . 15 ((𝑐𝑅):𝑅⟶(0...(𝐽 − (𝑐𝑍))) ↔ ((𝑐𝑅) Fn 𝑅 ∧ ∀𝑡𝑅 ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍)))))
160158, 159sylibr 235 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅):𝑅⟶(0...(𝐽 − (𝑐𝑍))))
161 ovexd 7180 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...(𝐽 − (𝑐𝑍))) ∈ V)
16218, 108ssexd 5220 . . . . . . . . . . . . . . . 16 (𝜑𝑅 ∈ V)
163162adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ V)
164161, 163elmapd 8410 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐𝑅) ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ↔ (𝑐𝑅):𝑅⟶(0...(𝐽 − (𝑐𝑍)))))
165160, 164mpbird 258 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅))
16696a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑡𝑅 → ((𝑐𝑅)‘𝑡) = (𝑐𝑡)))
16795, 166ralrimi 3216 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∀𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝑐𝑡))
168167sumeq2d 15049 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = Σ𝑡𝑅 (𝑐𝑡))
169123cbvsumv 15043 . . . . . . . . . . . . . . . 16 Σ𝑟𝑅 (𝑐𝑟) = Σ𝑡𝑅 (𝑐𝑡)
170169eqcomi 2830 . . . . . . . . . . . . . . 15 Σ𝑡𝑅 (𝑐𝑡) = Σ𝑟𝑅 (𝑐𝑟)
171170a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡𝑅 (𝑐𝑡) = Σ𝑟𝑅 (𝑐𝑟))
172149idi 1 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟𝑅 (𝑐𝑟) = (𝐽 − (𝑐𝑍)))
173168, 171, 1723eqtrd 2860 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝐽 − (𝑐𝑍)))
174165, 173jca 512 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐𝑅) ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∧ Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝐽 − (𝑐𝑍))))
175 eqidd 2822 . . . . . . . . . . . . . . 15 (𝑒 = (𝑐𝑅) → 𝑅 = 𝑅)
176 simpl 483 . . . . . . . . . . . . . . . 16 ((𝑒 = (𝑐𝑅) ∧ 𝑡𝑅) → 𝑒 = (𝑐𝑅))
177176fveq1d 6666 . . . . . . . . . . . . . . 15 ((𝑒 = (𝑐𝑅) ∧ 𝑡𝑅) → (𝑒𝑡) = ((𝑐𝑅)‘𝑡))
178175, 177sumeq12rdv 15054 . . . . . . . . . . . . . 14 (𝑒 = (𝑐𝑅) → Σ𝑡𝑅 (𝑒𝑡) = Σ𝑡𝑅 ((𝑐𝑅)‘𝑡))
179178eqeq1d 2823 . . . . . . . . . . . . 13 (𝑒 = (𝑐𝑅) → (Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍)) ↔ Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝐽 − (𝑐𝑍))))
180179elrab 3679 . . . . . . . . . . . 12 ((𝑐𝑅) ∈ {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))} ↔ ((𝑐𝑅) ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∧ Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝐽 − (𝑐𝑍))))
181174, 180sylibr 235 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) ∈ {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
182 oveq2 7153 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑅 → ((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m 𝑅))
183 rabeq 3484 . . . . . . . . . . . . . . . . . . 19 (((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m 𝑅) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
184182, 183syl 17 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
185 sumeq1 15035 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑅 → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡𝑅 (𝑐𝑡))
186185eqeq1d 2823 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑅 → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑛))
187186rabbidv 3481 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
188184, 187eqtrd 2856 . . . . . . . . . . . . . . . . 17 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
189188mpteq2dv 5154 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑅 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
190 elpwg 4543 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ V → (𝑅 ∈ 𝒫 𝑇𝑅𝑇))
191162, 190syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑅 ∈ 𝒫 𝑇𝑅𝑇))
192108, 191mpbird 258 . . . . . . . . . . . . . . . 16 (𝜑𝑅 ∈ 𝒫 𝑇)
19324mptex 6978 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) ∈ V
194193a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) ∈ V)
1958, 189, 192, 194fvmptd3 6784 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
196195adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐶𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
197 oveq2 7153 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑚 → (0...𝑛) = (0...𝑚))
198197oveq1d 7160 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑚 → ((0...𝑛) ↑m 𝑅) = ((0...𝑚) ↑m 𝑅))
199 rabeq 3484 . . . . . . . . . . . . . . . . . 18 (((0...𝑛) ↑m 𝑅) = ((0...𝑚) ↑m 𝑅) → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
200198, 199syl 17 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
201 eqeq2 2833 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑚 → (Σ𝑡𝑅 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑚))
202201rabbidv 3481 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚})
203200, 202eqtrd 2856 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚})
204203cbvmptv 5161 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) = (𝑚 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚})
205204a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) = (𝑚 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚}))
206196, 205eqtrd 2856 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐶𝑅) = (𝑚 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚}))
207 fveq1 6663 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑒 → (𝑐𝑡) = (𝑒𝑡))
208207sumeq2sdv 15051 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑒 → Σ𝑡𝑅 (𝑐𝑡) = Σ𝑡𝑅 (𝑒𝑡))
209208eqeq1d 2823 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑒 → (Σ𝑡𝑅 (𝑐𝑡) = 𝑚 ↔ Σ𝑡𝑅 (𝑒𝑡) = 𝑚))
210209cbvrabv 3492 . . . . . . . . . . . . . . . 16 {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚}
211210a1i 11 . . . . . . . . . . . . . . 15 (𝑚 = (𝐽 − (𝑐𝑍)) → {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚})
212 oveq2 7153 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝐽 − (𝑐𝑍)) → (0...𝑚) = (0...(𝐽 − (𝑐𝑍))))
213212oveq1d 7160 . . . . . . . . . . . . . . . 16 (𝑚 = (𝐽 − (𝑐𝑍)) → ((0...𝑚) ↑m 𝑅) = ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅))
214 rabeq 3484 . . . . . . . . . . . . . . . 16 (((0...𝑚) ↑m 𝑅) = ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) → {𝑒 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚})
215213, 214syl 17 . . . . . . . . . . . . . . 15 (𝑚 = (𝐽 − (𝑐𝑍)) → {𝑒 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚})
216 eqeq2 2833 . . . . . . . . . . . . . . . 16 (𝑚 = (𝐽 − (𝑐𝑍)) → (Σ𝑡𝑅 (𝑒𝑡) = 𝑚 ↔ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))))
217216rabbidv 3481 . . . . . . . . . . . . . . 15 (𝑚 = (𝐽 − (𝑐𝑍)) → {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
218211, 215, 2173eqtrd 2860 . . . . . . . . . . . . . 14 (𝑚 = (𝐽 − (𝑐𝑍)) → {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
219218adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑚 = (𝐽 − (𝑐𝑍))) → {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
22056, 63jca 512 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽 − (𝑐𝑍)) ∈ ℤ ∧ 0 ≤ (𝐽 − (𝑐𝑍))))
221 elnn0z 11983 . . . . . . . . . . . . . 14 ((𝐽 − (𝑐𝑍)) ∈ ℕ0 ↔ ((𝐽 − (𝑐𝑍)) ∈ ℤ ∧ 0 ≤ (𝐽 − (𝑐𝑍))))
222220, 221sylibr 235 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ ℕ0)
223 ovex 7178 . . . . . . . . . . . . . . 15 ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∈ V
224223rabex 5227 . . . . . . . . . . . . . 14 {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))} ∈ V
225224a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))} ∈ V)
226206, 219, 222, 225fvmptd 6768 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))) = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
227226eqcomd 2827 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))} = ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))
228181, 227eleqtrd 2915 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))
22970, 228jca 512 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍)))))
2301, 229jca 512 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∧ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))))
231 ovexd 7180 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ V)
232 vex 3498 . . . . . . . . . . 11 𝑐 ∈ V
233232resex 5893 . . . . . . . . . 10 (𝑐𝑅) ∈ V
234233a1i 11 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) ∈ V)
235 opeq12 4799 . . . . . . . . . . . 12 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → ⟨𝑘, 𝑑⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
236235eqeq2d 2832 . . . . . . . . . . 11 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → (⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ↔ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
237 eleq1 2900 . . . . . . . . . . . . 13 (𝑘 = (𝐽 − (𝑐𝑍)) → (𝑘 ∈ (0...𝐽) ↔ (𝐽 − (𝑐𝑍)) ∈ (0...𝐽)))
238237adantr 481 . . . . . . . . . . . 12 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → (𝑘 ∈ (0...𝐽) ↔ (𝐽 − (𝑐𝑍)) ∈ (0...𝐽)))
239 simpr 485 . . . . . . . . . . . . 13 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → 𝑑 = (𝑐𝑅))
240 fveq2 6664 . . . . . . . . . . . . . 14 (𝑘 = (𝐽 − (𝑐𝑍)) → ((𝐶𝑅)‘𝑘) = ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))
241240adantr 481 . . . . . . . . . . . . 13 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → ((𝐶𝑅)‘𝑘) = ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))
242239, 241eleq12d 2907 . . . . . . . . . . . 12 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → (𝑑 ∈ ((𝐶𝑅)‘𝑘) ↔ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍)))))
243238, 242anbi12d 630 . . . . . . . . . . 11 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → ((𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘)) ↔ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))))
244236, 243anbi12d 630 . . . . . . . . . 10 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → ((⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘))) ↔ (⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∧ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍)))))))
245244spc2egv 3599 . . . . . . . . 9 (((𝐽 − (𝑐𝑍)) ∈ V ∧ (𝑐𝑅) ∈ V) → ((⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∧ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))) → ∃𝑘𝑑(⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘)))))
246231, 234, 245syl2anc 584 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∧ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))) → ∃𝑘𝑑(⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘)))))
247230, 246mpd 15 . . . . . . 7 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∃𝑘𝑑(⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘))))
248 eliunxp 5702 . . . . . . 7 (⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ ∃𝑘𝑑(⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘))))
249247, 248sylibr 235 . . . . . 6 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
250 dvnprodlem1.d . . . . . 6 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
251249, 250fmptd 6871 . . . . 5 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
25293nfcri 2971 . . . . . . . . . . . 12 𝑡 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
25394, 252nfan 1891 . . . . . . . . . . 11 𝑡(𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
25477, 253nfan 1891 . . . . . . . . . 10 𝑡(𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)))
255 nfv 1906 . . . . . . . . . 10 𝑡(𝐷𝑐) = (𝐷𝑒)
256254, 255nfan 1891 . . . . . . . . 9 𝑡((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒))
25797eqcomd 2827 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) = ((𝑐𝑅)‘𝑡))
258257adantlrr 717 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ 𝑡𝑅) → (𝑐𝑡) = ((𝑐𝑅)‘𝑡))
259258adantlr 711 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (𝑐𝑡) = ((𝑐𝑅)‘𝑡))
260250a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
261 opex 5348 . . . . . . . . . . . . . . . . . . . 20 ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V
262261a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V)
263260, 262fvmpt2d 6774 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷𝑐) = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
264263fveq2d 6668 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (2nd ‘(𝐷𝑐)) = (2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
265264fveq1d 6666 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((2nd ‘(𝐷𝑐))‘𝑡) = ((2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)‘𝑡))
266 ovex 7178 . . . . . . . . . . . . . . . . . . 19 (𝐽 − (𝑐𝑍)) ∈ V
267266, 233op2nd 7689 . . . . . . . . . . . . . . . . . 18 (2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩) = (𝑐𝑅)
268267fveq1i 6665 . . . . . . . . . . . . . . . . 17 ((2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)‘𝑡) = ((𝑐𝑅)‘𝑡)
269268a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)‘𝑡) = ((𝑐𝑅)‘𝑡))
270265, 269eqtr2d 2857 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐𝑅)‘𝑡) = ((2nd ‘(𝐷𝑐))‘𝑡))
271270adantrr 713 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → ((𝑐𝑅)‘𝑡) = ((2nd ‘(𝐷𝑐))‘𝑡))
272271ad2antrr 722 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → ((𝑐𝑅)‘𝑡) = ((2nd ‘(𝐷𝑐))‘𝑡))
273 simpr 485 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐷𝑐) = (𝐷𝑒))
274 fveq1 6663 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑒 → (𝑐𝑍) = (𝑒𝑍))
275274oveq2d 7161 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = 𝑒 → (𝐽 − (𝑐𝑍)) = (𝐽 − (𝑒𝑍)))
276 reseq1 5841 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = 𝑒 → (𝑐𝑅) = (𝑒𝑅))
277275, 276opeq12d 4805 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 = 𝑒 → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
278 simpr 485 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
279 opex 5348 . . . . . . . . . . . . . . . . . . . . . . 23 ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩ ∈ V
280279a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩ ∈ V)
281250, 277, 278, 280fvmptd3 6784 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷𝑒) = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
282281adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐷𝑒) = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
283273, 282eqtrd 2856 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐷𝑐) = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
284283fveq2d 6668 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (2nd ‘(𝐷𝑐)) = (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
285284adantlrl 716 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (2nd ‘(𝐷𝑐)) = (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
286285adantr 481 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (2nd ‘(𝐷𝑐)) = (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
287 ovex 7178 . . . . . . . . . . . . . . . . . 18 (𝐽 − (𝑒𝑍)) ∈ V
288 vex 3498 . . . . . . . . . . . . . . . . . . 19 𝑒 ∈ V
289288resex 5893 . . . . . . . . . . . . . . . . . 18 (𝑒𝑅) ∈ V
290287, 289op2nd 7689 . . . . . . . . . . . . . . . . 17 (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩) = (𝑒𝑅)
291290a1i 11 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩) = (𝑒𝑅))
292286, 291eqtrd 2856 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (2nd ‘(𝐷𝑐)) = (𝑒𝑅))
293292fveq1d 6666 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → ((2nd ‘(𝐷𝑐))‘𝑡) = ((𝑒𝑅)‘𝑡))
294 fvres 6683 . . . . . . . . . . . . . . 15 (𝑡𝑅 → ((𝑒𝑅)‘𝑡) = (𝑒𝑡))
295294adantl 482 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → ((𝑒𝑅)‘𝑡) = (𝑒𝑡))
296293, 295eqtrd 2856 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → ((2nd ‘(𝐷𝑐))‘𝑡) = (𝑒𝑡))
297259, 272, 2963eqtrd 2860 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (𝑐𝑡) = (𝑒𝑡))
298297adantlr 711 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → (𝑐𝑡) = (𝑒𝑡))
299 simpl 483 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})))
300 elunnel1 4125 . . . . . . . . . . . . . 14 ((𝑡 ∈ (𝑅 ∪ {𝑍}) ∧ ¬ 𝑡𝑅) → 𝑡 ∈ {𝑍})
301 elsni 4576 . . . . . . . . . . . . . 14 (𝑡 ∈ {𝑍} → 𝑡 = 𝑍)
302300, 301syl 17 . . . . . . . . . . . . 13 ((𝑡 ∈ (𝑅 ∪ {𝑍}) ∧ ¬ 𝑡𝑅) → 𝑡 = 𝑍)
303302adantll 710 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → 𝑡 = 𝑍)
304 simpr 485 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → 𝑡 = 𝑍)
305304fveq2d 6668 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → (𝑐𝑡) = (𝑐𝑍))
3063nn0cnd 11946 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐽 ∈ ℂ)
307306adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
308307, 129nncand 10991 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝑐𝑍))
309308eqcomd 2827 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) = (𝐽 − (𝐽 − (𝑐𝑍))))
310309adantrr 713 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → (𝑐𝑍) = (𝐽 − (𝐽 − (𝑐𝑍))))
311310adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑐𝑍) = (𝐽 − (𝐽 − (𝑐𝑍))))
312263fveq2d 6668 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1st ‘(𝐷𝑐)) = (1st ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
313266, 233op1st 7688 . . . . . . . . . . . . . . . . . . . . 21 (1st ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩) = (𝐽 − (𝑐𝑍))
314313a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1st ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩) = (𝐽 − (𝑐𝑍)))
315312, 314eqtr2d 2857 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) = (1st ‘(𝐷𝑐)))
316315oveq2d 7161 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝐽 − (1st ‘(𝐷𝑐))))
317316adantrr 713 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝐽 − (1st ‘(𝐷𝑐))))
318317adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝐽 − (1st ‘(𝐷𝑐))))
319 fveq2 6664 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷𝑐) = (𝐷𝑒) → (1st ‘(𝐷𝑐)) = (1st ‘(𝐷𝑒)))
320319adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (1st ‘(𝐷𝑐)) = (1st ‘(𝐷𝑒)))
321281fveq2d 6668 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1st ‘(𝐷𝑒)) = (1st ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
322321adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (1st ‘(𝐷𝑒)) = (1st ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
323287, 289op1st 7688 . . . . . . . . . . . . . . . . . . . . 21 (1st ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩) = (𝐽 − (𝑒𝑍))
324323a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (1st ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩) = (𝐽 − (𝑒𝑍)))
325320, 322, 3243eqtrd 2860 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (1st ‘(𝐷𝑐)) = (𝐽 − (𝑒𝑍)))
326325oveq2d 7161 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (1st ‘(𝐷𝑐))) = (𝐽 − (𝐽 − (𝑒𝑍))))
327306adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
328 zsscn 11978 . . . . . . . . . . . . . . . . . . . . . . 23 ℤ ⊆ ℂ
3296, 328sstri 3975 . . . . . . . . . . . . . . . . . . . . . 22 (0...𝐽) ⊆ ℂ
330329a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ ℂ)
331 eleq1w 2895 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑒 → (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↔ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)))
332331anbi2d 628 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑒 → ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ↔ (𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))))
333 feq1 6489 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑒 → (𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽) ↔ 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽)))
334332, 333imbi12d 346 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = 𝑒 → (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽)) ↔ ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽))))
335334, 47chvarv 2408 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽))
33652adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
337335, 336ffvelrnd 6845 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑒𝑍) ∈ (0...𝐽))
338330, 337sseldd 3967 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑒𝑍) ∈ ℂ)
339327, 338nncand 10991 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑒𝑍))) = (𝑒𝑍))
340339adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (𝐽 − (𝑒𝑍))) = (𝑒𝑍))
341 eqidd 2822 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑒𝑍) = (𝑒𝑍))
342326, 340, 3413eqtrd 2860 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (1st ‘(𝐷𝑐))) = (𝑒𝑍))
343342adantlrl 716 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (1st ‘(𝐷𝑐))) = (𝑒𝑍))
344311, 318, 3433eqtrd 2860 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑐𝑍) = (𝑒𝑍))
345344adantr 481 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → (𝑐𝑍) = (𝑒𝑍))
346 fveq2 6664 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑍 → (𝑒𝑡) = (𝑒𝑍))
347346eqcomd 2827 . . . . . . . . . . . . . . 15 (𝑡 = 𝑍 → (𝑒𝑍) = (𝑒𝑡))
348347adantl 482 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → (𝑒𝑍) = (𝑒𝑡))
349305, 345, 3483eqtrd 2860 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → (𝑐𝑡) = (𝑒𝑡))
350349adantlr 711 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 = 𝑍) → (𝑐𝑡) = (𝑒𝑡))
351299, 303, 350syl2anc 584 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → (𝑐𝑡) = (𝑒𝑡))
352298, 351pm2.61dan 809 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐𝑡) = (𝑒𝑡))
353352ex 413 . . . . . . . . 9 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) → (𝑐𝑡) = (𝑒𝑡)))
354256, 353ralrimi 3216 . . . . . . . 8 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = (𝑒𝑡))
35572adantrr 713 . . . . . . . . . 10 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → 𝑐 Fn (𝑅 ∪ {𝑍}))
356355adantr 481 . . . . . . . . 9 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → 𝑐 Fn (𝑅 ∪ {𝑍}))
357335ffnd 6509 . . . . . . . . . . 11 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒 Fn (𝑅 ∪ {𝑍}))
358357adantrl 712 . . . . . . . . . 10 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → 𝑒 Fn (𝑅 ∪ {𝑍}))
359358adantr 481 . . . . . . . . 9 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → 𝑒 Fn (𝑅 ∪ {𝑍}))
360 eqfnfv 6795 . . . . . . . . 9 ((𝑐 Fn (𝑅 ∪ {𝑍}) ∧ 𝑒 Fn (𝑅 ∪ {𝑍})) → (𝑐 = 𝑒 ↔ ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = (𝑒𝑡)))
361356, 359, 360syl2anc 584 . . . . . . . 8 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑐 = 𝑒 ↔ ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = (𝑒𝑡)))
362354, 361mpbird 258 . . . . . . 7 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → 𝑐 = 𝑒)
363362ex 413 . . . . . 6 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → ((𝐷𝑐) = (𝐷𝑒) → 𝑐 = 𝑒))
364363ralrimivva 3191 . . . . 5 (𝜑 → ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷𝑐) = (𝐷𝑒) → 𝑐 = 𝑒))
365251, 364jca 512 . . . 4 (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷𝑐) = (𝐷𝑒) → 𝑐 = 𝑒)))
366 dff13 7004 . . . 4 (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷𝑐) = (𝐷𝑒) → 𝑐 = 𝑒)))
367365, 366sylibr 235 . . 3 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
368 eliun 4916 . . . . . . . . . . 11 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
369368biimpi 217 . . . . . . . . . 10 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
370369adantl 482 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
371 nfv 1906 . . . . . . . . . . 11 𝑘𝜑
372 nfcv 2977 . . . . . . . . . . . 12 𝑘𝑝
373 nfiu1 4945 . . . . . . . . . . . 12 𝑘 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))
374372, 373nfel 2992 . . . . . . . . . . 11 𝑘 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))
375371, 374nfan 1891 . . . . . . . . . 10 𝑘(𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
376 nfv 1906 . . . . . . . . . 10 𝑘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽}
377 nfv 1906 . . . . . . . . . . . . . . . . 17 𝑡 𝑘 ∈ (0...𝐽)
378 nfcv 2977 . . . . . . . . . . . . . . . . . 18 𝑡𝑝
379 nfcv 2977 . . . . . . . . . . . . . . . . . . 19 𝑡{𝑘}
380 nfcv 2977 . . . . . . . . . . . . . . . . . . . . 21 𝑡𝑅
38189, 380nffv 6674 . . . . . . . . . . . . . . . . . . . 20 𝑡(𝐶𝑅)
382 nfcv 2977 . . . . . . . . . . . . . . . . . . . 20 𝑡𝑘
383381, 382nffv 6674 . . . . . . . . . . . . . . . . . . 19 𝑡((𝐶𝑅)‘𝑘)
384379, 383nfxp 5582 . . . . . . . . . . . . . . . . . 18 𝑡({𝑘} × ((𝐶𝑅)‘𝑘))
385378, 384nfel 2992 . . . . . . . . . . . . . . . . 17 𝑡 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))
38677, 377, 385nf3an 1893 . . . . . . . . . . . . . . . 16 𝑡(𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
387 0zd 11982 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 0 ∈ ℤ)
3884adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝐽 ∈ ℤ)
3893883ad2antl1 1177 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝐽 ∈ ℤ)
390 iftrue 4471 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡𝑅 → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡))
391390adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡))
392 fzssz 12899 . . . . . . . . . . . . . . . . . . . . . . 23 (0...𝑘) ⊆ ℤ
393392a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → (0...𝑘) ⊆ ℤ)
394 simp1 1128 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝜑)
395 simp2 1129 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
396 xp2nd 7713 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝) ∈ ((𝐶𝑅)‘𝑘))
3973963ad2ant3 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ ((𝐶𝑅)‘𝑘))
398195adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐶𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
399 oveq2 7153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑛 = 𝑘 → (0...𝑛) = (0...𝑘))
400399oveq1d 7160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑛 = 𝑘 → ((0...𝑛) ↑m 𝑅) = ((0...𝑘) ↑m 𝑅))
401 rabeq 3484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((0...𝑛) ↑m 𝑅) = ((0...𝑘) ↑m 𝑅) → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
402400, 401syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
403 eqeq2 2833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑛 = 𝑘 → (Σ𝑡𝑅 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑘))
404403rabbidv 3481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
405402, 404eqtrd 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
406405adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑛 = 𝑘) → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
407 elfznn0 12990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℕ0)
408407adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℕ0)
409 ovex 7178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((0...𝑘) ↑m 𝑅) ∈ V
410409rabex 5227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ V
411410a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ V)
412398, 406, 408, 411fvmptd 6768 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
4134123adant3 1124 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝐶𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
414397, 413eleqtrd 2915 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
415 elrabi 3674 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2nd𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} → (2nd𝑝) ∈ ((0...𝑘) ↑m 𝑅))
4164153ad2ant3 1127 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0...𝐽) ∧ (2nd𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘}) → (2nd𝑝) ∈ ((0...𝑘) ↑m 𝑅))
417394, 395, 414, 416syl3anc 1363 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ ((0...𝑘) ↑m 𝑅))
418 elmapi 8418 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2nd𝑝) ∈ ((0...𝑘) ↑m 𝑅) → (2nd𝑝):𝑅⟶(0...𝑘))
419417, 418syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝):𝑅⟶(0...𝑘))
420419adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (2nd𝑝):𝑅⟶(0...𝑘))
421420ffvelrnda 6844 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ (0...𝑘))
422393, 421sseldd 3967 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ ℤ)
423391, 422eqeltrd 2913 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
424 simpl 483 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})))
425302adantll 710 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → 𝑡 = 𝑍)
426 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑡 = 𝑍) → 𝑡 = 𝑍)
427134adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑡 = 𝑍) → ¬ 𝑍𝑅)
428426, 427eqneltrd 2932 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑡 = 𝑍) → ¬ 𝑡𝑅)
429428iffalsed 4476 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
4304293ad2antl1 1177 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
4314adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑡 = 𝑍) → 𝐽 ∈ ℤ)
4324313ad2antl1 1177 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 𝐽 ∈ ℤ)
433 xp1st 7712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ {𝑘})
434 elsni 4576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((1st𝑝) ∈ {𝑘} → (1st𝑝) = 𝑘)
435433, 434syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) = 𝑘)
436435adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) = 𝑘)
4376sseli 3962 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℤ)
438437adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ ℤ)
439436, 438eqeltrd 2913 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ ℤ)
4404393adant1 1122 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ ℤ)
441440adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (1st𝑝) ∈ ℤ)
442432, 441zsubcld 12081 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − (1st𝑝)) ∈ ℤ)
443430, 442eqeltrd 2913 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
444443adantlr 711 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
445424, 425, 444syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
446423, 445pm2.61dan 809 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
447387, 389, 4463jca 1120 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ))
448419ffvelrnda 6844 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ (0...𝑘))
449 elfzle1 12900 . . . . . . . . . . . . . . . . . . . . . 22 (((2nd𝑝)‘𝑡) ∈ (0...𝑘) → 0 ≤ ((2nd𝑝)‘𝑡))
450448, 449syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 0 ≤ ((2nd𝑝)‘𝑡))
451390eqcomd 2827 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡𝑅 → ((2nd𝑝)‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
452451adantl 482 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
453450, 452breqtrd 5084 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
454453adantlr 711 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
455 simpll 763 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → (𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))))
456 elfzle2 12901 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (0...𝐽) → 𝑘𝐽)
457 elfzel2 12896 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℤ)
458457zred 12076 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℝ)
459113sseli 3962 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℝ)
460458, 459subge0d 11219 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (0...𝐽) → (0 ≤ (𝐽𝑘) ↔ 𝑘𝐽))
461456, 460mpbird 258 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ (0...𝐽) → 0 ≤ (𝐽𝑘))
462461adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ (0...𝐽) ∧ 𝑡 = 𝑍) → 0 ≤ (𝐽𝑘))
4634623ad2antl2 1178 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 0 ≤ (𝐽𝑘))
464394, 428sylan 580 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → ¬ 𝑡𝑅)
465464iffalsed 4476 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
4664363adant1 1122 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) = 𝑘)
467466oveq2d 7161 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) = (𝐽𝑘))
468467adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − (1st𝑝)) = (𝐽𝑘))
469465, 468eqtr2d 2857 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽𝑘) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
470463, 469breqtrd 5084 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
471455, 425, 470syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
472454, 471pm2.61dan 809 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
473 simpl2 1184 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 𝑘 ∈ (0...𝐽))
474392sseli 3962 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2nd𝑝)‘𝑡) ∈ (0...𝑘) → ((2nd𝑝)‘𝑡) ∈ ℤ)
475474zred 12076 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2nd𝑝)‘𝑡) ∈ (0...𝑘) → ((2nd𝑝)‘𝑡) ∈ ℝ)
476475adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2nd𝑝)‘𝑡) ∈ ℝ)
477459adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
478458adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
479 elfzle2 12901 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2nd𝑝)‘𝑡) ∈ (0...𝑘) → ((2nd𝑝)‘𝑡) ≤ 𝑘)
480479adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2nd𝑝)‘𝑡) ≤ 𝑘)
481456adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝑘𝐽)
482476, 477, 478, 480, 481letrd 10786 . . . . . . . . . . . . . . . . . . . . . 22 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2nd𝑝)‘𝑡) ≤ 𝐽)
483448, 473, 482syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ≤ 𝐽)
484483adantlr 711 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ≤ 𝐽)
485391, 484eqbrtrd 5080 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)
486469eqcomd 2827 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (𝐽𝑘))
487408nn0ge0d 11947 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (0...𝐽)) → 0 ≤ 𝑘)
488458adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
489459adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
490488, 489subge02d 11221 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (0...𝐽)) → (0 ≤ 𝑘 ↔ (𝐽𝑘) ≤ 𝐽))
491487, 490mpbid 233 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐽𝑘) ≤ 𝐽)
492491adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑡 = 𝑍) → (𝐽𝑘) ≤ 𝐽)
4934923adantl3 1160 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽𝑘) ≤ 𝐽)
494486, 493eqbrtrd 5080 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)
495455, 425, 494syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)
496485, 495pm2.61dan 809 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)
497447, 472, 496jca32 516 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ) ∧ (0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∧ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)))
498 elfz2 12889 . . . . . . . . . . . . . . . . 17 (if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ (0...𝐽) ↔ ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ) ∧ (0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∧ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)))
499497, 498sylibr 235 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ (0...𝐽))
500 eqid 2821 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
501386, 499, 500fmptdf 6874 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))):(𝑅 ∪ {𝑍})⟶(0...𝐽))
502 ovexd 7180 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (0...𝐽) ∈ V)
503394, 20syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑅 ∪ {𝑍}) ∈ V)
504502, 503elmapd 8410 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ↔ (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))):(𝑅 ∪ {𝑍})⟶(0...𝐽)))
505501, 504mpbird 258 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
506 eqidd 2822 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
507 eleq1w 2895 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = 𝑡 → (𝑟𝑅𝑡𝑅))
508 fveq2 6664 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = 𝑡 → ((2nd𝑝)‘𝑟) = ((2nd𝑝)‘𝑡))
509507, 508ifbieq1d 4488 . . . . . . . . . . . . . . . . . . . 20 (𝑟 = 𝑡 → if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
510509adantl 482 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑟 = 𝑡) → if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
511 simpr 485 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
512506, 510, 511, 446fvmptd 6768 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
513512ex 413 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) → ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))))
514386, 513ralrimi 3216 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ∀𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
515514sumeq2d 15049 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
516 nfcv 2977 . . . . . . . . . . . . . . . 16 𝑡if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝)))
517394, 110syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑅 ∈ Fin)
518394, 48syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑍𝑇)
519394, 134syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ¬ 𝑍𝑅)
520390adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡))
521448, 474syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ ℤ)
522521zcnd 12077 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ ℂ)
523520, 522eqeltrd 2913 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℂ)
524 eleq1 2900 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑍 → (𝑡𝑅𝑍𝑅))
525 fveq2 6664 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑍 → ((2nd𝑝)‘𝑡) = ((2nd𝑝)‘𝑍))
526524, 525ifbieq1d 4488 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑍 → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))))
527134adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ¬ 𝑍𝑅)
528527iffalsed 4476 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
5295283adant2 1123 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
53043ad2ant1 1125 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝐽 ∈ ℤ)
531530, 440zsubcld 12081 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ ℤ)
532531zcnd 12077 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ ℂ)
533529, 532eqeltrd 2913 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) ∈ ℂ)
534386, 516, 517, 518, 519, 523, 526, 533fsumsplitsn 15090 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) + if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝)))))
535390a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡𝑅 → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡)))
536386, 535ralrimi 3216 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ∀𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡))
537536sumeq2d 15049 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = Σ𝑡𝑅 ((2nd𝑝)‘𝑡))
538 eqidd 2822 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = (2nd𝑝) → 𝑅 = 𝑅)
539 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑐 = (2nd𝑝) ∧ 𝑡𝑅) → 𝑐 = (2nd𝑝))
540539fveq1d 6666 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑐 = (2nd𝑝) ∧ 𝑡𝑅) → (𝑐𝑡) = ((2nd𝑝)‘𝑡))
541538, 540sumeq12rdv 15054 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 = (2nd𝑝) → Σ𝑡𝑅 (𝑐𝑡) = Σ𝑡𝑅 ((2nd𝑝)‘𝑡))
542541eqeq1d 2823 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = (2nd𝑝) → (Σ𝑡𝑅 (𝑐𝑡) = 𝑘 ↔ Σ𝑡𝑅 ((2nd𝑝)‘𝑡) = 𝑘))
543542elrab 3679 . . . . . . . . . . . . . . . . . . . 20 ((2nd𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ↔ ((2nd𝑝) ∈ ((0...𝑘) ↑m 𝑅) ∧ Σ𝑡𝑅 ((2nd𝑝)‘𝑡) = 𝑘))
544414, 543sylib 219 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((2nd𝑝) ∈ ((0...𝑘) ↑m 𝑅) ∧ Σ𝑡𝑅 ((2nd𝑝)‘𝑡) = 𝑘))
545544simprd 496 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡𝑅 ((2nd𝑝)‘𝑡) = 𝑘)
546537, 545eqtrd 2856 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = 𝑘)
547519iffalsed 4476 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
548547, 467eqtrd 2856 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) = (𝐽𝑘))
549546, 548oveq12d 7163 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) + if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝)))) = (𝑘 + (𝐽𝑘)))
550329sseli 3962 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℂ)
5515503ad2ant2 1126 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ ℂ)
552394, 306syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝐽 ∈ ℂ)
553551, 552pncan3d 10989 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 + (𝐽𝑘)) = 𝐽)
554549, 553eqtrd 2856 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) + if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝)))) = 𝐽)
555515, 534, 5543eqtrd 2860 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = 𝐽)
556505, 555jca 512 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = 𝐽))
557 eleq1w 2895 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑟 → (𝑡𝑅𝑟𝑅))
558 fveq2 6664 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑟 → ((2nd𝑝)‘𝑡) = ((2nd𝑝)‘𝑟))
559557, 558ifbieq1d 4488 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑟 → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))
560559cbvmptv 5161 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))
561560eqeq2i 2834 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ↔ 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
562561biimpi 217 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
563 fveq1 6663 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))) → (𝑐𝑡) = ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡))
564563sumeq2sdv 15051 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡))
565562, 564syl 17 . . . . . . . . . . . . . . 15 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡))
566565eqeq1d 2823 . . . . . . . . . . . . . 14 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = 𝐽))
567566elrab 3679 . . . . . . . . . . . . 13 ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ↔ ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = 𝐽))
568556, 567sylibr 235 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
5695683exp 1111 . . . . . . . . . . 11 (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})))
570569adantr 481 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})))
571375, 376, 570rexlimd 3317 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽}))
572370, 571mpd 15 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
57339eqcomd 2827 . . . . . . . . 9 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} = ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
574573adantr 481 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} = ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
575572, 574eleqtrd 2915 . . . . . . 7 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
576250a1i 11 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
577 simpr 485 . . . . . . . . . . . . . . 15 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))))
578560a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
579577, 578eqtrd 2856 . . . . . . . . . . . . . 14 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
580 simpr 485 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟 = 𝑍) → 𝑟 = 𝑍)
581134adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟 = 𝑍) → ¬ 𝑍𝑅)
582580, 581eqneltrd 2932 . . . . . . . . . . . . . . . 16 ((𝜑𝑟 = 𝑍) → ¬ 𝑟𝑅)
583582iffalsed 4476 . . . . . . . . . . . . . . 15 ((𝜑𝑟 = 𝑍) → if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
584583adantlr 711 . . . . . . . . . . . . . 14 (((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) ∧ 𝑟 = 𝑍) → if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
58552adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
586 ovexd 7180 . . . . . . . . . . . . . 14 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (1st𝑝)) ∈ V)
587579, 584, 585, 586fvmptd 6768 . . . . . . . . . . . . 13 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑐𝑍) = (𝐽 − (1st𝑝)))
588587oveq2d 7161 . . . . . . . . . . . 12 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (𝑐𝑍)) = (𝐽 − (𝐽 − (1st𝑝))))
589588adantlr 711 . . . . . . . . . . 11 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (𝑐𝑍)) = (𝐽 − (𝐽 − (1st𝑝))))
590306ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝐽 ∈ ℂ)
591 nfv 1906 . . . . . . . . . . . . . . . . 17 𝑘(1st𝑝) ∈ (0...𝐽)
592 simpl 483 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
593 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ (0...𝐽) ∧ (1st𝑝) = 𝑘) → (1st𝑝) = 𝑘)
594 simpl 483 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ (0...𝐽) ∧ (1st𝑝) = 𝑘) → 𝑘 ∈ (0...𝐽))
595593, 594eqeltrd 2913 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ (0...𝐽) ∧ (1st𝑝) = 𝑘) → (1st𝑝) ∈ (0...𝐽))
596592, 436, 595syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ (0...𝐽))
597596ex 413 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽)))
598597a1i 11 . . . . . . . . . . . . . . . . 17 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽))))
599374, 591, 598rexlimd 3317 . . . . . . . . . . . . . . . 16 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽)))
600369, 599mpd 15 . . . . . . . . . . . . . . 15 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽))
6016sseli 3962 . . . . . . . . . . . . . . 15 ((1st𝑝) ∈ (0...𝐽) → (1st𝑝) ∈ ℤ)
602600, 601syl 17 . . . . . . . . . . . . . 14 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ ℤ)
603602zcnd 12077 . . . . . . . . . . . . 13 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ ℂ)
604603ad2antlr 723 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (1st𝑝) ∈ ℂ)
605590, 604nncand 10991 . . . . . . . . . . 11 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (𝐽 − (1st𝑝))) = (1st𝑝))
606589, 605eqtrd 2856 . . . . . . . . . 10 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (𝑐𝑍)) = (1st𝑝))
607 reseq1 5841 . . . . . . . . . . . 12 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → (𝑐𝑅) = ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ↾ 𝑅))
608607adantl 482 . . . . . . . . . . 11 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑐𝑅) = ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ↾ 𝑅))
60973a1i 11 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝑅 ⊆ (𝑅 ∪ {𝑍}))
610609resmptd 5902 . . . . . . . . . . 11 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ↾ 𝑅) = (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))))
611 nfv 1906 . . . . . . . . . . . . . 14 𝑘(𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝)
612390mpteq2ia 5149 . . . . . . . . . . . . . . . . . 18 (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (𝑡𝑅 ↦ ((2nd𝑝)‘𝑡))
613612a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (𝑡𝑅 ↦ ((2nd𝑝)‘𝑡)))
614419feqmptd 6727 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) = (𝑡𝑅 ↦ ((2nd𝑝)‘𝑡)))
615613, 614eqtr4d 2859 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))
6166153exp 1111 . . . . . . . . . . . . . . 15 (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))))
617616adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))))
618375, 611, 617rexlimd 3317 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝)))
619370, 618mpd 15 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))
620619adantr 481 . . . . . . . . . . 11 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))
621608, 610, 6203eqtrd 2860 . . . . . . . . . 10 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑐𝑅) = (2nd𝑝))
622606, 621opeq12d 4805 . . . . . . . . 9 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(1st𝑝), (2nd𝑝)⟩)
623 opex 5348 . . . . . . . . . 10 ⟨(1st𝑝), (2nd𝑝)⟩ ∈ V
624623a1i 11 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ⟨(1st𝑝), (2nd𝑝)⟩ ∈ V)
625576, 622, 575, 624fvmptd 6768 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) = ⟨(1st𝑝), (2nd𝑝)⟩)
626 nfv 1906 . . . . . . . . . 10 𝑘⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝
627 1st2nd2 7719 . . . . . . . . . . . . 13 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → 𝑝 = ⟨(1st𝑝), (2nd𝑝)⟩)
628627eqcomd 2827 . . . . . . . . . . . 12 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝)
629628a1i 11 . . . . . . . . . . 11 (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝))
630629a1i 11 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝)))
631375, 626, 630rexlimd 3317 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝))
632370, 631mpd 15 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝)
633625, 632eqtr2d 2857 . . . . . . 7 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑝 = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))))
634 fveq2 6664 . . . . . . . 8 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → (𝐷𝑐) = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))))
635634rspceeqv 3637 . . . . . . 7 (((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑝 = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))))) → ∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐))
636575, 633, 635syl2anc 584 . . . . . 6 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐))
637636ralrimiva 3182 . . . . 5 (𝜑 → ∀𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐))
638251, 637jca 512 . . . 4 (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ ∀𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐)))
639 dffo3 6861 . . . 4 (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ ∀𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐)))
640638, 639sylibr 235 . . 3 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
641367, 640jca 512 . 2 (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))))
642 df-f1o 6356 . 2 (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))))
643641, 642sylibr 235 1 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wex 1771  wcel 2105  wral 3138  wrex 3139  {crab 3142  Vcvv 3495  cun 3933  wss 3935  ifcif 4465  𝒫 cpw 4537  {csn 4559  cop 4565   ciun 4912   class class class wbr 5058  cmpt 5138   × cxp 5547  cres 5551   Fn wfn 6344  wf 6345  1-1wf1 6346  ontowfo 6347  1-1-ontowf1o 6348  cfv 6349  (class class class)co 7145  1st c1st 7678  2nd c2nd 7679  m cmap 8396  Fincfn 8498  cc 10524  cr 10525  0cc0 10526   + caddc 10529  cle 10665  cmin 10859  0cn0 11886  cz 11970  ...cfz 12882  Σcsu 15032
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-13 2383  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-inf2 9093  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-int 4870  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-se 5509  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-isom 6358  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7569  df-1st 7680  df-2nd 7681  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-1o 8093  df-oadd 8097  df-er 8279  df-map 8398  df-en 8499  df-dom 8500  df-sdom 8501  df-fin 8502  df-sup 8895  df-oi 8963  df-card 9357  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11628  df-2 11689  df-3 11690  df-n0 11887  df-z 11971  df-uz 12233  df-rp 12380  df-ico 12734  df-fz 12883  df-fzo 13024  df-seq 13360  df-exp 13420  df-hash 13681  df-cj 14448  df-re 14449  df-im 14450  df-sqrt 14584  df-abs 14585  df-clim 14835  df-sum 15033
This theorem is referenced by:  dvnprodlem2  42112
  Copyright terms: Public domain W3C validator