Theorem imasdsf1olem 21988

Description: Lemma for imasdsf1o 21989. (Contributed by Mario Carneiro, 21-Aug-2015.) (Proof shortened by AV, 6-Oct-2020.)

Hypotheses

Ref	Expression
imasdsf1o.u	⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))
imasdsf1o.v	⊢ (𝜑 → 𝑉 = (Base‘𝑅))
imasdsf1o.f	⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵)
imasdsf1o.r	⊢ (𝜑 → 𝑅 ∈ 𝑍)
imasdsf1o.e	⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))
imasdsf1o.d	⊢ 𝐷 = (dist‘𝑈)
imasdsf1o.m	⊢ (𝜑 → 𝐸 ∈ (∞Met‘𝑉))
imasdsf1o.x	⊢ (𝜑 → 𝑋 ∈ 𝑉)
imasdsf1o.y	⊢ (𝜑 → 𝑌 ∈ 𝑉)
imasdsf1o.w	⊢ 𝑊 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞}))
imasdsf1o.s	⊢ 𝑆 = {ℎ ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))}
imasdsf1o.t	⊢ 𝑇 = ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))

Assertion

Ref	Expression
imasdsf1olem	⊢ (𝜑 → ((𝐹‘𝑋)𝐷(𝐹‘𝑌)) = (𝑋𝐸𝑌))

Distinct variable groups:   𝑔,ℎ,𝑖,𝑛,𝐹   𝜑,𝑔,ℎ,𝑖,𝑛   𝑔,𝑉,ℎ,𝑖,𝑛   𝑔,𝐸,𝑖,𝑛   𝑅,𝑔,ℎ,𝑖,𝑛   𝑆,𝑔   𝑔,𝑋,ℎ,𝑖,𝑛   𝑔,𝑌,ℎ,𝑖,𝑛

Allowed substitution hints:   𝐵(𝑔,ℎ,𝑖,𝑛)   𝐷(𝑔,ℎ,𝑖,𝑛)   𝑆(ℎ,𝑖,𝑛)   𝑇(𝑔,ℎ,𝑖,𝑛)   𝑈(𝑔,ℎ,𝑖,𝑛)   𝐸(ℎ)   𝑊(𝑔,ℎ,𝑖,𝑛)   𝑍(𝑔,ℎ,𝑖,𝑛)

Proof of Theorem imasdsf1olem

Dummy variables 𝑓 𝑗 𝑚 𝑝 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		imasdsf1o.u	. . . 4 ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))
2		imasdsf1o.v	. . . 4 ⊢ (𝜑 → 𝑉 = (Base‘𝑅))
3		imasdsf1o.f	. . . . 5 ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵)
4		f1ofo 6057	. . . . 5 ⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹:𝑉–onto→𝐵)
5	3, 4	syl 17	. . . 4 ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
6		imasdsf1o.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑍)
7		eqid 2610	. . . 4 ⊢ (dist‘𝑅) = (dist‘𝑅)
8		imasdsf1o.d	. . . 4 ⊢ 𝐷 = (dist‘𝑈)
9		f1of 6050	. . . . . 6 ⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹:𝑉⟶𝐵)
10	3, 9	syl 17	. . . . 5 ⊢ (𝜑 → 𝐹:𝑉⟶𝐵)
11		imasdsf1o.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
12	10, 11	ffvelrnd 6268	. . . 4 ⊢ (𝜑 → (𝐹‘𝑋) ∈ 𝐵)
13		imasdsf1o.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
14	10, 13	ffvelrnd 6268	. . . 4 ⊢ (𝜑 → (𝐹‘𝑌) ∈ 𝐵)
15		imasdsf1o.s	. . . 4 ⊢ 𝑆 = {ℎ ∈ ((𝑉 × 𝑉) ↑𝑚 (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 15999	. . 3 ⊢ (𝜑 → ((𝐹‘𝑋)𝐷(𝐹‘𝑌)) = inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))), ℝ*, < ))
18		imasdsf1o.t	. . . 4 ⊢ 𝑇 = ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
19	18	infeq1i 8267	. . 3 ⊢ inf(𝑇, ℝ*, < ) = inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))), ℝ*, < )
20	17, 19	syl6eqr 2662	. 2 ⊢ (𝜑 → ((𝐹‘𝑋)𝐷(𝐹‘𝑌)) = inf(𝑇, ℝ*, < ))
21		xrsbas 19581	. . . . . . . . . . . 12 ⊢ ℝ* = (Base‘ℝ*𝑠)
22		xrsadd 19582	. . . . . . . . . . . 12 ⊢ +𝑒 = (+g‘ℝ*𝑠)
23		imasdsf1o.w	. . . . . . . . . . . 12 ⊢ 𝑊 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞}))
24		xrsex 19580	. . . . . . . . . . . . 13 ⊢ ℝ*𝑠 ∈ V
25	24	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ℝ*𝑠 ∈ V)
26		fzfid 12634	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1...𝑛) ∈ Fin)
27		difss 3699	. . . . . . . . . . . . 13 ⊢ (ℝ* ∖ {-∞}) ⊆ ℝ*
28	27	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ* ∖ {-∞}) ⊆ ℝ*)
29		imasdsf1o.m	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸 ∈ (∞Met‘𝑉))
30		xmetf 21944	. . . . . . . . . . . . . . . 16 ⊢ (𝐸 ∈ (∞Met‘𝑉) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
31		ffn 5958	. . . . . . . . . . . . . . . 16 ⊢ (𝐸:(𝑉 × 𝑉)⟶ℝ* → 𝐸 Fn (𝑉 × 𝑉))
32	29, 30, 31	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐸 Fn (𝑉 × 𝑉))
33		xmetcl 21946	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉) → (𝑓𝐸𝑔) ∈ ℝ*)
34		xmetge0 21959	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉) → 0 ≤ (𝑓𝐸𝑔))
35		ge0nemnf 11878	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓𝐸𝑔) ∈ ℝ* ∧ 0 ≤ (𝑓𝐸𝑔)) → (𝑓𝐸𝑔) ≠ -∞)
36	33, 34, 35	syl2anc 691	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉) → (𝑓𝐸𝑔) ≠ -∞)
37		eldifsn 4260	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}) ↔ ((𝑓𝐸𝑔) ∈ ℝ* ∧ (𝑓𝐸𝑔) ≠ -∞))
38	33, 36, 37	sylanbrc 695	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
39	38	3expb 1258	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉)) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
40	29, 39	sylan 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉)) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
41	40	ralrimivva 2954	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑓 ∈ 𝑉 ∀𝑔 ∈ 𝑉 (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
42		ffnov 6662	. . . . . . . . . . . . . . 15 ⊢ (𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}) ↔ (𝐸 Fn (𝑉 × 𝑉) ∧ ∀𝑓 ∈ 𝑉 ∀𝑔 ∈ 𝑉 (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞})))
43	32, 41, 42	sylanbrc 695	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
44	43	ad2antrr 758	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
45		ssrab2 3650	. . . . . . . . . . . . . . . . 17 ⊢ {ℎ ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))} ⊆ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))
46	15, 45	eqsstri 3598	. . . . . . . . . . . . . . . 16 ⊢ 𝑆 ⊆ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))
47	46	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑆 ⊆ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)))
48	47	sselda 3568	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)))
49		elmapi 7765	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
50	48, 49	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
51		fco 5971	. . . . . . . . . . . . 13 ⊢ ((𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}) ∧ 𝑔:(1...𝑛)⟶(𝑉 × 𝑉)) → (𝐸 ∘ 𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
52	44, 50, 51	syl2anc 691	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸 ∘ 𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
53		0re 9919	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
54		rexr 9964	. . . . . . . . . . . . . 14 ⊢ (0 ∈ ℝ → 0 ∈ ℝ*)
55		renemnf 9967	. . . . . . . . . . . . . 14 ⊢ (0 ∈ ℝ → 0 ≠ -∞)
56		eldifsn 4260	. . . . . . . . . . . . . 14 ⊢ (0 ∈ (ℝ* ∖ {-∞}) ↔ (0 ∈ ℝ* ∧ 0 ≠ -∞))
57	54, 55, 56	sylanbrc 695	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℝ → 0 ∈ (ℝ* ∖ {-∞}))
58	53, 57	mp1i 13	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 0 ∈ (ℝ* ∖ {-∞}))
59		xaddid2 11947	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ* → (0 +𝑒 𝑥) = 𝑥)
60		xaddid1 11946	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ* → (𝑥 +𝑒 0) = 𝑥)
61	59, 60	jca 553	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ* → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
62	61	adantl 481	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ 𝑥 ∈ ℝ*) → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
63	21, 22, 23, 25, 26, 28, 52, 58, 62	gsumress 17099	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) = (𝑊 Σg (𝐸 ∘ 𝑔)))
64	23, 21	ressbas2 15758	. . . . . . . . . . . . 13 ⊢ ((ℝ* ∖ {-∞}) ⊆ ℝ* → (ℝ* ∖ {-∞}) = (Base‘𝑊))
65	27, 64	ax-mp 5	. . . . . . . . . . . 12 ⊢ (ℝ* ∖ {-∞}) = (Base‘𝑊)
66	23	xrs10 19604	. . . . . . . . . . . 12 ⊢ 0 = (0g‘𝑊)
67	23	xrs1cmn 19605	. . . . . . . . . . . . 13 ⊢ 𝑊 ∈ CMnd
68	67	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑊 ∈ CMnd)
69		c0ex 9913	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
70	69	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 0 ∈ V)
71	52, 26, 70	fdmfifsupp 8168	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸 ∘ 𝑔) finSupp 0)
72	65, 66, 68, 26, 52, 71	gsumcl 18139	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σg (𝐸 ∘ 𝑔)) ∈ (ℝ* ∖ {-∞}))
73	63, 72	eqeltrd 2688	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ∈ (ℝ* ∖ {-∞}))
74	73	eldifad 3552	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ∈ ℝ*)
75		eqid 2610	. . . . . . . . 9 ⊢ (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) = (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
76	74, 75	fmptd 6292	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))):𝑆⟶ℝ*)
77		frn 5966	. . . . . . . 8 ⊢ ((𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))):𝑆⟶ℝ* → ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ⊆ ℝ*)
78	76, 77	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ⊆ ℝ*)
79	78	ralrimiva 2949	. . . . . 6 ⊢ (𝜑 → ∀𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ⊆ ℝ*)
80		iunss 4497	. . . . . 6 ⊢ (∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ⊆ ℝ* ↔ ∀𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ⊆ ℝ*)
81	79, 80	sylibr 223	. . . . 5 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ⊆ ℝ*)
82	18, 81	syl5eqss 3612	. . . 4 ⊢ (𝜑 → 𝑇 ⊆ ℝ*)
83		infxrcl 12035	. . . 4 ⊢ (𝑇 ⊆ ℝ* → inf(𝑇, ℝ*, < ) ∈ ℝ*)
84	82, 83	syl 17	. . 3 ⊢ (𝜑 → inf(𝑇, ℝ*, < ) ∈ ℝ*)
85		xmetcl 21946	. . . 4 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋𝐸𝑌) ∈ ℝ*)
86	29, 11, 13, 85	syl3anc 1318	. . 3 ⊢ (𝜑 → (𝑋𝐸𝑌) ∈ ℝ*)
87		1nn 10908	. . . . . . 7 ⊢ 1 ∈ ℕ
88		1ex 9914	. . . . . . . . . . . 12 ⊢ 1 ∈ V
89		opex 4859	. . . . . . . . . . . 12 ⊢ ⟨𝑋, 𝑌⟩ ∈ V
90	88, 89	f1osn 6088	. . . . . . . . . . 11 ⊢ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}–1-1-onto→{⟨𝑋, 𝑌⟩}
91		f1of 6050	. . . . . . . . . . 11 ⊢ ({⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}–1-1-onto→{⟨𝑋, 𝑌⟩} → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩})
92	90, 91	ax-mp 5	. . . . . . . . . 10 ⊢ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩}
93		opelxpi 5072	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉))
94	11, 13, 93	syl2anc 691	. . . . . . . . . . 11 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉))
95	94	snssd 4281	. . . . . . . . . 10 ⊢ (𝜑 → {⟨𝑋, 𝑌⟩} ⊆ (𝑉 × 𝑉))
96		fss 5969	. . . . . . . . . 10 ⊢ (({⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩} ∧ {⟨𝑋, 𝑌⟩} ⊆ (𝑉 × 𝑉)) → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉))
97	92, 95, 96	sylancr 694	. . . . . . . . 9 ⊢ (𝜑 → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉))
98	29	elfvexd 6132	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ∈ V)
99		xpexg 6858	. . . . . . . . . . 11 ⊢ ((𝑉 ∈ V ∧ 𝑉 ∈ V) → (𝑉 × 𝑉) ∈ V)
100	98, 98, 99	syl2anc 691	. . . . . . . . . 10 ⊢ (𝜑 → (𝑉 × 𝑉) ∈ V)
101		snex 4835	. . . . . . . . . 10 ⊢ {1} ∈ V
102		elmapg 7757	. . . . . . . . . 10 ⊢ (((𝑉 × 𝑉) ∈ V ∧ {1} ∈ V) → ({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑𝑚 {1}) ↔ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉)))
103	100, 101, 102	sylancl 693	. . . . . . . . 9 ⊢ (𝜑 → ({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑𝑚 {1}) ↔ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉)))
104	97, 103	mpbird 246	. . . . . . . 8 ⊢ (𝜑 → {⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑𝑚 {1}))
105		op1stg 7071	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋)
106	11, 13, 105	syl2anc 691	. . . . . . . . . 10 ⊢ (𝜑 → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋)
107	106	fveq2d 6107	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋))
108		op2ndg 7072	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
109	11, 13, 108	syl2anc 691	. . . . . . . . . 10 ⊢ (𝜑 → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
110	109	fveq2d 6107	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌))
111	107, 110	jca 553	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌)))
112	24	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ*𝑠 ∈ V)
113		snfi 7923	. . . . . . . . . . 11 ⊢ {1} ∈ Fin
114	113	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → {1} ∈ Fin)
115	27	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ* ∖ {-∞}) ⊆ ℝ*)
116		xmetge0 21959	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → 0 ≤ (𝑋𝐸𝑌))
117	29, 11, 13, 116	syl3anc 1318	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ≤ (𝑋𝐸𝑌))
118		ge0nemnf 11878	. . . . . . . . . . . . . 14 ⊢ (((𝑋𝐸𝑌) ∈ ℝ* ∧ 0 ≤ (𝑋𝐸𝑌)) → (𝑋𝐸𝑌) ≠ -∞)
119	86, 117, 118	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋𝐸𝑌) ≠ -∞)
120		eldifsn 4260	. . . . . . . . . . . . 13 ⊢ ((𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}) ↔ ((𝑋𝐸𝑌) ∈ ℝ* ∧ (𝑋𝐸𝑌) ≠ -∞))
121	86, 119, 120	sylanbrc 695	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}))
122		fconst6g 6007	. . . . . . . . . . . 12 ⊢ ((𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}) → ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞}))
123	121, 122	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞}))
124		fcoconst 6307	. . . . . . . . . . . . . 14 ⊢ ((𝐸 Fn (𝑉 × 𝑉) ∧ ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉)) → (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}))
125	32, 94, 124	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}))
126	88, 89	xpsn 6313	. . . . . . . . . . . . . 14 ⊢ ({1} × {⟨𝑋, 𝑌⟩}) = {⟨1, ⟨𝑋, 𝑌⟩⟩}
127	126	coeq2i 5204	. . . . . . . . . . . . 13 ⊢ (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})
128		df-ov 6552	. . . . . . . . . . . . . . . 16 ⊢ (𝑋𝐸𝑌) = (𝐸‘⟨𝑋, 𝑌⟩)
129	128	eqcomi 2619	. . . . . . . . . . . . . . 15 ⊢ (𝐸‘⟨𝑋, 𝑌⟩) = (𝑋𝐸𝑌)
130	129	sneqi 4136	. . . . . . . . . . . . . 14 ⊢ {(𝐸‘⟨𝑋, 𝑌⟩)} = {(𝑋𝐸𝑌)}
131	130	xpeq2i 5060	. . . . . . . . . . . . 13 ⊢ ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}) = ({1} × {(𝑋𝐸𝑌)})
132	125, 127, 131	3eqtr3g 2667	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}) = ({1} × {(𝑋𝐸𝑌)}))
133	132	feq1d 5943	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}):{1}⟶(ℝ* ∖ {-∞}) ↔ ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞})))
134	123, 133	mpbird 246	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}):{1}⟶(ℝ* ∖ {-∞}))
135	53, 57	mp1i 13	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ (ℝ* ∖ {-∞}))
136	61	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
137	21, 22, 23, 112, 114, 115, 134, 135, 136	gsumress 17099	. . . . . . . . 9 ⊢ (𝜑 → (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})) = (𝑊 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
138		fconstmpt 5085	. . . . . . . . . . 11 ⊢ ({1} × {(𝑋𝐸𝑌)}) = (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))
139	132, 138	syl6eq 2660	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}) = (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌)))
140	139	oveq2d 6565	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})) = (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))))
141		cmnmnd 18031	. . . . . . . . . . 11 ⊢ (𝑊 ∈ CMnd → 𝑊 ∈ Mnd)
142	67, 141	mp1i 13	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ Mnd)
143	87	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℕ)
144		eqidd 2611	. . . . . . . . . . 11 ⊢ (𝑗 = 1 → (𝑋𝐸𝑌) = (𝑋𝐸𝑌))
145	65, 144	gsumsn 18177	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Mnd ∧ 1 ∈ ℕ ∧ (𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞})) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))) = (𝑋𝐸𝑌))
146	142, 143, 121, 145	syl3anc 1318	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))) = (𝑋𝐸𝑌))
147	137, 140, 146	3eqtrrd 2649	. . . . . . . 8 ⊢ (𝜑 → (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
148		fveq1 6102	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝑔‘1) = ({⟨1, ⟨𝑋, 𝑌⟩⟩}‘1))
149	88, 89	fvsn 6351	. . . . . . . . . . . . . . 15 ⊢ ({⟨1, ⟨𝑋, 𝑌⟩⟩}‘1) = ⟨𝑋, 𝑌⟩
150	148, 149	syl6eq 2660	. . . . . . . . . . . . . 14 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝑔‘1) = ⟨𝑋, 𝑌⟩)
151	150	fveq2d 6107	. . . . . . . . . . . . 13 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (1st ‘(𝑔‘1)) = (1st ‘⟨𝑋, 𝑌⟩))
152	151	fveq2d 6107	. . . . . . . . . . . 12 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)))
153	152	eqeq1d 2612	. . . . . . . . . . 11 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ↔ (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋)))
154	150	fveq2d 6107	. . . . . . . . . . . . 13 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (2nd ‘(𝑔‘1)) = (2nd ‘⟨𝑋, 𝑌⟩))
155	154	fveq2d 6107	. . . . . . . . . . . 12 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)))
156	155	eqeq1d 2612	. . . . . . . . . . 11 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌) ↔ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌)))
157	153, 156	anbi12d 743	. . . . . . . . . 10 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ↔ ((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌))))
158		coeq2 5202	. . . . . . . . . . . 12 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝐸 ∘ 𝑔) = (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}))
159	158	oveq2d 6565	. . . . . . . . . . 11 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
160	159	eqeq2d 2620	. . . . . . . . . 10 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ↔ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}))))
161	157, 160	anbi12d 743	. . . . . . . . 9 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ (((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))))
162	161	rspcev 3282	. . . . . . . 8 ⊢ (({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑𝑚 {1}) ∧ (((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))) → ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
163	104, 111, 147, 162	syl12anc 1316	. . . . . . 7 ⊢ (𝜑 → ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
164		ovex 6577	. . . . . . . . . 10 ⊢ (𝑋𝐸𝑌) ∈ V
165	75	elrnmpt 5293	. . . . . . . . . 10 ⊢ ((𝑋𝐸𝑌) ∈ V → ((𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
166	164, 165	ax-mp 5	. . . . . . . . 9 ⊢ ((𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
167	15	rexeqi 3120	. . . . . . . . . . 11 ⊢ (∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ↔ ∃𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))} (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
168		fveq1 6102	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = 𝑔 → (ℎ‘1) = (𝑔‘1))
169	168	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ (ℎ = 𝑔 → (1st ‘(ℎ‘1)) = (1st ‘(𝑔‘1)))
170	169	fveq2d 6107	. . . . . . . . . . . . . 14 ⊢ (ℎ = 𝑔 → (𝐹‘(1st ‘(ℎ‘1))) = (𝐹‘(1st ‘(𝑔‘1))))
171	170	eqeq1d 2612	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑔 → ((𝐹‘(1st ‘(ℎ‘1))) = (𝐹‘𝑋) ↔ (𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋)))
172		fveq1 6102	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = 𝑔 → (ℎ‘𝑛) = (𝑔‘𝑛))
173	172	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ (ℎ = 𝑔 → (2nd ‘(ℎ‘𝑛)) = (2nd ‘(𝑔‘𝑛)))
174	173	fveq2d 6107	. . . . . . . . . . . . . 14 ⊢ (ℎ = 𝑔 → (𝐹‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘(2nd ‘(𝑔‘𝑛))))
175	174	eqeq1d 2612	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑔 → ((𝐹‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ↔ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)))
176		fveq1 6102	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = 𝑔 → (ℎ‘𝑖) = (𝑔‘𝑖))
177	176	fveq2d 6107	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = 𝑔 → (2nd ‘(ℎ‘𝑖)) = (2nd ‘(𝑔‘𝑖)))
178	177	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ (ℎ = 𝑔 → (𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(2nd ‘(𝑔‘𝑖))))
179		fveq1 6102	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = 𝑔 → (ℎ‘(𝑖 + 1)) = (𝑔‘(𝑖 + 1)))
180	179	fveq2d 6107	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = 𝑔 → (1st ‘(ℎ‘(𝑖 + 1))) = (1st ‘(𝑔‘(𝑖 + 1))))
181	180	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ (ℎ = 𝑔 → (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
182	178, 181	eqeq12d 2625	. . . . . . . . . . . . . 14 ⊢ (ℎ = 𝑔 → ((𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
183	182	ralbidv 2969	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑔 → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
184	171, 175, 183	3anbi123d 1391	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑔 → (((𝐹‘(1st ‘(ℎ‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
185	184	rexrab 3337	. . . . . . . . . . 11 ⊢ (∃𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))} (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
186	167, 185	bitri 263	. . . . . . . . . 10 ⊢ (∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
187		oveq2 6557	. . . . . . . . . . . . 13 ⊢ (𝑛 = 1 → (1...𝑛) = (1...1))
188		1z 11284	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℤ
189		fzsn 12254	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℤ → (1...1) = {1})
190	188, 189	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (1...1) = {1}
191	187, 190	syl6eq 2660	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (1...𝑛) = {1})
192	191	oveq2d 6565	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) = ((𝑉 × 𝑉) ↑𝑚 {1}))
193		df-3an 1033	. . . . . . . . . . . . 13 ⊢ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
194		ral0 4028	. . . . . . . . . . . . . . . 16 ⊢ ∀𝑖 ∈ ∅ (𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))
195		oveq1 6556	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 1 → (𝑛 − 1) = (1 − 1))
196		1m1e0 10966	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 − 1) = 0
197	195, 196	syl6eq 2660	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 1 → (𝑛 − 1) = 0)
198	197	oveq2d 6565	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 1 → (1...(𝑛 − 1)) = (1...0))
199		fz10 12233	. . . . . . . . . . . . . . . . . 18 ⊢ (1...0) = ∅
200	198, 199	syl6eq 2660	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 1 → (1...(𝑛 − 1)) = ∅)
201	200	raleqdv 3121	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1 → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ ∅ (𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
202	194, 201	mpbiri 247	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1 → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
203	202	biantrud 527	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
204		fveq2 6103	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 1 → (𝑔‘𝑛) = (𝑔‘1))
205	204	fveq2d 6107	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 1 → (2nd ‘(𝑔‘𝑛)) = (2nd ‘(𝑔‘1)))
206	205	fveq2d 6107	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1 → (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘(2nd ‘(𝑔‘1))))
207	206	eqeq1d 2612	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1 → ((𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ↔ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)))
208	207	anbi2d 736	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌))))
209	203, 208	bitr3d 269	. . . . . . . . . . . . 13 ⊢ (𝑛 = 1 → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌))))
210	193, 209	syl5bb 271	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌))))
211	210	anbi1d 737	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))))
212	192, 211	rexeqbidv 3130	. . . . . . . . . 10 ⊢ (𝑛 = 1 → (∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))))
213	186, 212	syl5bb 271	. . . . . . . . 9 ⊢ (𝑛 = 1 → (∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))))
214	166, 213	syl5bb 271	. . . . . . . 8 ⊢ (𝑛 = 1 → ((𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))))
215	214	rspcev 3282	. . . . . . 7 ⊢ ((1 ∈ ℕ ∧ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))) → ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
216	87, 163, 215	sylancr 694	. . . . . 6 ⊢ (𝜑 → ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
217		eliun 4460	. . . . . 6 ⊢ ((𝑋𝐸𝑌) ∈ ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
218	216, 217	sylibr 223	. . . . 5 ⊢ (𝜑 → (𝑋𝐸𝑌) ∈ ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
219	218, 18	syl6eleqr 2699	. . . 4 ⊢ (𝜑 → (𝑋𝐸𝑌) ∈ 𝑇)
220		infxrlb 12036	. . . 4 ⊢ ((𝑇 ⊆ ℝ* ∧ (𝑋𝐸𝑌) ∈ 𝑇) → inf(𝑇, ℝ*, < ) ≤ (𝑋𝐸𝑌))
221	82, 219, 220	syl2anc 691	. . 3 ⊢ (𝜑 → inf(𝑇, ℝ*, < ) ≤ (𝑋𝐸𝑌))
222	18	eleq2i 2680	. . . . . . 7 ⊢ (𝑝 ∈ 𝑇 ↔ 𝑝 ∈ ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
223		eliun 4460	. . . . . . 7 ⊢ (𝑝 ∈ ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
224	222, 223	bitri 263	. . . . . 6 ⊢ (𝑝 ∈ 𝑇 ↔ ∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
225		vex 3176	. . . . . . . . 9 ⊢ 𝑝 ∈ V
226	75	elrnmpt 5293	. . . . . . . . 9 ⊢ (𝑝 ∈ V → (𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ 𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
227	225, 226	ax-mp 5	. . . . . . . 8 ⊢ (𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ 𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
228	184, 15	elrab2 3333	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∈ 𝑆 ↔ (𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∧ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
229	228	simprbi 479	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 ∈ 𝑆 → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
230	229	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
231	230	simp2d 1067	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌))
232	3	ad2antrr 758	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐹:𝑉–1-1-onto→𝐵)
233		f1of1 6049	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹:𝑉–1-1→𝐵)
234	232, 233	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐹:𝑉–1-1→𝐵)
235		simplr 788	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑛 ∈ ℕ)
236		elfz1end 12242	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (1...𝑛))
237	235, 236	sylib 207	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑛 ∈ (1...𝑛))
238	50, 237	ffvelrnd 6268	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑔‘𝑛) ∈ (𝑉 × 𝑉))
239		xp2nd 7090	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔‘𝑛) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘𝑛)) ∈ 𝑉)
240	238, 239	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (2nd ‘(𝑔‘𝑛)) ∈ 𝑉)
241	13	ad2antrr 758	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑌 ∈ 𝑉)
242		f1fveq 6420	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ ((2nd ‘(𝑔‘𝑛)) ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ((𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ↔ (2nd ‘(𝑔‘𝑛)) = 𝑌))
243	234, 240, 241, 242	syl12anc 1316	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐹‘(2nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ↔ (2nd ‘(𝑔‘𝑛)) = 𝑌))
244	231, 243	mpbid 221	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (2nd ‘(𝑔‘𝑛)) = 𝑌)
245	244	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2nd ‘(𝑔‘𝑛))) = (𝑋𝐸𝑌))
246		eleq1 2676	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 1 → (𝑚 ∈ (1...𝑛) ↔ 1 ∈ (1...𝑛)))
247		fveq2 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 1 → (𝑔‘𝑚) = (𝑔‘1))
248	247	fveq2d 6107	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 1 → (2nd ‘(𝑔‘𝑚)) = (2nd ‘(𝑔‘1)))
249	248	oveq2d 6565	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 1 → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘1))))
250		oveq2 6557	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 1 → (1...𝑚) = (1...1))
251	250, 190	syl6eq 2660	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 1 → (1...𝑚) = {1})
252	251	reseq2d 5317	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 1 → ((𝐸 ∘ 𝑔) ↾ (1...𝑚)) = ((𝐸 ∘ 𝑔) ↾ {1}))
253	252	oveq2d 6565	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 1 → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1})))
254	249, 253	breq12d 4596	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 1 → ((𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1}))))
255	246, 254	imbi12d 333	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 1 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚)))) ↔ (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1})))))
256	255	imbi2d 329	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 1 → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))))) ↔ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1}))))))
257		eleq1 2676	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑥 → (𝑚 ∈ (1...𝑛) ↔ 𝑥 ∈ (1...𝑛)))
258		fveq2 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑥 → (𝑔‘𝑚) = (𝑔‘𝑥))
259	258	fveq2d 6107	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑥 → (2nd ‘(𝑔‘𝑚)) = (2nd ‘(𝑔‘𝑥)))
260	259	oveq2d 6565	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑥 → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘𝑥))))
261		oveq2 6557	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑥 → (1...𝑚) = (1...𝑥))
262	261	reseq2d 5317	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑥 → ((𝐸 ∘ 𝑔) ↾ (1...𝑚)) = ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))
263	262	oveq2d 6565	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑥 → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))))
264	260, 263	breq12d 4596	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑥 → ((𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))))
265	257, 264	imbi12d 333	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑥 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚)))) ↔ (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))))))
266	265	imbi2d 329	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑥 → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))))) ↔ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))))))
267		eleq1 2676	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑥 + 1) → (𝑚 ∈ (1...𝑛) ↔ (𝑥 + 1) ∈ (1...𝑛)))
268		fveq2 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = (𝑥 + 1) → (𝑔‘𝑚) = (𝑔‘(𝑥 + 1)))
269	268	fveq2d 6107	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = (𝑥 + 1) → (2nd ‘(𝑔‘𝑚)) = (2nd ‘(𝑔‘(𝑥 + 1))))
270	269	oveq2d 6565	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = (𝑥 + 1) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))))
271		oveq2 6557	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = (𝑥 + 1) → (1...𝑚) = (1...(𝑥 + 1)))
272	271	reseq2d 5317	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = (𝑥 + 1) → ((𝐸 ∘ 𝑔) ↾ (1...𝑚)) = ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))
273	272	oveq2d 6565	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = (𝑥 + 1) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))))
274	270, 273	breq12d 4596	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑥 + 1) → ((𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))))
275	267, 274	imbi12d 333	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝑥 + 1) → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚)))) ↔ ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))))))
276	275	imbi2d 329	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝑥 + 1) → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))))) ↔ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))))))
277		eleq1 2676	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ (1...𝑛) ↔ 𝑛 ∈ (1...𝑛)))
278		fveq2 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → (𝑔‘𝑚) = (𝑔‘𝑛))
279	278	fveq2d 6107	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → (2nd ‘(𝑔‘𝑚)) = (2nd ‘(𝑔‘𝑛)))
280	279	oveq2d 6565	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘𝑛))))
281		oveq2 6557	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
282	281	reseq2d 5317	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → ((𝐸 ∘ 𝑔) ↾ (1...𝑚)) = ((𝐸 ∘ 𝑔) ↾ (1...𝑛)))
283	282	oveq2d 6565	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))
284	280, 283	breq12d 4596	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → ((𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛)))))
285	277, 284	imbi12d 333	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑛 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚)))) ↔ (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))))
286	285	imbi2d 329	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑛 → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑚))))) ↔ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛)))))))
287	29	ad2antrr 758	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐸 ∈ (∞Met‘𝑉))
288	11	ad2antrr 758	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑋 ∈ 𝑉)
289		nnuz 11599	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℕ = (ℤ≥‘1)
290	235, 289	syl6eleq 2698	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑛 ∈ (ℤ≥‘1))
291		eluzfz1 12219	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (ℤ≥‘1) → 1 ∈ (1...𝑛))
292	290, 291	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 1 ∈ (1...𝑛))
293	50, 292	ffvelrnd 6268	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑔‘1) ∈ (𝑉 × 𝑉))
294		xp2nd 7090	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔‘1) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘1)) ∈ 𝑉)
295	293, 294	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (2nd ‘(𝑔‘1)) ∈ 𝑉)
296		xmetcl 21946	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ (2nd ‘(𝑔‘1)) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔‘1))) ∈ ℝ*)
297	287, 288, 295, 296	syl3anc 1318	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ∈ ℝ*)
298		xrleid 11859	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋𝐸(2nd ‘(𝑔‘1))) ∈ ℝ* → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑋𝐸(2nd ‘(𝑔‘1))))
299	297, 298	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑋𝐸(2nd ‘(𝑔‘1))))
300	142	ad2antrr 758	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑊 ∈ Mnd)
301	87	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 1 ∈ ℕ)
302	44, 293	ffvelrnd 6268	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸‘(𝑔‘1)) ∈ (ℝ* ∖ {-∞}))
303		fveq2 6103	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 1 → (𝑔‘𝑗) = (𝑔‘1))
304	303	fveq2d 6107	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 1 → (𝐸‘(𝑔‘𝑗)) = (𝐸‘(𝑔‘1)))
305	65, 304	gsumsn 18177	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Mnd ∧ 1 ∈ ℕ ∧ (𝐸‘(𝑔‘1)) ∈ (ℝ* ∖ {-∞})) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗)))) = (𝐸‘(𝑔‘1)))
306	300, 301, 302, 305	syl3anc 1318	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗)))) = (𝐸‘(𝑔‘1)))
307	287, 30	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
308		fcompt 6306	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐸:(𝑉 × 𝑉)⟶ℝ* ∧ 𝑔:(1...𝑛)⟶(𝑉 × 𝑉)) → (𝐸 ∘ 𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))))
309	307, 50, 308	syl2anc 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸 ∘ 𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))))
310	309	reseq1d 5316	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐸 ∘ 𝑔) ↾ {1}) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ {1}))
311	292	snssd 4281	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → {1} ⊆ (1...𝑛))
312	311	resmptd 5371	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ {1}) = (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗))))
313	310, 312	eqtrd 2644	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐸 ∘ 𝑔) ↾ {1}) = (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗))))
314	313	oveq2d 6565	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1})) = (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗)))))
315		df-ov 6552	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋𝐸(2nd ‘(𝑔‘1))) = (𝐸‘⟨𝑋, (2nd ‘(𝑔‘1))⟩)
316		1st2nd2 7096	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔‘1) ∈ (𝑉 × 𝑉) → (𝑔‘1) = ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩)
317	293, 316	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑔‘1) = ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩)
318	230	simp1d 1066	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋))
319		xp1st 7089	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔‘1) ∈ (𝑉 × 𝑉) → (1st ‘(𝑔‘1)) ∈ 𝑉)
320	293, 319	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1st ‘(𝑔‘1)) ∈ 𝑉)
321		f1fveq 6420	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ ((1st ‘(𝑔‘1)) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ↔ (1st ‘(𝑔‘1)) = 𝑋))
322	234, 320, 288, 321	syl12anc 1316	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘𝑋) ↔ (1st ‘(𝑔‘1)) = 𝑋))
323	318, 322	mpbid 221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1st ‘(𝑔‘1)) = 𝑋)
324	323	opeq1d 4346	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩ = ⟨𝑋, (2nd ‘(𝑔‘1))⟩)
325	317, 324	eqtr2d 2645	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ⟨𝑋, (2nd ‘(𝑔‘1))⟩ = (𝑔‘1))
326	325	fveq2d 6107	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸‘⟨𝑋, (2nd ‘(𝑔‘1))⟩) = (𝐸‘(𝑔‘1)))
327	315, 326	syl5eq 2656	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) = (𝐸‘(𝑔‘1)))
328	306, 314, 327	3eqtr4d 2654	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1})) = (𝑋𝐸(2nd ‘(𝑔‘1))))
329	299, 328	breqtrrd 4611	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1})))
330	329	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ {1}))))
331		simprl 790	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ ℕ)
332	331, 289	syl6eleq 2698	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (ℤ≥‘1))
333		simprr 792	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑥 + 1) ∈ (1...𝑛))
334		peano2fzr 12225	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (ℤ≥‘1) ∧ (𝑥 + 1) ∈ (1...𝑛)) → 𝑥 ∈ (1...𝑛))
335	332, 333, 334	syl2anc 691	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (1...𝑛))
336	335	expr 641	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 + 1) ∈ (1...𝑛) → 𝑥 ∈ (1...𝑛)))
337	336	imim1d 80	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))))))
338	287	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸 ∈ (∞Met‘𝑉))
339	288	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑋 ∈ 𝑉)
340	50	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
341	340, 335	ffvelrnd 6268	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘𝑥) ∈ (𝑉 × 𝑉))
342		xp2nd 7090	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔‘𝑥) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘𝑥)) ∈ 𝑉)
343	341, 342	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔‘𝑥)) ∈ 𝑉)
344		xmetcl 21946	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ (2nd ‘(𝑔‘𝑥)) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ∈ ℝ*)
345	338, 339, 343, 344	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ∈ ℝ*)
346	67	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑊 ∈ CMnd)
347		fzfid 12634	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...𝑥) ∈ Fin)
348	52	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸 ∘ 𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
349		fzsuc 12258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 ∈ (ℤ≥‘1) → (1...(𝑥 + 1)) = ((1...𝑥) ∪ {(𝑥 + 1)}))
350	332, 349	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...(𝑥 + 1)) = ((1...𝑥) ∪ {(𝑥 + 1)}))
351		elfzuz3 12210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 + 1) ∈ (1...𝑛) → 𝑛 ∈ (ℤ≥‘(𝑥 + 1)))
352	351	ad2antll 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑛 ∈ (ℤ≥‘(𝑥 + 1)))
353		fzss2 12252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 ∈ (ℤ≥‘(𝑥 + 1)) → (1...(𝑥 + 1)) ⊆ (1...𝑛))
354	352, 353	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...(𝑥 + 1)) ⊆ (1...𝑛))
355	350, 354	eqsstr3d 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((1...𝑥) ∪ {(𝑥 + 1)}) ⊆ (1...𝑛))
356	355	unssad 3752	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...𝑥) ⊆ (1...𝑛))
357	348, 356	fssresd 5984	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...𝑥)):(1...𝑥)⟶(ℝ* ∖ {-∞}))
358	69	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 0 ∈ V)
359	357, 347, 358	fdmfifsupp 8168	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...𝑥)) finSupp 0)
360	65, 66, 346, 347, 357, 359	gsumcl 18139	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) ∈ (ℝ* ∖ {-∞}))
361	360	eldifad 3552	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) ∈ ℝ*)
362	338, 30	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
363	340, 333	ffvelrnd 6268	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉))
364	362, 363	ffvelrnd 6268	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*)
365		xleadd1a 11955	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ∈ ℝ* ∧ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) ∈ ℝ* ∧ (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*) ∧ (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
366	365	ex 449	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ∈ ℝ* ∧ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) ∈ ℝ* ∧ (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
367	345, 361, 364, 366	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
368		xp2nd 7090	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
369	363, 368	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
370		xmettri 21966	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑋 ∈ 𝑉 ∧ (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉 ∧ (2nd ‘(𝑔‘𝑥)) ∈ 𝑉)) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 ((2nd ‘(𝑔‘𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
371	338, 339, 369, 343, 370	syl13anc 1320	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 ((2nd ‘(𝑔‘𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
372		1st2nd2 7096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (𝑔‘(𝑥 + 1)) = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
373	363, 372	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
374		nnz 11276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℤ)
375	374	ad2antrl 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ ℤ)
376		eluzp1m1 11587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ (ℤ≥‘(𝑥 + 1))) → (𝑛 − 1) ∈ (ℤ≥‘𝑥))
377	375, 352, 376	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑛 − 1) ∈ (ℤ≥‘𝑥))
378		elfzuzb 12207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 ∈ (1...(𝑛 − 1)) ↔ (𝑥 ∈ (ℤ≥‘1) ∧ (𝑛 − 1) ∈ (ℤ≥‘𝑥)))
379	332, 377, 378	sylanbrc 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (1...(𝑛 − 1)))
380	230	simp3d 1068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
381	380	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
382		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑖 = 𝑥 → (𝑔‘𝑖) = (𝑔‘𝑥))
383	382	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑖 = 𝑥 → (2nd ‘(𝑔‘𝑖)) = (2nd ‘(𝑔‘𝑥)))
384	383	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 = 𝑥 → (𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(2nd ‘(𝑔‘𝑥))))
385		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑖 = 𝑥 → (𝑖 + 1) = (𝑥 + 1))
386	385	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑖 = 𝑥 → (𝑔‘(𝑖 + 1)) = (𝑔‘(𝑥 + 1)))
387	386	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑖 = 𝑥 → (1st ‘(𝑔‘(𝑖 + 1))) = (1st ‘(𝑔‘(𝑥 + 1))))
388	387	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 = 𝑥 → (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))))
389	384, 388	eqeq12d 2625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 = 𝑥 → ((𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(𝑔‘𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1))))))
390	389	rspcv 3278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ (1...(𝑛 − 1)) → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔‘𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) → (𝐹‘(2nd ‘(𝑔‘𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1))))))
391	379, 381, 390	sylc 63	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐹‘(2nd ‘(𝑔‘𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))))
392	234	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐹:𝑉–1-1→𝐵)
393		xp1st 7089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
394	363, 393	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
395		f1fveq 6420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ ((2nd ‘(𝑔‘𝑥)) ∈ 𝑉 ∧ (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)) → ((𝐹‘(2nd ‘(𝑔‘𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))) ↔ (2nd ‘(𝑔‘𝑥)) = (1st ‘(𝑔‘(𝑥 + 1)))))
396	392, 343, 394, 395	syl12anc 1316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐹‘(2nd ‘(𝑔‘𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))) ↔ (2nd ‘(𝑔‘𝑥)) = (1st ‘(𝑔‘(𝑥 + 1)))))
397	391, 396	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔‘𝑥)) = (1st ‘(𝑔‘(𝑥 + 1))))
398	397	opeq1d 4346	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ⟨(2nd ‘(𝑔‘𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩ = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
399	373, 398	eqtr4d 2647	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) = ⟨(2nd ‘(𝑔‘𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
400	399	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) = (𝐸‘⟨(2nd ‘(𝑔‘𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩))
401		df-ov 6552	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((2nd ‘(𝑔‘𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) = (𝐸‘⟨(2nd ‘(𝑔‘𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
402	400, 401	syl6eqr 2662	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) = ((2nd ‘(𝑔‘𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1)))))
403	402	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) = ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 ((2nd ‘(𝑔‘𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
404	371, 403	breqtrrd 4611	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
405		xmetcl 21946	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
406	338, 339, 369, 405	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
407	345, 364	xaddcld 12003	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
408	361, 364	xaddcld 12003	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
409		xrletr 11865	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ* ∧ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ* ∧ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*) → (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∧ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
410	406, 407, 408, 409	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∧ ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
411	404, 410	mpand 707	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (((𝑋𝐸(2nd ‘(𝑔‘𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
412	367, 411	syld 46	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
413		xrex 11705	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ℝ* ∈ V
414	413, 27	ssexi 4731	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℝ* ∖ {-∞}) ∈ V
415	23, 22	ressplusg 15818	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℝ* ∖ {-∞}) ∈ V → +𝑒 = (+g‘𝑊))
416	414, 415	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ +𝑒 = (+g‘𝑊)
417	44	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
418		fzelp1 12263	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ (1...𝑥) → 𝑗 ∈ (1...(𝑥 + 1)))
419	50	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
420	354	sselda 3568	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → 𝑗 ∈ (1...𝑛))
421	419, 420	ffvelrnd 6268	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → (𝑔‘𝑗) ∈ (𝑉 × 𝑉))
422	418, 421	sylan2 490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → (𝑔‘𝑗) ∈ (𝑉 × 𝑉))
423	417, 422	ffvelrnd 6268	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → (𝐸‘(𝑔‘𝑗)) ∈ (ℝ* ∖ {-∞}))
424		fzp1disj 12269	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((1...𝑥) ∩ {(𝑥 + 1)}) = ∅
425	424	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((1...𝑥) ∩ {(𝑥 + 1)}) = ∅)
426		disjsn 4192	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1...𝑥) ∩ {(𝑥 + 1)}) = ∅ ↔ ¬ (𝑥 + 1) ∈ (1...𝑥))
427	425, 426	sylib 207	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ¬ (𝑥 + 1) ∈ (1...𝑥))
428	44	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
429	428, 363	ffvelrnd 6268	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) ∈ (ℝ* ∖ {-∞}))
430		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = (𝑥 + 1) → (𝑔‘𝑗) = (𝑔‘(𝑥 + 1)))
431	430	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = (𝑥 + 1) → (𝐸‘(𝑔‘𝑗)) = (𝐸‘(𝑔‘(𝑥 + 1))))
432	65, 416, 346, 347, 423, 333, 427, 429, 431	gsumunsn 18182	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔‘𝑗)))) = ((𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗)))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
433	309	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸 ∘ 𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))))
434	433, 350	reseq12d 5318	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ ((1...𝑥) ∪ {(𝑥 + 1)})))
435	355	resmptd 5371	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ ((1...𝑥) ∪ {(𝑥 + 1)})) = (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔‘𝑗))))
436	434, 435	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))) = (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔‘𝑗))))
437	436	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))) = (𝑊 Σg (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔‘𝑗)))))
438	433	reseq1d 5316	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...𝑥)) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ (1...𝑥)))
439	356	resmptd 5371	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ (1...𝑥)) = (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗))))
440	438, 439	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...𝑥)) = (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗))))
441	440	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) = (𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗)))))
442	441	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) = ((𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗)))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
443	432, 437, 442	3eqtr4d 2654	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))) = ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
444	443	breq2d 4595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))) ↔ (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
445	412, 444	sylibrd 248	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))))
446	445	expr 641	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 + 1) ∈ (1...𝑛) → ((𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))))))
447	446	a2d 29	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ 𝑥 ∈ ℕ) → (((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))))))
448	337, 447	syld 46	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))))))
449	448	expcom 450	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℕ → (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))))))
450	449	a2d 29	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℕ → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑥))))) → (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))))))
451	256, 266, 276, 286, 330, 450	nnind 10915	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))))
452	235, 451	mpcom 37	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛)))))
453	237, 452	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))
454	245, 453	eqbrtrrd 4607	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸𝑌) ≤ (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))
455		ffn 5958	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∘ 𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}) → (𝐸 ∘ 𝑔) Fn (1...𝑛))
456		fnresdm 5914	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∘ 𝑔) Fn (1...𝑛) → ((𝐸 ∘ 𝑔) ↾ (1...𝑛)) = (𝐸 ∘ 𝑔))
457	52, 455, 456	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐸 ∘ 𝑔) ↾ (1...𝑛)) = (𝐸 ∘ 𝑔))
458	457	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))) = (𝑊 Σg (𝐸 ∘ 𝑔)))
459	63, 458	eqtr4d 2647	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) = (𝑊 Σg ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))
460	454, 459	breqtrrd 4611	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸𝑌) ≤ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
461		breq2 4587	. . . . . . . . . 10 ⊢ (𝑝 = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) → ((𝑋𝐸𝑌) ≤ 𝑝 ↔ (𝑋𝐸𝑌) ≤ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
462	460, 461	syl5ibrcom 236	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑝 = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) → (𝑋𝐸𝑌) ≤ 𝑝))
463	462	rexlimdva 3013	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∃𝑔 ∈ 𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)) → (𝑋𝐸𝑌) ≤ 𝑝))
464	227, 463	syl5bi 231	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) → (𝑋𝐸𝑌) ≤ 𝑝))
465	464	rexlimdva 3013	. . . . . 6 ⊢ (𝜑 → (∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) → (𝑋𝐸𝑌) ≤ 𝑝))
466	224, 465	syl5bi 231	. . . . 5 ⊢ (𝜑 → (𝑝 ∈ 𝑇 → (𝑋𝐸𝑌) ≤ 𝑝))
467	466	ralrimiv 2948	. . . 4 ⊢ (𝜑 → ∀𝑝 ∈ 𝑇 (𝑋𝐸𝑌) ≤ 𝑝)
468		infxrgelb 12037	. . . . 5 ⊢ ((𝑇 ⊆ ℝ* ∧ (𝑋𝐸𝑌) ∈ ℝ*) → ((𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ) ↔ ∀𝑝 ∈ 𝑇 (𝑋𝐸𝑌) ≤ 𝑝))
469	82, 86, 468	syl2anc 691	. . . 4 ⊢ (𝜑 → ((𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ) ↔ ∀𝑝 ∈ 𝑇 (𝑋𝐸𝑌) ≤ 𝑝))
470	467, 469	mpbird 246	. . 3 ⊢ (𝜑 → (𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ))
471	84, 86, 221, 470	xrletrid 11862	. 2 ⊢ (𝜑 → inf(𝑇, ℝ*, < ) = (𝑋𝐸𝑌))
472	20, 471	eqtrd 2644	1 ⊢ (𝜑 → ((𝐹‘𝑋)𝐷(𝐹‘𝑌)) = (𝑋𝐸𝑌))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  {csn 4125  ⟨cop 4131  ∪ ciun 4455   class class class wbr 4583   ↦ cmpt 4643   × cxp 5036  ran crn 5039   ↾ cres 5040   ∘ ccom 5042   Fn wfn 5799  ⟶wf 5800  –1-1→wf1 5801  –onto→wfo 5802  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549  1^st c1st 7057  2^nd c2nd 7058   ↑_𝑚 cmap 7744  Fincfn 7841  infcinf 8230  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818  -∞cmnf 9951  ℝ^*cxr 9952   < clt 9953   ≤ cle 9954   − cmin 10145  ℕcn 10897  ℤcz 11254  ℤ_≥cuz 11563   +_𝑒 cxad 11820  ...cfz 12197  Basecbs 15695   ↾_s cress 15696  +_gcplusg 15768  distcds 15777   Σ_g cgsu 15924  ℝ^*_𝑠cxrs 15983   “_s cimas 15987  Mndcmnd 17117  CMndccmn 18016  ∞Metcxmt 19552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-fz 12198  df-fzo 12335  df-seq 12664  df-hash 12980  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-0g 15925  df-gsum 15926  df-xrs 15985  df-imas 15991  df-mre 16069  df-mrc 16070  df-acs 16072  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-mulg 17364  df-cntz 17573  df-cmn 18018  df-xmet 19560

This theorem is referenced by:  imasdsf1o  21989