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

Theorem imasdsf1olem 22912
Description: Lemma for imasdsf1o 22913. (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 𝑆 = { ∈ ((𝑉 × 𝑉) ↑m (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 6616 . . . . 5 (𝐹:𝑉1-1-onto𝐵𝐹:𝑉onto𝐵)
53, 4syl 17 . . . 4 (𝜑𝐹:𝑉onto𝐵)
6 imasdsf1o.r . . . 4 (𝜑𝑅𝑍)
7 eqid 2821 . . . 4 (dist‘𝑅) = (dist‘𝑅)
8 imasdsf1o.d . . . 4 𝐷 = (dist‘𝑈)
9 f1of 6609 . . . . . 6 (𝐹:𝑉1-1-onto𝐵𝐹:𝑉𝐵)
103, 9syl 17 . . . . 5 (𝜑𝐹:𝑉𝐵)
11 imasdsf1o.x . . . . 5 (𝜑𝑋𝑉)
1210, 11ffvelrnd 6845 . . . 4 (𝜑 → (𝐹𝑋) ∈ 𝐵)
13 imasdsf1o.y . . . . 5 (𝜑𝑌𝑉)
1410, 13ffvelrnd 6845 . . . 4 (𝜑 → (𝐹𝑌) ∈ 𝐵)
15 imasdsf1o.s . . . 4 𝑆 = { ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))}
16 imasdsf1o.e . . . 4 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))
171, 2, 5, 6, 7, 8, 12, 14, 15, 16imasdsval2 16779 . . 3 (𝜑 → ((𝐹𝑋)𝐷(𝐹𝑌)) = inf( 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < ))
18 imasdsf1o.t . . . 4 𝑇 = 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔)))
1918infeq1i 8931 . . 3 inf(𝑇, ℝ*, < ) = inf( 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < )
2017, 19syl6eqr 2874 . 2 (𝜑 → ((𝐹𝑋)𝐷(𝐹𝑌)) = inf(𝑇, ℝ*, < ))
21 xrsbas 20491 . . . . . . . . . . . 12 * = (Base‘ℝ*𝑠)
22 xrsadd 20492 . . . . . . . . . . . 12 +𝑒 = (+g‘ℝ*𝑠)
23 imasdsf1o.w . . . . . . . . . . . 12 𝑊 = (ℝ*𝑠s (ℝ* ∖ {-∞}))
24 xrsex 20490 . . . . . . . . . . . . 13 *𝑠 ∈ V
2524a1i 11 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ℝ*𝑠 ∈ V)
26 fzfid 13331 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1...𝑛) ∈ Fin)
27 difss 4107 . . . . . . . . . . . . 13 (ℝ* ∖ {-∞}) ⊆ ℝ*
2827a1i 11 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ* ∖ {-∞}) ⊆ ℝ*)
29 imasdsf1o.m . . . . . . . . . . . . . . . 16 (𝜑𝐸 ∈ (∞Met‘𝑉))
30 xmetf 22868 . . . . . . . . . . . . . . . 16 (𝐸 ∈ (∞Met‘𝑉) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
31 ffn 6508 . . . . . . . . . . . . . . . 16 (𝐸:(𝑉 × 𝑉)⟶ℝ*𝐸 Fn (𝑉 × 𝑉))
3229, 30, 313syl 18 . . . . . . . . . . . . . . 15 (𝜑𝐸 Fn (𝑉 × 𝑉))
33 xmetcl 22870 . . . . . . . . . . . . . . . . . . 19 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓𝑉𝑔𝑉) → (𝑓𝐸𝑔) ∈ ℝ*)
34 xmetge0 22883 . . . . . . . . . . . . . . . . . . . 20 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓𝑉𝑔𝑉) → 0 ≤ (𝑓𝐸𝑔))
35 ge0nemnf 12556 . . . . . . . . . . . . . . . . . . . 20 (((𝑓𝐸𝑔) ∈ ℝ* ∧ 0 ≤ (𝑓𝐸𝑔)) → (𝑓𝐸𝑔) ≠ -∞)
3633, 34, 35syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓𝑉𝑔𝑉) → (𝑓𝐸𝑔) ≠ -∞)
37 eldifsn 4713 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}) ↔ ((𝑓𝐸𝑔) ∈ ℝ* ∧ (𝑓𝐸𝑔) ≠ -∞))
3833, 36, 37sylanbrc 583 . . . . . . . . . . . . . . . . . 18 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓𝑉𝑔𝑉) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
39383expb 1112 . . . . . . . . . . . . . . . . 17 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓𝑉𝑔𝑉)) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
4029, 39sylan 580 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑓𝑉𝑔𝑉)) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
4140ralrimivva 3191 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑓𝑉𝑔𝑉 (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
42 ffnov 7267 . . . . . . . . . . . . . . 15 (𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}) ↔ (𝐸 Fn (𝑉 × 𝑉) ∧ ∀𝑓𝑉𝑔𝑉 (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞})))
4332, 41, 42sylanbrc 583 . . . . . . . . . . . . . 14 (𝜑𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
4443ad2antrr 722 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
4515ssrab3 4056 . . . . . . . . . . . . . . . 16 𝑆 ⊆ ((𝑉 × 𝑉) ↑m (1...𝑛))
4645a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → 𝑆 ⊆ ((𝑉 × 𝑉) ↑m (1...𝑛)))
4746sselda 3966 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑔 ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)))
48 elmapi 8418 . . . . . . . . . . . . . 14 (𝑔 ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
4947, 48syl 17 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
50 fco 6525 . . . . . . . . . . . . 13 ((𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}) ∧ 𝑔:(1...𝑛)⟶(𝑉 × 𝑉)) → (𝐸𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
5144, 49, 50syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
52 0re 10632 . . . . . . . . . . . . 13 0 ∈ ℝ
53 rexr 10676 . . . . . . . . . . . . . 14 (0 ∈ ℝ → 0 ∈ ℝ*)
54 renemnf 10679 . . . . . . . . . . . . . 14 (0 ∈ ℝ → 0 ≠ -∞)
55 eldifsn 4713 . . . . . . . . . . . . . 14 (0 ∈ (ℝ* ∖ {-∞}) ↔ (0 ∈ ℝ* ∧ 0 ≠ -∞))
5653, 54, 55sylanbrc 583 . . . . . . . . . . . . 13 (0 ∈ ℝ → 0 ∈ (ℝ* ∖ {-∞}))
5752, 56mp1i 13 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 0 ∈ (ℝ* ∖ {-∞}))
58 xaddid2 12625 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ* → (0 +𝑒 𝑥) = 𝑥)
59 xaddid1 12624 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ* → (𝑥 +𝑒 0) = 𝑥)
6058, 59jca 512 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ* → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
6160adantl 482 . . . . . . . . . . . 12 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℝ*) → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
6221, 22, 23, 25, 26, 28, 51, 57, 61gsumress 17882 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ*𝑠 Σg (𝐸𝑔)) = (𝑊 Σg (𝐸𝑔)))
6323, 21ressbas2 16545 . . . . . . . . . . . . 13 ((ℝ* ∖ {-∞}) ⊆ ℝ* → (ℝ* ∖ {-∞}) = (Base‘𝑊))
6427, 63ax-mp 5 . . . . . . . . . . . 12 (ℝ* ∖ {-∞}) = (Base‘𝑊)
6523xrs10 20514 . . . . . . . . . . . 12 0 = (0g𝑊)
6623xrs1cmn 20515 . . . . . . . . . . . . 13 𝑊 ∈ CMnd
6766a1i 11 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑊 ∈ CMnd)
68 c0ex 10624 . . . . . . . . . . . . . 14 0 ∈ V
6968a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 0 ∈ V)
7051, 26, 69fdmfifsupp 8832 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸𝑔) finSupp 0)
7164, 65, 67, 26, 51, 70gsumcl 18966 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg (𝐸𝑔)) ∈ (ℝ* ∖ {-∞}))
7262, 71eqeltrd 2913 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ*𝑠 Σg (𝐸𝑔)) ∈ (ℝ* ∖ {-∞}))
7372eldifad 3947 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ*𝑠 Σg (𝐸𝑔)) ∈ ℝ*)
7473fmpttd 6872 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))):𝑆⟶ℝ*)
7574frnd 6515 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
7675ralrimiva 3182 . . . . . 6 (𝜑 → ∀𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
77 iunss 4961 . . . . . 6 ( 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ* ↔ ∀𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
7876, 77sylibr 235 . . . . 5 (𝜑 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
7918, 78eqsstrid 4014 . . . 4 (𝜑𝑇 ⊆ ℝ*)
80 infxrcl 12716 . . . 4 (𝑇 ⊆ ℝ* → inf(𝑇, ℝ*, < ) ∈ ℝ*)
8179, 80syl 17 . . 3 (𝜑 → inf(𝑇, ℝ*, < ) ∈ ℝ*)
82 xmetcl 22870 . . . 4 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉𝑌𝑉) → (𝑋𝐸𝑌) ∈ ℝ*)
8329, 11, 13, 82syl3anc 1363 . . 3 (𝜑 → (𝑋𝐸𝑌) ∈ ℝ*)
84 1nn 11638 . . . . . . 7 1 ∈ ℕ
85 1ex 10626 . . . . . . . . . . . 12 1 ∈ V
86 opex 5348 . . . . . . . . . . . 12 𝑋, 𝑌⟩ ∈ V
8785, 86f1osn 6648 . . . . . . . . . . 11 {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}–1-1-onto→{⟨𝑋, 𝑌⟩}
88 f1of 6609 . . . . . . . . . . 11 ({⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}–1-1-onto→{⟨𝑋, 𝑌⟩} → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩})
8987, 88ax-mp 5 . . . . . . . . . 10 {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩}
9011, 13opelxpd 5587 . . . . . . . . . . 11 (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉))
9190snssd 4736 . . . . . . . . . 10 (𝜑 → {⟨𝑋, 𝑌⟩} ⊆ (𝑉 × 𝑉))
92 fss 6521 . . . . . . . . . 10 (({⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩} ∧ {⟨𝑋, 𝑌⟩} ⊆ (𝑉 × 𝑉)) → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉))
9389, 91, 92sylancr 587 . . . . . . . . 9 (𝜑 → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉))
9429elfvexd 6698 . . . . . . . . . . 11 (𝜑𝑉 ∈ V)
9594, 94xpexd 7462 . . . . . . . . . 10 (𝜑 → (𝑉 × 𝑉) ∈ V)
96 snex 5323 . . . . . . . . . 10 {1} ∈ V
97 elmapg 8409 . . . . . . . . . 10 (((𝑉 × 𝑉) ∈ V ∧ {1} ∈ V) → ({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑m {1}) ↔ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉)))
9895, 96, 97sylancl 586 . . . . . . . . 9 (𝜑 → ({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑m {1}) ↔ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉)))
9993, 98mpbird 258 . . . . . . . 8 (𝜑 → {⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑m {1}))
100 op1stg 7692 . . . . . . . . . . 11 ((𝑋𝑉𝑌𝑉) → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋)
10111, 13, 100syl2anc 584 . . . . . . . . . 10 (𝜑 → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋)
102101fveq2d 6668 . . . . . . . . 9 (𝜑 → (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋))
103 op2ndg 7693 . . . . . . . . . . 11 ((𝑋𝑉𝑌𝑉) → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
10411, 13, 103syl2anc 584 . . . . . . . . . 10 (𝜑 → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
105104fveq2d 6668 . . . . . . . . 9 (𝜑 → (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌))
106102, 105jca 512 . . . . . . . 8 (𝜑 → ((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌)))
10724a1i 11 . . . . . . . . . 10 (𝜑 → ℝ*𝑠 ∈ V)
108 snfi 8583 . . . . . . . . . . 11 {1} ∈ Fin
109108a1i 11 . . . . . . . . . 10 (𝜑 → {1} ∈ Fin)
11027a1i 11 . . . . . . . . . 10 (𝜑 → (ℝ* ∖ {-∞}) ⊆ ℝ*)
111 xmetge0 22883 . . . . . . . . . . . . . . 15 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉𝑌𝑉) → 0 ≤ (𝑋𝐸𝑌))
11229, 11, 13, 111syl3anc 1363 . . . . . . . . . . . . . 14 (𝜑 → 0 ≤ (𝑋𝐸𝑌))
113 ge0nemnf 12556 . . . . . . . . . . . . . 14 (((𝑋𝐸𝑌) ∈ ℝ* ∧ 0 ≤ (𝑋𝐸𝑌)) → (𝑋𝐸𝑌) ≠ -∞)
11483, 112, 113syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → (𝑋𝐸𝑌) ≠ -∞)
115 eldifsn 4713 . . . . . . . . . . . . 13 ((𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}) ↔ ((𝑋𝐸𝑌) ∈ ℝ* ∧ (𝑋𝐸𝑌) ≠ -∞))
11683, 114, 115sylanbrc 583 . . . . . . . . . . . 12 (𝜑 → (𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}))
117 fconst6g 6562 . . . . . . . . . . . 12 ((𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}) → ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞}))
118116, 117syl 17 . . . . . . . . . . 11 (𝜑 → ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞}))
119 fcoconst 6889 . . . . . . . . . . . . . 14 ((𝐸 Fn (𝑉 × 𝑉) ∧ ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉)) → (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}))
12032, 90, 119syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}))
12185, 86xpsn 6896 . . . . . . . . . . . . . 14 ({1} × {⟨𝑋, 𝑌⟩}) = {⟨1, ⟨𝑋, 𝑌⟩⟩}
122121coeq2i 5725 . . . . . . . . . . . . 13 (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})
123 df-ov 7148 . . . . . . . . . . . . . . . 16 (𝑋𝐸𝑌) = (𝐸‘⟨𝑋, 𝑌⟩)
124123eqcomi 2830 . . . . . . . . . . . . . . 15 (𝐸‘⟨𝑋, 𝑌⟩) = (𝑋𝐸𝑌)
125124sneqi 4570 . . . . . . . . . . . . . 14 {(𝐸‘⟨𝑋, 𝑌⟩)} = {(𝑋𝐸𝑌)}
126125xpeq2i 5576 . . . . . . . . . . . . 13 ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}) = ({1} × {(𝑋𝐸𝑌)})
127120, 122, 1263eqtr3g 2879 . . . . . . . . . . . 12 (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}) = ({1} × {(𝑋𝐸𝑌)}))
128127feq1d 6493 . . . . . . . . . . 11 (𝜑 → ((𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}):{1}⟶(ℝ* ∖ {-∞}) ↔ ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞})))
129118, 128mpbird 258 . . . . . . . . . 10 (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}):{1}⟶(ℝ* ∖ {-∞}))
13052, 56mp1i 13 . . . . . . . . . 10 (𝜑 → 0 ∈ (ℝ* ∖ {-∞}))
13160adantl 482 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ*) → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
13221, 22, 23, 107, 109, 110, 129, 130, 131gsumress 17882 . . . . . . . . 9 (𝜑 → (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})) = (𝑊 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
133 fconstmpt 5608 . . . . . . . . . . 11 ({1} × {(𝑋𝐸𝑌)}) = (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))
134127, 133syl6eq 2872 . . . . . . . . . 10 (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}) = (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌)))
135134oveq2d 7161 . . . . . . . . 9 (𝜑 → (𝑊 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})) = (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))))
136 cmnmnd 18853 . . . . . . . . . . 11 (𝑊 ∈ CMnd → 𝑊 ∈ Mnd)
13766, 136mp1i 13 . . . . . . . . . 10 (𝜑𝑊 ∈ Mnd)
13884a1i 11 . . . . . . . . . 10 (𝜑 → 1 ∈ ℕ)
139 eqidd 2822 . . . . . . . . . . 11 (𝑗 = 1 → (𝑋𝐸𝑌) = (𝑋𝐸𝑌))
14064, 139gsumsn 19005 . . . . . . . . . 10 ((𝑊 ∈ Mnd ∧ 1 ∈ ℕ ∧ (𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞})) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))) = (𝑋𝐸𝑌))
141137, 138, 116, 140syl3anc 1363 . . . . . . . . 9 (𝜑 → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))) = (𝑋𝐸𝑌))
142132, 135, 1413eqtrrd 2861 . . . . . . . 8 (𝜑 → (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
143 fveq1 6663 . . . . . . . . . . . . . 14 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝑔‘1) = ({⟨1, ⟨𝑋, 𝑌⟩⟩}‘1))
14485, 86fvsn 6936 . . . . . . . . . . . . . 14 ({⟨1, ⟨𝑋, 𝑌⟩⟩}‘1) = ⟨𝑋, 𝑌
145143, 144syl6eq 2872 . . . . . . . . . . . . 13 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝑔‘1) = ⟨𝑋, 𝑌⟩)
146145fveq2d 6668 . . . . . . . . . . . 12 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (1st ‘(𝑔‘1)) = (1st ‘⟨𝑋, 𝑌⟩))
147146fveqeq2d 6672 . . . . . . . . . . 11 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ↔ (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋)))
148145fveq2d 6668 . . . . . . . . . . . 12 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (2nd ‘(𝑔‘1)) = (2nd ‘⟨𝑋, 𝑌⟩))
149148fveqeq2d 6672 . . . . . . . . . . 11 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌) ↔ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌)))
150147, 149anbi12d 630 . . . . . . . . . 10 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ↔ ((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌))))
151 coeq2 5723 . . . . . . . . . . . 12 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝐸𝑔) = (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}))
152151oveq2d 7161 . . . . . . . . . . 11 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (ℝ*𝑠 Σg (𝐸𝑔)) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
153152eqeq2d 2832 . . . . . . . . . 10 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}))))
154150, 153anbi12d 630 . . . . . . . . 9 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))) ↔ (((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))))
155154rspcev 3622 . . . . . . . 8 (({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑m {1}) ∧ (((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))) → ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
15699, 106, 142, 155syl12anc 832 . . . . . . 7 (𝜑 → ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
157 ovex 7178 . . . . . . . . . 10 (𝑋𝐸𝑌) ∈ V
158 eqid 2821 . . . . . . . . . . 11 (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) = (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔)))
159158elrnmpt 5822 . . . . . . . . . 10 ((𝑋𝐸𝑌) ∈ V → ((𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
160157, 159ax-mp 5 . . . . . . . . 9 ((𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))
16115rexeqi 3415 . . . . . . . . . . 11 (∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ ∃𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))
162 fveq1 6663 . . . . . . . . . . . . . . 15 ( = 𝑔 → (‘1) = (𝑔‘1))
163162fveq2d 6668 . . . . . . . . . . . . . 14 ( = 𝑔 → (1st ‘(‘1)) = (1st ‘(𝑔‘1)))
164163fveqeq2d 6672 . . . . . . . . . . . . 13 ( = 𝑔 → ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ↔ (𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋)))
165 fveq1 6663 . . . . . . . . . . . . . . 15 ( = 𝑔 → (𝑛) = (𝑔𝑛))
166165fveq2d 6668 . . . . . . . . . . . . . 14 ( = 𝑔 → (2nd ‘(𝑛)) = (2nd ‘(𝑔𝑛)))
167166fveqeq2d 6672 . . . . . . . . . . . . 13 ( = 𝑔 → ((𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ↔ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)))
168 fveq1 6663 . . . . . . . . . . . . . . . . 17 ( = 𝑔 → (𝑖) = (𝑔𝑖))
169168fveq2d 6668 . . . . . . . . . . . . . . . 16 ( = 𝑔 → (2nd ‘(𝑖)) = (2nd ‘(𝑔𝑖)))
170169fveq2d 6668 . . . . . . . . . . . . . . 15 ( = 𝑔 → (𝐹‘(2nd ‘(𝑖))) = (𝐹‘(2nd ‘(𝑔𝑖))))
171 fveq1 6663 . . . . . . . . . . . . . . . . 17 ( = 𝑔 → (‘(𝑖 + 1)) = (𝑔‘(𝑖 + 1)))
172171fveq2d 6668 . . . . . . . . . . . . . . . 16 ( = 𝑔 → (1st ‘(‘(𝑖 + 1))) = (1st ‘(𝑔‘(𝑖 + 1))))
173172fveq2d 6668 . . . . . . . . . . . . . . 15 ( = 𝑔 → (𝐹‘(1st ‘(‘(𝑖 + 1)))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
174170, 173eqeq12d 2837 . . . . . . . . . . . . . 14 ( = 𝑔 → ((𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
175174ralbidv 3197 . . . . . . . . . . . . 13 ( = 𝑔 → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
176164, 167, 1753anbi123d 1427 . . . . . . . . . . . 12 ( = 𝑔 → (((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
177176rexrab 3686 . . . . . . . . . . 11 (∃𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
178161, 177bitri 276 . . . . . . . . . 10 (∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
179 oveq2 7153 . . . . . . . . . . . . 13 (𝑛 = 1 → (1...𝑛) = (1...1))
180 1z 12001 . . . . . . . . . . . . . 14 1 ∈ ℤ
181 fzsn 12939 . . . . . . . . . . . . . 14 (1 ∈ ℤ → (1...1) = {1})
182180, 181ax-mp 5 . . . . . . . . . . . . 13 (1...1) = {1}
183179, 182syl6eq 2872 . . . . . . . . . . . 12 (𝑛 = 1 → (1...𝑛) = {1})
184183oveq2d 7161 . . . . . . . . . . 11 (𝑛 = 1 → ((𝑉 × 𝑉) ↑m (1...𝑛)) = ((𝑉 × 𝑉) ↑m {1}))
185 df-3an 1081 . . . . . . . . . . . . 13 (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
186 ral0 4454 . . . . . . . . . . . . . . . 16 𝑖 ∈ ∅ (𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))
187 oveq1 7152 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → (𝑛 − 1) = (1 − 1))
188 1m1e0 11698 . . . . . . . . . . . . . . . . . . . 20 (1 − 1) = 0
189187, 188syl6eq 2872 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → (𝑛 − 1) = 0)
190189oveq2d 7161 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → (1...(𝑛 − 1)) = (1...0))
191 fz10 12918 . . . . . . . . . . . . . . . . . 18 (1...0) = ∅
192190, 191syl6eq 2872 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → (1...(𝑛 − 1)) = ∅)
193192raleqdv 3416 . . . . . . . . . . . . . . . 16 (𝑛 = 1 → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ ∅ (𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
194186, 193mpbiri 259 . . . . . . . . . . . . . . 15 (𝑛 = 1 → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
195194biantrud 532 . . . . . . . . . . . . . 14 (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
196 2fveq3 6669 . . . . . . . . . . . . . . . 16 (𝑛 = 1 → (2nd ‘(𝑔𝑛)) = (2nd ‘(𝑔‘1)))
197196fveqeq2d 6672 . . . . . . . . . . . . . . 15 (𝑛 = 1 → ((𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ↔ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)))
198197anbi2d 628 . . . . . . . . . . . . . 14 (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌))))
199195, 198bitr3d 282 . . . . . . . . . . . . 13 (𝑛 = 1 → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌))))
200185, 199syl5bb 284 . . . . . . . . . . . 12 (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌))))
201200anbi1d 629 . . . . . . . . . . 11 (𝑛 = 1 → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))))
202184, 201rexeqbidv 3403 . . . . . . . . . 10 (𝑛 = 1 → (∃𝑔 ∈ ((𝑉 × 𝑉) ↑m (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))))
203178, 202syl5bb 284 . . . . . . . . 9 (𝑛 = 1 → (∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))))
204160, 203syl5bb 284 . . . . . . . 8 (𝑛 = 1 → ((𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))))
205204rspcev 3622 . . . . . . 7 ((1 ∈ ℕ ∧ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))) → ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
20684, 156, 205sylancr 587 . . . . . 6 (𝜑 → ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
207 eliun 4916 . . . . . 6 ((𝑋𝐸𝑌) ∈ 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
208206, 207sylibr 235 . . . . 5 (𝜑 → (𝑋𝐸𝑌) ∈ 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
209208, 18eleqtrrdi 2924 . . . 4 (𝜑 → (𝑋𝐸𝑌) ∈ 𝑇)
210 infxrlb 12717 . . . 4 ((𝑇 ⊆ ℝ* ∧ (𝑋𝐸𝑌) ∈ 𝑇) → inf(𝑇, ℝ*, < ) ≤ (𝑋𝐸𝑌))
21179, 209, 210syl2anc 584 . . 3 (𝜑 → inf(𝑇, ℝ*, < ) ≤ (𝑋𝐸𝑌))
21218eleq2i 2904 . . . . . . 7 (𝑝𝑇𝑝 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
213 eliun 4916 . . . . . . 7 (𝑝 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
214212, 213bitri 276 . . . . . 6 (𝑝𝑇 ↔ ∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
215158elrnmpt 5822 . . . . . . . . 9 (𝑝 ∈ V → (𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸𝑔))))
216215elv 3500 . . . . . . . 8 (𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸𝑔)))
217176, 15elrab2 3682 . . . . . . . . . . . . . . . . 17 (𝑔𝑆 ↔ (𝑔 ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∧ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
218217simprbi 497 . . . . . . . . . . . . . . . 16 (𝑔𝑆 → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
219218adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
220219simp2d 1135 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌))
2213ad2antrr 722 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐹:𝑉1-1-onto𝐵)
222 f1of1 6608 . . . . . . . . . . . . . . . 16 (𝐹:𝑉1-1-onto𝐵𝐹:𝑉1-1𝐵)
223221, 222syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐹:𝑉1-1𝐵)
224 simplr 765 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑛 ∈ ℕ)
225 elfz1end 12927 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (1...𝑛))
226224, 225sylib 219 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑛 ∈ (1...𝑛))
22749, 226ffvelrnd 6845 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑔𝑛) ∈ (𝑉 × 𝑉))
228 xp2nd 7713 . . . . . . . . . . . . . . . 16 ((𝑔𝑛) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔𝑛)) ∈ 𝑉)
229227, 228syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (2nd ‘(𝑔𝑛)) ∈ 𝑉)
23013ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑌𝑉)
231 f1fveq 7011 . . . . . . . . . . . . . . 15 ((𝐹:𝑉1-1𝐵 ∧ ((2nd ‘(𝑔𝑛)) ∈ 𝑉𝑌𝑉)) → ((𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ↔ (2nd ‘(𝑔𝑛)) = 𝑌))
232223, 229, 230, 231syl12anc 832 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ↔ (2nd ‘(𝑔𝑛)) = 𝑌))
233220, 232mpbid 233 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (2nd ‘(𝑔𝑛)) = 𝑌)
234233oveq2d 7161 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔𝑛))) = (𝑋𝐸𝑌))
235 eleq1 2900 . . . . . . . . . . . . . . . . 17 (𝑚 = 1 → (𝑚 ∈ (1...𝑛) ↔ 1 ∈ (1...𝑛)))
236 2fveq3 6669 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 1 → (2nd ‘(𝑔𝑚)) = (2nd ‘(𝑔‘1)))
237236oveq2d 7161 . . . . . . . . . . . . . . . . . 18 (𝑚 = 1 → (𝑋𝐸(2nd ‘(𝑔𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘1))))
238 oveq2 7153 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 1 → (1...𝑚) = (1...1))
239238, 182syl6eq 2872 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 1 → (1...𝑚) = {1})
240239reseq2d 5847 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 1 → ((𝐸𝑔) ↾ (1...𝑚)) = ((𝐸𝑔) ↾ {1}))
241240oveq2d 7161 . . . . . . . . . . . . . . . . . 18 (𝑚 = 1 → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸𝑔) ↾ {1})))
242237, 241breq12d 5071 . . . . . . . . . . . . . . . . 17 (𝑚 = 1 → ((𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1}))))
243235, 242imbi12d 346 . . . . . . . . . . . . . . . 16 (𝑚 = 1 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚)))) ↔ (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1})))))
244243imbi2d 342 . . . . . . . . . . . . . . 15 (𝑚 = 1 → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))))) ↔ (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1}))))))
245 eleq1 2900 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑥 → (𝑚 ∈ (1...𝑛) ↔ 𝑥 ∈ (1...𝑛)))
246 2fveq3 6669 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑥 → (2nd ‘(𝑔𝑚)) = (2nd ‘(𝑔𝑥)))
247246oveq2d 7161 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑥 → (𝑋𝐸(2nd ‘(𝑔𝑚))) = (𝑋𝐸(2nd ‘(𝑔𝑥))))
248 oveq2 7153 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑥 → (1...𝑚) = (1...𝑥))
249248reseq2d 5847 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑥 → ((𝐸𝑔) ↾ (1...𝑚)) = ((𝐸𝑔) ↾ (1...𝑥)))
250249oveq2d 7161 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑥 → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))))
251247, 250breq12d 5071 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑥 → ((𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))))
252245, 251imbi12d 346 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑥 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚)))) ↔ (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))))))
253252imbi2d 342 . . . . . . . . . . . . . . 15 (𝑚 = 𝑥 → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))))) ↔ (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))))))
254 eleq1 2900 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑥 + 1) → (𝑚 ∈ (1...𝑛) ↔ (𝑥 + 1) ∈ (1...𝑛)))
255 2fveq3 6669 . . . . . . . . . . . . . . . . . . 19 (𝑚 = (𝑥 + 1) → (2nd ‘(𝑔𝑚)) = (2nd ‘(𝑔‘(𝑥 + 1))))
256255oveq2d 7161 . . . . . . . . . . . . . . . . . 18 (𝑚 = (𝑥 + 1) → (𝑋𝐸(2nd ‘(𝑔𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))))
257 oveq2 7153 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = (𝑥 + 1) → (1...𝑚) = (1...(𝑥 + 1)))
258257reseq2d 5847 . . . . . . . . . . . . . . . . . . 19 (𝑚 = (𝑥 + 1) → ((𝐸𝑔) ↾ (1...𝑚)) = ((𝐸𝑔) ↾ (1...(𝑥 + 1))))
259258oveq2d 7161 . . . . . . . . . . . . . . . . . 18 (𝑚 = (𝑥 + 1) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))))
260256, 259breq12d 5071 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑥 + 1) → ((𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))
261254, 260imbi12d 346 . . . . . . . . . . . . . . . 16 (𝑚 = (𝑥 + 1) → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚)))) ↔ ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))))))
262261imbi2d 342 . . . . . . . . . . . . . . 15 (𝑚 = (𝑥 + 1) → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))))) ↔ (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))))
263 eleq1 2900 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → (𝑚 ∈ (1...𝑛) ↔ 𝑛 ∈ (1...𝑛)))
264 2fveq3 6669 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → (2nd ‘(𝑔𝑚)) = (2nd ‘(𝑔𝑛)))
265264oveq2d 7161 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑛 → (𝑋𝐸(2nd ‘(𝑔𝑚))) = (𝑋𝐸(2nd ‘(𝑔𝑛))))
266 oveq2 7153 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
267266reseq2d 5847 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → ((𝐸𝑔) ↾ (1...𝑚)) = ((𝐸𝑔) ↾ (1...𝑛)))
268267oveq2d 7161 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑛 → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))
269265, 268breq12d 5071 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → ((𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛)))))
270263, 269imbi12d 346 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚)))) ↔ (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))))
271270imbi2d 342 . . . . . . . . . . . . . . 15 (𝑚 = 𝑛 → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))))) ↔ (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛)))))))
27229ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐸 ∈ (∞Met‘𝑉))
27311ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑋𝑉)
274 nnuz 12270 . . . . . . . . . . . . . . . . . . . . . . 23 ℕ = (ℤ‘1)
275224, 274eleqtrdi 2923 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑛 ∈ (ℤ‘1))
276 eluzfz1 12904 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (ℤ‘1) → 1 ∈ (1...𝑛))
277275, 276syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 1 ∈ (1...𝑛))
27849, 277ffvelrnd 6845 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑔‘1) ∈ (𝑉 × 𝑉))
279 xp2nd 7713 . . . . . . . . . . . . . . . . . . . 20 ((𝑔‘1) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘1)) ∈ 𝑉)
280278, 279syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (2nd ‘(𝑔‘1)) ∈ 𝑉)
281 xmetcl 22870 . . . . . . . . . . . . . . . . . . 19 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉 ∧ (2nd ‘(𝑔‘1)) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔‘1))) ∈ ℝ*)
282272, 273, 280, 281syl3anc 1363 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ∈ ℝ*)
283282xrleidd 12535 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑋𝐸(2nd ‘(𝑔‘1))))
284137ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑊 ∈ Mnd)
28584a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 1 ∈ ℕ)
28644, 278ffvelrnd 6845 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸‘(𝑔‘1)) ∈ (ℝ* ∖ {-∞}))
287 2fveq3 6669 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 1 → (𝐸‘(𝑔𝑗)) = (𝐸‘(𝑔‘1)))
28864, 287gsumsn 19005 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ Mnd ∧ 1 ∈ ℕ ∧ (𝐸‘(𝑔‘1)) ∈ (ℝ* ∖ {-∞})) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗)))) = (𝐸‘(𝑔‘1)))
289284, 285, 286, 288syl3anc 1363 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗)))) = (𝐸‘(𝑔‘1)))
290272, 30syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
291 fcompt 6888 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐸:(𝑉 × 𝑉)⟶ℝ*𝑔:(1...𝑛)⟶(𝑉 × 𝑉)) → (𝐸𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))))
292290, 49, 291syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))))
293292reseq1d 5846 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐸𝑔) ↾ {1}) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ {1}))
294277snssd 4736 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → {1} ⊆ (1...𝑛))
295294resmptd 5902 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ {1}) = (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗))))
296293, 295eqtrd 2856 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐸𝑔) ↾ {1}) = (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗))))
297296oveq2d 7161 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg ((𝐸𝑔) ↾ {1})) = (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗)))))
298 df-ov 7148 . . . . . . . . . . . . . . . . . . 19 (𝑋𝐸(2nd ‘(𝑔‘1))) = (𝐸‘⟨𝑋, (2nd ‘(𝑔‘1))⟩)
299 1st2nd2 7719 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔‘1) ∈ (𝑉 × 𝑉) → (𝑔‘1) = ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩)
300278, 299syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑔‘1) = ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩)
301219simp1d 1134 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋))
302 xp1st 7712 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔‘1) ∈ (𝑉 × 𝑉) → (1st ‘(𝑔‘1)) ∈ 𝑉)
303278, 302syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1st ‘(𝑔‘1)) ∈ 𝑉)
304 f1fveq 7011 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹:𝑉1-1𝐵 ∧ ((1st ‘(𝑔‘1)) ∈ 𝑉𝑋𝑉)) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ↔ (1st ‘(𝑔‘1)) = 𝑋))
305223, 303, 273, 304syl12anc 832 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ↔ (1st ‘(𝑔‘1)) = 𝑋))
306301, 305mpbid 233 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1st ‘(𝑔‘1)) = 𝑋)
307306opeq1d 4803 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩ = ⟨𝑋, (2nd ‘(𝑔‘1))⟩)
308300, 307eqtr2d 2857 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ⟨𝑋, (2nd ‘(𝑔‘1))⟩ = (𝑔‘1))
309308fveq2d 6668 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸‘⟨𝑋, (2nd ‘(𝑔‘1))⟩) = (𝐸‘(𝑔‘1)))
310298, 309syl5eq 2868 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) = (𝐸‘(𝑔‘1)))
311289, 297, 3103eqtr4d 2866 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg ((𝐸𝑔) ↾ {1})) = (𝑋𝐸(2nd ‘(𝑔‘1))))
312283, 311breqtrrd 5086 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1})))
313312a1d 25 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1}))))
314 simprl 767 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ ℕ)
315314, 274eleqtrdi 2923 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (ℤ‘1))
316 simprr 769 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑥 + 1) ∈ (1...𝑛))
317 peano2fzr 12910 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (ℤ‘1) ∧ (𝑥 + 1) ∈ (1...𝑛)) → 𝑥 ∈ (1...𝑛))
318315, 316, 317syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (1...𝑛))
319318expr 457 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 + 1) ∈ (1...𝑛) → 𝑥 ∈ (1...𝑛)))
320319imim1d 82 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))))))
321272adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸 ∈ (∞Met‘𝑉))
322273adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑋𝑉)
32349adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
324323, 318ffvelrnd 6845 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔𝑥) ∈ (𝑉 × 𝑉))
325 xp2nd 7713 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔𝑥) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔𝑥)) ∈ 𝑉)
326324, 325syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔𝑥)) ∈ 𝑉)
327 xmetcl 22870 . . . . . . . . . . . . . . . . . . . 20 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉 ∧ (2nd ‘(𝑔𝑥)) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ∈ ℝ*)
328321, 322, 326, 327syl3anc 1363 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ∈ ℝ*)
32966a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑊 ∈ CMnd)
330 fzfid 13331 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...𝑥) ∈ Fin)
33151adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
332 fzsuc 12944 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ (ℤ‘1) → (1...(𝑥 + 1)) = ((1...𝑥) ∪ {(𝑥 + 1)}))
333315, 332syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...(𝑥 + 1)) = ((1...𝑥) ∪ {(𝑥 + 1)}))
334 elfzuz3 12895 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 + 1) ∈ (1...𝑛) → 𝑛 ∈ (ℤ‘(𝑥 + 1)))
335334ad2antll 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑛 ∈ (ℤ‘(𝑥 + 1)))
336 fzss2 12937 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ (ℤ‘(𝑥 + 1)) → (1...(𝑥 + 1)) ⊆ (1...𝑛))
337335, 336syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...(𝑥 + 1)) ⊆ (1...𝑛))
338333, 337eqsstrrd 4005 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((1...𝑥) ∪ {(𝑥 + 1)}) ⊆ (1...𝑛))
339338unssad 4162 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...𝑥) ⊆ (1...𝑛))
340331, 339fssresd 6539 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...𝑥)):(1...𝑥)⟶(ℝ* ∖ {-∞}))
34168a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 0 ∈ V)
342340, 330, 341fdmfifsupp 8832 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...𝑥)) finSupp 0)
34364, 65, 329, 330, 340, 342gsumcl 18966 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) ∈ (ℝ* ∖ {-∞}))
344343eldifad 3947 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) ∈ ℝ*)
345321, 30syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
346323, 316ffvelrnd 6845 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉))
347345, 346ffvelrnd 6845 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*)
348 xleadd1a 12636 . . . . . . . . . . . . . . . . . . . 20 ((((𝑋𝐸(2nd ‘(𝑔𝑥))) ∈ ℝ* ∧ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) ∈ ℝ* ∧ (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*) ∧ (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
349348ex 413 . . . . . . . . . . . . . . . . . . 19 (((𝑋𝐸(2nd ‘(𝑔𝑥))) ∈ ℝ* ∧ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) ∈ ℝ* ∧ (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
350328, 344, 347, 349syl3anc 1363 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
351 xp2nd 7713 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
352346, 351syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
353 xmettri 22890 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑋𝑉 ∧ (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉 ∧ (2nd ‘(𝑔𝑥)) ∈ 𝑉)) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
354321, 322, 352, 326, 353syl13anc 1364 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
355 1st2nd2 7719 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (𝑔‘(𝑥 + 1)) = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
356346, 355syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
357 2fveq3 6669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑥 → (2nd ‘(𝑔𝑖)) = (2nd ‘(𝑔𝑥)))
358357fveq2d 6668 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 = 𝑥 → (𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(2nd ‘(𝑔𝑥))))
359 fvoveq1 7168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 = 𝑥 → (𝑔‘(𝑖 + 1)) = (𝑔‘(𝑥 + 1)))
360359fveq2d 6668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑥 → (1st ‘(𝑔‘(𝑖 + 1))) = (1st ‘(𝑔‘(𝑥 + 1))))
361360fveq2d 6668 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 = 𝑥 → (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))))
362358, 361eqeq12d 2837 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 = 𝑥 → ((𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(𝑔𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1))))))
363219simp3d 1136 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
364363adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
365 nnz 11993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℕ → 𝑥 ∈ ℤ)
366365ad2antrl 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ ℤ)
367 eluzp1m1 12257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑥 ∈ ℤ ∧ 𝑛 ∈ (ℤ‘(𝑥 + 1))) → (𝑛 − 1) ∈ (ℤ𝑥))
368366, 335, 367syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑛 − 1) ∈ (ℤ𝑥))
369 elfzuzb 12892 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ (1...(𝑛 − 1)) ↔ (𝑥 ∈ (ℤ‘1) ∧ (𝑛 − 1) ∈ (ℤ𝑥)))
370315, 368, 369sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (1...(𝑛 − 1)))
371362, 364, 370rspcdva 3624 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐹‘(2nd ‘(𝑔𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))))
372223adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐹:𝑉1-1𝐵)
373 xp1st 7712 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
374346, 373syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
375 f1fveq 7011 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹:𝑉1-1𝐵 ∧ ((2nd ‘(𝑔𝑥)) ∈ 𝑉 ∧ (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)) → ((𝐹‘(2nd ‘(𝑔𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))) ↔ (2nd ‘(𝑔𝑥)) = (1st ‘(𝑔‘(𝑥 + 1)))))
376372, 326, 374, 375syl12anc 832 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐹‘(2nd ‘(𝑔𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))) ↔ (2nd ‘(𝑔𝑥)) = (1st ‘(𝑔‘(𝑥 + 1)))))
377371, 376mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔𝑥)) = (1st ‘(𝑔‘(𝑥 + 1))))
378377opeq1d 4803 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ⟨(2nd ‘(𝑔𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩ = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
379356, 378eqtr4d 2859 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) = ⟨(2nd ‘(𝑔𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
380379fveq2d 6668 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) = (𝐸‘⟨(2nd ‘(𝑔𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩))
381 df-ov 7148 . . . . . . . . . . . . . . . . . . . . . 22 ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) = (𝐸‘⟨(2nd ‘(𝑔𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
382380, 381syl6eqr 2874 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) = ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1)))))
383382oveq2d 7161 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) = ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
384354, 383breqtrrd 5086 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
385 xmetcl 22870 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉 ∧ (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
386321, 322, 352, 385syl3anc 1363 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
387328, 347xaddcld 12684 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
388344, 347xaddcld 12684 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
389 xrletr 12541 . . . . . . . . . . . . . . . . . . . 20 (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ* ∧ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ* ∧ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*) → (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∧ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
390386, 387, 388, 389syl3anc 1363 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∧ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
391384, 390mpand 691 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
392350, 391syld 47 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
393 xrex 12376 . . . . . . . . . . . . . . . . . . . . . 22 * ∈ V
394393difexi 5224 . . . . . . . . . . . . . . . . . . . . 21 (ℝ* ∖ {-∞}) ∈ V
39523, 22ressplusg 16602 . . . . . . . . . . . . . . . . . . . . 21 ((ℝ* ∖ {-∞}) ∈ V → +𝑒 = (+g𝑊))
396394, 395ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 +𝑒 = (+g𝑊)
39744ad2antrr 722 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
398 fzelp1 12949 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ (1...𝑥) → 𝑗 ∈ (1...(𝑥 + 1)))
39949ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
400337sselda 3966 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → 𝑗 ∈ (1...𝑛))
401399, 400ffvelrnd 6845 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → (𝑔𝑗) ∈ (𝑉 × 𝑉))
402398, 401sylan2 592 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → (𝑔𝑗) ∈ (𝑉 × 𝑉))
403397, 402ffvelrnd 6845 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → (𝐸‘(𝑔𝑗)) ∈ (ℝ* ∖ {-∞}))
404 fzp1disj 12956 . . . . . . . . . . . . . . . . . . . . . 22 ((1...𝑥) ∩ {(𝑥 + 1)}) = ∅
405404a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((1...𝑥) ∩ {(𝑥 + 1)}) = ∅)
406 disjsn 4641 . . . . . . . . . . . . . . . . . . . . 21 (((1...𝑥) ∩ {(𝑥 + 1)}) = ∅ ↔ ¬ (𝑥 + 1) ∈ (1...𝑥))
407405, 406sylib 219 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ¬ (𝑥 + 1) ∈ (1...𝑥))
40844adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
409408, 346ffvelrnd 6845 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) ∈ (ℝ* ∖ {-∞}))
410 2fveq3 6669 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑥 + 1) → (𝐸‘(𝑔𝑗)) = (𝐸‘(𝑔‘(𝑥 + 1))))
41164, 396, 329, 330, 403, 316, 407, 409, 410gsumunsn 19011 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔𝑗)))) = ((𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗)))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
412292adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))))
413412, 333reseq12d 5848 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...(𝑥 + 1))) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ ((1...𝑥) ∪ {(𝑥 + 1)})))
414338resmptd 5902 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ ((1...𝑥) ∪ {(𝑥 + 1)})) = (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔𝑗))))
415413, 414eqtrd 2856 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...(𝑥 + 1))) = (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔𝑗))))
416415oveq2d 7161 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))) = (𝑊 Σg (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔𝑗)))))
417412reseq1d 5846 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...𝑥)) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ (1...𝑥)))
418339resmptd 5902 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ (1...𝑥)) = (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗))))
419417, 418eqtrd 2856 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...𝑥)) = (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗))))
420419oveq2d 7161 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) = (𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗)))))
421420oveq1d 7160 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) = ((𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗)))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
422411, 416, 4213eqtr4d 2866 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))) = ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
423422breq2d 5070 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))) ↔ (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
424392, 423sylibrd 260 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))
425320, 424animpimp2impd 840 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℕ → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))))) → (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))))
426244, 253, 262, 271, 313, 425nnind 11645 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))))
427224, 426mpcom 38 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛)))))
428226, 427mpd 15 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))
429234, 428eqbrtrrd 5082 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸𝑌) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))
430 ffn 6508 . . . . . . . . . . . . . 14 ((𝐸𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}) → (𝐸𝑔) Fn (1...𝑛))
431 fnresdm 6460 . . . . . . . . . . . . . 14 ((𝐸𝑔) Fn (1...𝑛) → ((𝐸𝑔) ↾ (1...𝑛)) = (𝐸𝑔))
43251, 430, 4313syl 18 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐸𝑔) ↾ (1...𝑛)) = (𝐸𝑔))
433432oveq2d 7161 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))) = (𝑊 Σg (𝐸𝑔)))
43462, 433eqtr4d 2859 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ*𝑠 Σg (𝐸𝑔)) = (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))
435429, 434breqtrrd 5086 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸𝑌) ≤ (ℝ*𝑠 Σg (𝐸𝑔)))
436 breq2 5062 . . . . . . . . . 10 (𝑝 = (ℝ*𝑠 Σg (𝐸𝑔)) → ((𝑋𝐸𝑌) ≤ 𝑝 ↔ (𝑋𝐸𝑌) ≤ (ℝ*𝑠 Σg (𝐸𝑔))))
437435, 436syl5ibrcom 248 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑝 = (ℝ*𝑠 Σg (𝐸𝑔)) → (𝑋𝐸𝑌) ≤ 𝑝))
438437rexlimdva 3284 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (∃𝑔𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸𝑔)) → (𝑋𝐸𝑌) ≤ 𝑝))
439216, 438syl5bi 243 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) → (𝑋𝐸𝑌) ≤ 𝑝))
440439rexlimdva 3284 . . . . . 6 (𝜑 → (∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) → (𝑋𝐸𝑌) ≤ 𝑝))
441214, 440syl5bi 243 . . . . 5 (𝜑 → (𝑝𝑇 → (𝑋𝐸𝑌) ≤ 𝑝))
442441ralrimiv 3181 . . . 4 (𝜑 → ∀𝑝𝑇 (𝑋𝐸𝑌) ≤ 𝑝)
443 infxrgelb 12718 . . . . 5 ((𝑇 ⊆ ℝ* ∧ (𝑋𝐸𝑌) ∈ ℝ*) → ((𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ) ↔ ∀𝑝𝑇 (𝑋𝐸𝑌) ≤ 𝑝))
44479, 83, 443syl2anc 584 . . . 4 (𝜑 → ((𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ) ↔ ∀𝑝𝑇 (𝑋𝐸𝑌) ≤ 𝑝))
445442, 444mpbird 258 . . 3 (𝜑 → (𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ))
44681, 83, 211, 445xrletrid 12538 . 2 (𝜑 → inf(𝑇, ℝ*, < ) = (𝑋𝐸𝑌))
44720, 446eqtrd 2856 1 (𝜑 → ((𝐹𝑋)𝐷(𝐹𝑌)) = (𝑋𝐸𝑌))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wcel 2105  wne 3016  wral 3138  wrex 3139  {crab 3142  Vcvv 3495  cdif 3932  cun 3933  cin 3934  wss 3935  c0 4290  {csn 4559  cop 4565   ciun 4912   class class class wbr 5058  cmpt 5138   × cxp 5547  ran crn 5550  cres 5551  ccom 5553   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  infcinf 8894  cr 10525  0cc0 10526  1c1 10527   + caddc 10529  -∞cmnf 10662  *cxr 10663   < clt 10664  cle 10665  cmin 10859  cn 11627  cz 11970  cuz 12232   +𝑒 cxad 12495  ...cfz 12882  Basecbs 16473  s cress 16474  +gcplusg 16555  distcds 16564   Σg cgsu 16704  *𝑠cxrs 16763  s cimas 16767  Mndcmnd 17901  CMndccmn 18837  ∞Metcxmet 20460
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-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  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-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-iin 4915  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-of 7398  df-om 7569  df-1st 7680  df-2nd 7681  df-supp 7822  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-fsupp 8823  df-sup 8895  df-inf 8896  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-4 11691  df-5 11692  df-6 11693  df-7 11694  df-8 11695  df-9 11696  df-n0 11887  df-z 11971  df-dec 12088  df-uz 12233  df-rp 12380  df-xneg 12497  df-xadd 12498  df-xmul 12499  df-fz 12883  df-fzo 13024  df-seq 13360  df-hash 13681  df-struct 16475  df-ndx 16476  df-slot 16477  df-base 16479  df-sets 16480  df-ress 16481  df-plusg 16568  df-mulr 16569  df-sca 16571  df-vsca 16572  df-ip 16573  df-tset 16574  df-ple 16575  df-ds 16577  df-0g 16705  df-gsum 16706  df-xrs 16765  df-imas 16771  df-mre 16847  df-mrc 16848  df-acs 16850  df-mgm 17842  df-sgrp 17891  df-mnd 17902  df-submnd 17947  df-mulg 18165  df-cntz 18387  df-cmn 18839  df-xmet 20468
This theorem is referenced by:  imasdsf1o  22913
  Copyright terms: Public domain W3C validator