Theorem imasdsf1olem 24317

Description: Lemma for imasdsf1o 24318. (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.

Step	Hyp	Ref	Expression
1		imasdsf1o.u	. . . 4 ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))
2		imasdsf1o.v	. . . 4 ⊢ (𝜑 → 𝑉 = (Base‘𝑅))
3		imasdsf1o.f	. . . . 5 ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵)
4		f1ofo 6830	. . . . 5 ⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹:𝑉–onto→𝐵)
5	3, 4	syl 17	. . . 4 ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
6		imasdsf1o.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑍)
7		eqid 2736	. . . 4 ⊢ (dist‘𝑅) = (dist‘𝑅)
8		imasdsf1o.d	. . . 4 ⊢ 𝐷 = (dist‘𝑈)
9		f1of 6823	. . . . . 6 ⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹:𝑉⟶𝐵)
10	3, 9	syl 17	. . . . 5 ⊢ (𝜑 → 𝐹:𝑉⟶𝐵)
11		imasdsf1o.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
12	10, 11	ffvelcdmd 7080	. . . 4 ⊢ (𝜑 → (𝐹‘𝑋) ∈ 𝐵)
13		imasdsf1o.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
14	10, 13	ffvelcdmd 7080	. . . 4 ⊢ (𝜑 → (𝐹‘𝑌) ∈ 𝐵)
15		imasdsf1o.s	. . . 4 ⊢ 𝑆 = {ℎ ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))}
16		imasdsf1o.e	. . . 4 ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))
17	1, 2, 5, 6, 7, 8, 12, 14, 15, 16	imasdsval2 17535	. . 3 ⊢ (𝜑 → ((𝐹‘𝑋)𝐷(𝐹‘𝑌)) = inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))), ℝ*, < ))
18		imasdsf1o.t	. . . 4 ⊢ 𝑇 = ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
19	18	infeq1i 9496	. . 3 ⊢ inf(𝑇, ℝ*, < ) = inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))), ℝ*, < )
20	17, 19	eqtr4di 2789	. 2 ⊢ (𝜑 → ((𝐹‘𝑋)𝐷(𝐹‘𝑌)) = inf(𝑇, ℝ*, < ))
21		xrsbas 21351	. . . . . . . . . . . 12 ⊢ ℝ* = (Base‘ℝ*𝑠)
22		xrsadd 21352	. . . . . . . . . . . 12 ⊢ +𝑒 = (+g‘ℝ*𝑠)
23		imasdsf1o.w	. . . . . . . . . . . 12 ⊢ 𝑊 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞}))
24		xrsex 21350	. . . . . . . . . . . . 13 ⊢ ℝ*𝑠 ∈ V
25	24	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ℝ*𝑠 ∈ V)
26		fzfid 13996	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1...𝑛) ∈ Fin)
27		difss 4116	. . . . . . . . . . . . 13 ⊢ (ℝ* ∖ {-∞}) ⊆ ℝ*
28	27	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ* ∖ {-∞}) ⊆ ℝ*)
29		imasdsf1o.m	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸 ∈ (∞Met‘𝑉))
30		xmetf 24273	. . . . . . . . . . . . . . . 16 ⊢ (𝐸 ∈ (∞Met‘𝑉) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
31		ffn 6711	. . . . . . . . . . . . . . . 16 ⊢ (𝐸:(𝑉 × 𝑉)⟶ℝ* → 𝐸 Fn (𝑉 × 𝑉))
32	29, 30, 31	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐸 Fn (𝑉 × 𝑉))
33		xmetcl 24275	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉) → (𝑓𝐸𝑔) ∈ ℝ*)
34		xmetge0 24288	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉) → 0 ≤ (𝑓𝐸𝑔))
35		ge0nemnf 13194	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓𝐸𝑔) ∈ ℝ* ∧ 0 ≤ (𝑓𝐸𝑔)) → (𝑓𝐸𝑔) ≠ -∞)
36	33, 34, 35	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉) → (𝑓𝐸𝑔) ≠ -∞)
37		eldifsn 4767	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}) ↔ ((𝑓𝐸𝑔) ∈ ℝ* ∧ (𝑓𝐸𝑔) ≠ -∞))
38	33, 36, 37	sylanbrc 583	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
39	38	3expb 1120	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉)) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
40	29, 39	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉)) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
41	40	ralrimivva 3188	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑓 ∈ 𝑉 ∀𝑔 ∈ 𝑉 (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
42		ffnov 7538	. . . . . . . . . . . . . . 15 ⊢ (𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}) ↔ (𝐸 Fn (𝑉 × 𝑉) ∧ ∀𝑓 ∈ 𝑉 ∀𝑔 ∈ 𝑉 (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞})))
43	32, 41, 42	sylanbrc 583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
44	43	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
45	15	ssrab3 4062	. . . . . . . . . . . . . . . 16 ⊢ 𝑆 ⊆ ((𝑉 × 𝑉) ↑m (1...𝑛))
46	45	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑆 ⊆ ((𝑉 × 𝑉) ↑m (1...𝑛)))
47	46	sselda 3963	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑔 ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)))
48		elmapi 8868	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
49	47, 48	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
50		fco 6735	. . . . . . . . . . . . 13 ⊢ ((𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}) ∧ 𝑔:(1...𝑛)⟶(𝑉 × 𝑉)) → (𝐸 ∘ 𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
51	44, 49, 50	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸 ∘ 𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
52		0re 11242	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
53		rexr 11286	. . . . . . . . . . . . . 14 ⊢ (0 ∈ ℝ → 0 ∈ ℝ*)
54		renemnf 11289	. . . . . . . . . . . . . 14 ⊢ (0 ∈ ℝ → 0 ≠ -∞)
55		eldifsn 4767	. . . . . . . . . . . . . 14 ⊢ (0 ∈ (ℝ* ∖ {-∞}) ↔ (0 ∈ ℝ* ∧ 0 ≠ -∞))
56	53, 54, 55	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℝ → 0 ∈ (ℝ* ∖ {-∞}))
57	52, 56	mp1i 13	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 0 ∈ (ℝ* ∖ {-∞}))
58		xaddlid 13263	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ* → (0 +𝑒 𝑥) = 𝑥)
59		xaddrid 13262	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ* → (𝑥 +𝑒 0) = 𝑥)
60	58, 59	jca 511	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ* → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
61	60	adantl 481	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ 𝑥 ∈ ℝ*) → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
62	21, 22, 23, 25, 26, 28, 51, 57, 61	gsumress 18665	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) = (𝑊 Σg (𝐸 ∘ 𝑔)))
63	23, 21	ressbas2 17264	. . . . . . . . . . . . 13 ⊢ ((ℝ* ∖ {-∞}) ⊆ ℝ* → (ℝ* ∖ {-∞}) = (Base‘𝑊))
64	27, 63	ax-mp 5	. . . . . . . . . . . 12 ⊢ (ℝ* ∖ {-∞}) = (Base‘𝑊)
65	23	xrs10 21378	. . . . . . . . . . . 12 ⊢ 0 = (0g‘𝑊)
66	23	xrs1cmn 21379	. . . . . . . . . . . . 13 ⊢ 𝑊 ∈ CMnd
67	66	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑊 ∈ CMnd)
68		c0ex 11234	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
69	68	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 0 ∈ V)
70	51, 26, 69	fdmfifsupp 9392	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸 ∘ 𝑔) finSupp 0)
71	64, 65, 67, 26, 51, 70	gsumcl 19901	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σg (𝐸 ∘ 𝑔)) ∈ (ℝ* ∖ {-∞}))
72	62, 71	eqeltrd 2835	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ∈ (ℝ* ∖ {-∞}))
73	72	eldifad 3943	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ∈ ℝ*)
74	73	fmpttd 7110	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))):𝑆⟶ℝ*)
75	74	frnd 6719	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ⊆ ℝ*)
76	75	ralrimiva 3133	. . . . . 6 ⊢ (𝜑 → ∀𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ⊆ ℝ*)
77		iunss 5026	. . . . . 6 ⊢ (∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ⊆ ℝ* ↔ ∀𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ⊆ ℝ*)
78	76, 77	sylibr 234	. . . . 5 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ⊆ ℝ*)
79	18, 78	eqsstrid 4002	. . . 4 ⊢ (𝜑 → 𝑇 ⊆ ℝ*)
80		infxrcl 13355	. . . 4 ⊢ (𝑇 ⊆ ℝ* → inf(𝑇, ℝ*, < ) ∈ ℝ*)
81	79, 80	syl 17	. . 3 ⊢ (𝜑 → inf(𝑇, ℝ*, < ) ∈ ℝ*)
82		xmetcl 24275	. . . 4 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋𝐸𝑌) ∈ ℝ*)
83	29, 11, 13, 82	syl3anc 1373	. . 3 ⊢ (𝜑 → (𝑋𝐸𝑌) ∈ ℝ*)
84		1nn 12256	. . . . . . 7 ⊢ 1 ∈ ℕ
85		1ex 11236	. . . . . . . . . . . 12 ⊢ 1 ∈ V
86		opex 5444	. . . . . . . . . . . 12 ⊢ ⟨𝑋, 𝑌⟩ ∈ V
87	85, 86	f1osn 6863	. . . . . . . . . . 11 ⊢ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}–1-1-onto→{⟨𝑋, 𝑌⟩}
88		f1of 6823	. . . . . . . . . . 11 ⊢ ({⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}–1-1-onto→{⟨𝑋, 𝑌⟩} → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩})
89	87, 88	ax-mp 5	. . . . . . . . . 10 ⊢ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩}
90	11, 13	opelxpd 5698	. . . . . . . . . . 11 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉))
91	90	snssd 4790	. . . . . . . . . 10 ⊢ (𝜑 → {⟨𝑋, 𝑌⟩} ⊆ (𝑉 × 𝑉))
92		fss 6727	. . . . . . . . . 10 ⊢ (({⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩} ∧ {⟨𝑋, 𝑌⟩} ⊆ (𝑉 × 𝑉)) → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉))
93	89, 91, 92	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉))
94	29	elfvexd 6920	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ∈ V)
95	94, 94	xpexd 7750	. . . . . . . . . 10 ⊢ (𝜑 → (𝑉 × 𝑉) ∈ V)
96		snex 5411	. . . . . . . . . 10 ⊢ {1} ∈ V
97		elmapg 8858	. . . . . . . . . 10 ⊢ (((𝑉 × 𝑉) ∈ V ∧ {1} ∈ V) → ({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑m {1}) ↔ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉)))
98	95, 96, 97	sylancl 586	. . . . . . . . 9 ⊢ (𝜑 → ({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑m {1}) ↔ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉)))
99	93, 98	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → {⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑m {1}))
100		op1stg 8005	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋)
101	11, 13, 100	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋)
102	101	fveq2d 6885	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋))
103		op2ndg 8006	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
104	11, 13, 103	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
105	104	fveq2d 6885	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌))
106	102, 105	jca 511	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌)))
107	24	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ*𝑠 ∈ V)
108		snfi 9062	. . . . . . . . . . 11 ⊢ {1} ∈ Fin
109	108	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → {1} ∈ Fin)
110	27	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ* ∖ {-∞}) ⊆ ℝ*)
111		xmetge0 24288	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → 0 ≤ (𝑋𝐸𝑌))
112	29, 11, 13, 111	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ≤ (𝑋𝐸𝑌))
113		ge0nemnf 13194	. . . . . . . . . . . . . 14 ⊢ (((𝑋𝐸𝑌) ∈ ℝ* ∧ 0 ≤ (𝑋𝐸𝑌)) → (𝑋𝐸𝑌) ≠ -∞)
114	83, 112, 113	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋𝐸𝑌) ≠ -∞)
115		eldifsn 4767	. . . . . . . . . . . . 13 ⊢ ((𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}) ↔ ((𝑋𝐸𝑌) ∈ ℝ* ∧ (𝑋𝐸𝑌) ≠ -∞))
116	83, 114, 115	sylanbrc 583	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}))
117		fconst6g 6772	. . . . . . . . . . . 12 ⊢ ((𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}) → ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞}))
118	116, 117	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞}))
119		fcoconst 7129	. . . . . . . . . . . . . 14 ⊢ ((𝐸 Fn (𝑉 × 𝑉) ∧ ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉)) → (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}))
120	32, 90, 119	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}))
121	85, 86	xpsn 7136	. . . . . . . . . . . . . 14 ⊢ ({1} × {⟨𝑋, 𝑌⟩}) = {⟨1, ⟨𝑋, 𝑌⟩⟩}
122	121	coeq2i 5845	. . . . . . . . . . . . 13 ⊢ (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})
123		df-ov 7413	. . . . . . . . . . . . . . . 16 ⊢ (𝑋𝐸𝑌) = (𝐸‘⟨𝑋, 𝑌⟩)
124	123	eqcomi 2745	. . . . . . . . . . . . . . 15 ⊢ (𝐸‘⟨𝑋, 𝑌⟩) = (𝑋𝐸𝑌)
125	124	sneqi 4617	. . . . . . . . . . . . . 14 ⊢ {(𝐸‘⟨𝑋, 𝑌⟩)} = {(𝑋𝐸𝑌)}
126	125	xpeq2i 5686	. . . . . . . . . . . . 13 ⊢ ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}) = ({1} × {(𝑋𝐸𝑌)})
127	120, 122, 126	3eqtr3g 2794	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}) = ({1} × {(𝑋𝐸𝑌)}))
128	127	feq1d 6695	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}):{1}⟶(ℝ* ∖ {-∞}) ↔ ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞})))
129	118, 128	mpbird 257	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}):{1}⟶(ℝ* ∖ {-∞}))
130	52, 56	mp1i 13	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ (ℝ* ∖ {-∞}))
131	60	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
132	21, 22, 23, 107, 109, 110, 129, 130, 131	gsumress 18665	. . . . . . . . 9 ⊢ (𝜑 → (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})) = (𝑊 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
133		fconstmpt 5721	. . . . . . . . . . 11 ⊢ ({1} × {(𝑋𝐸𝑌)}) = (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))
134	127, 133	eqtrdi 2787	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}) = (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌)))
135	134	oveq2d 7426	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})) = (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))))
136		cmnmnd 19783	. . . . . . . . . . 11 ⊢ (𝑊 ∈ CMnd → 𝑊 ∈ Mnd)
137	66, 136	mp1i 13	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ Mnd)
138	84	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℕ)
139		eqidd 2737	. . . . . . . . . . 11 ⊢ (𝑗 = 1 → (𝑋𝐸𝑌) = (𝑋𝐸𝑌))
140	64, 139	gsumsn 19940	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Mnd ∧ 1 ∈ ℕ ∧ (𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞})) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))) = (𝑋𝐸𝑌))
141	137, 138, 116, 140	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))) = (𝑋𝐸𝑌))
142	132, 135, 141	3eqtrrd 2776	. . . . . . . 8 ⊢ (𝜑 → (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
143		fveq1 6880	. . . . . . . . . . . . . 14 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝑔‘1) = ({⟨1, ⟨𝑋, 𝑌⟩⟩}‘1))
144	85, 86	fvsn 7178	. . . . . . . . . . . . . 14 ⊢ ({⟨1, ⟨𝑋, 𝑌⟩⟩}‘1) = ⟨𝑋, 𝑌⟩
145	143, 144	eqtrdi 2787	. . . . . . . . . . . . 13 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝑔‘1) = ⟨𝑋, 𝑌⟩)
146	145	fveq2d 6885	. . . . . . . . . . . 12 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (1st ‘(𝑔‘1)) = (1st ‘⟨𝑋, 𝑌⟩))
147	146	fveqeq2d 6889	. . . . . . . . . . 11 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ↔ (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋)))
148	145	fveq2d 6885	. . . . . . . . . . . 12 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (2nd ‘(𝑔‘1)) = (2nd ‘⟨𝑋, 𝑌⟩))
149	148	fveqeq2d 6889	. . . . . . . . . . 11 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌) ↔ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌)))
150	147, 149	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ↔ ((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌))))
151		coeq2 5843	. . . . . . . . . . . 12 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝐸 ∘ 𝑔) = (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}))
152	151	oveq2d 7426	. . . . . . . . . . 11 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
153	152	eqeq2d 2747	. . . . . . . . . 10 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ↔ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}))))
154	150, 153	anbi12d 632	. . . . . . . . 9 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ (((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))))
155	154	rspcev 3606	. . . . . . . 8 ⊢ (({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑m {1}) ∧ (((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))) → ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
156	99, 106, 142, 155	syl12anc 836	. . . . . . 7 ⊢ (𝜑 → ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
157		ovex 7443	. . . . . . . . . 10 ⊢ (𝑋𝐸𝑌) ∈ V
158		eqid 2736	. . . . . . . . . . 11 ⊢ (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) = (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
159	158	elrnmpt 5943	. . . . . . . . . 10 ⊢ ((𝑋𝐸𝑌) ∈ V → ((𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
160	157, 159	ax-mp 5	. . . . . . . . 9 ⊢ ((𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
161	15	rexeqi 3308	. . . . . . . . . . 11 ⊢ (∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ↔ ∃𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))} (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
162		fveq1 6880	. . . . . . . . . . . . . . 15 ⊢ (ℎ = 𝑔 → (ℎ‘1) = (𝑔‘1))
163	162	fveq2d 6885	. . . . . . . . . . . . . 14 ⊢ (ℎ = 𝑔 → (1st ‘(ℎ‘1)) = (1st ‘(𝑔‘1)))
164	163	fveqeq2d 6889	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑔 → ((𝐹‘(1st ‘(ℎ‘1))) = (𝐹‘𝑋) ↔ (𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋)))
165		fveq1 6880	. . . . . . . . . . . . . . 15 ⊢ (ℎ = 𝑔 → (ℎ‘𝑛) = (𝑔‘𝑛))
166	165	fveq2d 6885	. . . . . . . . . . . . . 14 ⊢ (ℎ = 𝑔 → (2nd ‘(ℎ‘𝑛)) = (2nd ‘(𝑔‘𝑛)))
167	166	fveqeq2d 6889	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑔 → ((𝐹‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ↔ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)))
168		fveq1 6880	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = 𝑔 → (ℎ‘𝑖) = (𝑔‘𝑖))
169	168	fveq2d 6885	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = 𝑔 → (2nd ‘(ℎ‘𝑖)) = (2nd ‘(𝑔‘𝑖)))
170	169	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ (ℎ = 𝑔 → (𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(2nd ‘(𝑔‘𝑖))))
171		fveq1 6880	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = 𝑔 → (ℎ‘(𝑖 + 1)) = (𝑔‘(𝑖 + 1)))
172	171	fveq2d 6885	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = 𝑔 → (1st ‘(ℎ‘(𝑖 + 1))) = (1st ‘(𝑔‘(𝑖 + 1))))
173	172	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ (ℎ = 𝑔 → (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
174	170, 173	eqeq12d 2752	. . . . . . . . . . . . . 14 ⊢ (ℎ = 𝑔 → ((𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
175	174	ralbidv 3164	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑔 → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
176	164, 167, 175	3anbi123d 1438	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑔 → (((𝐹‘(1st ‘(ℎ‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
177	176	rexrab 3684	. . . . . . . . . . 11 ⊢ (∃𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))} (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
178	161, 177	bitri 275	. . . . . . . . . 10 ⊢ (∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
179		oveq2 7418	. . . . . . . . . . . . 13 ⊢ (𝑛 = 1 → (1...𝑛) = (1...1))
180		1z 12627	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℤ
181		fzsn 13588	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℤ → (1...1) = {1})
182	180, 181	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (1...1) = {1}
183	179, 182	eqtrdi 2787	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (1...𝑛) = {1})
184	183	oveq2d 7426	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → ((𝑉 × 𝑉) ↑m (1...𝑛)) = ((𝑉 × 𝑉) ↑m {1}))
185		df-3an 1088	. . . . . . . . . . . . 13 ⊢ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
186		ral0 4493	. . . . . . . . . . . . . . . 16 ⊢ ∀𝑖 ∈ ∅ (𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))
187		oveq1 7417	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 1 → (𝑛 − 1) = (1 − 1))
188		1m1e0 12317	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 − 1) = 0
189	187, 188	eqtrdi 2787	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 1 → (𝑛 − 1) = 0)
190	189	oveq2d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 1 → (1...(𝑛 − 1)) = (1...0))
191		fz10 13567	. . . . . . . . . . . . . . . . . 18 ⊢ (1...0) = ∅
192	190, 191	eqtrdi 2787	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 1 → (1...(𝑛 − 1)) = ∅)
193	192	raleqdv 3309	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1 → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ ∅ (𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
194	186, 193	mpbiri 258	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1 → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
195	194	biantrud 531	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
196		2fveq3 6886	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1 → (2nd ‘(𝑔‘𝑛)) = (2nd ‘(𝑔‘1)))
197	196	fveqeq2d 6889	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1 → ((𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ↔ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)))
198	197	anbi2d 630	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌))))
199	195, 198	bitr3d 281	. . . . . . . . . . . . 13 ⊢ (𝑛 = 1 → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌))))
200	185, 199	bitrid 283	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌))))
201	200	anbi1d 631	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))))
202	184, 201	rexeqbidv 3330	. . . . . . . . . 10 ⊢ (𝑛 = 1 → (∃𝑔 ∈ ((𝑉 × 𝑉) ↑m (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))))
203	178, 202	bitrid 283	. . . . . . . . 9 ⊢ (𝑛 = 1 → (∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))))
204	160, 203	bitrid 283	. . . . . . . 8 ⊢ (𝑛 = 1 → ((𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))))
205	204	rspcev 3606	. . . . . . 7 ⊢ ((1 ∈ ℕ ∧ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))) → ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
206	84, 156, 205	sylancr 587	. . . . . 6 ⊢ (𝜑 → ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
207		eliun 4976	. . . . . 6 ⊢ ((𝑋𝐸𝑌) ∈ ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
208	206, 207	sylibr 234	. . . . 5 ⊢ (𝜑 → (𝑋𝐸𝑌) ∈ ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
209	208, 18	eleqtrrdi 2846	. . . 4 ⊢ (𝜑 → (𝑋𝐸𝑌) ∈ 𝑇)
210		infxrlb 13356	. . . 4 ⊢ ((𝑇 ⊆ ℝ* ∧ (𝑋𝐸𝑌) ∈ 𝑇) → inf(𝑇, ℝ*, < ) ≤ (𝑋𝐸𝑌))
211	79, 209, 210	syl2anc 584	. . 3 ⊢ (𝜑 → inf(𝑇, ℝ*, < ) ≤ (𝑋𝐸𝑌))
212	18	eleq2i 2827	. . . . . . 7 ⊢ (𝑝 ∈ 𝑇 ↔ 𝑝 ∈ ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
213		eliun 4976	. . . . . . 7 ⊢ (𝑝 ∈ ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
214	212, 213	bitri 275	. . . . . 6 ⊢ (𝑝 ∈ 𝑇 ↔ ∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
215	158	elrnmpt 5943	. . . . . . . . 9 ⊢ (𝑝 ∈ V → (𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ 𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
216	215	elv 3469	. . . . . . . 8 ⊢ (𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ 𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
217	176, 15	elrab2 3679	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∈ 𝑆 ↔ (𝑔 ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∧ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
218	217	simprbi 496	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 ∈ 𝑆 → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
219	218	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
220	219	simp2d 1143	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌))
221	3	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐹:𝑉–1-1-onto→𝐵)
222		f1of1 6822	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹:𝑉–1-1→𝐵)
223	221, 222	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐹:𝑉–1-1→𝐵)
224		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑛 ∈ ℕ)
225		elfz1end 13576	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (1...𝑛))
226	224, 225	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑛 ∈ (1...𝑛))
227	49, 226	ffvelcdmd 7080	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑔‘𝑛) ∈ (𝑉 × 𝑉))
228		xp2nd 8026	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔‘𝑛) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘𝑛)) ∈ 𝑉)
229	227, 228	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (2nd ‘(𝑔‘𝑛)) ∈ 𝑉)
230	13	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑌 ∈ 𝑉)
231		f1fveq 7260	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ ((2nd ‘(𝑔‘𝑛)) ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ((𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ↔ (2nd ‘(𝑔‘𝑛)) = 𝑌))
232	223, 229, 230, 231	syl12anc 836	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ↔ (2nd ‘(𝑔‘𝑛)) = 𝑌))
233	220, 232	mpbid 232	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (2nd ‘(𝑔‘𝑛)) = 𝑌)
234	233	oveq2d 7426	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2nd ‘(𝑔‘𝑛))) = (𝑋𝐸𝑌))
235		eleq1 2823	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 1 → (𝑚 ∈ (1...𝑛) ↔ 1 ∈ (1...𝑛)))
236		2fveq3 6886	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 1 → (2nd ‘(𝑔‘𝑚)) = (2nd ‘(𝑔‘1)))
237	236	oveq2d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 1 → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘1))))
238		oveq2 7418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 1 → (1...𝑚) = (1...1))
239	238, 182	eqtrdi 2787	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 1 → (1...𝑚) = {1})
240	239	reseq2d 5971	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 1 → ((𝐸 ∘ 𝑔) ↾ (1...𝑚)) = ((𝐸 ∘ 𝑔) ↾ {1}))
241	240	oveq2d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 1 → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1})))
242	237, 241	breq12d 5137	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 1 → ((𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1}))))
243	235, 242	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 1 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚)))) ↔ (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1})))))
244	243	imbi2d 340	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 1 → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))))) ↔ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1}))))))
245		eleq1 2823	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑥 → (𝑚 ∈ (1...𝑛) ↔ 𝑥 ∈ (1...𝑛)))
246		2fveq3 6886	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑥 → (2nd ‘(𝑔‘𝑚)) = (2nd ‘(𝑔‘𝑥)))
247	246	oveq2d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑥 → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘𝑥))))
248		oveq2 7418	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑥 → (1...𝑚) = (1...𝑥))
249	248	reseq2d 5971	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑥 → ((𝐸 ∘ 𝑔) ↾ (1...𝑚)) = ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))
250	249	oveq2d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑥 → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))))
251	247, 250	breq12d 5137	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑥 → ((𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))))
252	245, 251	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑥 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚)))) ↔ (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))))))
253	252	imbi2d 340	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑥 → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))))) ↔ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))))))
254		eleq1 2823	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑥 + 1) → (𝑚 ∈ (1...𝑛) ↔ (𝑥 + 1) ∈ (1...𝑛)))
255		2fveq3 6886	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = (𝑥 + 1) → (2nd ‘(𝑔‘𝑚)) = (2nd ‘(𝑔‘(𝑥 + 1))))
256	255	oveq2d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = (𝑥 + 1) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))))
257		oveq2 7418	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = (𝑥 + 1) → (1...𝑚) = (1...(𝑥 + 1)))
258	257	reseq2d 5971	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = (𝑥 + 1) → ((𝐸 ∘ 𝑔) ↾ (1...𝑚)) = ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))
259	258	oveq2d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = (𝑥 + 1) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))))
260	256, 259	breq12d 5137	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑥 + 1) → ((𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))))
261	254, 260	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝑥 + 1) → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚)))) ↔ ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))))))
262	261	imbi2d 340	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝑥 + 1) → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))))) ↔ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))))))
263		eleq1 2823	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ (1...𝑛) ↔ 𝑛 ∈ (1...𝑛)))
264		2fveq3 6886	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → (2nd ‘(𝑔‘𝑚)) = (2nd ‘(𝑔‘𝑛)))
265	264	oveq2d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘𝑛))))
266		oveq2 7418	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
267	266	reseq2d 5971	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → ((𝐸 ∘ 𝑔) ↾ (1...𝑚)) = ((𝐸 ∘ 𝑔) ↾ (1...𝑛)))
268	267	oveq2d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))
269	265, 268	breq12d 5137	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → ((𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛)))))
270	263, 269	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑛 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚)))) ↔ (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))))
271	270	imbi2d 340	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑛 → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))))) ↔ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛)))))))
272	29	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐸 ∈ (∞Met‘𝑉))
273	11	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑋 ∈ 𝑉)
274		nnuz 12900	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℕ = (ℤ≥‘1)
275	224, 274	eleqtrdi 2845	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑛 ∈ (ℤ≥‘1))
276		eluzfz1 13553	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (ℤ≥‘1) → 1 ∈ (1...𝑛))
277	275, 276	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 1 ∈ (1...𝑛))
278	49, 277	ffvelcdmd 7080	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑔‘1) ∈ (𝑉 × 𝑉))
279		xp2nd 8026	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔‘1) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘1)) ∈ 𝑉)
280	278, 279	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (2nd ‘(𝑔‘1)) ∈ 𝑉)
281		xmetcl 24275	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ (2nd ‘(𝑔‘1)) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔‘1))) ∈ ℝ*)
282	272, 273, 280, 281	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ∈ ℝ*)
283	282	xrleidd 13173	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑋𝐸(2nd ‘(𝑔‘1))))
284	137	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑊 ∈ Mnd)
285	84	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 1 ∈ ℕ)
286	44, 278	ffvelcdmd 7080	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸‘(𝑔‘1)) ∈ (ℝ* ∖ {-∞}))
287		2fveq3 6886	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 1 → (𝐸‘(𝑔‘𝑗)) = (𝐸‘(𝑔‘1)))
288	64, 287	gsumsn 19940	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Mnd ∧ 1 ∈ ℕ ∧ (𝐸‘(𝑔‘1)) ∈ (ℝ* ∖ {-∞})) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗)))) = (𝐸‘(𝑔‘1)))
289	284, 285, 286, 288	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗)))) = (𝐸‘(𝑔‘1)))
290	272, 30	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
291		fcompt 7128	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐸:(𝑉 × 𝑉)⟶ℝ* ∧ 𝑔:(1...𝑛)⟶(𝑉 × 𝑉)) → (𝐸 ∘ 𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))))
292	290, 49, 291	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸 ∘ 𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))))
293	292	reseq1d 5970	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐸 ∘ 𝑔) ↾ {1}) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ {1}))
294	277	snssd 4790	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → {1} ⊆ (1...𝑛))
295	294	resmptd 6032	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ {1}) = (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗))))
296	293, 295	eqtrd 2771	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐸 ∘ 𝑔) ↾ {1}) = (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗))))
297	296	oveq2d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1})) = (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗)))))
298		df-ov 7413	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋𝐸(2nd ‘(𝑔‘1))) = (𝐸‘⟨𝑋, (2nd ‘(𝑔‘1))⟩)
299		1st2nd2 8032	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔‘1) ∈ (𝑉 × 𝑉) → (𝑔‘1) = ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩)
300	278, 299	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑔‘1) = ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩)
301	219	simp1d 1142	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋))
302		xp1st 8025	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔‘1) ∈ (𝑉 × 𝑉) → (1st ‘(𝑔‘1)) ∈ 𝑉)
303	278, 302	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1st ‘(𝑔‘1)) ∈ 𝑉)
304		f1fveq 7260	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ ((1st ‘(𝑔‘1)) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ↔ (1st ‘(𝑔‘1)) = 𝑋))
305	223, 303, 273, 304	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ↔ (1st ‘(𝑔‘1)) = 𝑋))
306	301, 305	mpbid 232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1st ‘(𝑔‘1)) = 𝑋)
307	306	opeq1d 4860	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩ = ⟨𝑋, (2nd ‘(𝑔‘1))⟩)
308	300, 307	eqtr2d 2772	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ⟨𝑋, (2nd ‘(𝑔‘1))⟩ = (𝑔‘1))
309	308	fveq2d 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸‘⟨𝑋, (2nd ‘(𝑔‘1))⟩) = (𝐸‘(𝑔‘1)))
310	298, 309	eqtrid 2783	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) = (𝐸‘(𝑔‘1)))
311	289, 297, 310	3eqtr4d 2781	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1})) = (𝑋𝐸(2nd ‘(𝑔‘1))))
312	283, 311	breqtrrd 5152	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1})))
313	312	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1}))))
314		simprl 770	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ ℕ)
315	314, 274	eleqtrdi 2845	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (ℤ≥‘1))
316		simprr 772	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑥 + 1) ∈ (1...𝑛))
317		peano2fzr 13559	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (ℤ≥‘1) ∧ (𝑥 + 1) ∈ (1...𝑛)) → 𝑥 ∈ (1...𝑛))
318	315, 316, 317	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (1...𝑛))
319	318	expr 456	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 + 1) ∈ (1...𝑛) → 𝑥 ∈ (1...𝑛)))
320	319	imim1d 82	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))))))
321	272	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸 ∈ (∞Met‘𝑉))
322	273	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑋 ∈ 𝑉)
323	49	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
324	323, 318	ffvelcdmd 7080	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘𝑥) ∈ (𝑉 × 𝑉))
325		xp2nd 8026	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔‘𝑥) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘𝑥)) ∈ 𝑉)
326	324, 325	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔‘𝑥)) ∈ 𝑉)
327		xmetcl 24275	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ (2nd ‘(𝑔‘𝑥)) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ∈ ℝ*)
328	321, 322, 326, 327	syl3anc 1373	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ∈ ℝ*)
329	66	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑊 ∈ CMnd)
330		fzfid 13996	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...𝑥) ∈ Fin)
331	51	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸 ∘ 𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
332		fzsuc 13593	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (ℤ≥‘1) → (1...(𝑥 + 1)) = ((1...𝑥) ∪ {(𝑥 + 1)}))
333	315, 332	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...(𝑥 + 1)) = ((1...𝑥) ∪ {(𝑥 + 1)}))
334		elfzuz3 13543	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 + 1) ∈ (1...𝑛) → 𝑛 ∈ (ℤ≥‘(𝑥 + 1)))
335	334	ad2antll 729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑛 ∈ (ℤ≥‘(𝑥 + 1)))
336		fzss2 13586	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ (ℤ≥‘(𝑥 + 1)) → (1...(𝑥 + 1)) ⊆ (1...𝑛))
337	335, 336	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...(𝑥 + 1)) ⊆ (1...𝑛))
338	333, 337	eqsstrrd 3999	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((1...𝑥) ∪ {(𝑥 + 1)}) ⊆ (1...𝑛))
339	338	unssad 4173	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...𝑥) ⊆ (1...𝑛))
340	331, 339	fssresd 6750	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...𝑥)):(1...𝑥)⟶(ℝ* ∖ {-∞}))
341	68	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 0 ∈ V)
342	340, 330, 341	fdmfifsupp 9392	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...𝑥)) finSupp 0)
343	64, 65, 329, 330, 340, 342	gsumcl 19901	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) ∈ (ℝ* ∖ {-∞}))
344	343	eldifad 3943	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) ∈ ℝ*)
345	321, 30	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
346	323, 316	ffvelcdmd 7080	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉))
347	345, 346	ffvelcdmd 7080	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*)
348		xleadd1a 13274	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ∈ ℝ* ∧ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) ∈ ℝ* ∧ (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*) ∧ (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
349	348	ex 412	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ∈ ℝ* ∧ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) ∈ ℝ* ∧ (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
350	328, 344, 347, 349	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
351		xp2nd 8026	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
352	346, 351	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
353		xmettri 24295	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑋 ∈ 𝑉 ∧ (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉 ∧ (2nd ‘(𝑔‘𝑥)) ∈ 𝑉)) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 ((2nd ‘(𝑔‘𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
354	321, 322, 352, 326, 353	syl13anc 1374	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 ((2nd ‘(𝑔‘𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
355		1st2nd2 8032	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (𝑔‘(𝑥 + 1)) = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
356	346, 355	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
357		2fveq3 6886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 = 𝑥 → (2nd ‘(𝑔‘𝑖)) = (2nd ‘(𝑔‘𝑥)))
358	357	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝑥 → (𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(2nd ‘(𝑔‘𝑥))))
359		fvoveq1 7433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = 𝑥 → (𝑔‘(𝑖 + 1)) = (𝑔‘(𝑥 + 1)))
360	359	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 = 𝑥 → (1st ‘(𝑔‘(𝑖 + 1))) = (1st ‘(𝑔‘(𝑥 + 1))))
361	360	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝑥 → (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))))
362	358, 361	eqeq12d 2752	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 = 𝑥 → ((𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(𝑔‘𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1))))))
363	219	simp3d 1144	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
364	363	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
365		nnz 12614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℤ)
366	365	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ ℤ)
367		eluzp1m1 12883	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ (ℤ≥‘(𝑥 + 1))) → (𝑛 − 1) ∈ (ℤ≥‘𝑥))
368	366, 335, 367	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑛 − 1) ∈ (ℤ≥‘𝑥))
369		elfzuzb 13540	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ (1...(𝑛 − 1)) ↔ (𝑥 ∈ (ℤ≥‘1) ∧ (𝑛 − 1) ∈ (ℤ≥‘𝑥)))
370	315, 368, 369	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (1...(𝑛 − 1)))
371	362, 364, 370	rspcdva 3607	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐹‘(2nd ‘(𝑔‘𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))))
372	223	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐹:𝑉–1-1→𝐵)
373		xp1st 8025	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
374	346, 373	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
375		f1fveq 7260	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ ((2nd ‘(𝑔‘𝑥)) ∈ 𝑉 ∧ (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)) → ((𝐹‘(2nd ‘(𝑔‘𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))) ↔ (2nd ‘(𝑔‘𝑥)) = (1st ‘(𝑔‘(𝑥 + 1)))))
376	372, 326, 374, 375	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐹‘(2nd ‘(𝑔‘𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))) ↔ (2nd ‘(𝑔‘𝑥)) = (1st ‘(𝑔‘(𝑥 + 1)))))
377	371, 376	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔‘𝑥)) = (1st ‘(𝑔‘(𝑥 + 1))))
378	377	opeq1d 4860	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ⟨(2nd ‘(𝑔‘𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩ = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
379	356, 378	eqtr4d 2774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) = ⟨(2nd ‘(𝑔‘𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
380	379	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) = (𝐸‘⟨(2nd ‘(𝑔‘𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩))
381		df-ov 7413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2nd ‘(𝑔‘𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) = (𝐸‘⟨(2nd ‘(𝑔‘𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
382	380, 381	eqtr4di 2789	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) = ((2nd ‘(𝑔‘𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1)))))
383	382	oveq2d 7426	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) = ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 ((2nd ‘(𝑔‘𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
384	354, 383	breqtrrd 5152	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
385		xmetcl 24275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
386	321, 322, 352, 385	syl3anc 1373	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
387	328, 347	xaddcld 13322	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
388	344, 347	xaddcld 13322	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
389		xrletr 13179	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ* ∧ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ* ∧ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*) → (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∧ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
390	386, 387, 388, 389	syl3anc 1373	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∧ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
391	384, 390	mpand 695	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
392	350, 391	syld 47	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
393		xrex 13008	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℝ* ∈ V
394	393	difexi 5305	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℝ* ∖ {-∞}) ∈ V
395	23, 22	ressplusg 17310	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℝ* ∖ {-∞}) ∈ V → +𝑒 = (+g‘𝑊))
396	394, 395	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ +𝑒 = (+g‘𝑊)
397	44	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
398		fzelp1 13598	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (1...𝑥) → 𝑗 ∈ (1...(𝑥 + 1)))
399	49	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
400	337	sselda 3963	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → 𝑗 ∈ (1...𝑛))
401	399, 400	ffvelcdmd 7080	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → (𝑔‘𝑗) ∈ (𝑉 × 𝑉))
402	398, 401	sylan2 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → (𝑔‘𝑗) ∈ (𝑉 × 𝑉))
403	397, 402	ffvelcdmd 7080	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → (𝐸‘(𝑔‘𝑗)) ∈ (ℝ* ∖ {-∞}))
404		fzp1disj 13605	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1...𝑥) ∩ {(𝑥 + 1)}) = ∅
405	404	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((1...𝑥) ∩ {(𝑥 + 1)}) = ∅)
406		disjsn 4692	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1...𝑥) ∩ {(𝑥 + 1)}) = ∅ ↔ ¬ (𝑥 + 1) ∈ (1...𝑥))
407	405, 406	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ¬ (𝑥 + 1) ∈ (1...𝑥))
408	44	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
409	408, 346	ffvelcdmd 7080	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) ∈ (ℝ* ∖ {-∞}))
410		2fveq3 6886	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑥 + 1) → (𝐸‘(𝑔‘𝑗)) = (𝐸‘(𝑔‘(𝑥 + 1))))
411	64, 396, 329, 330, 403, 316, 407, 409, 410	gsumunsn 19946	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔‘𝑗)))) = ((𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗)))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
412	292	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸 ∘ 𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))))
413	412, 333	reseq12d 5972	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ ((1...𝑥) ∪ {(𝑥 + 1)})))
414	338	resmptd 6032	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ ((1...𝑥) ∪ {(𝑥 + 1)})) = (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔‘𝑗))))
415	413, 414	eqtrd 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))) = (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔‘𝑗))))
416	415	oveq2d 7426	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))) = (𝑊 Σg (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔‘𝑗)))))
417	412	reseq1d 5970	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...𝑥)) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ (1...𝑥)))
418	339	resmptd 6032	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ (1...𝑥)) = (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗))))
419	417, 418	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...𝑥)) = (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗))))
420	419	oveq2d 7426	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) = (𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗)))))
421	420	oveq1d 7425	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) = ((𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗)))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
422	411, 416, 421	3eqtr4d 2781	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))) = ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
423	422	breq2d 5136	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))) ↔ (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
424	392, 423	sylibrd 259	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))))
425	320, 424	animpimp2impd 846	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℕ → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))))) → (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))))))
426	244, 253, 262, 271, 313, 425	nnind 12263	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))))
427	224, 426	mpcom 38	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛)))))
428	226, 427	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))
429	234, 428	eqbrtrrd 5148	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸𝑌) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))
430		ffn 6711	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∘ 𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}) → (𝐸 ∘ 𝑔) Fn (1...𝑛))
431		fnresdm 6662	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∘ 𝑔) Fn (1...𝑛) → ((𝐸 ∘ 𝑔) ↾ (1...𝑛)) = (𝐸 ∘ 𝑔))
432	51, 430, 431	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐸 ∘ 𝑔) ↾ (1...𝑛)) = (𝐸 ∘ 𝑔))
433	432	oveq2d 7426	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))) = (𝑊 Σg (𝐸 ∘ 𝑔)))
434	62, 433	eqtr4d 2774	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) = (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))
435	429, 434	breqtrrd 5152	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸𝑌) ≤ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
436		breq2 5128	. . . . . . . . . 10 ⊢ (𝑝 = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) → ((𝑋𝐸𝑌) ≤ 𝑝 ↔ (𝑋𝐸𝑌) ≤ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
437	435, 436	syl5ibrcom 247	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑝 = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) → (𝑋𝐸𝑌) ≤ 𝑝))
438	437	rexlimdva 3142	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∃𝑔 ∈ 𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) → (𝑋𝐸𝑌) ≤ 𝑝))
439	216, 438	biimtrid 242	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) → (𝑋𝐸𝑌) ≤ 𝑝))
440	439	rexlimdva 3142	. . . . . 6 ⊢ (𝜑 → (∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) → (𝑋𝐸𝑌) ≤ 𝑝))
441	214, 440	biimtrid 242	. . . . 5 ⊢ (𝜑 → (𝑝 ∈ 𝑇 → (𝑋𝐸𝑌) ≤ 𝑝))
442	441	ralrimiv 3132	. . . 4 ⊢ (𝜑 → ∀𝑝 ∈ 𝑇 (𝑋𝐸𝑌) ≤ 𝑝)
443		infxrgelb 13357	. . . . 5 ⊢ ((𝑇 ⊆ ℝ* ∧ (𝑋𝐸𝑌) ∈ ℝ*) → ((𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ) ↔ ∀𝑝 ∈ 𝑇 (𝑋𝐸𝑌) ≤ 𝑝))
444	79, 83, 443	syl2anc 584	. . . 4 ⊢ (𝜑 → ((𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ) ↔ ∀𝑝 ∈ 𝑇 (𝑋𝐸𝑌) ≤ 𝑝))
445	442, 444	mpbird 257	. . 3 ⊢ (𝜑 → (𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ))
446	81, 83, 211, 445	xrletrid 13176	. 2 ⊢ (𝜑 → inf(𝑇, ℝ*, < ) = (𝑋𝐸𝑌))
447	20, 446	eqtrd 2771	1 ⊢ (𝜑 → ((𝐹‘𝑋)𝐷(𝐹‘𝑌)) = (𝑋𝐸𝑌))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2933  ∀wral 3052  ∃wrex 3061  {crab 3420  Vcvv 3464   ∖ cdif 3928   ∪ cun 3929   ∩ cin 3930   ⊆ wss 3931  ∅c0 4313  {csn 4606  ⟨cop 4612  ∪ ciun 4972   class class class wbr 5124   ↦ cmpt 5206   × cxp 5657  ran crn 5660   ↾ cres 5661   ∘ ccom 5663   Fn wfn 6531  ⟶wf 6532  –1-1→wf1 6533  –onto→wfo 6534  –1-1-onto→wf1o 6535  ‘cfv 6536  (class class class)co 7410  1^st c1st 7991  2^nd c2nd 7992   ↑_m cmap 8845  Fincfn 8964  infcinf 9458  ℝcr 11133  0cc0 11134  1c1 11135   + caddc 11137  -∞cmnf 11272  ℝ^*cxr 11273   < clt 11274   ≤ cle 11275   − cmin 11471  ℕcn 12245  ℤcz 12593  ℤ_≥cuz 12857   +_𝑒 cxad 13131  ...cfz 13529  Basecbs 17233   ↾_s cress 17256  +_gcplusg 17276  distcds 17285   Σ_g cgsu 17459  ℝ^*_𝑠cxrs 17519   “_s cimas 17523  Mndcmnd 18717  CMndccmn 19766  ∞Metcxmet 21305

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-rep 5254  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-cnex 11190  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211  ax-pre-sup 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-tp 4611  df-op 4613  df-uni 4889  df-int 4928  df-iun 4974  df-iin 4975  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-se 5612  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-of 7676  df-om 7867  df-1st 7993  df-2nd 7994  df-supp 8165  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-2o 8486  df-er 8724  df-map 8847  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fsupp 9379  df-sup 9459  df-inf 9460  df-oi 9529  df-card 9958  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474  df-div 11900  df-nn 12246  df-2 12308  df-3 12309  df-4 12310  df-5 12311  df-6 12312  df-7 12313  df-8 12314  df-9 12315  df-n0 12507  df-z 12594  df-dec 12714  df-uz 12858  df-rp 13014  df-xneg 13133  df-xadd 13134  df-xmul 13135  df-fz 13530  df-fzo 13677  df-seq 14025  df-hash 14354  df-struct 17171  df-sets 17188  df-slot 17206  df-ndx 17218  df-base 17234  df-ress 17257  df-plusg 17289  df-mulr 17290  df-sca 17292  df-vsca 17293  df-ip 17294  df-tset 17295  df-ple 17296  df-ds 17298  df-0g 17460  df-gsum 17461  df-xrs 17521  df-imas 17527  df-mre 17603  df-mrc 17604  df-acs 17606  df-mgm 18623  df-sgrp 18702  df-mnd 18718  df-submnd 18767  df-mulg 19056  df-cntz 19305  df-cmn 19768  df-xmet 21313

This theorem is referenced by:  imasdsf1o  24318