Theorem imasdsf1olem 23526

Description: Lemma for imasdsf1o 23527. (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 6723	. . . . 5 ⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹:𝑉–onto→𝐵)
5	3, 4	syl 17	. . . 4 ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
6		imasdsf1o.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑍)
7		eqid 2738	. . . 4 ⊢ (dist‘𝑅) = (dist‘𝑅)
8		imasdsf1o.d	. . . 4 ⊢ 𝐷 = (dist‘𝑈)
9		f1of 6716	. . . . . 6 ⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹:𝑉⟶𝐵)
10	3, 9	syl 17	. . . . 5 ⊢ (𝜑 → 𝐹:𝑉⟶𝐵)
11		imasdsf1o.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
12	10, 11	ffvelrnd 6962	. . . 4 ⊢ (𝜑 → (𝐹‘𝑋) ∈ 𝐵)
13		imasdsf1o.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
14	10, 13	ffvelrnd 6962	. . . 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 17227	. . 3 ⊢ (𝜑 → ((𝐹‘𝑋)𝐷(𝐹‘𝑌)) = inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))), ℝ*, < ))
18		imasdsf1o.t	. . . 4 ⊢ 𝑇 = ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
19	18	infeq1i 9237	. . 3 ⊢ inf(𝑇, ℝ*, < ) = inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))), ℝ*, < )
20	17, 19	eqtr4di 2796	. 2 ⊢ (𝜑 → ((𝐹‘𝑋)𝐷(𝐹‘𝑌)) = inf(𝑇, ℝ*, < ))
21		xrsbas 20614	. . . . . . . . . . . 12 ⊢ ℝ* = (Base‘ℝ*𝑠)
22		xrsadd 20615	. . . . . . . . . . . 12 ⊢ +𝑒 = (+g‘ℝ*𝑠)
23		imasdsf1o.w	. . . . . . . . . . . 12 ⊢ 𝑊 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞}))
24		xrsex 20613	. . . . . . . . . . . . 13 ⊢ ℝ*𝑠 ∈ V
25	24	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ℝ*𝑠 ∈ V)
26		fzfid 13693	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1...𝑛) ∈ Fin)
27		difss 4066	. . . . . . . . . . . . 13 ⊢ (ℝ* ∖ {-∞}) ⊆ ℝ*
28	27	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ* ∖ {-∞}) ⊆ ℝ*)
29		imasdsf1o.m	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸 ∈ (∞Met‘𝑉))
30		xmetf 23482	. . . . . . . . . . . . . . . 16 ⊢ (𝐸 ∈ (∞Met‘𝑉) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
31		ffn 6600	. . . . . . . . . . . . . . . 16 ⊢ (𝐸:(𝑉 × 𝑉)⟶ℝ* → 𝐸 Fn (𝑉 × 𝑉))
32	29, 30, 31	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐸 Fn (𝑉 × 𝑉))
33		xmetcl 23484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉) → (𝑓𝐸𝑔) ∈ ℝ*)
34		xmetge0 23497	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉) → 0 ≤ (𝑓𝐸𝑔))
35		ge0nemnf 12907	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓𝐸𝑔) ∈ ℝ* ∧ 0 ≤ (𝑓𝐸𝑔)) → (𝑓𝐸𝑔) ≠ -∞)
36	33, 34, 35	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉) → (𝑓𝐸𝑔) ≠ -∞)
37		eldifsn 4720	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}) ↔ ((𝑓𝐸𝑔) ∈ ℝ* ∧ (𝑓𝐸𝑔) ≠ -∞))
38	33, 36, 37	sylanbrc 583	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
39	38	3expb 1119	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉)) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
40	29, 39	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉)) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
41	40	ralrimivva 3123	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑓 ∈ 𝑉 ∀𝑔 ∈ 𝑉 (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
42		ffnov 7401	. . . . . . . . . . . . . . 15 ⊢ (𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}) ↔ (𝐸 Fn (𝑉 × 𝑉) ∧ ∀𝑓 ∈ 𝑉 ∀𝑔 ∈ 𝑉 (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞})))
43	32, 41, 42	sylanbrc 583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
44	43	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
45	15	ssrab3 4015	. . . . . . . . . . . . . . . 16 ⊢ 𝑆 ⊆ ((𝑉 × 𝑉) ↑m (1...𝑛))
46	45	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑆 ⊆ ((𝑉 × 𝑉) ↑m (1...𝑛)))
47	46	sselda 3921	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑔 ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)))
48		elmapi 8637	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
49	47, 48	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
50		fco 6624	. . . . . . . . . . . . 13 ⊢ ((𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}) ∧ 𝑔:(1...𝑛)⟶(𝑉 × 𝑉)) → (𝐸 ∘ 𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
51	44, 49, 50	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸 ∘ 𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
52		0re 10977	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
53		rexr 11021	. . . . . . . . . . . . . 14 ⊢ (0 ∈ ℝ → 0 ∈ ℝ*)
54		renemnf 11024	. . . . . . . . . . . . . 14 ⊢ (0 ∈ ℝ → 0 ≠ -∞)
55		eldifsn 4720	. . . . . . . . . . . . . 14 ⊢ (0 ∈ (ℝ* ∖ {-∞}) ↔ (0 ∈ ℝ* ∧ 0 ≠ -∞))
56	53, 54, 55	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℝ → 0 ∈ (ℝ* ∖ {-∞}))
57	52, 56	mp1i 13	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 0 ∈ (ℝ* ∖ {-∞}))
58		xaddid2 12976	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ* → (0 +𝑒 𝑥) = 𝑥)
59		xaddid1 12975	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ* → (𝑥 +𝑒 0) = 𝑥)
60	58, 59	jca 512	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ* → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
61	60	adantl 482	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ 𝑥 ∈ ℝ*) → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
62	21, 22, 23, 25, 26, 28, 51, 57, 61	gsumress 18366	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) = (𝑊 Σg (𝐸 ∘ 𝑔)))
63	23, 21	ressbas2 16949	. . . . . . . . . . . . 13 ⊢ ((ℝ* ∖ {-∞}) ⊆ ℝ* → (ℝ* ∖ {-∞}) = (Base‘𝑊))
64	27, 63	ax-mp 5	. . . . . . . . . . . 12 ⊢ (ℝ* ∖ {-∞}) = (Base‘𝑊)
65	23	xrs10 20637	. . . . . . . . . . . 12 ⊢ 0 = (0g‘𝑊)
66	23	xrs1cmn 20638	. . . . . . . . . . . . 13 ⊢ 𝑊 ∈ CMnd
67	66	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑊 ∈ CMnd)
68		c0ex 10969	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
69	68	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 0 ∈ V)
70	51, 26, 69	fdmfifsupp 9138	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸 ∘ 𝑔) finSupp 0)
71	64, 65, 67, 26, 51, 70	gsumcl 19516	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σg (𝐸 ∘ 𝑔)) ∈ (ℝ* ∖ {-∞}))
72	62, 71	eqeltrd 2839	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ∈ (ℝ* ∖ {-∞}))
73	72	eldifad 3899	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ∈ ℝ*)
74	73	fmpttd 6989	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))):𝑆⟶ℝ*)
75	74	frnd 6608	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ⊆ ℝ*)
76	75	ralrimiva 3103	. . . . . 6 ⊢ (𝜑 → ∀𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ⊆ ℝ*)
77		iunss 4975	. . . . . 6 ⊢ (∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ⊆ ℝ* ↔ ∀𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ⊆ ℝ*)
78	76, 77	sylibr 233	. . . . 5 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ⊆ ℝ*)
79	18, 78	eqsstrid 3969	. . . 4 ⊢ (𝜑 → 𝑇 ⊆ ℝ*)
80		infxrcl 13067	. . . 4 ⊢ (𝑇 ⊆ ℝ* → inf(𝑇, ℝ*, < ) ∈ ℝ*)
81	79, 80	syl 17	. . 3 ⊢ (𝜑 → inf(𝑇, ℝ*, < ) ∈ ℝ*)
82		xmetcl 23484	. . . 4 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋𝐸𝑌) ∈ ℝ*)
83	29, 11, 13, 82	syl3anc 1370	. . 3 ⊢ (𝜑 → (𝑋𝐸𝑌) ∈ ℝ*)
84		1nn 11984	. . . . . . 7 ⊢ 1 ∈ ℕ
85		1ex 10971	. . . . . . . . . . . 12 ⊢ 1 ∈ V
86		opex 5379	. . . . . . . . . . . 12 ⊢ ⟨𝑋, 𝑌⟩ ∈ V
87	85, 86	f1osn 6756	. . . . . . . . . . 11 ⊢ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}–1-1-onto→{⟨𝑋, 𝑌⟩}
88		f1of 6716	. . . . . . . . . . 11 ⊢ ({⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}–1-1-onto→{⟨𝑋, 𝑌⟩} → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩})
89	87, 88	ax-mp 5	. . . . . . . . . 10 ⊢ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩}
90	11, 13	opelxpd 5627	. . . . . . . . . . 11 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉))
91	90	snssd 4742	. . . . . . . . . 10 ⊢ (𝜑 → {⟨𝑋, 𝑌⟩} ⊆ (𝑉 × 𝑉))
92		fss 6617	. . . . . . . . . 10 ⊢ (({⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩} ∧ {⟨𝑋, 𝑌⟩} ⊆ (𝑉 × 𝑉)) → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉))
93	89, 91, 92	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉))
94	29	elfvexd 6808	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ∈ V)
95	94, 94	xpexd 7601	. . . . . . . . . 10 ⊢ (𝜑 → (𝑉 × 𝑉) ∈ V)
96		snex 5354	. . . . . . . . . 10 ⊢ {1} ∈ V
97		elmapg 8628	. . . . . . . . . 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 256	. . . . . . . 8 ⊢ (𝜑 → {⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑m {1}))
100		op1stg 7843	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋)
101	11, 13, 100	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋)
102	101	fveq2d 6778	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋))
103		op2ndg 7844	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
104	11, 13, 103	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
105	104	fveq2d 6778	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌))
106	102, 105	jca 512	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌)))
107	24	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ*𝑠 ∈ V)
108		snfi 8834	. . . . . . . . . . 11 ⊢ {1} ∈ Fin
109	108	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → {1} ∈ Fin)
110	27	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ* ∖ {-∞}) ⊆ ℝ*)
111		xmetge0 23497	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → 0 ≤ (𝑋𝐸𝑌))
112	29, 11, 13, 111	syl3anc 1370	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ≤ (𝑋𝐸𝑌))
113		ge0nemnf 12907	. . . . . . . . . . . . . 14 ⊢ (((𝑋𝐸𝑌) ∈ ℝ* ∧ 0 ≤ (𝑋𝐸𝑌)) → (𝑋𝐸𝑌) ≠ -∞)
114	83, 112, 113	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋𝐸𝑌) ≠ -∞)
115		eldifsn 4720	. . . . . . . . . . . . 13 ⊢ ((𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}) ↔ ((𝑋𝐸𝑌) ∈ ℝ* ∧ (𝑋𝐸𝑌) ≠ -∞))
116	83, 114, 115	sylanbrc 583	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}))
117		fconst6g 6663	. . . . . . . . . . . 12 ⊢ ((𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}) → ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞}))
118	116, 117	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞}))
119		fcoconst 7006	. . . . . . . . . . . . . 14 ⊢ ((𝐸 Fn (𝑉 × 𝑉) ∧ ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉)) → (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}))
120	32, 90, 119	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}))
121	85, 86	xpsn 7013	. . . . . . . . . . . . . 14 ⊢ ({1} × {⟨𝑋, 𝑌⟩}) = {⟨1, ⟨𝑋, 𝑌⟩⟩}
122	121	coeq2i 5769	. . . . . . . . . . . . 13 ⊢ (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})
123		df-ov 7278	. . . . . . . . . . . . . . . 16 ⊢ (𝑋𝐸𝑌) = (𝐸‘⟨𝑋, 𝑌⟩)
124	123	eqcomi 2747	. . . . . . . . . . . . . . 15 ⊢ (𝐸‘⟨𝑋, 𝑌⟩) = (𝑋𝐸𝑌)
125	124	sneqi 4572	. . . . . . . . . . . . . 14 ⊢ {(𝐸‘⟨𝑋, 𝑌⟩)} = {(𝑋𝐸𝑌)}
126	125	xpeq2i 5616	. . . . . . . . . . . . 13 ⊢ ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}) = ({1} × {(𝑋𝐸𝑌)})
127	120, 122, 126	3eqtr3g 2801	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}) = ({1} × {(𝑋𝐸𝑌)}))
128	127	feq1d 6585	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}):{1}⟶(ℝ* ∖ {-∞}) ↔ ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞})))
129	118, 128	mpbird 256	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}):{1}⟶(ℝ* ∖ {-∞}))
130	52, 56	mp1i 13	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ (ℝ* ∖ {-∞}))
131	60	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
132	21, 22, 23, 107, 109, 110, 129, 130, 131	gsumress 18366	. . . . . . . . 9 ⊢ (𝜑 → (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})) = (𝑊 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
133		fconstmpt 5649	. . . . . . . . . . 11 ⊢ ({1} × {(𝑋𝐸𝑌)}) = (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))
134	127, 133	eqtrdi 2794	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}) = (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌)))
135	134	oveq2d 7291	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})) = (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))))
136		cmnmnd 19402	. . . . . . . . . . 11 ⊢ (𝑊 ∈ CMnd → 𝑊 ∈ Mnd)
137	66, 136	mp1i 13	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ Mnd)
138	84	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℕ)
139		eqidd 2739	. . . . . . . . . . 11 ⊢ (𝑗 = 1 → (𝑋𝐸𝑌) = (𝑋𝐸𝑌))
140	64, 139	gsumsn 19555	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Mnd ∧ 1 ∈ ℕ ∧ (𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞})) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))) = (𝑋𝐸𝑌))
141	137, 138, 116, 140	syl3anc 1370	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))) = (𝑋𝐸𝑌))
142	132, 135, 141	3eqtrrd 2783	. . . . . . . 8 ⊢ (𝜑 → (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
143		fveq1 6773	. . . . . . . . . . . . . 14 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝑔‘1) = ({⟨1, ⟨𝑋, 𝑌⟩⟩}‘1))
144	85, 86	fvsn 7053	. . . . . . . . . . . . . 14 ⊢ ({⟨1, ⟨𝑋, 𝑌⟩⟩}‘1) = ⟨𝑋, 𝑌⟩
145	143, 144	eqtrdi 2794	. . . . . . . . . . . . 13 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝑔‘1) = ⟨𝑋, 𝑌⟩)
146	145	fveq2d 6778	. . . . . . . . . . . 12 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (1st ‘(𝑔‘1)) = (1st ‘⟨𝑋, 𝑌⟩))
147	146	fveqeq2d 6782	. . . . . . . . . . 11 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ↔ (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋)))
148	145	fveq2d 6778	. . . . . . . . . . . 12 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (2nd ‘(𝑔‘1)) = (2nd ‘⟨𝑋, 𝑌⟩))
149	148	fveqeq2d 6782	. . . . . . . . . . 11 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌) ↔ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌)))
150	147, 149	anbi12d 631	. . . . . . . . . 10 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ↔ ((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌))))
151		coeq2 5767	. . . . . . . . . . . 12 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝐸 ∘ 𝑔) = (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}))
152	151	oveq2d 7291	. . . . . . . . . . 11 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
153	152	eqeq2d 2749	. . . . . . . . . 10 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ↔ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}))))
154	150, 153	anbi12d 631	. . . . . . . . 9 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ (((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))))
155	154	rspcev 3561	. . . . . . . 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 7308	. . . . . . . . . 10 ⊢ (𝑋𝐸𝑌) ∈ V
158		eqid 2738	. . . . . . . . . . 11 ⊢ (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) = (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
159	158	elrnmpt 5865	. . . . . . . . . 10 ⊢ ((𝑋𝐸𝑌) ∈ V → ((𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
160	157, 159	ax-mp 5	. . . . . . . . 9 ⊢ ((𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
161	15	rexeqi 3347	. . . . . . . . . . 11 ⊢ (∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ↔ ∃𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))} (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
162		fveq1 6773	. . . . . . . . . . . . . . 15 ⊢ (ℎ = 𝑔 → (ℎ‘1) = (𝑔‘1))
163	162	fveq2d 6778	. . . . . . . . . . . . . 14 ⊢ (ℎ = 𝑔 → (1st ‘(ℎ‘1)) = (1st ‘(𝑔‘1)))
164	163	fveqeq2d 6782	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑔 → ((𝐹‘(1st ‘(ℎ‘1))) = (𝐹‘𝑋) ↔ (𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋)))
165		fveq1 6773	. . . . . . . . . . . . . . 15 ⊢ (ℎ = 𝑔 → (ℎ‘𝑛) = (𝑔‘𝑛))
166	165	fveq2d 6778	. . . . . . . . . . . . . 14 ⊢ (ℎ = 𝑔 → (2nd ‘(ℎ‘𝑛)) = (2nd ‘(𝑔‘𝑛)))
167	166	fveqeq2d 6782	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑔 → ((𝐹‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ↔ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)))
168		fveq1 6773	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = 𝑔 → (ℎ‘𝑖) = (𝑔‘𝑖))
169	168	fveq2d 6778	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = 𝑔 → (2nd ‘(ℎ‘𝑖)) = (2nd ‘(𝑔‘𝑖)))
170	169	fveq2d 6778	. . . . . . . . . . . . . . 15 ⊢ (ℎ = 𝑔 → (𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(2nd ‘(𝑔‘𝑖))))
171		fveq1 6773	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = 𝑔 → (ℎ‘(𝑖 + 1)) = (𝑔‘(𝑖 + 1)))
172	171	fveq2d 6778	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = 𝑔 → (1st ‘(ℎ‘(𝑖 + 1))) = (1st ‘(𝑔‘(𝑖 + 1))))
173	172	fveq2d 6778	. . . . . . . . . . . . . . 15 ⊢ (ℎ = 𝑔 → (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
174	170, 173	eqeq12d 2754	. . . . . . . . . . . . . 14 ⊢ (ℎ = 𝑔 → ((𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
175	174	ralbidv 3112	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑔 → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
176	164, 167, 175	3anbi123d 1435	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑔 → (((𝐹‘(1st ‘(ℎ‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
177	176	rexrab 3633	. . . . . . . . . . 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 274	. . . . . . . . . 10 ⊢ (∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
179		oveq2 7283	. . . . . . . . . . . . 13 ⊢ (𝑛 = 1 → (1...𝑛) = (1...1))
180		1z 12350	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℤ
181		fzsn 13298	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℤ → (1...1) = {1})
182	180, 181	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (1...1) = {1}
183	179, 182	eqtrdi 2794	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (1...𝑛) = {1})
184	183	oveq2d 7291	. . . . . . . . . . 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 4443	. . . . . . . . . . . . . . . 16 ⊢ ∀𝑖 ∈ ∅ (𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))
187		oveq1 7282	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 1 → (𝑛 − 1) = (1 − 1))
188		1m1e0 12045	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 − 1) = 0
189	187, 188	eqtrdi 2794	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 1 → (𝑛 − 1) = 0)
190	189	oveq2d 7291	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 1 → (1...(𝑛 − 1)) = (1...0))
191		fz10 13277	. . . . . . . . . . . . . . . . . 18 ⊢ (1...0) = ∅
192	190, 191	eqtrdi 2794	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 1 → (1...(𝑛 − 1)) = ∅)
193	192	raleqdv 3348	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1 → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ ∅ (𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
194	186, 193	mpbiri 257	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1 → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
195	194	biantrud 532	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
196		2fveq3 6779	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1 → (2nd ‘(𝑔‘𝑛)) = (2nd ‘(𝑔‘1)))
197	196	fveqeq2d 6782	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1 → ((𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ↔ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)))
198	197	anbi2d 629	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌))))
199	195, 198	bitr3d 280	. . . . . . . . . . . . 13 ⊢ (𝑛 = 1 → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌))))
200	185, 199	bitrid 282	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌))))
201	200	anbi1d 630	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))))
202	184, 201	rexeqbidv 3337	. . . . . . . . . 10 ⊢ (𝑛 = 1 → (∃𝑔 ∈ ((𝑉 × 𝑉) ↑m (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))))
203	178, 202	bitrid 282	. . . . . . . . 9 ⊢ (𝑛 = 1 → (∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))))
204	160, 203	bitrid 282	. . . . . . . 8 ⊢ (𝑛 = 1 → ((𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))))
205	204	rspcev 3561	. . . . . . 7 ⊢ ((1 ∈ ℕ ∧ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑m {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))) → ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
206	84, 156, 205	sylancr 587	. . . . . 6 ⊢ (𝜑 → ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
207		eliun 4928	. . . . . 6 ⊢ ((𝑋𝐸𝑌) ∈ ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
208	206, 207	sylibr 233	. . . . 5 ⊢ (𝜑 → (𝑋𝐸𝑌) ∈ ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
209	208, 18	eleqtrrdi 2850	. . . 4 ⊢ (𝜑 → (𝑋𝐸𝑌) ∈ 𝑇)
210		infxrlb 13068	. . . 4 ⊢ ((𝑇 ⊆ ℝ* ∧ (𝑋𝐸𝑌) ∈ 𝑇) → inf(𝑇, ℝ*, < ) ≤ (𝑋𝐸𝑌))
211	79, 209, 210	syl2anc 584	. . 3 ⊢ (𝜑 → inf(𝑇, ℝ*, < ) ≤ (𝑋𝐸𝑌))
212	18	eleq2i 2830	. . . . . . 7 ⊢ (𝑝 ∈ 𝑇 ↔ 𝑝 ∈ ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
213		eliun 4928	. . . . . . 7 ⊢ (𝑝 ∈ ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
214	212, 213	bitri 274	. . . . . 6 ⊢ (𝑝 ∈ 𝑇 ↔ ∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
215	158	elrnmpt 5865	. . . . . . . . 9 ⊢ (𝑝 ∈ V → (𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ 𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
216	215	elv 3438	. . . . . . . 8 ⊢ (𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ 𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
217	176, 15	elrab2 3627	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∈ 𝑆 ↔ (𝑔 ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∧ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
218	217	simprbi 497	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 ∈ 𝑆 → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
219	218	adantl 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
220	219	simp2d 1142	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌))
221	3	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐹:𝑉–1-1-onto→𝐵)
222		f1of1 6715	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹:𝑉–1-1→𝐵)
223	221, 222	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐹:𝑉–1-1→𝐵)
224		simplr 766	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑛 ∈ ℕ)
225		elfz1end 13286	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (1...𝑛))
226	224, 225	sylib 217	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑛 ∈ (1...𝑛))
227	49, 226	ffvelrnd 6962	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑔‘𝑛) ∈ (𝑉 × 𝑉))
228		xp2nd 7864	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔‘𝑛) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘𝑛)) ∈ 𝑉)
229	227, 228	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (2nd ‘(𝑔‘𝑛)) ∈ 𝑉)
230	13	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑌 ∈ 𝑉)
231		f1fveq 7135	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ ((2nd ‘(𝑔‘𝑛)) ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ((𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ↔ (2nd ‘(𝑔‘𝑛)) = 𝑌))
232	223, 229, 230, 231	syl12anc 834	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ↔ (2nd ‘(𝑔‘𝑛)) = 𝑌))
233	220, 232	mpbid 231	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (2nd ‘(𝑔‘𝑛)) = 𝑌)
234	233	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2nd ‘(𝑔‘𝑛))) = (𝑋𝐸𝑌))
235		eleq1 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 1 → (𝑚 ∈ (1...𝑛) ↔ 1 ∈ (1...𝑛)))
236		2fveq3 6779	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 1 → (2nd ‘(𝑔‘𝑚)) = (2nd ‘(𝑔‘1)))
237	236	oveq2d 7291	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 1 → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘1))))
238		oveq2 7283	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 1 → (1...𝑚) = (1...1))
239	238, 182	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 1 → (1...𝑚) = {1})
240	239	reseq2d 5891	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 1 → ((𝐸 ∘ 𝑔) ↾ (1...𝑚)) = ((𝐸 ∘ 𝑔) ↾ {1}))
241	240	oveq2d 7291	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 1 → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1})))
242	237, 241	breq12d 5087	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 1 → ((𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1}))))
243	235, 242	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 1 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚)))) ↔ (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1})))))
244	243	imbi2d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 1 → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))))) ↔ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1}))))))
245		eleq1 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑥 → (𝑚 ∈ (1...𝑛) ↔ 𝑥 ∈ (1...𝑛)))
246		2fveq3 6779	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑥 → (2nd ‘(𝑔‘𝑚)) = (2nd ‘(𝑔‘𝑥)))
247	246	oveq2d 7291	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑥 → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘𝑥))))
248		oveq2 7283	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑥 → (1...𝑚) = (1...𝑥))
249	248	reseq2d 5891	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑥 → ((𝐸 ∘ 𝑔) ↾ (1...𝑚)) = ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))
250	249	oveq2d 7291	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑥 → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))))
251	247, 250	breq12d 5087	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑥 → ((𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))))
252	245, 251	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑥 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚)))) ↔ (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))))))
253	252	imbi2d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑥 → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))))) ↔ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))))))
254		eleq1 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑥 + 1) → (𝑚 ∈ (1...𝑛) ↔ (𝑥 + 1) ∈ (1...𝑛)))
255		2fveq3 6779	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = (𝑥 + 1) → (2nd ‘(𝑔‘𝑚)) = (2nd ‘(𝑔‘(𝑥 + 1))))
256	255	oveq2d 7291	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = (𝑥 + 1) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))))
257		oveq2 7283	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = (𝑥 + 1) → (1...𝑚) = (1...(𝑥 + 1)))
258	257	reseq2d 5891	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = (𝑥 + 1) → ((𝐸 ∘ 𝑔) ↾ (1...𝑚)) = ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))
259	258	oveq2d 7291	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = (𝑥 + 1) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))))
260	256, 259	breq12d 5087	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑥 + 1) → ((𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))))
261	254, 260	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝑥 + 1) → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚)))) ↔ ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))))))
262	261	imbi2d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝑥 + 1) → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))))) ↔ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))))))
263		eleq1 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ (1...𝑛) ↔ 𝑛 ∈ (1...𝑛)))
264		2fveq3 6779	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → (2nd ‘(𝑔‘𝑚)) = (2nd ‘(𝑔‘𝑛)))
265	264	oveq2d 7291	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘𝑛))))
266		oveq2 7283	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
267	266	reseq2d 5891	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → ((𝐸 ∘ 𝑔) ↾ (1...𝑚)) = ((𝐸 ∘ 𝑔) ↾ (1...𝑛)))
268	267	oveq2d 7291	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))
269	265, 268	breq12d 5087	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → ((𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛)))))
270	263, 269	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑛 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚)))) ↔ (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))))
271	270	imbi2d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑛 → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))))) ↔ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛)))))))
272	29	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐸 ∈ (∞Met‘𝑉))
273	11	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑋 ∈ 𝑉)
274		nnuz 12621	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℕ = (ℤ≥‘1)
275	224, 274	eleqtrdi 2849	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑛 ∈ (ℤ≥‘1))
276		eluzfz1 13263	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (ℤ≥‘1) → 1 ∈ (1...𝑛))
277	275, 276	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 1 ∈ (1...𝑛))
278	49, 277	ffvelrnd 6962	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑔‘1) ∈ (𝑉 × 𝑉))
279		xp2nd 7864	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔‘1) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘1)) ∈ 𝑉)
280	278, 279	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (2nd ‘(𝑔‘1)) ∈ 𝑉)
281		xmetcl 23484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ (2nd ‘(𝑔‘1)) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔‘1))) ∈ ℝ*)
282	272, 273, 280, 281	syl3anc 1370	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ∈ ℝ*)
283	282	xrleidd 12886	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑋𝐸(2nd ‘(𝑔‘1))))
284	137	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑊 ∈ Mnd)
285	84	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 1 ∈ ℕ)
286	44, 278	ffvelrnd 6962	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸‘(𝑔‘1)) ∈ (ℝ* ∖ {-∞}))
287		2fveq3 6779	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 1 → (𝐸‘(𝑔‘𝑗)) = (𝐸‘(𝑔‘1)))
288	64, 287	gsumsn 19555	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Mnd ∧ 1 ∈ ℕ ∧ (𝐸‘(𝑔‘1)) ∈ (ℝ* ∖ {-∞})) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗)))) = (𝐸‘(𝑔‘1)))
289	284, 285, 286, 288	syl3anc 1370	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗)))) = (𝐸‘(𝑔‘1)))
290	272, 30	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
291		fcompt 7005	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐸:(𝑉 × 𝑉)⟶ℝ* ∧ 𝑔:(1...𝑛)⟶(𝑉 × 𝑉)) → (𝐸 ∘ 𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))))
292	290, 49, 291	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸 ∘ 𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))))
293	292	reseq1d 5890	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐸 ∘ 𝑔) ↾ {1}) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ {1}))
294	277	snssd 4742	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → {1} ⊆ (1...𝑛))
295	294	resmptd 5948	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ {1}) = (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗))))
296	293, 295	eqtrd 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐸 ∘ 𝑔) ↾ {1}) = (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗))))
297	296	oveq2d 7291	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1})) = (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗)))))
298		df-ov 7278	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋𝐸(2nd ‘(𝑔‘1))) = (𝐸‘⟨𝑋, (2nd ‘(𝑔‘1))⟩)
299		1st2nd2 7870	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔‘1) ∈ (𝑉 × 𝑉) → (𝑔‘1) = ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩)
300	278, 299	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑔‘1) = ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩)
301	219	simp1d 1141	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋))
302		xp1st 7863	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔‘1) ∈ (𝑉 × 𝑉) → (1st ‘(𝑔‘1)) ∈ 𝑉)
303	278, 302	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1st ‘(𝑔‘1)) ∈ 𝑉)
304		f1fveq 7135	. . . . . . . . . . . . . . . . . . . . . . . 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 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1st ‘(𝑔‘1)) = 𝑋)
307	306	opeq1d 4810	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩ = ⟨𝑋, (2nd ‘(𝑔‘1))⟩)
308	300, 307	eqtr2d 2779	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ⟨𝑋, (2nd ‘(𝑔‘1))⟩ = (𝑔‘1))
309	308	fveq2d 6778	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸‘⟨𝑋, (2nd ‘(𝑔‘1))⟩) = (𝐸‘(𝑔‘1)))
310	298, 309	eqtrid 2790	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) = (𝐸‘(𝑔‘1)))
311	289, 297, 310	3eqtr4d 2788	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1})) = (𝑋𝐸(2nd ‘(𝑔‘1))))
312	283, 311	breqtrrd 5102	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1})))
313	312	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1}))))
314		simprl 768	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ ℕ)
315	314, 274	eleqtrdi 2849	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (ℤ≥‘1))
316		simprr 770	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑥 + 1) ∈ (1...𝑛))
317		peano2fzr 13269	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (ℤ≥‘1) ∧ (𝑥 + 1) ∈ (1...𝑛)) → 𝑥 ∈ (1...𝑛))
318	315, 316, 317	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (1...𝑛))
319	318	expr 457	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 + 1) ∈ (1...𝑛) → 𝑥 ∈ (1...𝑛)))
320	319	imim1d 82	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))))))
321	272	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸 ∈ (∞Met‘𝑉))
322	273	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑋 ∈ 𝑉)
323	49	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
324	323, 318	ffvelrnd 6962	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘𝑥) ∈ (𝑉 × 𝑉))
325		xp2nd 7864	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔‘𝑥) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘𝑥)) ∈ 𝑉)
326	324, 325	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔‘𝑥)) ∈ 𝑉)
327		xmetcl 23484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ (2nd ‘(𝑔‘𝑥)) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ∈ ℝ*)
328	321, 322, 326, 327	syl3anc 1370	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ∈ ℝ*)
329	66	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑊 ∈ CMnd)
330		fzfid 13693	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...𝑥) ∈ Fin)
331	51	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸 ∘ 𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
332		fzsuc 13303	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (ℤ≥‘1) → (1...(𝑥 + 1)) = ((1...𝑥) ∪ {(𝑥 + 1)}))
333	315, 332	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...(𝑥 + 1)) = ((1...𝑥) ∪ {(𝑥 + 1)}))
334		elfzuz3 13253	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 + 1) ∈ (1...𝑛) → 𝑛 ∈ (ℤ≥‘(𝑥 + 1)))
335	334	ad2antll 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑛 ∈ (ℤ≥‘(𝑥 + 1)))
336		fzss2 13296	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ (ℤ≥‘(𝑥 + 1)) → (1...(𝑥 + 1)) ⊆ (1...𝑛))
337	335, 336	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...(𝑥 + 1)) ⊆ (1...𝑛))
338	333, 337	eqsstrrd 3960	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((1...𝑥) ∪ {(𝑥 + 1)}) ⊆ (1...𝑛))
339	338	unssad 4121	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...𝑥) ⊆ (1...𝑛))
340	331, 339	fssresd 6641	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...𝑥)):(1...𝑥)⟶(ℝ* ∖ {-∞}))
341	68	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 0 ∈ V)
342	340, 330, 341	fdmfifsupp 9138	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...𝑥)) finSupp 0)
343	64, 65, 329, 330, 340, 342	gsumcl 19516	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) ∈ (ℝ* ∖ {-∞}))
344	343	eldifad 3899	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) ∈ ℝ*)
345	321, 30	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
346	323, 316	ffvelrnd 6962	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉))
347	345, 346	ffvelrnd 6962	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*)
348		xleadd1a 12987	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ∈ ℝ* ∧ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) ∈ ℝ* ∧ (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*) ∧ (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
349	348	ex 413	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ∈ ℝ* ∧ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) ∈ ℝ* ∧ (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
350	328, 344, 347, 349	syl3anc 1370	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
351		xp2nd 7864	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
352	346, 351	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
353		xmettri 23504	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑋 ∈ 𝑉 ∧ (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉 ∧ (2nd ‘(𝑔‘𝑥)) ∈ 𝑉)) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 ((2nd ‘(𝑔‘𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
354	321, 322, 352, 326, 353	syl13anc 1371	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 ((2nd ‘(𝑔‘𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
355		1st2nd2 7870	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (𝑔‘(𝑥 + 1)) = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
356	346, 355	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
357		2fveq3 6779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 = 𝑥 → (2nd ‘(𝑔‘𝑖)) = (2nd ‘(𝑔‘𝑥)))
358	357	fveq2d 6778	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝑥 → (𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(2nd ‘(𝑔‘𝑥))))
359		fvoveq1 7298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = 𝑥 → (𝑔‘(𝑖 + 1)) = (𝑔‘(𝑥 + 1)))
360	359	fveq2d 6778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 = 𝑥 → (1st ‘(𝑔‘(𝑖 + 1))) = (1st ‘(𝑔‘(𝑥 + 1))))
361	360	fveq2d 6778	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝑥 → (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))))
362	358, 361	eqeq12d 2754	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 = 𝑥 → ((𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(𝑔‘𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1))))))
363	219	simp3d 1143	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
364	363	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
365		nnz 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℤ)
366	365	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ ℤ)
367		eluzp1m1 12608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ (ℤ≥‘(𝑥 + 1))) → (𝑛 − 1) ∈ (ℤ≥‘𝑥))
368	366, 335, 367	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑛 − 1) ∈ (ℤ≥‘𝑥))
369		elfzuzb 13250	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ (1...(𝑛 − 1)) ↔ (𝑥 ∈ (ℤ≥‘1) ∧ (𝑛 − 1) ∈ (ℤ≥‘𝑥)))
370	315, 368, 369	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (1...(𝑛 − 1)))
371	362, 364, 370	rspcdva 3562	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐹‘(2nd ‘(𝑔‘𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))))
372	223	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐹:𝑉–1-1→𝐵)
373		xp1st 7863	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
374	346, 373	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
375		f1fveq 7135	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 231	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔‘𝑥)) = (1st ‘(𝑔‘(𝑥 + 1))))
378	377	opeq1d 4810	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ⟨(2nd ‘(𝑔‘𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩ = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
379	356, 378	eqtr4d 2781	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) = ⟨(2nd ‘(𝑔‘𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
380	379	fveq2d 6778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) = (𝐸‘⟨(2nd ‘(𝑔‘𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩))
381		df-ov 7278	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2nd ‘(𝑔‘𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) = (𝐸‘⟨(2nd ‘(𝑔‘𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
382	380, 381	eqtr4di 2796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) = ((2nd ‘(𝑔‘𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1)))))
383	382	oveq2d 7291	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) = ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 ((2nd ‘(𝑔‘𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
384	354, 383	breqtrrd 5102	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
385		xmetcl 23484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
386	321, 322, 352, 385	syl3anc 1370	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
387	328, 347	xaddcld 13035	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
388	344, 347	xaddcld 13035	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
389		xrletr 12892	. . . . . . . . . . . . . . . . . . . 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 1370	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∧ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
391	384, 390	mpand 692	. . . . . . . . . . . . . . . . . 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 12727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℝ* ∈ V
394	393	difexi 5252	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℝ* ∖ {-∞}) ∈ V
395	23, 22	ressplusg 17000	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℝ* ∖ {-∞}) ∈ V → +𝑒 = (+g‘𝑊))
396	394, 395	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ +𝑒 = (+g‘𝑊)
397	44	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
398		fzelp1 13308	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (1...𝑥) → 𝑗 ∈ (1...(𝑥 + 1)))
399	49	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
400	337	sselda 3921	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → 𝑗 ∈ (1...𝑛))
401	399, 400	ffvelrnd 6962	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → (𝑔‘𝑗) ∈ (𝑉 × 𝑉))
402	398, 401	sylan2 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → (𝑔‘𝑗) ∈ (𝑉 × 𝑉))
403	397, 402	ffvelrnd 6962	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → (𝐸‘(𝑔‘𝑗)) ∈ (ℝ* ∖ {-∞}))
404		fzp1disj 13315	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1...𝑥) ∩ {(𝑥 + 1)}) = ∅
405	404	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((1...𝑥) ∩ {(𝑥 + 1)}) = ∅)
406		disjsn 4647	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1...𝑥) ∩ {(𝑥 + 1)}) = ∅ ↔ ¬ (𝑥 + 1) ∈ (1...𝑥))
407	405, 406	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ¬ (𝑥 + 1) ∈ (1...𝑥))
408	44	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
409	408, 346	ffvelrnd 6962	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) ∈ (ℝ* ∖ {-∞}))
410		2fveq3 6779	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑥 + 1) → (𝐸‘(𝑔‘𝑗)) = (𝐸‘(𝑔‘(𝑥 + 1))))
411	64, 396, 329, 330, 403, 316, 407, 409, 410	gsumunsn 19561	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔‘𝑗)))) = ((𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗)))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
412	292	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸 ∘ 𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))))
413	412, 333	reseq12d 5892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ ((1...𝑥) ∪ {(𝑥 + 1)})))
414	338	resmptd 5948	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ ((1...𝑥) ∪ {(𝑥 + 1)})) = (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔‘𝑗))))
415	413, 414	eqtrd 2778	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))) = (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔‘𝑗))))
416	415	oveq2d 7291	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))) = (𝑊 Σg (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔‘𝑗)))))
417	412	reseq1d 5890	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...𝑥)) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ (1...𝑥)))
418	339	resmptd 5948	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ (1...𝑥)) = (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗))))
419	417, 418	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...𝑥)) = (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗))))
420	419	oveq2d 7291	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) = (𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗)))))
421	420	oveq1d 7290	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) = ((𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗)))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
422	411, 416, 421	3eqtr4d 2788	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))) = ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
423	422	breq2d 5086	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))) ↔ (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
424	392, 423	sylibrd 258	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))))
425	320, 424	animpimp2impd 843	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℕ → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))))) → (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))))))
426	244, 253, 262, 271, 313, 425	nnind 11991	. . . . . . . . . . . . . 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 5098	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸𝑌) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))
430		ffn 6600	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∘ 𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}) → (𝐸 ∘ 𝑔) Fn (1...𝑛))
431		fnresdm 6551	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∘ 𝑔) Fn (1...𝑛) → ((𝐸 ∘ 𝑔) ↾ (1...𝑛)) = (𝐸 ∘ 𝑔))
432	51, 430, 431	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐸 ∘ 𝑔) ↾ (1...𝑛)) = (𝐸 ∘ 𝑔))
433	432	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))) = (𝑊 Σg (𝐸 ∘ 𝑔)))
434	62, 433	eqtr4d 2781	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) = (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))
435	429, 434	breqtrrd 5102	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸𝑌) ≤ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
436		breq2 5078	. . . . . . . . . 10 ⊢ (𝑝 = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) → ((𝑋𝐸𝑌) ≤ 𝑝 ↔ (𝑋𝐸𝑌) ≤ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
437	435, 436	syl5ibrcom 246	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑝 = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) → (𝑋𝐸𝑌) ≤ 𝑝))
438	437	rexlimdva 3213	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∃𝑔 ∈ 𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) → (𝑋𝐸𝑌) ≤ 𝑝))
439	216, 438	syl5bi 241	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) → (𝑋𝐸𝑌) ≤ 𝑝))
440	439	rexlimdva 3213	. . . . . 6 ⊢ (𝜑 → (∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) → (𝑋𝐸𝑌) ≤ 𝑝))
441	214, 440	syl5bi 241	. . . . 5 ⊢ (𝜑 → (𝑝 ∈ 𝑇 → (𝑋𝐸𝑌) ≤ 𝑝))
442	441	ralrimiv 3102	. . . 4 ⊢ (𝜑 → ∀𝑝 ∈ 𝑇 (𝑋𝐸𝑌) ≤ 𝑝)
443		infxrgelb 13069	. . . . 5 ⊢ ((𝑇 ⊆ ℝ* ∧ (𝑋𝐸𝑌) ∈ ℝ*) → ((𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ) ↔ ∀𝑝 ∈ 𝑇 (𝑋𝐸𝑌) ≤ 𝑝))
444	79, 83, 443	syl2anc 584	. . . 4 ⊢ (𝜑 → ((𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ) ↔ ∀𝑝 ∈ 𝑇 (𝑋𝐸𝑌) ≤ 𝑝))
445	442, 444	mpbird 256	. . 3 ⊢ (𝜑 → (𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ))
446	81, 83, 211, 445	xrletrid 12889	. 2 ⊢ (𝜑 → inf(𝑇, ℝ*, < ) = (𝑋𝐸𝑌))
447	20, 446	eqtrd 2778	1 ⊢ (𝜑 → ((𝐹‘𝑋)𝐷(𝐹‘𝑌)) = (𝑋𝐸𝑌))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3065  {crab 3068  Vcvv 3432   ∖ cdif 3884   ∪ cun 3885   ∩ cin 3886   ⊆ wss 3887  ∅c0 4256  {csn 4561  ⟨cop 4567  ∪ ciun 4924   class class class wbr 5074   ↦ cmpt 5157   × cxp 5587  ran crn 5590   ↾ cres 5591   ∘ ccom 5593   Fn wfn 6428  ⟶wf 6429  –1-1→wf1 6430  –onto→wfo 6431  –1-1-onto→wf1o 6432  ‘cfv 6433  (class class class)co 7275  1^st c1st 7829  2^nd c2nd 7830   ↑_m cmap 8615  Fincfn 8733  infcinf 9200  ℝcr 10870  0cc0 10871  1c1 10872   + caddc 10874  -∞cmnf 11007  ℝ^*cxr 11008   < clt 11009   ≤ cle 11010   − cmin 11205  ℕcn 11973  ℤcz 12319  ℤ_≥cuz 12582   +_𝑒 cxad 12846  ...cfz 13239  Basecbs 16912   ↾_s cress 16941  +_gcplusg 16962  distcds 16971   Σ_g cgsu 17151  ℝ^*_𝑠cxrs 17211   “_s cimas 17215  Mndcmnd 18385  CMndccmn 19386  ∞Metcxmet 20582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948  ax-pre-sup 10949

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-iin 4927  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-of 7533  df-om 7713  df-1st 7831  df-2nd 7832  df-supp 7978  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-er 8498  df-map 8617  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-fsupp 9129  df-sup 9201  df-inf 9202  df-oi 9269  df-card 9697  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-4 12038  df-5 12039  df-6 12040  df-7 12041  df-8 12042  df-9 12043  df-n0 12234  df-z 12320  df-dec 12438  df-uz 12583  df-rp 12731  df-xneg 12848  df-xadd 12849  df-xmul 12850  df-fz 13240  df-fzo 13383  df-seq 13722  df-hash 14045  df-struct 16848  df-sets 16865  df-slot 16883  df-ndx 16895  df-base 16913  df-ress 16942  df-plusg 16975  df-mulr 16976  df-sca 16978  df-vsca 16979  df-ip 16980  df-tset 16981  df-ple 16982  df-ds 16984  df-0g 17152  df-gsum 17153  df-xrs 17213  df-imas 17219  df-mre 17295  df-mrc 17296  df-acs 17298  df-mgm 18326  df-sgrp 18375  df-mnd 18386  df-submnd 18431  df-mulg 18701  df-cntz 18923  df-cmn 19388  df-xmet 20590

This theorem is referenced by:  imasdsf1o  23527