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

Theorem imasdsf1olem 22460
Description: Lemma for imasdsf1o 22461. (Contributed by Mario Carneiro, 21-Aug-2015.) (Proof shortened by AV, 6-Oct-2020.)
Hypotheses
Ref Expression
imasdsf1o.u (𝜑𝑈 = (𝐹s 𝑅))
imasdsf1o.v (𝜑𝑉 = (Base‘𝑅))
imasdsf1o.f (𝜑𝐹:𝑉1-1-onto𝐵)
imasdsf1o.r (𝜑𝑅𝑍)
imasdsf1o.e 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))
imasdsf1o.d 𝐷 = (dist‘𝑈)
imasdsf1o.m (𝜑𝐸 ∈ (∞Met‘𝑉))
imasdsf1o.x (𝜑𝑋𝑉)
imasdsf1o.y (𝜑𝑌𝑉)
imasdsf1o.w 𝑊 = (ℝ*𝑠s (ℝ* ∖ {-∞}))
imasdsf1o.s 𝑆 = { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))}
imasdsf1o.t 𝑇 = 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔)))
Assertion
Ref Expression
imasdsf1olem (𝜑 → ((𝐹𝑋)𝐷(𝐹𝑌)) = (𝑋𝐸𝑌))
Distinct variable groups:   𝑔,,𝑖,𝑛,𝐹   𝜑,𝑔,,𝑖,𝑛   𝑔,𝑉,,𝑖,𝑛   𝑔,𝐸,𝑖,𝑛   𝑅,𝑔,,𝑖,𝑛   𝑆,𝑔   𝑔,𝑋,,𝑖,𝑛   𝑔,𝑌,,𝑖,𝑛
Allowed substitution hints:   𝐵(𝑔,,𝑖,𝑛)   𝐷(𝑔,,𝑖,𝑛)   𝑆(,𝑖,𝑛)   𝑇(𝑔,,𝑖,𝑛)   𝑈(𝑔,,𝑖,𝑛)   𝐸()   𝑊(𝑔,,𝑖,𝑛)   𝑍(𝑔,,𝑖,𝑛)

Proof of Theorem imasdsf1olem
Dummy variables 𝑓 𝑗 𝑚 𝑝 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imasdsf1o.u . . . 4 (𝜑𝑈 = (𝐹s 𝑅))
2 imasdsf1o.v . . . 4 (𝜑𝑉 = (Base‘𝑅))
3 imasdsf1o.f . . . . 5 (𝜑𝐹:𝑉1-1-onto𝐵)
4 f1ofo 6329 . . . . 5 (𝐹:𝑉1-1-onto𝐵𝐹:𝑉onto𝐵)
53, 4syl 17 . . . 4 (𝜑𝐹:𝑉onto𝐵)
6 imasdsf1o.r . . . 4 (𝜑𝑅𝑍)
7 eqid 2765 . . . 4 (dist‘𝑅) = (dist‘𝑅)
8 imasdsf1o.d . . . 4 𝐷 = (dist‘𝑈)
9 f1of 6322 . . . . . 6 (𝐹:𝑉1-1-onto𝐵𝐹:𝑉𝐵)
103, 9syl 17 . . . . 5 (𝜑𝐹:𝑉𝐵)
11 imasdsf1o.x . . . . 5 (𝜑𝑋𝑉)
1210, 11ffvelrnd 6552 . . . 4 (𝜑 → (𝐹𝑋) ∈ 𝐵)
13 imasdsf1o.y . . . . 5 (𝜑𝑌𝑉)
1410, 13ffvelrnd 6552 . . . 4 (𝜑 → (𝐹𝑌) ∈ 𝐵)
15 imasdsf1o.s . . . 4 𝑆 = { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))}
16 imasdsf1o.e . . . 4 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))
171, 2, 5, 6, 7, 8, 12, 14, 15, 16imasdsval2 16445 . . 3 (𝜑 → ((𝐹𝑋)𝐷(𝐹𝑌)) = inf( 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < ))
18 imasdsf1o.t . . . 4 𝑇 = 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔)))
1918infeq1i 8593 . . 3 inf(𝑇, ℝ*, < ) = inf( 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < )
2017, 19syl6eqr 2817 . 2 (𝜑 → ((𝐹𝑋)𝐷(𝐹𝑌)) = inf(𝑇, ℝ*, < ))
21 xrsbas 20038 . . . . . . . . . . . 12 * = (Base‘ℝ*𝑠)
22 xrsadd 20039 . . . . . . . . . . . 12 +𝑒 = (+g‘ℝ*𝑠)
23 imasdsf1o.w . . . . . . . . . . . 12 𝑊 = (ℝ*𝑠s (ℝ* ∖ {-∞}))
24 xrsex 20037 . . . . . . . . . . . . 13 *𝑠 ∈ V
2524a1i 11 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ℝ*𝑠 ∈ V)
26 fzfid 12983 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1...𝑛) ∈ Fin)
27 difss 3901 . . . . . . . . . . . . 13 (ℝ* ∖ {-∞}) ⊆ ℝ*
2827a1i 11 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ* ∖ {-∞}) ⊆ ℝ*)
29 imasdsf1o.m . . . . . . . . . . . . . . . 16 (𝜑𝐸 ∈ (∞Met‘𝑉))
30 xmetf 22416 . . . . . . . . . . . . . . . 16 (𝐸 ∈ (∞Met‘𝑉) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
31 ffn 6225 . . . . . . . . . . . . . . . 16 (𝐸:(𝑉 × 𝑉)⟶ℝ*𝐸 Fn (𝑉 × 𝑉))
3229, 30, 313syl 18 . . . . . . . . . . . . . . 15 (𝜑𝐸 Fn (𝑉 × 𝑉))
33 xmetcl 22418 . . . . . . . . . . . . . . . . . . 19 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓𝑉𝑔𝑉) → (𝑓𝐸𝑔) ∈ ℝ*)
34 xmetge0 22431 . . . . . . . . . . . . . . . . . . . 20 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓𝑉𝑔𝑉) → 0 ≤ (𝑓𝐸𝑔))
35 ge0nemnf 12209 . . . . . . . . . . . . . . . . . . . 20 (((𝑓𝐸𝑔) ∈ ℝ* ∧ 0 ≤ (𝑓𝐸𝑔)) → (𝑓𝐸𝑔) ≠ -∞)
3633, 34, 35syl2anc 579 . . . . . . . . . . . . . . . . . . 19 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓𝑉𝑔𝑉) → (𝑓𝐸𝑔) ≠ -∞)
37 eldifsn 4474 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}) ↔ ((𝑓𝐸𝑔) ∈ ℝ* ∧ (𝑓𝐸𝑔) ≠ -∞))
3833, 36, 37sylanbrc 578 . . . . . . . . . . . . . . . . . 18 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓𝑉𝑔𝑉) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
39383expb 1149 . . . . . . . . . . . . . . . . 17 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓𝑉𝑔𝑉)) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
4029, 39sylan 575 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑓𝑉𝑔𝑉)) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
4140ralrimivva 3118 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑓𝑉𝑔𝑉 (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
42 ffnov 6964 . . . . . . . . . . . . . . 15 (𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}) ↔ (𝐸 Fn (𝑉 × 𝑉) ∧ ∀𝑓𝑉𝑔𝑉 (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞})))
4332, 41, 42sylanbrc 578 . . . . . . . . . . . . . 14 (𝜑𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
4443ad2antrr 717 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
45 ssrab2 3849 . . . . . . . . . . . . . . . . 17 { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ⊆ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))
4615, 45eqsstri 3797 . . . . . . . . . . . . . . . 16 𝑆 ⊆ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))
4746a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → 𝑆 ⊆ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)))
4847sselda 3763 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)))
49 elmapi 8084 . . . . . . . . . . . . . 14 (𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
5048, 49syl 17 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
51 fco 6242 . . . . . . . . . . . . 13 ((𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}) ∧ 𝑔:(1...𝑛)⟶(𝑉 × 𝑉)) → (𝐸𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
5244, 50, 51syl2anc 579 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
53 0re 10297 . . . . . . . . . . . . 13 0 ∈ ℝ
54 rexr 10341 . . . . . . . . . . . . . 14 (0 ∈ ℝ → 0 ∈ ℝ*)
55 renemnf 10344 . . . . . . . . . . . . . 14 (0 ∈ ℝ → 0 ≠ -∞)
56 eldifsn 4474 . . . . . . . . . . . . . 14 (0 ∈ (ℝ* ∖ {-∞}) ↔ (0 ∈ ℝ* ∧ 0 ≠ -∞))
5754, 55, 56sylanbrc 578 . . . . . . . . . . . . 13 (0 ∈ ℝ → 0 ∈ (ℝ* ∖ {-∞}))
5853, 57mp1i 13 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 0 ∈ (ℝ* ∖ {-∞}))
59 xaddid2 12278 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ* → (0 +𝑒 𝑥) = 𝑥)
60 xaddid1 12277 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ* → (𝑥 +𝑒 0) = 𝑥)
6159, 60jca 507 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ* → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
6261adantl 473 . . . . . . . . . . . 12 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℝ*) → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
6321, 22, 23, 25, 26, 28, 52, 58, 62gsumress 17545 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ*𝑠 Σg (𝐸𝑔)) = (𝑊 Σg (𝐸𝑔)))
6423, 21ressbas2 16206 . . . . . . . . . . . . 13 ((ℝ* ∖ {-∞}) ⊆ ℝ* → (ℝ* ∖ {-∞}) = (Base‘𝑊))
6527, 64ax-mp 5 . . . . . . . . . . . 12 (ℝ* ∖ {-∞}) = (Base‘𝑊)
6623xrs10 20061 . . . . . . . . . . . 12 0 = (0g𝑊)
6723xrs1cmn 20062 . . . . . . . . . . . . 13 𝑊 ∈ CMnd
6867a1i 11 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑊 ∈ CMnd)
69 c0ex 10289 . . . . . . . . . . . . . 14 0 ∈ V
7069a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 0 ∈ V)
7152, 26, 70fdmfifsupp 8494 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸𝑔) finSupp 0)
7265, 66, 68, 26, 52, 71gsumcl 18585 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg (𝐸𝑔)) ∈ (ℝ* ∖ {-∞}))
7363, 72eqeltrd 2844 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ*𝑠 Σg (𝐸𝑔)) ∈ (ℝ* ∖ {-∞}))
7473eldifad 3746 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ*𝑠 Σg (𝐸𝑔)) ∈ ℝ*)
7574fmpttd 6577 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))):𝑆⟶ℝ*)
7675frnd 6232 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
7776ralrimiva 3113 . . . . . 6 (𝜑 → ∀𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
78 iunss 4719 . . . . . 6 ( 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ* ↔ ∀𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
7977, 78sylibr 225 . . . . 5 (𝜑 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
8018, 79syl5eqss 3811 . . . 4 (𝜑𝑇 ⊆ ℝ*)
81 infxrcl 12368 . . . 4 (𝑇 ⊆ ℝ* → inf(𝑇, ℝ*, < ) ∈ ℝ*)
8280, 81syl 17 . . 3 (𝜑 → inf(𝑇, ℝ*, < ) ∈ ℝ*)
83 xmetcl 22418 . . . 4 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉𝑌𝑉) → (𝑋𝐸𝑌) ∈ ℝ*)
8429, 11, 13, 83syl3anc 1490 . . 3 (𝜑 → (𝑋𝐸𝑌) ∈ ℝ*)
85 1nn 11289 . . . . . . 7 1 ∈ ℕ
86 1ex 10291 . . . . . . . . . . . 12 1 ∈ V
87 opex 5090 . . . . . . . . . . . 12 𝑋, 𝑌⟩ ∈ V
8886, 87f1osn 6361 . . . . . . . . . . 11 {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}–1-1-onto→{⟨𝑋, 𝑌⟩}
89 f1of 6322 . . . . . . . . . . 11 ({⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}–1-1-onto→{⟨𝑋, 𝑌⟩} → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩})
9088, 89ax-mp 5 . . . . . . . . . 10 {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩}
91 opelxpi 5316 . . . . . . . . . . . 12 ((𝑋𝑉𝑌𝑉) → ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉))
9211, 13, 91syl2anc 579 . . . . . . . . . . 11 (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉))
9392snssd 4496 . . . . . . . . . 10 (𝜑 → {⟨𝑋, 𝑌⟩} ⊆ (𝑉 × 𝑉))
94 fss 6238 . . . . . . . . . 10 (({⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩} ∧ {⟨𝑋, 𝑌⟩} ⊆ (𝑉 × 𝑉)) → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉))
9590, 93, 94sylancr 581 . . . . . . . . 9 (𝜑 → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉))
9629elfvexd 6412 . . . . . . . . . . 11 (𝜑𝑉 ∈ V)
97 xpexg 7160 . . . . . . . . . . 11 ((𝑉 ∈ V ∧ 𝑉 ∈ V) → (𝑉 × 𝑉) ∈ V)
9896, 96, 97syl2anc 579 . . . . . . . . . 10 (𝜑 → (𝑉 × 𝑉) ∈ V)
99 snex 5066 . . . . . . . . . 10 {1} ∈ V
100 elmapg 8075 . . . . . . . . . 10 (((𝑉 × 𝑉) ∈ V ∧ {1} ∈ V) → ({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑𝑚 {1}) ↔ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉)))
10198, 99, 100sylancl 580 . . . . . . . . 9 (𝜑 → ({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑𝑚 {1}) ↔ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉)))
10295, 101mpbird 248 . . . . . . . 8 (𝜑 → {⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑𝑚 {1}))
103 op1stg 7380 . . . . . . . . . . 11 ((𝑋𝑉𝑌𝑉) → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋)
10411, 13, 103syl2anc 579 . . . . . . . . . 10 (𝜑 → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋)
105104fveq2d 6381 . . . . . . . . 9 (𝜑 → (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋))
106 op2ndg 7381 . . . . . . . . . . 11 ((𝑋𝑉𝑌𝑉) → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
10711, 13, 106syl2anc 579 . . . . . . . . . 10 (𝜑 → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
108107fveq2d 6381 . . . . . . . . 9 (𝜑 → (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌))
109105, 108jca 507 . . . . . . . 8 (𝜑 → ((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌)))
11024a1i 11 . . . . . . . . . 10 (𝜑 → ℝ*𝑠 ∈ V)
111 snfi 8247 . . . . . . . . . . 11 {1} ∈ Fin
112111a1i 11 . . . . . . . . . 10 (𝜑 → {1} ∈ Fin)
11327a1i 11 . . . . . . . . . 10 (𝜑 → (ℝ* ∖ {-∞}) ⊆ ℝ*)
114 xmetge0 22431 . . . . . . . . . . . . . . 15 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉𝑌𝑉) → 0 ≤ (𝑋𝐸𝑌))
11529, 11, 13, 114syl3anc 1490 . . . . . . . . . . . . . 14 (𝜑 → 0 ≤ (𝑋𝐸𝑌))
116 ge0nemnf 12209 . . . . . . . . . . . . . 14 (((𝑋𝐸𝑌) ∈ ℝ* ∧ 0 ≤ (𝑋𝐸𝑌)) → (𝑋𝐸𝑌) ≠ -∞)
11784, 115, 116syl2anc 579 . . . . . . . . . . . . 13 (𝜑 → (𝑋𝐸𝑌) ≠ -∞)
118 eldifsn 4474 . . . . . . . . . . . . 13 ((𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}) ↔ ((𝑋𝐸𝑌) ∈ ℝ* ∧ (𝑋𝐸𝑌) ≠ -∞))
11984, 117, 118sylanbrc 578 . . . . . . . . . . . 12 (𝜑 → (𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}))
120 fconst6g 6278 . . . . . . . . . . . 12 ((𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}) → ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞}))
121119, 120syl 17 . . . . . . . . . . 11 (𝜑 → ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞}))
122 fcoconst 6594 . . . . . . . . . . . . . 14 ((𝐸 Fn (𝑉 × 𝑉) ∧ ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉)) → (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}))
12332, 92, 122syl2anc 579 . . . . . . . . . . . . 13 (𝜑 → (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}))
12486, 87xpsn 6600 . . . . . . . . . . . . . 14 ({1} × {⟨𝑋, 𝑌⟩}) = {⟨1, ⟨𝑋, 𝑌⟩⟩}
125124coeq2i 5453 . . . . . . . . . . . . 13 (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})
126 df-ov 6847 . . . . . . . . . . . . . . . 16 (𝑋𝐸𝑌) = (𝐸‘⟨𝑋, 𝑌⟩)
127126eqcomi 2774 . . . . . . . . . . . . . . 15 (𝐸‘⟨𝑋, 𝑌⟩) = (𝑋𝐸𝑌)
128127sneqi 4347 . . . . . . . . . . . . . 14 {(𝐸‘⟨𝑋, 𝑌⟩)} = {(𝑋𝐸𝑌)}
129128xpeq2i 5306 . . . . . . . . . . . . 13 ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}) = ({1} × {(𝑋𝐸𝑌)})
130123, 125, 1293eqtr3g 2822 . . . . . . . . . . . 12 (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}) = ({1} × {(𝑋𝐸𝑌)}))
131130feq1d 6210 . . . . . . . . . . 11 (𝜑 → ((𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}):{1}⟶(ℝ* ∖ {-∞}) ↔ ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞})))
132121, 131mpbird 248 . . . . . . . . . 10 (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}):{1}⟶(ℝ* ∖ {-∞}))
13353, 57mp1i 13 . . . . . . . . . 10 (𝜑 → 0 ∈ (ℝ* ∖ {-∞}))
13461adantl 473 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ*) → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
13521, 22, 23, 110, 112, 113, 132, 133, 134gsumress 17545 . . . . . . . . 9 (𝜑 → (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})) = (𝑊 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
136 fconstmpt 5335 . . . . . . . . . . 11 ({1} × {(𝑋𝐸𝑌)}) = (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))
137130, 136syl6eq 2815 . . . . . . . . . 10 (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}) = (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌)))
138137oveq2d 6860 . . . . . . . . 9 (𝜑 → (𝑊 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})) = (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))))
139 cmnmnd 18477 . . . . . . . . . . 11 (𝑊 ∈ CMnd → 𝑊 ∈ Mnd)
14067, 139mp1i 13 . . . . . . . . . 10 (𝜑𝑊 ∈ Mnd)
14185a1i 11 . . . . . . . . . 10 (𝜑 → 1 ∈ ℕ)
142 eqidd 2766 . . . . . . . . . . 11 (𝑗 = 1 → (𝑋𝐸𝑌) = (𝑋𝐸𝑌))
14365, 142gsumsn 18623 . . . . . . . . . 10 ((𝑊 ∈ Mnd ∧ 1 ∈ ℕ ∧ (𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞})) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))) = (𝑋𝐸𝑌))
144140, 141, 119, 143syl3anc 1490 . . . . . . . . 9 (𝜑 → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))) = (𝑋𝐸𝑌))
145135, 138, 1443eqtrrd 2804 . . . . . . . 8 (𝜑 → (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
146 fveq1 6376 . . . . . . . . . . . . . 14 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝑔‘1) = ({⟨1, ⟨𝑋, 𝑌⟩⟩}‘1))
14786, 87fvsn 6641 . . . . . . . . . . . . . 14 ({⟨1, ⟨𝑋, 𝑌⟩⟩}‘1) = ⟨𝑋, 𝑌
148146, 147syl6eq 2815 . . . . . . . . . . . . 13 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝑔‘1) = ⟨𝑋, 𝑌⟩)
149148fveq2d 6381 . . . . . . . . . . . 12 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (1st ‘(𝑔‘1)) = (1st ‘⟨𝑋, 𝑌⟩))
150149fveqeq2d 6385 . . . . . . . . . . 11 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ↔ (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋)))
151148fveq2d 6381 . . . . . . . . . . . 12 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (2nd ‘(𝑔‘1)) = (2nd ‘⟨𝑋, 𝑌⟩))
152151fveqeq2d 6385 . . . . . . . . . . 11 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌) ↔ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌)))
153150, 152anbi12d 624 . . . . . . . . . 10 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ↔ ((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌))))
154 coeq2 5451 . . . . . . . . . . . 12 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝐸𝑔) = (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}))
155154oveq2d 6860 . . . . . . . . . . 11 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (ℝ*𝑠 Σg (𝐸𝑔)) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
156155eqeq2d 2775 . . . . . . . . . 10 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}))))
157153, 156anbi12d 624 . . . . . . . . 9 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))) ↔ (((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))))
158157rspcev 3462 . . . . . . . 8 (({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑𝑚 {1}) ∧ (((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))) → ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
159102, 109, 145, 158syl12anc 865 . . . . . . 7 (𝜑 → ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
160 ovex 6876 . . . . . . . . . 10 (𝑋𝐸𝑌) ∈ V
161 eqid 2765 . . . . . . . . . . 11 (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) = (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔)))
162161elrnmpt 5543 . . . . . . . . . 10 ((𝑋𝐸𝑌) ∈ V → ((𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
163160, 162ax-mp 5 . . . . . . . . 9 ((𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))
16415rexeqi 3291 . . . . . . . . . . 11 (∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ ∃𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))
165 fveq1 6376 . . . . . . . . . . . . . . 15 ( = 𝑔 → (‘1) = (𝑔‘1))
166165fveq2d 6381 . . . . . . . . . . . . . 14 ( = 𝑔 → (1st ‘(‘1)) = (1st ‘(𝑔‘1)))
167166fveqeq2d 6385 . . . . . . . . . . . . 13 ( = 𝑔 → ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ↔ (𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋)))
168 fveq1 6376 . . . . . . . . . . . . . . 15 ( = 𝑔 → (𝑛) = (𝑔𝑛))
169168fveq2d 6381 . . . . . . . . . . . . . 14 ( = 𝑔 → (2nd ‘(𝑛)) = (2nd ‘(𝑔𝑛)))
170169fveqeq2d 6385 . . . . . . . . . . . . 13 ( = 𝑔 → ((𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ↔ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)))
171 fveq1 6376 . . . . . . . . . . . . . . . . 17 ( = 𝑔 → (𝑖) = (𝑔𝑖))
172171fveq2d 6381 . . . . . . . . . . . . . . . 16 ( = 𝑔 → (2nd ‘(𝑖)) = (2nd ‘(𝑔𝑖)))
173172fveq2d 6381 . . . . . . . . . . . . . . 15 ( = 𝑔 → (𝐹‘(2nd ‘(𝑖))) = (𝐹‘(2nd ‘(𝑔𝑖))))
174 fveq1 6376 . . . . . . . . . . . . . . . . 17 ( = 𝑔 → (‘(𝑖 + 1)) = (𝑔‘(𝑖 + 1)))
175174fveq2d 6381 . . . . . . . . . . . . . . . 16 ( = 𝑔 → (1st ‘(‘(𝑖 + 1))) = (1st ‘(𝑔‘(𝑖 + 1))))
176175fveq2d 6381 . . . . . . . . . . . . . . 15 ( = 𝑔 → (𝐹‘(1st ‘(‘(𝑖 + 1)))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
177173, 176eqeq12d 2780 . . . . . . . . . . . . . 14 ( = 𝑔 → ((𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
178177ralbidv 3133 . . . . . . . . . . . . 13 ( = 𝑔 → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
179167, 170, 1783anbi123d 1560 . . . . . . . . . . . 12 ( = 𝑔 → (((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
180179rexrab 3529 . . . . . . . . . . 11 (∃𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
181164, 180bitri 266 . . . . . . . . . 10 (∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
182 oveq2 6852 . . . . . . . . . . . . 13 (𝑛 = 1 → (1...𝑛) = (1...1))
183 1z 11657 . . . . . . . . . . . . . 14 1 ∈ ℤ
184 fzsn 12593 . . . . . . . . . . . . . 14 (1 ∈ ℤ → (1...1) = {1})
185183, 184ax-mp 5 . . . . . . . . . . . . 13 (1...1) = {1}
186182, 185syl6eq 2815 . . . . . . . . . . . 12 (𝑛 = 1 → (1...𝑛) = {1})
187186oveq2d 6860 . . . . . . . . . . 11 (𝑛 = 1 → ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) = ((𝑉 × 𝑉) ↑𝑚 {1}))
188 df-3an 1109 . . . . . . . . . . . . 13 (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
189 ral0 4237 . . . . . . . . . . . . . . . 16 𝑖 ∈ ∅ (𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))
190 oveq1 6851 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → (𝑛 − 1) = (1 − 1))
191 1m1e0 11346 . . . . . . . . . . . . . . . . . . . 20 (1 − 1) = 0
192190, 191syl6eq 2815 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → (𝑛 − 1) = 0)
193192oveq2d 6860 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → (1...(𝑛 − 1)) = (1...0))
194 fz10 12572 . . . . . . . . . . . . . . . . . 18 (1...0) = ∅
195193, 194syl6eq 2815 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → (1...(𝑛 − 1)) = ∅)
196195raleqdv 3292 . . . . . . . . . . . . . . . 16 (𝑛 = 1 → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ ∅ (𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
197189, 196mpbiri 249 . . . . . . . . . . . . . . 15 (𝑛 = 1 → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
198197biantrud 527 . . . . . . . . . . . . . 14 (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
199 2fveq3 6382 . . . . . . . . . . . . . . . 16 (𝑛 = 1 → (2nd ‘(𝑔𝑛)) = (2nd ‘(𝑔‘1)))
200199fveqeq2d 6385 . . . . . . . . . . . . . . 15 (𝑛 = 1 → ((𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ↔ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)))
201200anbi2d 622 . . . . . . . . . . . . . 14 (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌))))
202198, 201bitr3d 272 . . . . . . . . . . . . 13 (𝑛 = 1 → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌))))
203188, 202syl5bb 274 . . . . . . . . . . . 12 (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌))))
204203anbi1d 623 . . . . . . . . . . 11 (𝑛 = 1 → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))))
205187, 204rexeqbidv 3301 . . . . . . . . . 10 (𝑛 = 1 → (∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))))
206181, 205syl5bb 274 . . . . . . . . 9 (𝑛 = 1 → (∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))))
207163, 206syl5bb 274 . . . . . . . 8 (𝑛 = 1 → ((𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))))
208207rspcev 3462 . . . . . . 7 ((1 ∈ ℕ ∧ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))) → ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
20985, 159, 208sylancr 581 . . . . . 6 (𝜑 → ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
210 eliun 4682 . . . . . 6 ((𝑋𝐸𝑌) ∈ 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
211209, 210sylibr 225 . . . . 5 (𝜑 → (𝑋𝐸𝑌) ∈ 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
212211, 18syl6eleqr 2855 . . . 4 (𝜑 → (𝑋𝐸𝑌) ∈ 𝑇)
213 infxrlb 12369 . . . 4 ((𝑇 ⊆ ℝ* ∧ (𝑋𝐸𝑌) ∈ 𝑇) → inf(𝑇, ℝ*, < ) ≤ (𝑋𝐸𝑌))
21480, 212, 213syl2anc 579 . . 3 (𝜑 → inf(𝑇, ℝ*, < ) ≤ (𝑋𝐸𝑌))
21518eleq2i 2836 . . . . . . 7 (𝑝𝑇𝑝 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
216 eliun 4682 . . . . . . 7 (𝑝 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
217215, 216bitri 266 . . . . . 6 (𝑝𝑇 ↔ ∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
218 vex 3353 . . . . . . . . 9 𝑝 ∈ V
219161elrnmpt 5543 . . . . . . . . 9 (𝑝 ∈ V → (𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸𝑔))))
220218, 219ax-mp 5 . . . . . . . 8 (𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸𝑔)))
221179, 15elrab2 3525 . . . . . . . . . . . . . . . . 17 (𝑔𝑆 ↔ (𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∧ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
222221simprbi 490 . . . . . . . . . . . . . . . 16 (𝑔𝑆 → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
223222adantl 473 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
224223simp2d 1173 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌))
2253ad2antrr 717 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐹:𝑉1-1-onto𝐵)
226 f1of1 6321 . . . . . . . . . . . . . . . 16 (𝐹:𝑉1-1-onto𝐵𝐹:𝑉1-1𝐵)
227225, 226syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐹:𝑉1-1𝐵)
228 simplr 785 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑛 ∈ ℕ)
229 elfz1end 12581 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (1...𝑛))
230228, 229sylib 209 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑛 ∈ (1...𝑛))
23150, 230ffvelrnd 6552 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑔𝑛) ∈ (𝑉 × 𝑉))
232 xp2nd 7401 . . . . . . . . . . . . . . . 16 ((𝑔𝑛) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔𝑛)) ∈ 𝑉)
233231, 232syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (2nd ‘(𝑔𝑛)) ∈ 𝑉)
23413ad2antrr 717 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑌𝑉)
235 f1fveq 6713 . . . . . . . . . . . . . . 15 ((𝐹:𝑉1-1𝐵 ∧ ((2nd ‘(𝑔𝑛)) ∈ 𝑉𝑌𝑉)) → ((𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ↔ (2nd ‘(𝑔𝑛)) = 𝑌))
236227, 233, 234, 235syl12anc 865 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ↔ (2nd ‘(𝑔𝑛)) = 𝑌))
237224, 236mpbid 223 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (2nd ‘(𝑔𝑛)) = 𝑌)
238237oveq2d 6860 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔𝑛))) = (𝑋𝐸𝑌))
239 eleq1 2832 . . . . . . . . . . . . . . . . 17 (𝑚 = 1 → (𝑚 ∈ (1...𝑛) ↔ 1 ∈ (1...𝑛)))
240 2fveq3 6382 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 1 → (2nd ‘(𝑔𝑚)) = (2nd ‘(𝑔‘1)))
241240oveq2d 6860 . . . . . . . . . . . . . . . . . 18 (𝑚 = 1 → (𝑋𝐸(2nd ‘(𝑔𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘1))))
242 oveq2 6852 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 1 → (1...𝑚) = (1...1))
243242, 185syl6eq 2815 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 1 → (1...𝑚) = {1})
244243reseq2d 5567 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 1 → ((𝐸𝑔) ↾ (1...𝑚)) = ((𝐸𝑔) ↾ {1}))
245244oveq2d 6860 . . . . . . . . . . . . . . . . . 18 (𝑚 = 1 → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸𝑔) ↾ {1})))
246241, 245breq12d 4824 . . . . . . . . . . . . . . . . 17 (𝑚 = 1 → ((𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1}))))
247239, 246imbi12d 335 . . . . . . . . . . . . . . . 16 (𝑚 = 1 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚)))) ↔ (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1})))))
248247imbi2d 331 . . . . . . . . . . . . . . 15 (𝑚 = 1 → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))))) ↔ (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1}))))))
249 eleq1 2832 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑥 → (𝑚 ∈ (1...𝑛) ↔ 𝑥 ∈ (1...𝑛)))
250 2fveq3 6382 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑥 → (2nd ‘(𝑔𝑚)) = (2nd ‘(𝑔𝑥)))
251250oveq2d 6860 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑥 → (𝑋𝐸(2nd ‘(𝑔𝑚))) = (𝑋𝐸(2nd ‘(𝑔𝑥))))
252 oveq2 6852 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑥 → (1...𝑚) = (1...𝑥))
253252reseq2d 5567 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑥 → ((𝐸𝑔) ↾ (1...𝑚)) = ((𝐸𝑔) ↾ (1...𝑥)))
254253oveq2d 6860 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑥 → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))))
255251, 254breq12d 4824 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑥 → ((𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))))
256249, 255imbi12d 335 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑥 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚)))) ↔ (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))))))
257256imbi2d 331 . . . . . . . . . . . . . . 15 (𝑚 = 𝑥 → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))))) ↔ (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))))))
258 eleq1 2832 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑥 + 1) → (𝑚 ∈ (1...𝑛) ↔ (𝑥 + 1) ∈ (1...𝑛)))
259 2fveq3 6382 . . . . . . . . . . . . . . . . . . 19 (𝑚 = (𝑥 + 1) → (2nd ‘(𝑔𝑚)) = (2nd ‘(𝑔‘(𝑥 + 1))))
260259oveq2d 6860 . . . . . . . . . . . . . . . . . 18 (𝑚 = (𝑥 + 1) → (𝑋𝐸(2nd ‘(𝑔𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))))
261 oveq2 6852 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = (𝑥 + 1) → (1...𝑚) = (1...(𝑥 + 1)))
262261reseq2d 5567 . . . . . . . . . . . . . . . . . . 19 (𝑚 = (𝑥 + 1) → ((𝐸𝑔) ↾ (1...𝑚)) = ((𝐸𝑔) ↾ (1...(𝑥 + 1))))
263262oveq2d 6860 . . . . . . . . . . . . . . . . . 18 (𝑚 = (𝑥 + 1) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))))
264260, 263breq12d 4824 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑥 + 1) → ((𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))
265258, 264imbi12d 335 . . . . . . . . . . . . . . . 16 (𝑚 = (𝑥 + 1) → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚)))) ↔ ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))))))
266265imbi2d 331 . . . . . . . . . . . . . . 15 (𝑚 = (𝑥 + 1) → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))))) ↔ (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))))
267 eleq1 2832 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → (𝑚 ∈ (1...𝑛) ↔ 𝑛 ∈ (1...𝑛)))
268 2fveq3 6382 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → (2nd ‘(𝑔𝑚)) = (2nd ‘(𝑔𝑛)))
269268oveq2d 6860 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑛 → (𝑋𝐸(2nd ‘(𝑔𝑚))) = (𝑋𝐸(2nd ‘(𝑔𝑛))))
270 oveq2 6852 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
271270reseq2d 5567 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → ((𝐸𝑔) ↾ (1...𝑚)) = ((𝐸𝑔) ↾ (1...𝑛)))
272271oveq2d 6860 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑛 → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))
273269, 272breq12d 4824 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → ((𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛)))))
274267, 273imbi12d 335 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚)))) ↔ (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))))
275274imbi2d 331 . . . . . . . . . . . . . . 15 (𝑚 = 𝑛 → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))))) ↔ (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛)))))))
27629ad2antrr 717 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐸 ∈ (∞Met‘𝑉))
27711ad2antrr 717 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑋𝑉)
278 nnuz 11926 . . . . . . . . . . . . . . . . . . . . . . 23 ℕ = (ℤ‘1)
279228, 278syl6eleq 2854 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑛 ∈ (ℤ‘1))
280 eluzfz1 12558 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (ℤ‘1) → 1 ∈ (1...𝑛))
281279, 280syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 1 ∈ (1...𝑛))
28250, 281ffvelrnd 6552 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑔‘1) ∈ (𝑉 × 𝑉))
283 xp2nd 7401 . . . . . . . . . . . . . . . . . . . 20 ((𝑔‘1) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘1)) ∈ 𝑉)
284282, 283syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (2nd ‘(𝑔‘1)) ∈ 𝑉)
285 xmetcl 22418 . . . . . . . . . . . . . . . . . . 19 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉 ∧ (2nd ‘(𝑔‘1)) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔‘1))) ∈ ℝ*)
286276, 277, 284, 285syl3anc 1490 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ∈ ℝ*)
287286xrleidd 12188 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑋𝐸(2nd ‘(𝑔‘1))))
288140ad2antrr 717 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑊 ∈ Mnd)
28985a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 1 ∈ ℕ)
29044, 282ffvelrnd 6552 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸‘(𝑔‘1)) ∈ (ℝ* ∖ {-∞}))
291 2fveq3 6382 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 1 → (𝐸‘(𝑔𝑗)) = (𝐸‘(𝑔‘1)))
29265, 291gsumsn 18623 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ Mnd ∧ 1 ∈ ℕ ∧ (𝐸‘(𝑔‘1)) ∈ (ℝ* ∖ {-∞})) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗)))) = (𝐸‘(𝑔‘1)))
293288, 289, 290, 292syl3anc 1490 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗)))) = (𝐸‘(𝑔‘1)))
294276, 30syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
295 fcompt 6593 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐸:(𝑉 × 𝑉)⟶ℝ*𝑔:(1...𝑛)⟶(𝑉 × 𝑉)) → (𝐸𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))))
296294, 50, 295syl2anc 579 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))))
297296reseq1d 5566 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐸𝑔) ↾ {1}) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ {1}))
298281snssd 4496 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → {1} ⊆ (1...𝑛))
299298resmptd 5631 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ {1}) = (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗))))
300297, 299eqtrd 2799 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐸𝑔) ↾ {1}) = (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗))))
301300oveq2d 6860 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg ((𝐸𝑔) ↾ {1})) = (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗)))))
302 df-ov 6847 . . . . . . . . . . . . . . . . . . 19 (𝑋𝐸(2nd ‘(𝑔‘1))) = (𝐸‘⟨𝑋, (2nd ‘(𝑔‘1))⟩)
303 1st2nd2 7407 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔‘1) ∈ (𝑉 × 𝑉) → (𝑔‘1) = ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩)
304282, 303syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑔‘1) = ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩)
305223simp1d 1172 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋))
306 xp1st 7400 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔‘1) ∈ (𝑉 × 𝑉) → (1st ‘(𝑔‘1)) ∈ 𝑉)
307282, 306syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1st ‘(𝑔‘1)) ∈ 𝑉)
308 f1fveq 6713 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹:𝑉1-1𝐵 ∧ ((1st ‘(𝑔‘1)) ∈ 𝑉𝑋𝑉)) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ↔ (1st ‘(𝑔‘1)) = 𝑋))
309227, 307, 277, 308syl12anc 865 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ↔ (1st ‘(𝑔‘1)) = 𝑋))
310305, 309mpbid 223 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1st ‘(𝑔‘1)) = 𝑋)
311310opeq1d 4567 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩ = ⟨𝑋, (2nd ‘(𝑔‘1))⟩)
312304, 311eqtr2d 2800 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ⟨𝑋, (2nd ‘(𝑔‘1))⟩ = (𝑔‘1))
313312fveq2d 6381 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸‘⟨𝑋, (2nd ‘(𝑔‘1))⟩) = (𝐸‘(𝑔‘1)))
314302, 313syl5eq 2811 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) = (𝐸‘(𝑔‘1)))
315293, 301, 3143eqtr4d 2809 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg ((𝐸𝑔) ↾ {1})) = (𝑋𝐸(2nd ‘(𝑔‘1))))
316287, 315breqtrrd 4839 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1})))
317316a1d 25 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1}))))
318 simprl 787 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ ℕ)
319318, 278syl6eleq 2854 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (ℤ‘1))
320 simprr 789 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑥 + 1) ∈ (1...𝑛))
321 peano2fzr 12564 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (ℤ‘1) ∧ (𝑥 + 1) ∈ (1...𝑛)) → 𝑥 ∈ (1...𝑛))
322319, 320, 321syl2anc 579 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (1...𝑛))
323322expr 448 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 + 1) ∈ (1...𝑛) → 𝑥 ∈ (1...𝑛)))
324323imim1d 82 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))))))
325276adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸 ∈ (∞Met‘𝑉))
326277adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑋𝑉)
32750adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
328327, 322ffvelrnd 6552 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔𝑥) ∈ (𝑉 × 𝑉))
329 xp2nd 7401 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔𝑥) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔𝑥)) ∈ 𝑉)
330328, 329syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔𝑥)) ∈ 𝑉)
331 xmetcl 22418 . . . . . . . . . . . . . . . . . . . 20 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉 ∧ (2nd ‘(𝑔𝑥)) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ∈ ℝ*)
332325, 326, 330, 331syl3anc 1490 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ∈ ℝ*)
33367a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑊 ∈ CMnd)
334 fzfid 12983 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...𝑥) ∈ Fin)
33552adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
336 fzsuc 12598 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ (ℤ‘1) → (1...(𝑥 + 1)) = ((1...𝑥) ∪ {(𝑥 + 1)}))
337319, 336syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...(𝑥 + 1)) = ((1...𝑥) ∪ {(𝑥 + 1)}))
338 elfzuz3 12549 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 + 1) ∈ (1...𝑛) → 𝑛 ∈ (ℤ‘(𝑥 + 1)))
339338ad2antll 720 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑛 ∈ (ℤ‘(𝑥 + 1)))
340 fzss2 12591 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ (ℤ‘(𝑥 + 1)) → (1...(𝑥 + 1)) ⊆ (1...𝑛))
341339, 340syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...(𝑥 + 1)) ⊆ (1...𝑛))
342337, 341eqsstr3d 3802 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((1...𝑥) ∪ {(𝑥 + 1)}) ⊆ (1...𝑛))
343342unssad 3954 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...𝑥) ⊆ (1...𝑛))
344335, 343fssresd 6255 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...𝑥)):(1...𝑥)⟶(ℝ* ∖ {-∞}))
34569a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 0 ∈ V)
346344, 334, 345fdmfifsupp 8494 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...𝑥)) finSupp 0)
34765, 66, 333, 334, 344, 346gsumcl 18585 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) ∈ (ℝ* ∖ {-∞}))
348347eldifad 3746 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) ∈ ℝ*)
349325, 30syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
350327, 320ffvelrnd 6552 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉))
351349, 350ffvelrnd 6552 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*)
352 xleadd1a 12288 . . . . . . . . . . . . . . . . . . . 20 ((((𝑋𝐸(2nd ‘(𝑔𝑥))) ∈ ℝ* ∧ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) ∈ ℝ* ∧ (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*) ∧ (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
353352ex 401 . . . . . . . . . . . . . . . . . . 19 (((𝑋𝐸(2nd ‘(𝑔𝑥))) ∈ ℝ* ∧ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) ∈ ℝ* ∧ (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
354332, 348, 351, 353syl3anc 1490 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
355 xp2nd 7401 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
356350, 355syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
357 xmettri 22438 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑋𝑉 ∧ (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉 ∧ (2nd ‘(𝑔𝑥)) ∈ 𝑉)) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
358325, 326, 356, 330, 357syl13anc 1491 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
359 1st2nd2 7407 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (𝑔‘(𝑥 + 1)) = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
360350, 359syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
361 2fveq3 6382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑥 → (2nd ‘(𝑔𝑖)) = (2nd ‘(𝑔𝑥)))
362361fveq2d 6381 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 = 𝑥 → (𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(2nd ‘(𝑔𝑥))))
363 fvoveq1 6867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 = 𝑥 → (𝑔‘(𝑖 + 1)) = (𝑔‘(𝑥 + 1)))
364363fveq2d 6381 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑥 → (1st ‘(𝑔‘(𝑖 + 1))) = (1st ‘(𝑔‘(𝑥 + 1))))
365364fveq2d 6381 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 = 𝑥 → (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))))
366362, 365eqeq12d 2780 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 = 𝑥 → ((𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(𝑔𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1))))))
367223simp3d 1174 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
368367adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
369 nnz 11649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℕ → 𝑥 ∈ ℤ)
370369ad2antrl 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ ℤ)
371 eluzp1m1 11913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑥 ∈ ℤ ∧ 𝑛 ∈ (ℤ‘(𝑥 + 1))) → (𝑛 − 1) ∈ (ℤ𝑥))
372370, 339, 371syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑛 − 1) ∈ (ℤ𝑥))
373 elfzuzb 12546 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ (1...(𝑛 − 1)) ↔ (𝑥 ∈ (ℤ‘1) ∧ (𝑛 − 1) ∈ (ℤ𝑥)))
374319, 372, 373sylanbrc 578 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (1...(𝑛 − 1)))
375366, 368, 374rspcdva 3468 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐹‘(2nd ‘(𝑔𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))))
376227adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐹:𝑉1-1𝐵)
377 xp1st 7400 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
378350, 377syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
379 f1fveq 6713 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹:𝑉1-1𝐵 ∧ ((2nd ‘(𝑔𝑥)) ∈ 𝑉 ∧ (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)) → ((𝐹‘(2nd ‘(𝑔𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))) ↔ (2nd ‘(𝑔𝑥)) = (1st ‘(𝑔‘(𝑥 + 1)))))
380376, 330, 378, 379syl12anc 865 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐹‘(2nd ‘(𝑔𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))) ↔ (2nd ‘(𝑔𝑥)) = (1st ‘(𝑔‘(𝑥 + 1)))))
381375, 380mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔𝑥)) = (1st ‘(𝑔‘(𝑥 + 1))))
382381opeq1d 4567 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ⟨(2nd ‘(𝑔𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩ = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
383360, 382eqtr4d 2802 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) = ⟨(2nd ‘(𝑔𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
384383fveq2d 6381 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) = (𝐸‘⟨(2nd ‘(𝑔𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩))
385 df-ov 6847 . . . . . . . . . . . . . . . . . . . . . 22 ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) = (𝐸‘⟨(2nd ‘(𝑔𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
386384, 385syl6eqr 2817 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) = ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1)))))
387386oveq2d 6860 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) = ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
388358, 387breqtrrd 4839 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
389 xmetcl 22418 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉 ∧ (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
390325, 326, 356, 389syl3anc 1490 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
391332, 351xaddcld 12336 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
392348, 351xaddcld 12336 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
393 xrletr 12194 . . . . . . . . . . . . . . . . . . . 20 (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ* ∧ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ* ∧ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*) → (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∧ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
394390, 391, 392, 393syl3anc 1490 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∧ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
395388, 394mpand 686 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
396354, 395syld 47 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
397 xrex 12028 . . . . . . . . . . . . . . . . . . . . . 22 * ∈ V
398397, 27ssexi 4966 . . . . . . . . . . . . . . . . . . . . 21 (ℝ* ∖ {-∞}) ∈ V
39923, 22ressplusg 16268 . . . . . . . . . . . . . . . . . . . . 21 ((ℝ* ∖ {-∞}) ∈ V → +𝑒 = (+g𝑊))
400398, 399ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 +𝑒 = (+g𝑊)
40144ad2antrr 717 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
402 fzelp1 12603 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ (1...𝑥) → 𝑗 ∈ (1...(𝑥 + 1)))
40350ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
404341sselda 3763 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → 𝑗 ∈ (1...𝑛))
405403, 404ffvelrnd 6552 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → (𝑔𝑗) ∈ (𝑉 × 𝑉))
406402, 405sylan2 586 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → (𝑔𝑗) ∈ (𝑉 × 𝑉))
407401, 406ffvelrnd 6552 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → (𝐸‘(𝑔𝑗)) ∈ (ℝ* ∖ {-∞}))
408 fzp1disj 12609 . . . . . . . . . . . . . . . . . . . . . 22 ((1...𝑥) ∩ {(𝑥 + 1)}) = ∅
409408a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((1...𝑥) ∩ {(𝑥 + 1)}) = ∅)
410 disjsn 4404 . . . . . . . . . . . . . . . . . . . . 21 (((1...𝑥) ∩ {(𝑥 + 1)}) = ∅ ↔ ¬ (𝑥 + 1) ∈ (1...𝑥))
411409, 410sylib 209 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ¬ (𝑥 + 1) ∈ (1...𝑥))
41244adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
413412, 350ffvelrnd 6552 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) ∈ (ℝ* ∖ {-∞}))
414 2fveq3 6382 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑥 + 1) → (𝐸‘(𝑔𝑗)) = (𝐸‘(𝑔‘(𝑥 + 1))))
41565, 400, 333, 334, 407, 320, 411, 413, 414gsumunsn 18628 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔𝑗)))) = ((𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗)))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
416296adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))))
417416, 337reseq12d 5568 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...(𝑥 + 1))) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ ((1...𝑥) ∪ {(𝑥 + 1)})))
418342resmptd 5631 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ ((1...𝑥) ∪ {(𝑥 + 1)})) = (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔𝑗))))
419417, 418eqtrd 2799 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...(𝑥 + 1))) = (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔𝑗))))
420419oveq2d 6860 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))) = (𝑊 Σg (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔𝑗)))))
421416reseq1d 5566 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...𝑥)) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ (1...𝑥)))
422343resmptd 5631 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ (1...𝑥)) = (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗))))
423421, 422eqtrd 2799 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...𝑥)) = (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗))))
424423oveq2d 6860 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) = (𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗)))))
425424oveq1d 6859 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) = ((𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗)))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
426415, 420, 4253eqtr4d 2809 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))) = ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
427426breq2d 4823 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))) ↔ (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
428396, 427sylibrd 250 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))
429324, 428animpimp2impd 872 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℕ → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))))) → (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))))
430248, 257, 266, 275, 317, 429nnind 11296 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))))
431228, 430mpcom 38 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛)))))
432230, 431mpd 15 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))
433238, 432eqbrtrrd 4835 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸𝑌) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))
434 ffn 6225 . . . . . . . . . . . . . 14 ((𝐸𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}) → (𝐸𝑔) Fn (1...𝑛))
435 fnresdm 6180 . . . . . . . . . . . . . 14 ((𝐸𝑔) Fn (1...𝑛) → ((𝐸𝑔) ↾ (1...𝑛)) = (𝐸𝑔))
43652, 434, 4353syl 18 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐸𝑔) ↾ (1...𝑛)) = (𝐸𝑔))
437436oveq2d 6860 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))) = (𝑊 Σg (𝐸𝑔)))
43863, 437eqtr4d 2802 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ*𝑠 Σg (𝐸𝑔)) = (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))
439433, 438breqtrrd 4839 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸𝑌) ≤ (ℝ*𝑠 Σg (𝐸𝑔)))
440 breq2 4815 . . . . . . . . . 10 (𝑝 = (ℝ*𝑠 Σg (𝐸𝑔)) → ((𝑋𝐸𝑌) ≤ 𝑝 ↔ (𝑋𝐸𝑌) ≤ (ℝ*𝑠 Σg (𝐸𝑔))))
441439, 440syl5ibrcom 238 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑝 = (ℝ*𝑠 Σg (𝐸𝑔)) → (𝑋𝐸𝑌) ≤ 𝑝))
442441rexlimdva 3178 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (∃𝑔𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸𝑔)) → (𝑋𝐸𝑌) ≤ 𝑝))
443220, 442syl5bi 233 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) → (𝑋𝐸𝑌) ≤ 𝑝))
444443rexlimdva 3178 . . . . . 6 (𝜑 → (∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) → (𝑋𝐸𝑌) ≤ 𝑝))
445217, 444syl5bi 233 . . . . 5 (𝜑 → (𝑝𝑇 → (𝑋𝐸𝑌) ≤ 𝑝))
446445ralrimiv 3112 . . . 4 (𝜑 → ∀𝑝𝑇 (𝑋𝐸𝑌) ≤ 𝑝)
447 infxrgelb 12370 . . . . 5 ((𝑇 ⊆ ℝ* ∧ (𝑋𝐸𝑌) ∈ ℝ*) → ((𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ) ↔ ∀𝑝𝑇 (𝑋𝐸𝑌) ≤ 𝑝))
44880, 84, 447syl2anc 579 . . . 4 (𝜑 → ((𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ) ↔ ∀𝑝𝑇 (𝑋𝐸𝑌) ≤ 𝑝))
449446, 448mpbird 248 . . 3 (𝜑 → (𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ))
45082, 84, 214, 449xrletrid 12191 . 2 (𝜑 → inf(𝑇, ℝ*, < ) = (𝑋𝐸𝑌))
45120, 450eqtrd 2799 1 (𝜑 → ((𝐹𝑋)𝐷(𝐹𝑌)) = (𝑋𝐸𝑌))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056  {crab 3059  Vcvv 3350  cdif 3731  cun 3732  cin 3733  wss 3734  c0 4081  {csn 4336  cop 4342   ciun 4678   class class class wbr 4811  cmpt 4890   × cxp 5277  ran crn 5280  cres 5281  ccom 5283   Fn wfn 6065  wf 6066  1-1wf1 6067  ontowfo 6068  1-1-ontowf1o 6069  cfv 6070  (class class class)co 6844  1st c1st 7366  2nd c2nd 7367  𝑚 cmap 8062  Fincfn 8162  infcinf 8556  cr 10190  0cc0 10191  1c1 10192   + caddc 10194  -∞cmnf 10328  *cxr 10329   < clt 10330  cle 10331  cmin 10522  cn 11276  cz 11626  cuz 11889   +𝑒 cxad 12147  ...cfz 12536  Basecbs 16133  s cress 16134  +gcplusg 16217  distcds 16226   Σg cgsu 16370  *𝑠cxrs 16429  s cimas 16433  Mndcmnd 17563  CMndccmn 18462  ∞Metcxmet 20007
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149  ax-inf2 8755  ax-cnex 10247  ax-resscn 10248  ax-1cn 10249  ax-icn 10250  ax-addcl 10251  ax-addrcl 10252  ax-mulcl 10253  ax-mulrcl 10254  ax-mulcom 10255  ax-addass 10256  ax-mulass 10257  ax-distr 10258  ax-i2m1 10259  ax-1ne0 10260  ax-1rid 10261  ax-rnegex 10262  ax-rrecex 10263  ax-cnre 10264  ax-pre-lttri 10265  ax-pre-lttrn 10266  ax-pre-ltadd 10267  ax-pre-mulgt0 10268  ax-pre-sup 10269
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-iin 4681  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-se 5239  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-isom 6079  df-riota 6805  df-ov 6847  df-oprab 6848  df-mpt2 6849  df-of 7097  df-om 7266  df-1st 7368  df-2nd 7369  df-supp 7500  df-wrecs 7612  df-recs 7674  df-rdg 7712  df-1o 7766  df-oadd 7770  df-er 7949  df-map 8064  df-en 8163  df-dom 8164  df-sdom 8165  df-fin 8166  df-fsupp 8485  df-sup 8557  df-inf 8558  df-oi 8624  df-card 9018  df-pnf 10332  df-mnf 10333  df-xr 10334  df-ltxr 10335  df-le 10336  df-sub 10524  df-neg 10525  df-div 10941  df-nn 11277  df-2 11337  df-3 11338  df-4 11339  df-5 11340  df-6 11341  df-7 11342  df-8 11343  df-9 11344  df-n0 11541  df-z 11627  df-dec 11744  df-uz 11890  df-rp 12032  df-xneg 12149  df-xadd 12150  df-xmul 12151  df-fz 12537  df-fzo 12677  df-seq 13012  df-hash 13325  df-struct 16135  df-ndx 16136  df-slot 16137  df-base 16139  df-sets 16140  df-ress 16141  df-plusg 16230  df-mulr 16231  df-sca 16233  df-vsca 16234  df-ip 16235  df-tset 16236  df-ple 16237  df-ds 16239  df-0g 16371  df-gsum 16372  df-xrs 16431  df-imas 16437  df-mre 16515  df-mrc 16516  df-acs 16518  df-mgm 17511  df-sgrp 17553  df-mnd 17564  df-submnd 17605  df-mulg 17811  df-cntz 18016  df-cmn 18464  df-xmet 20015
This theorem is referenced by:  imasdsf1o  22461
  Copyright terms: Public domain W3C validator