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

Theorem imasdsf1olem 21988
 Description: Lemma for imasdsf1o 21989. (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 6057 . . . . 5 (𝐹:𝑉1-1-onto𝐵𝐹:𝑉onto𝐵)
53, 4syl 17 . . . 4 (𝜑𝐹:𝑉onto𝐵)
6 imasdsf1o.r . . . 4 (𝜑𝑅𝑍)
7 eqid 2610 . . . 4 (dist‘𝑅) = (dist‘𝑅)
8 imasdsf1o.d . . . 4 𝐷 = (dist‘𝑈)
9 f1of 6050 . . . . . 6 (𝐹:𝑉1-1-onto𝐵𝐹:𝑉𝐵)
103, 9syl 17 . . . . 5 (𝜑𝐹:𝑉𝐵)
11 imasdsf1o.x . . . . 5 (𝜑𝑋𝑉)
1210, 11ffvelrnd 6268 . . . 4 (𝜑 → (𝐹𝑋) ∈ 𝐵)
13 imasdsf1o.y . . . . 5 (𝜑𝑌𝑉)
1410, 13ffvelrnd 6268 . . . 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 15999 . . 3 (𝜑 → ((𝐹𝑋)𝐷(𝐹𝑌)) = inf( 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < ))
18 imasdsf1o.t . . . 4 𝑇 = 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔)))
1918infeq1i 8267 . . 3 inf(𝑇, ℝ*, < ) = inf( 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < )
2017, 19syl6eqr 2662 . 2 (𝜑 → ((𝐹𝑋)𝐷(𝐹𝑌)) = inf(𝑇, ℝ*, < ))
21 xrsbas 19581 . . . . . . . . . . . 12 * = (Base‘ℝ*𝑠)
22 xrsadd 19582 . . . . . . . . . . . 12 +𝑒 = (+g‘ℝ*𝑠)
23 imasdsf1o.w . . . . . . . . . . . 12 𝑊 = (ℝ*𝑠s (ℝ* ∖ {-∞}))
24 xrsex 19580 . . . . . . . . . . . . 13 *𝑠 ∈ V
2524a1i 11 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ℝ*𝑠 ∈ V)
26 fzfid 12634 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1...𝑛) ∈ Fin)
27 difss 3699 . . . . . . . . . . . . 13 (ℝ* ∖ {-∞}) ⊆ ℝ*
2827a1i 11 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ* ∖ {-∞}) ⊆ ℝ*)
29 imasdsf1o.m . . . . . . . . . . . . . . . 16 (𝜑𝐸 ∈ (∞Met‘𝑉))
30 xmetf 21944 . . . . . . . . . . . . . . . 16 (𝐸 ∈ (∞Met‘𝑉) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
31 ffn 5958 . . . . . . . . . . . . . . . 16 (𝐸:(𝑉 × 𝑉)⟶ℝ*𝐸 Fn (𝑉 × 𝑉))
3229, 30, 313syl 18 . . . . . . . . . . . . . . 15 (𝜑𝐸 Fn (𝑉 × 𝑉))
33 xmetcl 21946 . . . . . . . . . . . . . . . . . . 19 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓𝑉𝑔𝑉) → (𝑓𝐸𝑔) ∈ ℝ*)
34 xmetge0 21959 . . . . . . . . . . . . . . . . . . . 20 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓𝑉𝑔𝑉) → 0 ≤ (𝑓𝐸𝑔))
35 ge0nemnf 11878 . . . . . . . . . . . . . . . . . . . 20 (((𝑓𝐸𝑔) ∈ ℝ* ∧ 0 ≤ (𝑓𝐸𝑔)) → (𝑓𝐸𝑔) ≠ -∞)
3633, 34, 35syl2anc 691 . . . . . . . . . . . . . . . . . . 19 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓𝑉𝑔𝑉) → (𝑓𝐸𝑔) ≠ -∞)
37 eldifsn 4260 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}) ↔ ((𝑓𝐸𝑔) ∈ ℝ* ∧ (𝑓𝐸𝑔) ≠ -∞))
3833, 36, 37sylanbrc 695 . . . . . . . . . . . . . . . . . 18 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓𝑉𝑔𝑉) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
39383expb 1258 . . . . . . . . . . . . . . . . 17 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓𝑉𝑔𝑉)) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
4029, 39sylan 487 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑓𝑉𝑔𝑉)) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
4140ralrimivva 2954 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑓𝑉𝑔𝑉 (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
42 ffnov 6662 . . . . . . . . . . . . . . 15 (𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}) ↔ (𝐸 Fn (𝑉 × 𝑉) ∧ ∀𝑓𝑉𝑔𝑉 (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞})))
4332, 41, 42sylanbrc 695 . . . . . . . . . . . . . 14 (𝜑𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
4443ad2antrr 758 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
45 ssrab2 3650 . . . . . . . . . . . . . . . . 17 { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ⊆ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))
4615, 45eqsstri 3598 . . . . . . . . . . . . . . . 16 𝑆 ⊆ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))
4746a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → 𝑆 ⊆ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)))
4847sselda 3568 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)))
49 elmapi 7765 . . . . . . . . . . . . . 14 (𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
5048, 49syl 17 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
51 fco 5971 . . . . . . . . . . . . 13 ((𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}) ∧ 𝑔:(1...𝑛)⟶(𝑉 × 𝑉)) → (𝐸𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
5244, 50, 51syl2anc 691 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
53 0re 9919 . . . . . . . . . . . . 13 0 ∈ ℝ
54 rexr 9964 . . . . . . . . . . . . . 14 (0 ∈ ℝ → 0 ∈ ℝ*)
55 renemnf 9967 . . . . . . . . . . . . . 14 (0 ∈ ℝ → 0 ≠ -∞)
56 eldifsn 4260 . . . . . . . . . . . . . 14 (0 ∈ (ℝ* ∖ {-∞}) ↔ (0 ∈ ℝ* ∧ 0 ≠ -∞))
5754, 55, 56sylanbrc 695 . . . . . . . . . . . . 13 (0 ∈ ℝ → 0 ∈ (ℝ* ∖ {-∞}))
5853, 57mp1i 13 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 0 ∈ (ℝ* ∖ {-∞}))
59 xaddid2 11947 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ* → (0 +𝑒 𝑥) = 𝑥)
60 xaddid1 11946 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ* → (𝑥 +𝑒 0) = 𝑥)
6159, 60jca 553 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ* → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
6261adantl 481 . . . . . . . . . . . 12 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℝ*) → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
6321, 22, 23, 25, 26, 28, 52, 58, 62gsumress 17099 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ*𝑠 Σg (𝐸𝑔)) = (𝑊 Σg (𝐸𝑔)))
6423, 21ressbas2 15758 . . . . . . . . . . . . 13 ((ℝ* ∖ {-∞}) ⊆ ℝ* → (ℝ* ∖ {-∞}) = (Base‘𝑊))
6527, 64ax-mp 5 . . . . . . . . . . . 12 (ℝ* ∖ {-∞}) = (Base‘𝑊)
6623xrs10 19604 . . . . . . . . . . . 12 0 = (0g𝑊)
6723xrs1cmn 19605 . . . . . . . . . . . . 13 𝑊 ∈ CMnd
6867a1i 11 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑊 ∈ CMnd)
69 c0ex 9913 . . . . . . . . . . . . . 14 0 ∈ V
7069a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 0 ∈ V)
7152, 26, 70fdmfifsupp 8168 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸𝑔) finSupp 0)
7265, 66, 68, 26, 52, 71gsumcl 18139 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg (𝐸𝑔)) ∈ (ℝ* ∖ {-∞}))
7363, 72eqeltrd 2688 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ*𝑠 Σg (𝐸𝑔)) ∈ (ℝ* ∖ {-∞}))
7473eldifad 3552 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ*𝑠 Σg (𝐸𝑔)) ∈ ℝ*)
75 eqid 2610 . . . . . . . . 9 (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) = (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔)))
7674, 75fmptd 6292 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))):𝑆⟶ℝ*)
77 frn 5966 . . . . . . . 8 ((𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))):𝑆⟶ℝ* → ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
7876, 77syl 17 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
7978ralrimiva 2949 . . . . . 6 (𝜑 → ∀𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
80 iunss 4497 . . . . . 6 ( 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ* ↔ ∀𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
8179, 80sylibr 223 . . . . 5 (𝜑 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
8218, 81syl5eqss 3612 . . . 4 (𝜑𝑇 ⊆ ℝ*)
83 infxrcl 12035 . . . 4 (𝑇 ⊆ ℝ* → inf(𝑇, ℝ*, < ) ∈ ℝ*)
8482, 83syl 17 . . 3 (𝜑 → inf(𝑇, ℝ*, < ) ∈ ℝ*)
85 xmetcl 21946 . . . 4 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉𝑌𝑉) → (𝑋𝐸𝑌) ∈ ℝ*)
8629, 11, 13, 85syl3anc 1318 . . 3 (𝜑 → (𝑋𝐸𝑌) ∈ ℝ*)
87 1nn 10908 . . . . . . 7 1 ∈ ℕ
88 1ex 9914 . . . . . . . . . . . 12 1 ∈ V
89 opex 4859 . . . . . . . . . . . 12 𝑋, 𝑌⟩ ∈ V
9088, 89f1osn 6088 . . . . . . . . . . 11 {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}–1-1-onto→{⟨𝑋, 𝑌⟩}
91 f1of 6050 . . . . . . . . . . 11 ({⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}–1-1-onto→{⟨𝑋, 𝑌⟩} → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩})
9290, 91ax-mp 5 . . . . . . . . . 10 {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩}
93 opelxpi 5072 . . . . . . . . . . . 12 ((𝑋𝑉𝑌𝑉) → ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉))
9411, 13, 93syl2anc 691 . . . . . . . . . . 11 (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉))
9594snssd 4281 . . . . . . . . . 10 (𝜑 → {⟨𝑋, 𝑌⟩} ⊆ (𝑉 × 𝑉))
96 fss 5969 . . . . . . . . . 10 (({⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩} ∧ {⟨𝑋, 𝑌⟩} ⊆ (𝑉 × 𝑉)) → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉))
9792, 95, 96sylancr 694 . . . . . . . . 9 (𝜑 → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉))
9829elfvexd 6132 . . . . . . . . . . 11 (𝜑𝑉 ∈ V)
99 xpexg 6858 . . . . . . . . . . 11 ((𝑉 ∈ V ∧ 𝑉 ∈ V) → (𝑉 × 𝑉) ∈ V)
10098, 98, 99syl2anc 691 . . . . . . . . . 10 (𝜑 → (𝑉 × 𝑉) ∈ V)
101 snex 4835 . . . . . . . . . 10 {1} ∈ V
102 elmapg 7757 . . . . . . . . . 10 (((𝑉 × 𝑉) ∈ V ∧ {1} ∈ V) → ({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑𝑚 {1}) ↔ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉)))
103100, 101, 102sylancl 693 . . . . . . . . 9 (𝜑 → ({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑𝑚 {1}) ↔ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉)))
10497, 103mpbird 246 . . . . . . . 8 (𝜑 → {⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑𝑚 {1}))
105 op1stg 7071 . . . . . . . . . . 11 ((𝑋𝑉𝑌𝑉) → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋)
10611, 13, 105syl2anc 691 . . . . . . . . . 10 (𝜑 → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋)
107106fveq2d 6107 . . . . . . . . 9 (𝜑 → (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋))
108 op2ndg 7072 . . . . . . . . . . 11 ((𝑋𝑉𝑌𝑉) → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
10911, 13, 108syl2anc 691 . . . . . . . . . 10 (𝜑 → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
110109fveq2d 6107 . . . . . . . . 9 (𝜑 → (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌))
111107, 110jca 553 . . . . . . . 8 (𝜑 → ((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌)))
11224a1i 11 . . . . . . . . . 10 (𝜑 → ℝ*𝑠 ∈ V)
113 snfi 7923 . . . . . . . . . . 11 {1} ∈ Fin
114113a1i 11 . . . . . . . . . 10 (𝜑 → {1} ∈ Fin)
11527a1i 11 . . . . . . . . . 10 (𝜑 → (ℝ* ∖ {-∞}) ⊆ ℝ*)
116 xmetge0 21959 . . . . . . . . . . . . . . 15 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉𝑌𝑉) → 0 ≤ (𝑋𝐸𝑌))
11729, 11, 13, 116syl3anc 1318 . . . . . . . . . . . . . 14 (𝜑 → 0 ≤ (𝑋𝐸𝑌))
118 ge0nemnf 11878 . . . . . . . . . . . . . 14 (((𝑋𝐸𝑌) ∈ ℝ* ∧ 0 ≤ (𝑋𝐸𝑌)) → (𝑋𝐸𝑌) ≠ -∞)
11986, 117, 118syl2anc 691 . . . . . . . . . . . . 13 (𝜑 → (𝑋𝐸𝑌) ≠ -∞)
120 eldifsn 4260 . . . . . . . . . . . . 13 ((𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}) ↔ ((𝑋𝐸𝑌) ∈ ℝ* ∧ (𝑋𝐸𝑌) ≠ -∞))
12186, 119, 120sylanbrc 695 . . . . . . . . . . . 12 (𝜑 → (𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}))
122 fconst6g 6007 . . . . . . . . . . . 12 ((𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}) → ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞}))
123121, 122syl 17 . . . . . . . . . . 11 (𝜑 → ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞}))
124 fcoconst 6307 . . . . . . . . . . . . . 14 ((𝐸 Fn (𝑉 × 𝑉) ∧ ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉)) → (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}))
12532, 94, 124syl2anc 691 . . . . . . . . . . . . 13 (𝜑 → (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}))
12688, 89xpsn 6313 . . . . . . . . . . . . . 14 ({1} × {⟨𝑋, 𝑌⟩}) = {⟨1, ⟨𝑋, 𝑌⟩⟩}
127126coeq2i 5204 . . . . . . . . . . . . 13 (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})
128 df-ov 6552 . . . . . . . . . . . . . . . 16 (𝑋𝐸𝑌) = (𝐸‘⟨𝑋, 𝑌⟩)
129128eqcomi 2619 . . . . . . . . . . . . . . 15 (𝐸‘⟨𝑋, 𝑌⟩) = (𝑋𝐸𝑌)
130129sneqi 4136 . . . . . . . . . . . . . 14 {(𝐸‘⟨𝑋, 𝑌⟩)} = {(𝑋𝐸𝑌)}
131130xpeq2i 5060 . . . . . . . . . . . . 13 ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}) = ({1} × {(𝑋𝐸𝑌)})
132125, 127, 1313eqtr3g 2667 . . . . . . . . . . . 12 (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}) = ({1} × {(𝑋𝐸𝑌)}))
133132feq1d 5943 . . . . . . . . . . 11 (𝜑 → ((𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}):{1}⟶(ℝ* ∖ {-∞}) ↔ ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞})))
134123, 133mpbird 246 . . . . . . . . . 10 (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}):{1}⟶(ℝ* ∖ {-∞}))
13553, 57mp1i 13 . . . . . . . . . 10 (𝜑 → 0 ∈ (ℝ* ∖ {-∞}))
13661adantl 481 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ*) → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
13721, 22, 23, 112, 114, 115, 134, 135, 136gsumress 17099 . . . . . . . . 9 (𝜑 → (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})) = (𝑊 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
138 fconstmpt 5085 . . . . . . . . . . 11 ({1} × {(𝑋𝐸𝑌)}) = (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))
139132, 138syl6eq 2660 . . . . . . . . . 10 (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}) = (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌)))
140139oveq2d 6565 . . . . . . . . 9 (𝜑 → (𝑊 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})) = (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))))
141 cmnmnd 18031 . . . . . . . . . . 11 (𝑊 ∈ CMnd → 𝑊 ∈ Mnd)
14267, 141mp1i 13 . . . . . . . . . 10 (𝜑𝑊 ∈ Mnd)
14387a1i 11 . . . . . . . . . 10 (𝜑 → 1 ∈ ℕ)
144 eqidd 2611 . . . . . . . . . . 11 (𝑗 = 1 → (𝑋𝐸𝑌) = (𝑋𝐸𝑌))
14565, 144gsumsn 18177 . . . . . . . . . 10 ((𝑊 ∈ Mnd ∧ 1 ∈ ℕ ∧ (𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞})) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))) = (𝑋𝐸𝑌))
146142, 143, 121, 145syl3anc 1318 . . . . . . . . 9 (𝜑 → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))) = (𝑋𝐸𝑌))
147137, 140, 1463eqtrrd 2649 . . . . . . . 8 (𝜑 → (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
148 fveq1 6102 . . . . . . . . . . . . . . 15 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝑔‘1) = ({⟨1, ⟨𝑋, 𝑌⟩⟩}‘1))
14988, 89fvsn 6351 . . . . . . . . . . . . . . 15 ({⟨1, ⟨𝑋, 𝑌⟩⟩}‘1) = ⟨𝑋, 𝑌
150148, 149syl6eq 2660 . . . . . . . . . . . . . 14 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝑔‘1) = ⟨𝑋, 𝑌⟩)
151150fveq2d 6107 . . . . . . . . . . . . 13 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (1st ‘(𝑔‘1)) = (1st ‘⟨𝑋, 𝑌⟩))
152151fveq2d 6107 . . . . . . . . . . . 12 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)))
153152eqeq1d 2612 . . . . . . . . . . 11 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ↔ (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋)))
154150fveq2d 6107 . . . . . . . . . . . . 13 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (2nd ‘(𝑔‘1)) = (2nd ‘⟨𝑋, 𝑌⟩))
155154fveq2d 6107 . . . . . . . . . . . 12 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)))
156155eqeq1d 2612 . . . . . . . . . . 11 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌) ↔ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌)))
157153, 156anbi12d 743 . . . . . . . . . 10 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ↔ ((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌))))
158 coeq2 5202 . . . . . . . . . . . 12 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝐸𝑔) = (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}))
159158oveq2d 6565 . . . . . . . . . . 11 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (ℝ*𝑠 Σg (𝐸𝑔)) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
160159eqeq2d 2620 . . . . . . . . . 10 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}))))
161157, 160anbi12d 743 . . . . . . . . 9 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))) ↔ (((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))))
162161rspcev 3282 . . . . . . . 8 (({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑𝑚 {1}) ∧ (((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))) → ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
163104, 111, 147, 162syl12anc 1316 . . . . . . 7 (𝜑 → ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
164 ovex 6577 . . . . . . . . . 10 (𝑋𝐸𝑌) ∈ V
16575elrnmpt 5293 . . . . . . . . . 10 ((𝑋𝐸𝑌) ∈ V → ((𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
166164, 165ax-mp 5 . . . . . . . . 9 ((𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))
16715rexeqi 3120 . . . . . . . . . . 11 (∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ ∃𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))
168 fveq1 6102 . . . . . . . . . . . . . . . 16 ( = 𝑔 → (‘1) = (𝑔‘1))
169168fveq2d 6107 . . . . . . . . . . . . . . 15 ( = 𝑔 → (1st ‘(‘1)) = (1st ‘(𝑔‘1)))
170169fveq2d 6107 . . . . . . . . . . . . . 14 ( = 𝑔 → (𝐹‘(1st ‘(‘1))) = (𝐹‘(1st ‘(𝑔‘1))))
171170eqeq1d 2612 . . . . . . . . . . . . 13 ( = 𝑔 → ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ↔ (𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋)))
172 fveq1 6102 . . . . . . . . . . . . . . . 16 ( = 𝑔 → (𝑛) = (𝑔𝑛))
173172fveq2d 6107 . . . . . . . . . . . . . . 15 ( = 𝑔 → (2nd ‘(𝑛)) = (2nd ‘(𝑔𝑛)))
174173fveq2d 6107 . . . . . . . . . . . . . 14 ( = 𝑔 → (𝐹‘(2nd ‘(𝑛))) = (𝐹‘(2nd ‘(𝑔𝑛))))
175174eqeq1d 2612 . . . . . . . . . . . . 13 ( = 𝑔 → ((𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ↔ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)))
176 fveq1 6102 . . . . . . . . . . . . . . . . 17 ( = 𝑔 → (𝑖) = (𝑔𝑖))
177176fveq2d 6107 . . . . . . . . . . . . . . . 16 ( = 𝑔 → (2nd ‘(𝑖)) = (2nd ‘(𝑔𝑖)))
178177fveq2d 6107 . . . . . . . . . . . . . . 15 ( = 𝑔 → (𝐹‘(2nd ‘(𝑖))) = (𝐹‘(2nd ‘(𝑔𝑖))))
179 fveq1 6102 . . . . . . . . . . . . . . . . 17 ( = 𝑔 → (‘(𝑖 + 1)) = (𝑔‘(𝑖 + 1)))
180179fveq2d 6107 . . . . . . . . . . . . . . . 16 ( = 𝑔 → (1st ‘(‘(𝑖 + 1))) = (1st ‘(𝑔‘(𝑖 + 1))))
181180fveq2d 6107 . . . . . . . . . . . . . . 15 ( = 𝑔 → (𝐹‘(1st ‘(‘(𝑖 + 1)))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
182178, 181eqeq12d 2625 . . . . . . . . . . . . . 14 ( = 𝑔 → ((𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
183182ralbidv 2969 . . . . . . . . . . . . 13 ( = 𝑔 → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
184171, 175, 1833anbi123d 1391 . . . . . . . . . . . 12 ( = 𝑔 → (((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
185184rexrab 3337 . . . . . . . . . . 11 (∃𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
186167, 185bitri 263 . . . . . . . . . 10 (∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
187 oveq2 6557 . . . . . . . . . . . . 13 (𝑛 = 1 → (1...𝑛) = (1...1))
188 1z 11284 . . . . . . . . . . . . . 14 1 ∈ ℤ
189 fzsn 12254 . . . . . . . . . . . . . 14 (1 ∈ ℤ → (1...1) = {1})
190188, 189ax-mp 5 . . . . . . . . . . . . 13 (1...1) = {1}
191187, 190syl6eq 2660 . . . . . . . . . . . 12 (𝑛 = 1 → (1...𝑛) = {1})
192191oveq2d 6565 . . . . . . . . . . 11 (𝑛 = 1 → ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) = ((𝑉 × 𝑉) ↑𝑚 {1}))
193 df-3an 1033 . . . . . . . . . . . . 13 (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
194 ral0 4028 . . . . . . . . . . . . . . . 16 𝑖 ∈ ∅ (𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))
195 oveq1 6556 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → (𝑛 − 1) = (1 − 1))
196 1m1e0 10966 . . . . . . . . . . . . . . . . . . . 20 (1 − 1) = 0
197195, 196syl6eq 2660 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → (𝑛 − 1) = 0)
198197oveq2d 6565 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → (1...(𝑛 − 1)) = (1...0))
199 fz10 12233 . . . . . . . . . . . . . . . . . 18 (1...0) = ∅
200198, 199syl6eq 2660 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → (1...(𝑛 − 1)) = ∅)
201200raleqdv 3121 . . . . . . . . . . . . . . . 16 (𝑛 = 1 → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ ∅ (𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
202194, 201mpbiri 247 . . . . . . . . . . . . . . 15 (𝑛 = 1 → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
203202biantrud 527 . . . . . . . . . . . . . 14 (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
204 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → (𝑔𝑛) = (𝑔‘1))
205204fveq2d 6107 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → (2nd ‘(𝑔𝑛)) = (2nd ‘(𝑔‘1)))
206205fveq2d 6107 . . . . . . . . . . . . . . . 16 (𝑛 = 1 → (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹‘(2nd ‘(𝑔‘1))))
207206eqeq1d 2612 . . . . . . . . . . . . . . 15 (𝑛 = 1 → ((𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ↔ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)))
208207anbi2d 736 . . . . . . . . . . . . . 14 (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌))))
209203, 208bitr3d 269 . . . . . . . . . . . . 13 (𝑛 = 1 → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌))))
210193, 209syl5bb 271 . . . . . . . . . . . 12 (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌))))
211210anbi1d 737 . . . . . . . . . . 11 (𝑛 = 1 → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))))
212192, 211rexeqbidv 3130 . . . . . . . . . 10 (𝑛 = 1 → (∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))))
213186, 212syl5bb 271 . . . . . . . . 9 (𝑛 = 1 → (∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))))
214166, 213syl5bb 271 . . . . . . . 8 (𝑛 = 1 → ((𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))))
215214rspcev 3282 . . . . . . 7 ((1 ∈ ℕ ∧ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))) → ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
21687, 163, 215sylancr 694 . . . . . 6 (𝜑 → ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
217 eliun 4460 . . . . . 6 ((𝑋𝐸𝑌) ∈ 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
218216, 217sylibr 223 . . . . 5 (𝜑 → (𝑋𝐸𝑌) ∈ 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
219218, 18syl6eleqr 2699 . . . 4 (𝜑 → (𝑋𝐸𝑌) ∈ 𝑇)
220 infxrlb 12036 . . . 4 ((𝑇 ⊆ ℝ* ∧ (𝑋𝐸𝑌) ∈ 𝑇) → inf(𝑇, ℝ*, < ) ≤ (𝑋𝐸𝑌))
22182, 219, 220syl2anc 691 . . 3 (𝜑 → inf(𝑇, ℝ*, < ) ≤ (𝑋𝐸𝑌))
22218eleq2i 2680 . . . . . . 7 (𝑝𝑇𝑝 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
223 eliun 4460 . . . . . . 7 (𝑝 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
224222, 223bitri 263 . . . . . 6 (𝑝𝑇 ↔ ∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
225 vex 3176 . . . . . . . . 9 𝑝 ∈ V
22675elrnmpt 5293 . . . . . . . . 9 (𝑝 ∈ V → (𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸𝑔))))
227225, 226ax-mp 5 . . . . . . . 8 (𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸𝑔)))
228184, 15elrab2 3333 . . . . . . . . . . . . . . . . 17 (𝑔𝑆 ↔ (𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∧ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
229228simprbi 479 . . . . . . . . . . . . . . . 16 (𝑔𝑆 → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
230229adantl 481 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
231230simp2d 1067 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌))
2323ad2antrr 758 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐹:𝑉1-1-onto𝐵)
233 f1of1 6049 . . . . . . . . . . . . . . . 16 (𝐹:𝑉1-1-onto𝐵𝐹:𝑉1-1𝐵)
234232, 233syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐹:𝑉1-1𝐵)
235 simplr 788 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑛 ∈ ℕ)
236 elfz1end 12242 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (1...𝑛))
237235, 236sylib 207 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑛 ∈ (1...𝑛))
23850, 237ffvelrnd 6268 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑔𝑛) ∈ (𝑉 × 𝑉))
239 xp2nd 7090 . . . . . . . . . . . . . . . 16 ((𝑔𝑛) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔𝑛)) ∈ 𝑉)
240238, 239syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (2nd ‘(𝑔𝑛)) ∈ 𝑉)
24113ad2antrr 758 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑌𝑉)
242 f1fveq 6420 . . . . . . . . . . . . . . 15 ((𝐹:𝑉1-1𝐵 ∧ ((2nd ‘(𝑔𝑛)) ∈ 𝑉𝑌𝑉)) → ((𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ↔ (2nd ‘(𝑔𝑛)) = 𝑌))
243234, 240, 241, 242syl12anc 1316 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ↔ (2nd ‘(𝑔𝑛)) = 𝑌))
244231, 243mpbid 221 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (2nd ‘(𝑔𝑛)) = 𝑌)
245244oveq2d 6565 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔𝑛))) = (𝑋𝐸𝑌))
246 eleq1 2676 . . . . . . . . . . . . . . . . 17 (𝑚 = 1 → (𝑚 ∈ (1...𝑛) ↔ 1 ∈ (1...𝑛)))
247 fveq2 6103 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 1 → (𝑔𝑚) = (𝑔‘1))
248247fveq2d 6107 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 1 → (2nd ‘(𝑔𝑚)) = (2nd ‘(𝑔‘1)))
249248oveq2d 6565 . . . . . . . . . . . . . . . . . 18 (𝑚 = 1 → (𝑋𝐸(2nd ‘(𝑔𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘1))))
250 oveq2 6557 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 1 → (1...𝑚) = (1...1))
251250, 190syl6eq 2660 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 1 → (1...𝑚) = {1})
252251reseq2d 5317 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 1 → ((𝐸𝑔) ↾ (1...𝑚)) = ((𝐸𝑔) ↾ {1}))
253252oveq2d 6565 . . . . . . . . . . . . . . . . . 18 (𝑚 = 1 → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸𝑔) ↾ {1})))
254249, 253breq12d 4596 . . . . . . . . . . . . . . . . 17 (𝑚 = 1 → ((𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1}))))
255246, 254imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑚 = 1 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚)))) ↔ (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1})))))
256255imbi2d 329 . . . . . . . . . . . . . . 15 (𝑚 = 1 → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))))) ↔ (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1}))))))
257 eleq1 2676 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑥 → (𝑚 ∈ (1...𝑛) ↔ 𝑥 ∈ (1...𝑛)))
258 fveq2 6103 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑥 → (𝑔𝑚) = (𝑔𝑥))
259258fveq2d 6107 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑥 → (2nd ‘(𝑔𝑚)) = (2nd ‘(𝑔𝑥)))
260259oveq2d 6565 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑥 → (𝑋𝐸(2nd ‘(𝑔𝑚))) = (𝑋𝐸(2nd ‘(𝑔𝑥))))
261 oveq2 6557 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑥 → (1...𝑚) = (1...𝑥))
262261reseq2d 5317 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑥 → ((𝐸𝑔) ↾ (1...𝑚)) = ((𝐸𝑔) ↾ (1...𝑥)))
263262oveq2d 6565 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑥 → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))))
264260, 263breq12d 4596 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑥 → ((𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))))
265257, 264imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑥 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚)))) ↔ (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))))))
266265imbi2d 329 . . . . . . . . . . . . . . 15 (𝑚 = 𝑥 → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))))) ↔ (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))))))
267 eleq1 2676 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑥 + 1) → (𝑚 ∈ (1...𝑛) ↔ (𝑥 + 1) ∈ (1...𝑛)))
268 fveq2 6103 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = (𝑥 + 1) → (𝑔𝑚) = (𝑔‘(𝑥 + 1)))
269268fveq2d 6107 . . . . . . . . . . . . . . . . . . 19 (𝑚 = (𝑥 + 1) → (2nd ‘(𝑔𝑚)) = (2nd ‘(𝑔‘(𝑥 + 1))))
270269oveq2d 6565 . . . . . . . . . . . . . . . . . 18 (𝑚 = (𝑥 + 1) → (𝑋𝐸(2nd ‘(𝑔𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))))
271 oveq2 6557 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = (𝑥 + 1) → (1...𝑚) = (1...(𝑥 + 1)))
272271reseq2d 5317 . . . . . . . . . . . . . . . . . . 19 (𝑚 = (𝑥 + 1) → ((𝐸𝑔) ↾ (1...𝑚)) = ((𝐸𝑔) ↾ (1...(𝑥 + 1))))
273272oveq2d 6565 . . . . . . . . . . . . . . . . . 18 (𝑚 = (𝑥 + 1) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))))
274270, 273breq12d 4596 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑥 + 1) → ((𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))
275267, 274imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑚 = (𝑥 + 1) → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚)))) ↔ ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))))))
276275imbi2d 329 . . . . . . . . . . . . . . 15 (𝑚 = (𝑥 + 1) → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))))) ↔ (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))))
277 eleq1 2676 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → (𝑚 ∈ (1...𝑛) ↔ 𝑛 ∈ (1...𝑛)))
278 fveq2 6103 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → (𝑔𝑚) = (𝑔𝑛))
279278fveq2d 6107 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → (2nd ‘(𝑔𝑚)) = (2nd ‘(𝑔𝑛)))
280279oveq2d 6565 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑛 → (𝑋𝐸(2nd ‘(𝑔𝑚))) = (𝑋𝐸(2nd ‘(𝑔𝑛))))
281 oveq2 6557 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
282281reseq2d 5317 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → ((𝐸𝑔) ↾ (1...𝑚)) = ((𝐸𝑔) ↾ (1...𝑛)))
283282oveq2d 6565 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑛 → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))
284280, 283breq12d 4596 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → ((𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛)))))
285277, 284imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚)))) ↔ (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))))
286285imbi2d 329 . . . . . . . . . . . . . . 15 (𝑚 = 𝑛 → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))))) ↔ (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛)))))))
28729ad2antrr 758 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐸 ∈ (∞Met‘𝑉))
28811ad2antrr 758 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑋𝑉)
289 nnuz 11599 . . . . . . . . . . . . . . . . . . . . . . 23 ℕ = (ℤ‘1)
290235, 289syl6eleq 2698 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑛 ∈ (ℤ‘1))
291 eluzfz1 12219 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (ℤ‘1) → 1 ∈ (1...𝑛))
292290, 291syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 1 ∈ (1...𝑛))
29350, 292ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑔‘1) ∈ (𝑉 × 𝑉))
294 xp2nd 7090 . . . . . . . . . . . . . . . . . . . 20 ((𝑔‘1) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘1)) ∈ 𝑉)
295293, 294syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (2nd ‘(𝑔‘1)) ∈ 𝑉)
296 xmetcl 21946 . . . . . . . . . . . . . . . . . . 19 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉 ∧ (2nd ‘(𝑔‘1)) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔‘1))) ∈ ℝ*)
297287, 288, 295, 296syl3anc 1318 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ∈ ℝ*)
298 xrleid 11859 . . . . . . . . . . . . . . . . . 18 ((𝑋𝐸(2nd ‘(𝑔‘1))) ∈ ℝ* → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑋𝐸(2nd ‘(𝑔‘1))))
299297, 298syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑋𝐸(2nd ‘(𝑔‘1))))
300142ad2antrr 758 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑊 ∈ Mnd)
30187a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 1 ∈ ℕ)
30244, 293ffvelrnd 6268 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸‘(𝑔‘1)) ∈ (ℝ* ∖ {-∞}))
303 fveq2 6103 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 1 → (𝑔𝑗) = (𝑔‘1))
304303fveq2d 6107 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 1 → (𝐸‘(𝑔𝑗)) = (𝐸‘(𝑔‘1)))
30565, 304gsumsn 18177 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ Mnd ∧ 1 ∈ ℕ ∧ (𝐸‘(𝑔‘1)) ∈ (ℝ* ∖ {-∞})) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗)))) = (𝐸‘(𝑔‘1)))
306300, 301, 302, 305syl3anc 1318 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗)))) = (𝐸‘(𝑔‘1)))
307287, 30syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
308 fcompt 6306 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐸:(𝑉 × 𝑉)⟶ℝ*𝑔:(1...𝑛)⟶(𝑉 × 𝑉)) → (𝐸𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))))
309307, 50, 308syl2anc 691 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))))
310309reseq1d 5316 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐸𝑔) ↾ {1}) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ {1}))
311292snssd 4281 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → {1} ⊆ (1...𝑛))
312311resmptd 5371 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ {1}) = (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗))))
313310, 312eqtrd 2644 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐸𝑔) ↾ {1}) = (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗))))
314313oveq2d 6565 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg ((𝐸𝑔) ↾ {1})) = (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗)))))
315 df-ov 6552 . . . . . . . . . . . . . . . . . . 19 (𝑋𝐸(2nd ‘(𝑔‘1))) = (𝐸‘⟨𝑋, (2nd ‘(𝑔‘1))⟩)
316 1st2nd2 7096 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔‘1) ∈ (𝑉 × 𝑉) → (𝑔‘1) = ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩)
317293, 316syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑔‘1) = ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩)
318230simp1d 1066 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋))
319 xp1st 7089 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔‘1) ∈ (𝑉 × 𝑉) → (1st ‘(𝑔‘1)) ∈ 𝑉)
320293, 319syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1st ‘(𝑔‘1)) ∈ 𝑉)
321 f1fveq 6420 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹:𝑉1-1𝐵 ∧ ((1st ‘(𝑔‘1)) ∈ 𝑉𝑋𝑉)) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ↔ (1st ‘(𝑔‘1)) = 𝑋))
322234, 320, 288, 321syl12anc 1316 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ↔ (1st ‘(𝑔‘1)) = 𝑋))
323318, 322mpbid 221 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1st ‘(𝑔‘1)) = 𝑋)
324323opeq1d 4346 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩ = ⟨𝑋, (2nd ‘(𝑔‘1))⟩)
325317, 324eqtr2d 2645 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ⟨𝑋, (2nd ‘(𝑔‘1))⟩ = (𝑔‘1))
326325fveq2d 6107 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸‘⟨𝑋, (2nd ‘(𝑔‘1))⟩) = (𝐸‘(𝑔‘1)))
327315, 326syl5eq 2656 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) = (𝐸‘(𝑔‘1)))
328306, 314, 3273eqtr4d 2654 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg ((𝐸𝑔) ↾ {1})) = (𝑋𝐸(2nd ‘(𝑔‘1))))
329299, 328breqtrrd 4611 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1})))
330329a1d 25 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1}))))
331 simprl 790 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ ℕ)
332331, 289syl6eleq 2698 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (ℤ‘1))
333 simprr 792 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑥 + 1) ∈ (1...𝑛))
334 peano2fzr 12225 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (ℤ‘1) ∧ (𝑥 + 1) ∈ (1...𝑛)) → 𝑥 ∈ (1...𝑛))
335332, 333, 334syl2anc 691 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (1...𝑛))
336335expr 641 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 + 1) ∈ (1...𝑛) → 𝑥 ∈ (1...𝑛)))
337336imim1d 80 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))))))
338287adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸 ∈ (∞Met‘𝑉))
339288adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑋𝑉)
34050adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
341340, 335ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔𝑥) ∈ (𝑉 × 𝑉))
342 xp2nd 7090 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔𝑥) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔𝑥)) ∈ 𝑉)
343341, 342syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔𝑥)) ∈ 𝑉)
344 xmetcl 21946 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉 ∧ (2nd ‘(𝑔𝑥)) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ∈ ℝ*)
345338, 339, 343, 344syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ∈ ℝ*)
34667a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑊 ∈ CMnd)
347 fzfid 12634 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...𝑥) ∈ Fin)
34852adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
349 fzsuc 12258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ (ℤ‘1) → (1...(𝑥 + 1)) = ((1...𝑥) ∪ {(𝑥 + 1)}))
350332, 349syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...(𝑥 + 1)) = ((1...𝑥) ∪ {(𝑥 + 1)}))
351 elfzuz3 12210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 + 1) ∈ (1...𝑛) → 𝑛 ∈ (ℤ‘(𝑥 + 1)))
352351ad2antll 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑛 ∈ (ℤ‘(𝑥 + 1)))
353 fzss2 12252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 ∈ (ℤ‘(𝑥 + 1)) → (1...(𝑥 + 1)) ⊆ (1...𝑛))
354352, 353syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...(𝑥 + 1)) ⊆ (1...𝑛))
355350, 354eqsstr3d 3603 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((1...𝑥) ∪ {(𝑥 + 1)}) ⊆ (1...𝑛))
356355unssad 3752 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...𝑥) ⊆ (1...𝑛))
357348, 356fssresd 5984 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...𝑥)):(1...𝑥)⟶(ℝ* ∖ {-∞}))
35869a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 0 ∈ V)
359357, 347, 358fdmfifsupp 8168 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...𝑥)) finSupp 0)
36065, 66, 346, 347, 357, 359gsumcl 18139 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) ∈ (ℝ* ∖ {-∞}))
361360eldifad 3552 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) ∈ ℝ*)
362338, 30syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
363340, 333ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉))
364362, 363ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*)
365 xleadd1a 11955 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑋𝐸(2nd ‘(𝑔𝑥))) ∈ ℝ* ∧ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) ∈ ℝ* ∧ (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*) ∧ (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
366365ex 449 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑋𝐸(2nd ‘(𝑔𝑥))) ∈ ℝ* ∧ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) ∈ ℝ* ∧ (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
367345, 361, 364, 366syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
368 xp2nd 7090 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
369363, 368syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
370 xmettri 21966 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑋𝑉 ∧ (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉 ∧ (2nd ‘(𝑔𝑥)) ∈ 𝑉)) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
371338, 339, 369, 343, 370syl13anc 1320 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
372 1st2nd2 7096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (𝑔‘(𝑥 + 1)) = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
373363, 372syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
374 nnz 11276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 ∈ ℕ → 𝑥 ∈ ℤ)
375374ad2antrl 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ ℤ)
376 eluzp1m1 11587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑥 ∈ ℤ ∧ 𝑛 ∈ (ℤ‘(𝑥 + 1))) → (𝑛 − 1) ∈ (ℤ𝑥))
377375, 352, 376syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑛 − 1) ∈ (ℤ𝑥))
378 elfzuzb 12207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ (1...(𝑛 − 1)) ↔ (𝑥 ∈ (ℤ‘1) ∧ (𝑛 − 1) ∈ (ℤ𝑥)))
379332, 377, 378sylanbrc 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (1...(𝑛 − 1)))
380230simp3d 1068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
381380adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
382 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑖 = 𝑥 → (𝑔𝑖) = (𝑔𝑥))
383382fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑖 = 𝑥 → (2nd ‘(𝑔𝑖)) = (2nd ‘(𝑔𝑥)))
384383fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 = 𝑥 → (𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(2nd ‘(𝑔𝑥))))
385 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑖 = 𝑥 → (𝑖 + 1) = (𝑥 + 1))
386385fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑖 = 𝑥 → (𝑔‘(𝑖 + 1)) = (𝑔‘(𝑥 + 1)))
387386fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑖 = 𝑥 → (1st ‘(𝑔‘(𝑖 + 1))) = (1st ‘(𝑔‘(𝑥 + 1))))
388387fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 = 𝑥 → (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))))
389384, 388eqeq12d 2625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 = 𝑥 → ((𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(𝑔𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1))))))
390389rspcv 3278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ (1...(𝑛 − 1)) → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) → (𝐹‘(2nd ‘(𝑔𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1))))))
391379, 381, 390sylc 63 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐹‘(2nd ‘(𝑔𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))))
392234adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐹:𝑉1-1𝐵)
393 xp1st 7089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
394363, 393syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
395 f1fveq 6420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐹:𝑉1-1𝐵 ∧ ((2nd ‘(𝑔𝑥)) ∈ 𝑉 ∧ (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)) → ((𝐹‘(2nd ‘(𝑔𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))) ↔ (2nd ‘(𝑔𝑥)) = (1st ‘(𝑔‘(𝑥 + 1)))))
396392, 343, 394, 395syl12anc 1316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐹‘(2nd ‘(𝑔𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))) ↔ (2nd ‘(𝑔𝑥)) = (1st ‘(𝑔‘(𝑥 + 1)))))
397391, 396mpbid 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔𝑥)) = (1st ‘(𝑔‘(𝑥 + 1))))
398397opeq1d 4346 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ⟨(2nd ‘(𝑔𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩ = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
399373, 398eqtr4d 2647 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) = ⟨(2nd ‘(𝑔𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
400399fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) = (𝐸‘⟨(2nd ‘(𝑔𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩))
401 df-ov 6552 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) = (𝐸‘⟨(2nd ‘(𝑔𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
402400, 401syl6eqr 2662 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) = ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1)))))
403402oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) = ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
404371, 403breqtrrd 4611 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
405 xmetcl 21946 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉 ∧ (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
406338, 339, 369, 405syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
407345, 364xaddcld 12003 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
408361, 364xaddcld 12003 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
409 xrletr 11865 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ* ∧ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ* ∧ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*) → (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∧ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
410406, 407, 408, 409syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∧ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
411404, 410mpand 707 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
412367, 411syld 46 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
413 xrex 11705 . . . . . . . . . . . . . . . . . . . . . . . . . 26 * ∈ V
414413, 27ssexi 4731 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ℝ* ∖ {-∞}) ∈ V
41523, 22ressplusg 15818 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ℝ* ∖ {-∞}) ∈ V → +𝑒 = (+g𝑊))
416414, 415ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 +𝑒 = (+g𝑊)
41744ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
418 fzelp1 12263 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ (1...𝑥) → 𝑗 ∈ (1...(𝑥 + 1)))
41950ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
420354sselda 3568 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → 𝑗 ∈ (1...𝑛))
421419, 420ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → (𝑔𝑗) ∈ (𝑉 × 𝑉))
422418, 421sylan2 490 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → (𝑔𝑗) ∈ (𝑉 × 𝑉))
423417, 422ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → (𝐸‘(𝑔𝑗)) ∈ (ℝ* ∖ {-∞}))
424 fzp1disj 12269 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1...𝑥) ∩ {(𝑥 + 1)}) = ∅
425424a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((1...𝑥) ∩ {(𝑥 + 1)}) = ∅)
426 disjsn 4192 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((1...𝑥) ∩ {(𝑥 + 1)}) = ∅ ↔ ¬ (𝑥 + 1) ∈ (1...𝑥))
427425, 426sylib 207 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ¬ (𝑥 + 1) ∈ (1...𝑥))
42844adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
429428, 363ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) ∈ (ℝ* ∖ {-∞}))
430 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = (𝑥 + 1) → (𝑔𝑗) = (𝑔‘(𝑥 + 1)))
431430fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = (𝑥 + 1) → (𝐸‘(𝑔𝑗)) = (𝐸‘(𝑔‘(𝑥 + 1))))
43265, 416, 346, 347, 423, 333, 427, 429, 431gsumunsn 18182 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔𝑗)))) = ((𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗)))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
433309adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))))
434433, 350reseq12d 5318 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...(𝑥 + 1))) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ ((1...𝑥) ∪ {(𝑥 + 1)})))
435355resmptd 5371 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ ((1...𝑥) ∪ {(𝑥 + 1)})) = (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔𝑗))))
436434, 435eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...(𝑥 + 1))) = (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔𝑗))))
437436oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))) = (𝑊 Σg (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔𝑗)))))
438433reseq1d 5316 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...𝑥)) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ (1...𝑥)))
439356resmptd 5371 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ (1...𝑥)) = (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗))))
440438, 439eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...𝑥)) = (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗))))
441440oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) = (𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗)))))
442441oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) = ((𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗)))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
443432, 437, 4423eqtr4d 2654 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))) = ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
444443breq2d 4595 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))) ↔ (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
445412, 444sylibrd 248 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))
446445expr 641 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 + 1) ∈ (1...𝑛) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))))))
447446a2d 29 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℕ) → (((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))))))
448337, 447syld 46 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))))))
449448expcom 450 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℕ → (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))))
450449a2d 29 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℕ → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))))) → (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))))
451256, 266, 276, 286, 330, 450nnind 10915 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))))
452235, 451mpcom 37 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛)))))
453237, 452mpd 15 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))
454245, 453eqbrtrrd 4607 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸𝑌) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))
455 ffn 5958 . . . . . . . . . . . . . 14 ((𝐸𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}) → (𝐸𝑔) Fn (1...𝑛))
456 fnresdm 5914 . . . . . . . . . . . . . 14 ((𝐸𝑔) Fn (1...𝑛) → ((𝐸𝑔) ↾ (1...𝑛)) = (𝐸𝑔))
45752, 455, 4563syl 18 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐸𝑔) ↾ (1...𝑛)) = (𝐸𝑔))
458457oveq2d 6565 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))) = (𝑊 Σg (𝐸𝑔)))
45963, 458eqtr4d 2647 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ*𝑠 Σg (𝐸𝑔)) = (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))
460454, 459breqtrrd 4611 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸𝑌) ≤ (ℝ*𝑠 Σg (𝐸𝑔)))
461 breq2 4587 . . . . . . . . . 10 (𝑝 = (ℝ*𝑠 Σg (𝐸𝑔)) → ((𝑋𝐸𝑌) ≤ 𝑝 ↔ (𝑋𝐸𝑌) ≤ (ℝ*𝑠 Σg (𝐸𝑔))))
462460, 461syl5ibrcom 236 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑝 = (ℝ*𝑠 Σg (𝐸𝑔)) → (𝑋𝐸𝑌) ≤ 𝑝))
463462rexlimdva 3013 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (∃𝑔𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸𝑔)) → (𝑋𝐸𝑌) ≤ 𝑝))
464227, 463syl5bi 231 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) → (𝑋𝐸𝑌) ≤ 𝑝))
465464rexlimdva 3013 . . . . . 6 (𝜑 → (∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) → (𝑋𝐸𝑌) ≤ 𝑝))
466224, 465syl5bi 231 . . . . 5 (𝜑 → (𝑝𝑇 → (𝑋𝐸𝑌) ≤ 𝑝))
467466ralrimiv 2948 . . . 4 (𝜑 → ∀𝑝𝑇 (𝑋𝐸𝑌) ≤ 𝑝)
468 infxrgelb 12037 . . . . 5 ((𝑇 ⊆ ℝ* ∧ (𝑋𝐸𝑌) ∈ ℝ*) → ((𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ) ↔ ∀𝑝𝑇 (𝑋𝐸𝑌) ≤ 𝑝))
46982, 86, 468syl2anc 691 . . . 4 (𝜑 → ((𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ) ↔ ∀𝑝𝑇 (𝑋𝐸𝑌) ≤ 𝑝))
470467, 469mpbird 246 . . 3 (𝜑 → (𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ))
47184, 86, 221, 470xrletrid 11862 . 2 (𝜑 → inf(𝑇, ℝ*, < ) = (𝑋𝐸𝑌))
47220, 471eqtrd 2644 1 (𝜑 → ((𝐹𝑋)𝐷(𝐹𝑌)) = (𝑋𝐸𝑌))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  {csn 4125  ⟨cop 4131  ∪ ciun 4455   class class class wbr 4583   ↦ cmpt 4643   × cxp 5036  ran crn 5039   ↾ cres 5040   ∘ ccom 5042   Fn wfn 5799  ⟶wf 5800  –1-1→wf1 5801  –onto→wfo 5802  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549  1st c1st 7057  2nd c2nd 7058   ↑𝑚 cmap 7744  Fincfn 7841  infcinf 8230  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818  -∞cmnf 9951  ℝ*cxr 9952   < clt 9953   ≤ cle 9954   − cmin 10145  ℕcn 10897  ℤcz 11254  ℤ≥cuz 11563   +𝑒 cxad 11820  ...cfz 12197  Basecbs 15695   ↾s cress 15696  +gcplusg 15768  distcds 15777   Σg cgsu 15924  ℝ*𝑠cxrs 15983   “s cimas 15987  Mndcmnd 17117  CMndccmn 18016  ∞Metcxmt 19552 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-fz 12198  df-fzo 12335  df-seq 12664  df-hash 12980  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-0g 15925  df-gsum 15926  df-xrs 15985  df-imas 15991  df-mre 16069  df-mrc 16070  df-acs 16072  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-mulg 17364  df-cntz 17573  df-cmn 18018  df-xmet 19560 This theorem is referenced by:  imasdsf1o  21989
 Copyright terms: Public domain W3C validator