Theorem imasdsf1olem 22977

Description: Lemma for imasdsf1o 22978. (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 6617	. . . . 5 ⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹:𝑉–onto→𝐵)
5	3, 4	syl 17	. . . 4 ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
6		imasdsf1o.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑍)
7		eqid 2821	. . . 4 ⊢ (dist‘𝑅) = (dist‘𝑅)
8		imasdsf1o.d	. . . 4 ⊢ 𝐷 = (dist‘𝑈)
9		f1of 6610	. . . . . 6 ⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹:𝑉⟶𝐵)
10	3, 9	syl 17	. . . . 5 ⊢ (𝜑 → 𝐹:𝑉⟶𝐵)
11		imasdsf1o.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
12	10, 11	ffvelrnd 6847	. . . 4 ⊢ (𝜑 → (𝐹‘𝑋) ∈ 𝐵)
13		imasdsf1o.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
14	10, 13	ffvelrnd 6847	. . . 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 16783	. . 3 ⊢ (𝜑 → ((𝐹‘𝑋)𝐷(𝐹‘𝑌)) = inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))), ℝ*, < ))
18		imasdsf1o.t	. . . 4 ⊢ 𝑇 = ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
19	18	infeq1i 8936	. . 3 ⊢ inf(𝑇, ℝ*, < ) = inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))), ℝ*, < )
20	17, 19	syl6eqr 2874	. 2 ⊢ (𝜑 → ((𝐹‘𝑋)𝐷(𝐹‘𝑌)) = inf(𝑇, ℝ*, < ))
21		xrsbas 20555	. . . . . . . . . . . 12 ⊢ ℝ* = (Base‘ℝ*𝑠)
22		xrsadd 20556	. . . . . . . . . . . 12 ⊢ +𝑒 = (+g‘ℝ*𝑠)
23		imasdsf1o.w	. . . . . . . . . . . 12 ⊢ 𝑊 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞}))
24		xrsex 20554	. . . . . . . . . . . . 13 ⊢ ℝ*𝑠 ∈ V
25	24	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ℝ*𝑠 ∈ V)
26		fzfid 13335	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1...𝑛) ∈ Fin)
27		difss 4108	. . . . . . . . . . . . 13 ⊢ (ℝ* ∖ {-∞}) ⊆ ℝ*
28	27	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ* ∖ {-∞}) ⊆ ℝ*)
29		imasdsf1o.m	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸 ∈ (∞Met‘𝑉))
30		xmetf 22933	. . . . . . . . . . . . . . . 16 ⊢ (𝐸 ∈ (∞Met‘𝑉) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
31		ffn 6509	. . . . . . . . . . . . . . . 16 ⊢ (𝐸:(𝑉 × 𝑉)⟶ℝ* → 𝐸 Fn (𝑉 × 𝑉))
32	29, 30, 31	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐸 Fn (𝑉 × 𝑉))
33		xmetcl 22935	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉) → (𝑓𝐸𝑔) ∈ ℝ*)
34		xmetge0 22948	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉) → 0 ≤ (𝑓𝐸𝑔))
35		ge0nemnf 12560	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓𝐸𝑔) ∈ ℝ* ∧ 0 ≤ (𝑓𝐸𝑔)) → (𝑓𝐸𝑔) ≠ -∞)
36	33, 34, 35	syl2anc 586	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉) → (𝑓𝐸𝑔) ≠ -∞)
37		eldifsn 4713	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}) ↔ ((𝑓𝐸𝑔) ∈ ℝ* ∧ (𝑓𝐸𝑔) ≠ -∞))
38	33, 36, 37	sylanbrc 585	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
39	38	3expb 1116	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉)) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
40	29, 39	sylan 582	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉)) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
41	40	ralrimivva 3191	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑓 ∈ 𝑉 ∀𝑔 ∈ 𝑉 (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
42		ffnov 7272	. . . . . . . . . . . . . . 15 ⊢ (𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}) ↔ (𝐸 Fn (𝑉 × 𝑉) ∧ ∀𝑓 ∈ 𝑉 ∀𝑔 ∈ 𝑉 (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞})))
43	32, 41, 42	sylanbrc 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
44	43	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
45	15	ssrab3 4057	. . . . . . . . . . . . . . . 16 ⊢ 𝑆 ⊆ ((𝑉 × 𝑉) ↑m (1...𝑛))
46	45	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑆 ⊆ ((𝑉 × 𝑉) ↑m (1...𝑛)))
47	46	sselda 3967	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑔 ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)))
48		elmapi 8422	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
49	47, 48	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
50		fco 6526	. . . . . . . . . . . . 13 ⊢ ((𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}) ∧ 𝑔:(1...𝑛)⟶(𝑉 × 𝑉)) → (𝐸 ∘ 𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
51	44, 49, 50	syl2anc 586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸 ∘ 𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
52		0re 10637	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
53		rexr 10681	. . . . . . . . . . . . . 14 ⊢ (0 ∈ ℝ → 0 ∈ ℝ*)
54		renemnf 10684	. . . . . . . . . . . . . 14 ⊢ (0 ∈ ℝ → 0 ≠ -∞)
55		eldifsn 4713	. . . . . . . . . . . . . 14 ⊢ (0 ∈ (ℝ* ∖ {-∞}) ↔ (0 ∈ ℝ* ∧ 0 ≠ -∞))
56	53, 54, 55	sylanbrc 585	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℝ → 0 ∈ (ℝ* ∖ {-∞}))
57	52, 56	mp1i 13	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 0 ∈ (ℝ* ∖ {-∞}))
58		xaddid2 12629	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ* → (0 +𝑒 𝑥) = 𝑥)
59		xaddid1 12628	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ* → (𝑥 +𝑒 0) = 𝑥)
60	58, 59	jca 514	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ* → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
61	60	adantl 484	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ 𝑥 ∈ ℝ*) → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
62	21, 22, 23, 25, 26, 28, 51, 57, 61	gsumress 17886	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) = (𝑊 Σg (𝐸 ∘ 𝑔)))
63	23, 21	ressbas2 16549	. . . . . . . . . . . . 13 ⊢ ((ℝ* ∖ {-∞}) ⊆ ℝ* → (ℝ* ∖ {-∞}) = (Base‘𝑊))
64	27, 63	ax-mp 5	. . . . . . . . . . . 12 ⊢ (ℝ* ∖ {-∞}) = (Base‘𝑊)
65	23	xrs10 20578	. . . . . . . . . . . 12 ⊢ 0 = (0g‘𝑊)
66	23	xrs1cmn 20579	. . . . . . . . . . . . 13 ⊢ 𝑊 ∈ CMnd
67	66	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑊 ∈ CMnd)
68		c0ex 10629	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
69	68	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 0 ∈ V)
70	51, 26, 69	fdmfifsupp 8837	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸 ∘ 𝑔) finSupp 0)
71	64, 65, 67, 26, 51, 70	gsumcl 19029	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σg (𝐸 ∘ 𝑔)) ∈ (ℝ* ∖ {-∞}))
72	62, 71	eqeltrd 2913	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ∈ (ℝ* ∖ {-∞}))
73	72	eldifad 3948	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ∈ ℝ*)
74	73	fmpttd 6874	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))):𝑆⟶ℝ*)
75	74	frnd 6516	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ⊆ ℝ*)
76	75	ralrimiva 3182	. . . . . 6 ⊢ (𝜑 → ∀𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ⊆ ℝ*)
77		iunss 4962	. . . . . 6 ⊢ (∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ⊆ ℝ* ↔ ∀𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ⊆ ℝ*)
78	76, 77	sylibr 236	. . . . 5 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ⊆ ℝ*)
79	18, 78	eqsstrid 4015	. . . 4 ⊢ (𝜑 → 𝑇 ⊆ ℝ*)
80		infxrcl 12720	. . . 4 ⊢ (𝑇 ⊆ ℝ* → inf(𝑇, ℝ*, < ) ∈ ℝ*)
81	79, 80	syl 17	. . 3 ⊢ (𝜑 → inf(𝑇, ℝ*, < ) ∈ ℝ*)
82		xmetcl 22935	. . . 4 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋𝐸𝑌) ∈ ℝ*)
83	29, 11, 13, 82	syl3anc 1367	. . 3 ⊢ (𝜑 → (𝑋𝐸𝑌) ∈ ℝ*)
84		1nn 11643	. . . . . . 7 ⊢ 1 ∈ ℕ
85		1ex 10631	. . . . . . . . . . . 12 ⊢ 1 ∈ V
86		opex 5349	. . . . . . . . . . . 12 ⊢ ⟨𝑋, 𝑌⟩ ∈ V
87	85, 86	f1osn 6649	. . . . . . . . . . 11 ⊢ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}–1-1-onto→{⟨𝑋, 𝑌⟩}
88		f1of 6610	. . . . . . . . . . 11 ⊢ ({⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}–1-1-onto→{⟨𝑋, 𝑌⟩} → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩})
89	87, 88	ax-mp 5	. . . . . . . . . 10 ⊢ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩}
90	11, 13	opelxpd 5588	. . . . . . . . . . 11 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉))
91	90	snssd 4736	. . . . . . . . . 10 ⊢ (𝜑 → {⟨𝑋, 𝑌⟩} ⊆ (𝑉 × 𝑉))
92		fss 6522	. . . . . . . . . 10 ⊢ (({⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩} ∧ {⟨𝑋, 𝑌⟩} ⊆ (𝑉 × 𝑉)) → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉))
93	89, 91, 92	sylancr 589	. . . . . . . . 9 ⊢ (𝜑 → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉))
94	29	elfvexd 6699	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ∈ V)
95	94, 94	xpexd 7468	. . . . . . . . . 10 ⊢ (𝜑 → (𝑉 × 𝑉) ∈ V)
96		snex 5324	. . . . . . . . . 10 ⊢ {1} ∈ V
97		elmapg 8413	. . . . . . . . . 10 ⊢ (((𝑉 × 𝑉) ∈ V ∧ {1} ∈ V) → ({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑m {1}) ↔ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉)))
98	95, 96, 97	sylancl 588	. . . . . . . . 9 ⊢ (𝜑 → ({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑m {1}) ↔ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉)))
99	93, 98	mpbird 259	. . . . . . . 8 ⊢ (𝜑 → {⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑m {1}))
100		op1stg 7695	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋)
101	11, 13, 100	syl2anc 586	. . . . . . . . . 10 ⊢ (𝜑 → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋)
102	101	fveq2d 6669	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋))
103		op2ndg 7696	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
104	11, 13, 103	syl2anc 586	. . . . . . . . . 10 ⊢ (𝜑 → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
105	104	fveq2d 6669	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌))
106	102, 105	jca 514	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌)))
107	24	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ*𝑠 ∈ V)
108		snfi 8588	. . . . . . . . . . 11 ⊢ {1} ∈ Fin
109	108	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → {1} ∈ Fin)
110	27	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ* ∖ {-∞}) ⊆ ℝ*)
111		xmetge0 22948	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → 0 ≤ (𝑋𝐸𝑌))
112	29, 11, 13, 111	syl3anc 1367	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ≤ (𝑋𝐸𝑌))
113		ge0nemnf 12560	. . . . . . . . . . . . . 14 ⊢ (((𝑋𝐸𝑌) ∈ ℝ* ∧ 0 ≤ (𝑋𝐸𝑌)) → (𝑋𝐸𝑌) ≠ -∞)
114	83, 112, 113	syl2anc 586	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋𝐸𝑌) ≠ -∞)
115		eldifsn 4713	. . . . . . . . . . . . 13 ⊢ ((𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}) ↔ ((𝑋𝐸𝑌) ∈ ℝ* ∧ (𝑋𝐸𝑌) ≠ -∞))
116	83, 114, 115	sylanbrc 585	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}))
117		fconst6g 6563	. . . . . . . . . . . 12 ⊢ ((𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}) → ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞}))
118	116, 117	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞}))
119		fcoconst 6891	. . . . . . . . . . . . . 14 ⊢ ((𝐸 Fn (𝑉 × 𝑉) ∧ ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉)) → (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}))
120	32, 90, 119	syl2anc 586	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}))
121	85, 86	xpsn 6898	. . . . . . . . . . . . . 14 ⊢ ({1} × {⟨𝑋, 𝑌⟩}) = {⟨1, ⟨𝑋, 𝑌⟩⟩}
122	121	coeq2i 5726	. . . . . . . . . . . . 13 ⊢ (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})
123		df-ov 7153	. . . . . . . . . . . . . . . 16 ⊢ (𝑋𝐸𝑌) = (𝐸‘⟨𝑋, 𝑌⟩)
124	123	eqcomi 2830	. . . . . . . . . . . . . . 15 ⊢ (𝐸‘⟨𝑋, 𝑌⟩) = (𝑋𝐸𝑌)
125	124	sneqi 4572	. . . . . . . . . . . . . 14 ⊢ {(𝐸‘⟨𝑋, 𝑌⟩)} = {(𝑋𝐸𝑌)}
126	125	xpeq2i 5577	. . . . . . . . . . . . 13 ⊢ ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}) = ({1} × {(𝑋𝐸𝑌)})
127	120, 122, 126	3eqtr3g 2879	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}) = ({1} × {(𝑋𝐸𝑌)}))
128	127	feq1d 6494	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}):{1}⟶(ℝ* ∖ {-∞}) ↔ ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞})))
129	118, 128	mpbird 259	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}):{1}⟶(ℝ* ∖ {-∞}))
130	52, 56	mp1i 13	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ (ℝ* ∖ {-∞}))
131	60	adantl 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
132	21, 22, 23, 107, 109, 110, 129, 130, 131	gsumress 17886	. . . . . . . . 9 ⊢ (𝜑 → (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})) = (𝑊 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
133		fconstmpt 5609	. . . . . . . . . . 11 ⊢ ({1} × {(𝑋𝐸𝑌)}) = (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))
134	127, 133	syl6eq 2872	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}) = (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌)))
135	134	oveq2d 7166	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})) = (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))))
136		cmnmnd 18916	. . . . . . . . . . 11 ⊢ (𝑊 ∈ CMnd → 𝑊 ∈ Mnd)
137	66, 136	mp1i 13	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ Mnd)
138	84	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℕ)
139		eqidd 2822	. . . . . . . . . . 11 ⊢ (𝑗 = 1 → (𝑋𝐸𝑌) = (𝑋𝐸𝑌))
140	64, 139	gsumsn 19068	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Mnd ∧ 1 ∈ ℕ ∧ (𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞})) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))) = (𝑋𝐸𝑌))
141	137, 138, 116, 140	syl3anc 1367	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))) = (𝑋𝐸𝑌))
142	132, 135, 141	3eqtrrd 2861	. . . . . . . 8 ⊢ (𝜑 → (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
143		fveq1 6664	. . . . . . . . . . . . . 14 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝑔‘1) = ({⟨1, ⟨𝑋, 𝑌⟩⟩}‘1))
144	85, 86	fvsn 6938	. . . . . . . . . . . . . 14 ⊢ ({⟨1, ⟨𝑋, 𝑌⟩⟩}‘1) = ⟨𝑋, 𝑌⟩
145	143, 144	syl6eq 2872	. . . . . . . . . . . . 13 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝑔‘1) = ⟨𝑋, 𝑌⟩)
146	145	fveq2d 6669	. . . . . . . . . . . 12 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (1st ‘(𝑔‘1)) = (1st ‘⟨𝑋, 𝑌⟩))
147	146	fveqeq2d 6673	. . . . . . . . . . 11 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ↔ (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋)))
148	145	fveq2d 6669	. . . . . . . . . . . 12 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (2nd ‘(𝑔‘1)) = (2nd ‘⟨𝑋, 𝑌⟩))
149	148	fveqeq2d 6673	. . . . . . . . . . 11 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌) ↔ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌)))
150	147, 149	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ↔ ((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌))))
151		coeq2 5724	. . . . . . . . . . . 12 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝐸 ∘ 𝑔) = (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}))
152	151	oveq2d 7166	. . . . . . . . . . 11 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
153	152	eqeq2d 2832	. . . . . . . . . 10 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ↔ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}))))
154	150, 153	anbi12d 632	. . . . . . . . 9 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ (((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))))
155	154	rspcev 3623	. . . . . . . 8 ⊢ (({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑m {1}) ∧ (((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))) → ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
156	99, 106, 142, 155	syl12anc 834	. . . . . . 7 ⊢ (𝜑 → ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
157		ovex 7183	. . . . . . . . . 10 ⊢ (𝑋𝐸𝑌) ∈ V
158		eqid 2821	. . . . . . . . . . 11 ⊢ (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) = (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
159	158	elrnmpt 5823	. . . . . . . . . 10 ⊢ ((𝑋𝐸𝑌) ∈ V → ((𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
160	157, 159	ax-mp 5	. . . . . . . . 9 ⊢ ((𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
161	15	rexeqi 3415	. . . . . . . . . . 11 ⊢ (∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ↔ ∃𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))} (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
162		fveq1 6664	. . . . . . . . . . . . . . 15 ⊢ (ℎ = 𝑔 → (ℎ‘1) = (𝑔‘1))
163	162	fveq2d 6669	. . . . . . . . . . . . . 14 ⊢ (ℎ = 𝑔 → (1st ‘(ℎ‘1)) = (1st ‘(𝑔‘1)))
164	163	fveqeq2d 6673	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑔 → ((𝐹‘(1st ‘(ℎ‘1))) = (𝐹‘𝑋) ↔ (𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋)))
165		fveq1 6664	. . . . . . . . . . . . . . 15 ⊢ (ℎ = 𝑔 → (ℎ‘𝑛) = (𝑔‘𝑛))
166	165	fveq2d 6669	. . . . . . . . . . . . . 14 ⊢ (ℎ = 𝑔 → (2nd ‘(ℎ‘𝑛)) = (2nd ‘(𝑔‘𝑛)))
167	166	fveqeq2d 6673	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑔 → ((𝐹‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ↔ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)))
168		fveq1 6664	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = 𝑔 → (ℎ‘𝑖) = (𝑔‘𝑖))
169	168	fveq2d 6669	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = 𝑔 → (2nd ‘(ℎ‘𝑖)) = (2nd ‘(𝑔‘𝑖)))
170	169	fveq2d 6669	. . . . . . . . . . . . . . 15 ⊢ (ℎ = 𝑔 → (𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(2nd ‘(𝑔‘𝑖))))
171		fveq1 6664	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = 𝑔 → (ℎ‘(𝑖 + 1)) = (𝑔‘(𝑖 + 1)))
172	171	fveq2d 6669	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = 𝑔 → (1st ‘(ℎ‘(𝑖 + 1))) = (1st ‘(𝑔‘(𝑖 + 1))))
173	172	fveq2d 6669	. . . . . . . . . . . . . . 15 ⊢ (ℎ = 𝑔 → (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
174	170, 173	eqeq12d 2837	. . . . . . . . . . . . . 14 ⊢ (ℎ = 𝑔 → ((𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
175	174	ralbidv 3197	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑔 → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
176	164, 167, 175	3anbi123d 1432	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑔 → (((𝐹‘(1st ‘(ℎ‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
177	176	rexrab 3687	. . . . . . . . . . 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 277	. . . . . . . . . 10 ⊢ (∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
179		oveq2 7158	. . . . . . . . . . . . 13 ⊢ (𝑛 = 1 → (1...𝑛) = (1...1))
180		1z 12006	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℤ
181		fzsn 12943	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℤ → (1...1) = {1})
182	180, 181	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (1...1) = {1}
183	179, 182	syl6eq 2872	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (1...𝑛) = {1})
184	183	oveq2d 7166	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → ((𝑉 × 𝑉) ↑m (1...𝑛)) = ((𝑉 × 𝑉) ↑m {1}))
185		df-3an 1085	. . . . . . . . . . . . 13 ⊢ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
186		ral0 4456	. . . . . . . . . . . . . . . 16 ⊢ ∀𝑖 ∈ ∅ (𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))
187		oveq1 7157	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 1 → (𝑛 − 1) = (1 − 1))
188		1m1e0 11703	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 − 1) = 0
189	187, 188	syl6eq 2872	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 1 → (𝑛 − 1) = 0)
190	189	oveq2d 7166	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 1 → (1...(𝑛 − 1)) = (1...0))
191		fz10 12922	. . . . . . . . . . . . . . . . . 18 ⊢ (1...0) = ∅
192	190, 191	syl6eq 2872	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 1 → (1...(𝑛 − 1)) = ∅)
193	192	raleqdv 3416	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1 → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ ∅ (𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
194	186, 193	mpbiri 260	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1 → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
195	194	biantrud 534	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
196		2fveq3 6670	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1 → (2nd ‘(𝑔‘𝑛)) = (2nd ‘(𝑔‘1)))
197	196	fveqeq2d 6673	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1 → ((𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ↔ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)))
198	197	anbi2d 630	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌))))
199	195, 198	bitr3d 283	. . . . . . . . . . . . 13 ⊢ (𝑛 = 1 → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌))))
200	185, 199	syl5bb 285	. . . . . . . . . . . 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 3403	. . . . . . . . . 10 ⊢ (𝑛 = 1 → (∃𝑔 ∈ ((𝑉 × 𝑉) ↑m (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))))
203	178, 202	syl5bb 285	. . . . . . . . 9 ⊢ (𝑛 = 1 → (∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))))
204	160, 203	syl5bb 285	. . . . . . . 8 ⊢ (𝑛 = 1 → ((𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))))
205	204	rspcev 3623	. . . . . . 7 ⊢ ((1 ∈ ℕ ∧ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))) → ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
206	84, 156, 205	sylancr 589	. . . . . 6 ⊢ (𝜑 → ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
207		eliun 4916	. . . . . 6 ⊢ ((𝑋𝐸𝑌) ∈ ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
208	206, 207	sylibr 236	. . . . 5 ⊢ (𝜑 → (𝑋𝐸𝑌) ∈ ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
209	208, 18	eleqtrrdi 2924	. . . 4 ⊢ (𝜑 → (𝑋𝐸𝑌) ∈ 𝑇)
210		infxrlb 12721	. . . 4 ⊢ ((𝑇 ⊆ ℝ* ∧ (𝑋𝐸𝑌) ∈ 𝑇) → inf(𝑇, ℝ*, < ) ≤ (𝑋𝐸𝑌))
211	79, 209, 210	syl2anc 586	. . 3 ⊢ (𝜑 → inf(𝑇, ℝ*, < ) ≤ (𝑋𝐸𝑌))
212	18	eleq2i 2904	. . . . . . 7 ⊢ (𝑝 ∈ 𝑇 ↔ 𝑝 ∈ ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
213		eliun 4916	. . . . . . 7 ⊢ (𝑝 ∈ ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
214	212, 213	bitri 277	. . . . . 6 ⊢ (𝑝 ∈ 𝑇 ↔ ∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
215	158	elrnmpt 5823	. . . . . . . . 9 ⊢ (𝑝 ∈ V → (𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ 𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
216	215	elv 3500	. . . . . . . 8 ⊢ (𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ 𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
217	176, 15	elrab2 3683	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∈ 𝑆 ↔ (𝑔 ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∧ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
218	217	simprbi 499	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 ∈ 𝑆 → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
219	218	adantl 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
220	219	simp2d 1139	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌))
221	3	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐹:𝑉–1-1-onto→𝐵)
222		f1of1 6609	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹:𝑉–1-1→𝐵)
223	221, 222	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐹:𝑉–1-1→𝐵)
224		simplr 767	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑛 ∈ ℕ)
225		elfz1end 12931	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (1...𝑛))
226	224, 225	sylib 220	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑛 ∈ (1...𝑛))
227	49, 226	ffvelrnd 6847	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑔‘𝑛) ∈ (𝑉 × 𝑉))
228		xp2nd 7716	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔‘𝑛) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘𝑛)) ∈ 𝑉)
229	227, 228	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (2nd ‘(𝑔‘𝑛)) ∈ 𝑉)
230	13	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑌 ∈ 𝑉)
231		f1fveq 7014	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ ((2nd ‘(𝑔‘𝑛)) ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ((𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ↔ (2nd ‘(𝑔‘𝑛)) = 𝑌))
232	223, 229, 230, 231	syl12anc 834	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ↔ (2nd ‘(𝑔‘𝑛)) = 𝑌))
233	220, 232	mpbid 234	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (2nd ‘(𝑔‘𝑛)) = 𝑌)
234	233	oveq2d 7166	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2nd ‘(𝑔‘𝑛))) = (𝑋𝐸𝑌))
235		eleq1 2900	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 1 → (𝑚 ∈ (1...𝑛) ↔ 1 ∈ (1...𝑛)))
236		2fveq3 6670	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 1 → (2nd ‘(𝑔‘𝑚)) = (2nd ‘(𝑔‘1)))
237	236	oveq2d 7166	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 1 → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘1))))
238		oveq2 7158	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 1 → (1...𝑚) = (1...1))
239	238, 182	syl6eq 2872	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 1 → (1...𝑚) = {1})
240	239	reseq2d 5848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 1 → ((𝐸 ∘ 𝑔) ↾ (1...𝑚)) = ((𝐸 ∘ 𝑔) ↾ {1}))
241	240	oveq2d 7166	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 1 → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1})))
242	237, 241	breq12d 5072	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 1 → ((𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1}))))
243	235, 242	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 1 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚)))) ↔ (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1})))))
244	243	imbi2d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 1 → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))))) ↔ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1}))))))
245		eleq1 2900	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑥 → (𝑚 ∈ (1...𝑛) ↔ 𝑥 ∈ (1...𝑛)))
246		2fveq3 6670	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑥 → (2nd ‘(𝑔‘𝑚)) = (2nd ‘(𝑔‘𝑥)))
247	246	oveq2d 7166	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑥 → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘𝑥))))
248		oveq2 7158	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑥 → (1...𝑚) = (1...𝑥))
249	248	reseq2d 5848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑥 → ((𝐸 ∘ 𝑔) ↾ (1...𝑚)) = ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))
250	249	oveq2d 7166	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑥 → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))))
251	247, 250	breq12d 5072	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑥 → ((𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))))
252	245, 251	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑥 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚)))) ↔ (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))))))
253	252	imbi2d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑥 → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))))) ↔ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))))))
254		eleq1 2900	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑥 + 1) → (𝑚 ∈ (1...𝑛) ↔ (𝑥 + 1) ∈ (1...𝑛)))
255		2fveq3 6670	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = (𝑥 + 1) → (2nd ‘(𝑔‘𝑚)) = (2nd ‘(𝑔‘(𝑥 + 1))))
256	255	oveq2d 7166	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = (𝑥 + 1) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))))
257		oveq2 7158	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = (𝑥 + 1) → (1...𝑚) = (1...(𝑥 + 1)))
258	257	reseq2d 5848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = (𝑥 + 1) → ((𝐸 ∘ 𝑔) ↾ (1...𝑚)) = ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))
259	258	oveq2d 7166	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = (𝑥 + 1) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))))
260	256, 259	breq12d 5072	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑥 + 1) → ((𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))))
261	254, 260	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝑥 + 1) → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚)))) ↔ ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))))))
262	261	imbi2d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝑥 + 1) → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))))) ↔ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))))))
263		eleq1 2900	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ (1...𝑛) ↔ 𝑛 ∈ (1...𝑛)))
264		2fveq3 6670	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → (2nd ‘(𝑔‘𝑚)) = (2nd ‘(𝑔‘𝑛)))
265	264	oveq2d 7166	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘𝑛))))
266		oveq2 7158	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
267	266	reseq2d 5848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → ((𝐸 ∘ 𝑔) ↾ (1...𝑚)) = ((𝐸 ∘ 𝑔) ↾ (1...𝑛)))
268	267	oveq2d 7166	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))
269	265, 268	breq12d 5072	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → ((𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛)))))
270	263, 269	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑛 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚)))) ↔ (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))))
271	270	imbi2d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑛 → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))))) ↔ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛)))))))
272	29	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐸 ∈ (∞Met‘𝑉))
273	11	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑋 ∈ 𝑉)
274		nnuz 12275	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℕ = (ℤ≥‘1)
275	224, 274	eleqtrdi 2923	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑛 ∈ (ℤ≥‘1))
276		eluzfz1 12908	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (ℤ≥‘1) → 1 ∈ (1...𝑛))
277	275, 276	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 1 ∈ (1...𝑛))
278	49, 277	ffvelrnd 6847	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑔‘1) ∈ (𝑉 × 𝑉))
279		xp2nd 7716	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔‘1) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘1)) ∈ 𝑉)
280	278, 279	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (2nd ‘(𝑔‘1)) ∈ 𝑉)
281		xmetcl 22935	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ (2nd ‘(𝑔‘1)) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔‘1))) ∈ ℝ*)
282	272, 273, 280, 281	syl3anc 1367	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ∈ ℝ*)
283	282	xrleidd 12539	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑋𝐸(2nd ‘(𝑔‘1))))
284	137	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑊 ∈ Mnd)
285	84	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 1 ∈ ℕ)
286	44, 278	ffvelrnd 6847	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸‘(𝑔‘1)) ∈ (ℝ* ∖ {-∞}))
287		2fveq3 6670	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 1 → (𝐸‘(𝑔‘𝑗)) = (𝐸‘(𝑔‘1)))
288	64, 287	gsumsn 19068	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Mnd ∧ 1 ∈ ℕ ∧ (𝐸‘(𝑔‘1)) ∈ (ℝ* ∖ {-∞})) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗)))) = (𝐸‘(𝑔‘1)))
289	284, 285, 286, 288	syl3anc 1367	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗)))) = (𝐸‘(𝑔‘1)))
290	272, 30	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
291		fcompt 6890	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐸:(𝑉 × 𝑉)⟶ℝ* ∧ 𝑔:(1...𝑛)⟶(𝑉 × 𝑉)) → (𝐸 ∘ 𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))))
292	290, 49, 291	syl2anc 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸 ∘ 𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))))
293	292	reseq1d 5847	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐸 ∘ 𝑔) ↾ {1}) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ {1}))
294	277	snssd 4736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → {1} ⊆ (1...𝑛))
295	294	resmptd 5903	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ {1}) = (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗))))
296	293, 295	eqtrd 2856	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐸 ∘ 𝑔) ↾ {1}) = (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗))))
297	296	oveq2d 7166	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1})) = (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗)))))
298		df-ov 7153	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋𝐸(2nd ‘(𝑔‘1))) = (𝐸‘⟨𝑋, (2nd ‘(𝑔‘1))⟩)
299		1st2nd2 7722	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔‘1) ∈ (𝑉 × 𝑉) → (𝑔‘1) = ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩)
300	278, 299	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑔‘1) = ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩)
301	219	simp1d 1138	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋))
302		xp1st 7715	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔‘1) ∈ (𝑉 × 𝑉) → (1st ‘(𝑔‘1)) ∈ 𝑉)
303	278, 302	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1st ‘(𝑔‘1)) ∈ 𝑉)
304		f1fveq 7014	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ ((1st ‘(𝑔‘1)) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ↔ (1st ‘(𝑔‘1)) = 𝑋))
305	223, 303, 273, 304	syl12anc 834	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ↔ (1st ‘(𝑔‘1)) = 𝑋))
306	301, 305	mpbid 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1st ‘(𝑔‘1)) = 𝑋)
307	306	opeq1d 4803	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩ = ⟨𝑋, (2nd ‘(𝑔‘1))⟩)
308	300, 307	eqtr2d 2857	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ⟨𝑋, (2nd ‘(𝑔‘1))⟩ = (𝑔‘1))
309	308	fveq2d 6669	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸‘⟨𝑋, (2nd ‘(𝑔‘1))⟩) = (𝐸‘(𝑔‘1)))
310	298, 309	syl5eq 2868	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) = (𝐸‘(𝑔‘1)))
311	289, 297, 310	3eqtr4d 2866	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1})) = (𝑋𝐸(2nd ‘(𝑔‘1))))
312	283, 311	breqtrrd 5087	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1})))
313	312	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1}))))
314		simprl 769	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ ℕ)
315	314, 274	eleqtrdi 2923	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (ℤ≥‘1))
316		simprr 771	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑥 + 1) ∈ (1...𝑛))
317		peano2fzr 12914	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (ℤ≥‘1) ∧ (𝑥 + 1) ∈ (1...𝑛)) → 𝑥 ∈ (1...𝑛))
318	315, 316, 317	syl2anc 586	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (1...𝑛))
319	318	expr 459	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 + 1) ∈ (1...𝑛) → 𝑥 ∈ (1...𝑛)))
320	319	imim1d 82	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))))))
321	272	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸 ∈ (∞Met‘𝑉))
322	273	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑋 ∈ 𝑉)
323	49	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
324	323, 318	ffvelrnd 6847	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘𝑥) ∈ (𝑉 × 𝑉))
325		xp2nd 7716	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔‘𝑥) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘𝑥)) ∈ 𝑉)
326	324, 325	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔‘𝑥)) ∈ 𝑉)
327		xmetcl 22935	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ (2nd ‘(𝑔‘𝑥)) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ∈ ℝ*)
328	321, 322, 326, 327	syl3anc 1367	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ∈ ℝ*)
329	66	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑊 ∈ CMnd)
330		fzfid 13335	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...𝑥) ∈ Fin)
331	51	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸 ∘ 𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
332		fzsuc 12948	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (ℤ≥‘1) → (1...(𝑥 + 1)) = ((1...𝑥) ∪ {(𝑥 + 1)}))
333	315, 332	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...(𝑥 + 1)) = ((1...𝑥) ∪ {(𝑥 + 1)}))
334		elfzuz3 12899	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 + 1) ∈ (1...𝑛) → 𝑛 ∈ (ℤ≥‘(𝑥 + 1)))
335	334	ad2antll 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑛 ∈ (ℤ≥‘(𝑥 + 1)))
336		fzss2 12941	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ (ℤ≥‘(𝑥 + 1)) → (1...(𝑥 + 1)) ⊆ (1...𝑛))
337	335, 336	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...(𝑥 + 1)) ⊆ (1...𝑛))
338	333, 337	eqsstrrd 4006	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((1...𝑥) ∪ {(𝑥 + 1)}) ⊆ (1...𝑛))
339	338	unssad 4163	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...𝑥) ⊆ (1...𝑛))
340	331, 339	fssresd 6540	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...𝑥)):(1...𝑥)⟶(ℝ* ∖ {-∞}))
341	68	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 0 ∈ V)
342	340, 330, 341	fdmfifsupp 8837	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...𝑥)) finSupp 0)
343	64, 65, 329, 330, 340, 342	gsumcl 19029	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) ∈ (ℝ* ∖ {-∞}))
344	343	eldifad 3948	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) ∈ ℝ*)
345	321, 30	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
346	323, 316	ffvelrnd 6847	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉))
347	345, 346	ffvelrnd 6847	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*)
348		xleadd1a 12640	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ∈ ℝ* ∧ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) ∈ ℝ* ∧ (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*) ∧ (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
349	348	ex 415	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ∈ ℝ* ∧ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) ∈ ℝ* ∧ (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
350	328, 344, 347, 349	syl3anc 1367	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
351		xp2nd 7716	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
352	346, 351	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
353		xmettri 22955	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑋 ∈ 𝑉 ∧ (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉 ∧ (2nd ‘(𝑔‘𝑥)) ∈ 𝑉)) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 ((2nd ‘(𝑔‘𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
354	321, 322, 352, 326, 353	syl13anc 1368	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 ((2nd ‘(𝑔‘𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
355		1st2nd2 7722	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (𝑔‘(𝑥 + 1)) = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
356	346, 355	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
357		2fveq3 6670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 = 𝑥 → (2nd ‘(𝑔‘𝑖)) = (2nd ‘(𝑔‘𝑥)))
358	357	fveq2d 6669	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝑥 → (𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(2nd ‘(𝑔‘𝑥))))
359		fvoveq1 7173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = 𝑥 → (𝑔‘(𝑖 + 1)) = (𝑔‘(𝑥 + 1)))
360	359	fveq2d 6669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 = 𝑥 → (1st ‘(𝑔‘(𝑖 + 1))) = (1st ‘(𝑔‘(𝑥 + 1))))
361	360	fveq2d 6669	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝑥 → (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))))
362	358, 361	eqeq12d 2837	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 = 𝑥 → ((𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(𝑔‘𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1))))))
363	219	simp3d 1140	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
364	363	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
365		nnz 11998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℤ)
366	365	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ ℤ)
367		eluzp1m1 12262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ (ℤ≥‘(𝑥 + 1))) → (𝑛 − 1) ∈ (ℤ≥‘𝑥))
368	366, 335, 367	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑛 − 1) ∈ (ℤ≥‘𝑥))
369		elfzuzb 12896	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ (1...(𝑛 − 1)) ↔ (𝑥 ∈ (ℤ≥‘1) ∧ (𝑛 − 1) ∈ (ℤ≥‘𝑥)))
370	315, 368, 369	sylanbrc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (1...(𝑛 − 1)))
371	362, 364, 370	rspcdva 3625	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐹‘(2nd ‘(𝑔‘𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))))
372	223	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐹:𝑉–1-1→𝐵)
373		xp1st 7715	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
374	346, 373	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
375		f1fveq 7014	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ ((2nd ‘(𝑔‘𝑥)) ∈ 𝑉 ∧ (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)) → ((𝐹‘(2nd ‘(𝑔‘𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))) ↔ (2nd ‘(𝑔‘𝑥)) = (1st ‘(𝑔‘(𝑥 + 1)))))
376	372, 326, 374, 375	syl12anc 834	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐹‘(2nd ‘(𝑔‘𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))) ↔ (2nd ‘(𝑔‘𝑥)) = (1st ‘(𝑔‘(𝑥 + 1)))))
377	371, 376	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔‘𝑥)) = (1st ‘(𝑔‘(𝑥 + 1))))
378	377	opeq1d 4803	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ⟨(2nd ‘(𝑔‘𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩ = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
379	356, 378	eqtr4d 2859	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) = ⟨(2nd ‘(𝑔‘𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
380	379	fveq2d 6669	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) = (𝐸‘⟨(2nd ‘(𝑔‘𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩))
381		df-ov 7153	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2nd ‘(𝑔‘𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) = (𝐸‘⟨(2nd ‘(𝑔‘𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
382	380, 381	syl6eqr 2874	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) = ((2nd ‘(𝑔‘𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1)))))
383	382	oveq2d 7166	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) = ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 ((2nd ‘(𝑔‘𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
384	354, 383	breqtrrd 5087	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
385		xmetcl 22935	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
386	321, 322, 352, 385	syl3anc 1367	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
387	328, 347	xaddcld 12688	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
388	344, 347	xaddcld 12688	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
389		xrletr 12545	. . . . . . . . . . . . . . . . . . . 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 1367	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∧ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
391	384, 390	mpand 693	. . . . . . . . . . . . . . . . . 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 12380	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℝ* ∈ V
394	393	difexi 5225	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℝ* ∖ {-∞}) ∈ V
395	23, 22	ressplusg 16606	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℝ* ∖ {-∞}) ∈ V → +𝑒 = (+g‘𝑊))
396	394, 395	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ +𝑒 = (+g‘𝑊)
397	44	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
398		fzelp1 12953	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (1...𝑥) → 𝑗 ∈ (1...(𝑥 + 1)))
399	49	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
400	337	sselda 3967	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → 𝑗 ∈ (1...𝑛))
401	399, 400	ffvelrnd 6847	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → (𝑔‘𝑗) ∈ (𝑉 × 𝑉))
402	398, 401	sylan2 594	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → (𝑔‘𝑗) ∈ (𝑉 × 𝑉))
403	397, 402	ffvelrnd 6847	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → (𝐸‘(𝑔‘𝑗)) ∈ (ℝ* ∖ {-∞}))
404		fzp1disj 12960	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1...𝑥) ∩ {(𝑥 + 1)}) = ∅
405	404	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((1...𝑥) ∩ {(𝑥 + 1)}) = ∅)
406		disjsn 4641	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1...𝑥) ∩ {(𝑥 + 1)}) = ∅ ↔ ¬ (𝑥 + 1) ∈ (1...𝑥))
407	405, 406	sylib 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ¬ (𝑥 + 1) ∈ (1...𝑥))
408	44	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
409	408, 346	ffvelrnd 6847	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) ∈ (ℝ* ∖ {-∞}))
410		2fveq3 6670	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑥 + 1) → (𝐸‘(𝑔‘𝑗)) = (𝐸‘(𝑔‘(𝑥 + 1))))
411	64, 396, 329, 330, 403, 316, 407, 409, 410	gsumunsn 19074	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔‘𝑗)))) = ((𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗)))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
412	292	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸 ∘ 𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))))
413	412, 333	reseq12d 5849	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ ((1...𝑥) ∪ {(𝑥 + 1)})))
414	338	resmptd 5903	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ ((1...𝑥) ∪ {(𝑥 + 1)})) = (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔‘𝑗))))
415	413, 414	eqtrd 2856	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))) = (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔‘𝑗))))
416	415	oveq2d 7166	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))) = (𝑊 Σg (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔‘𝑗)))))
417	412	reseq1d 5847	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...𝑥)) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ (1...𝑥)))
418	339	resmptd 5903	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ (1...𝑥)) = (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗))))
419	417, 418	eqtrd 2856	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...𝑥)) = (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗))))
420	419	oveq2d 7166	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) = (𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗)))))
421	420	oveq1d 7165	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) = ((𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗)))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
422	411, 416, 421	3eqtr4d 2866	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))) = ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
423	422	breq2d 5071	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))) ↔ (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
424	392, 423	sylibrd 261	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))))
425	320, 424	animpimp2impd 842	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℕ → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))))) → (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))))))
426	244, 253, 262, 271, 313, 425	nnind 11650	. . . . . . . . . . . . . 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 5083	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸𝑌) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))
430		ffn 6509	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∘ 𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}) → (𝐸 ∘ 𝑔) Fn (1...𝑛))
431		fnresdm 6461	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∘ 𝑔) Fn (1...𝑛) → ((𝐸 ∘ 𝑔) ↾ (1...𝑛)) = (𝐸 ∘ 𝑔))
432	51, 430, 431	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐸 ∘ 𝑔) ↾ (1...𝑛)) = (𝐸 ∘ 𝑔))
433	432	oveq2d 7166	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))) = (𝑊 Σg (𝐸 ∘ 𝑔)))
434	62, 433	eqtr4d 2859	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) = (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))
435	429, 434	breqtrrd 5087	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸𝑌) ≤ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
436		breq2 5063	. . . . . . . . . 10 ⊢ (𝑝 = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) → ((𝑋𝐸𝑌) ≤ 𝑝 ↔ (𝑋𝐸𝑌) ≤ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
437	435, 436	syl5ibrcom 249	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑝 = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) → (𝑋𝐸𝑌) ≤ 𝑝))
438	437	rexlimdva 3284	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∃𝑔 ∈ 𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) → (𝑋𝐸𝑌) ≤ 𝑝))
439	216, 438	syl5bi 244	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) → (𝑋𝐸𝑌) ≤ 𝑝))
440	439	rexlimdva 3284	. . . . . 6 ⊢ (𝜑 → (∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) → (𝑋𝐸𝑌) ≤ 𝑝))
441	214, 440	syl5bi 244	. . . . 5 ⊢ (𝜑 → (𝑝 ∈ 𝑇 → (𝑋𝐸𝑌) ≤ 𝑝))
442	441	ralrimiv 3181	. . . 4 ⊢ (𝜑 → ∀𝑝 ∈ 𝑇 (𝑋𝐸𝑌) ≤ 𝑝)
443		infxrgelb 12722	. . . . 5 ⊢ ((𝑇 ⊆ ℝ* ∧ (𝑋𝐸𝑌) ∈ ℝ*) → ((𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ) ↔ ∀𝑝 ∈ 𝑇 (𝑋𝐸𝑌) ≤ 𝑝))
444	79, 83, 443	syl2anc 586	. . . 4 ⊢ (𝜑 → ((𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ) ↔ ∀𝑝 ∈ 𝑇 (𝑋𝐸𝑌) ≤ 𝑝))
445	442, 444	mpbird 259	. . 3 ⊢ (𝜑 → (𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ))
446	81, 83, 211, 445	xrletrid 12542	. 2 ⊢ (𝜑 → inf(𝑇, ℝ*, < ) = (𝑋𝐸𝑌))
447	20, 446	eqtrd 2856	1 ⊢ (𝜑 → ((𝐹‘𝑋)𝐷(𝐹‘𝑌)) = (𝑋𝐸𝑌))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110   ≠ wne 3016  ∀wral 3138  ∃wrex 3139  {crab 3142  Vcvv 3495   ∖ cdif 3933   ∪ cun 3934   ∩ cin 3935   ⊆ wss 3936  ∅c0 4291  {csn 4561  ⟨cop 4567  ∪ ciun 4912   class class class wbr 5059   ↦ cmpt 5139   × cxp 5548  ran crn 5551   ↾ cres 5552   ∘ ccom 5554   Fn wfn 6345  ⟶wf 6346  –1-1→wf1 6347  –onto→wfo 6348  –1-1-onto→wf1o 6349  ‘cfv 6350  (class class class)co 7150  1^st c1st 7681  2^nd c2nd 7682   ↑_m cmap 8400  Fincfn 8503  infcinf 8899  ℝcr 10530  0cc0 10531  1c1 10532   + caddc 10534  -∞cmnf 10667  ℝ^*cxr 10668   < clt 10669   ≤ cle 10670   − cmin 10864  ℕcn 11632  ℤcz 11975  ℤ_≥cuz 12237   +_𝑒 cxad 12499  ...cfz 12886  Basecbs 16477   ↾_s cress 16478  +_gcplusg 16559  distcds 16568   Σ_g cgsu 16708  ℝ^*_𝑠cxrs 16767   “_s cimas 16771  Mndcmnd 17905  CMndccmn 18900  ∞Metcxmet 20524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-rep 5183  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4833  df-int 4870  df-iun 4914  df-iin 4915  df-br 5060  df-opab 5122  df-mpt 5140  df-tr 5166  df-id 5455  df-eprel 5460  df-po 5469  df-so 5470  df-fr 5509  df-se 5510  df-we 5511  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-pred 6143  df-ord 6189  df-on 6190  df-lim 6191  df-suc 6192  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-isom 6359  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7403  df-om 7575  df-1st 7683  df-2nd 7684  df-supp 7825  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-oadd 8100  df-er 8283  df-map 8402  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-fsupp 8828  df-sup 8900  df-inf 8901  df-oi 8968  df-card 9362  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-3 11695  df-4 11696  df-5 11697  df-6 11698  df-7 11699  df-8 11700  df-9 11701  df-n0 11892  df-z 11976  df-dec 12093  df-uz 12238  df-rp 12384  df-xneg 12501  df-xadd 12502  df-xmul 12503  df-fz 12887  df-fzo 13028  df-seq 13364  df-hash 13685  df-struct 16479  df-ndx 16480  df-slot 16481  df-base 16483  df-sets 16484  df-ress 16485  df-plusg 16572  df-mulr 16573  df-sca 16575  df-vsca 16576  df-ip 16577  df-tset 16578  df-ple 16579  df-ds 16581  df-0g 16709  df-gsum 16710  df-xrs 16769  df-imas 16775  df-mre 16851  df-mrc 16852  df-acs 16854  df-mgm 17846  df-sgrp 17895  df-mnd 17906  df-submnd 17951  df-mulg 18219  df-cntz 18441  df-cmn 18902  df-xmet 20532

This theorem is referenced by:  imasdsf1o  22978