imasdsf1olem - Metamath Proof Explorer

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

Theorem imasdsf1olem 23871

Description: Lemma for imasdsf1o 23872. (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...𝑛)) ∣ ((𝐹‘(1^st ‘(ℎ‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(ℎ‘𝑖))) = (𝐹‘(1^st ‘(ℎ‘(𝑖 + 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 6838	. . . . 5 ⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹:𝑉–onto→𝐵)
5	3, 4	syl 17	. . . 4 ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
6		imasdsf1o.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑍)
7		eqid 2733	. . . 4 ⊢ (dist‘𝑅) = (dist‘𝑅)
8		imasdsf1o.d	. . . 4 ⊢ 𝐷 = (dist‘𝑈)
9		f1of 6831	. . . . . 6 ⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹:𝑉⟶𝐵)
10	3, 9	syl 17	. . . . 5 ⊢ (𝜑 → 𝐹:𝑉⟶𝐵)
11		imasdsf1o.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
12	10, 11	ffvelcdmd 7085	. . . 4 ⊢ (𝜑 → (𝐹‘𝑋) ∈ 𝐵)
13		imasdsf1o.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
14	10, 13	ffvelcdmd 7085	. . . 4 ⊢ (𝜑 → (𝐹‘𝑌) ∈ 𝐵)
15		imasdsf1o.s	. . . 4 ⊢ 𝑆 = {ℎ ∈ ((𝑉 × 𝑉) ↑_m (1...𝑛)) ∣ ((𝐹‘(1^st ‘(ℎ‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(ℎ‘𝑖))) = (𝐹‘(1^st ‘(ℎ‘(𝑖 + 1)))))}
16		imasdsf1o.e	. . . 4 ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))
17	1, 2, 5, 6, 7, 8, 12, 14, 15, 16	imasdsval2 17459	. . 3 ⊢ (𝜑 → ((𝐹‘𝑋)𝐷(𝐹‘𝑌)) = inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))), ℝ^, < ))
18		imasdsf1o.t	. . . 4 ⊢ 𝑇 = ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ^*_𝑠 Σ_g (𝐸 ∘ 𝑔)))
19	18	infeq1i 9470	. . 3 ⊢ inf(𝑇, ℝ^, < ) = inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))), ℝ^*, < )
20	17, 19	eqtr4di 2791	. 2 ⊢ (𝜑 → ((𝐹‘𝑋)𝐷(𝐹‘𝑌)) = inf(𝑇, ℝ^*, < ))
21		xrsbas 20954	. . . . . . . . . . . 12 ⊢ ℝ^* = (Base‘ℝ^*_𝑠)
22		xrsadd 20955	. . . . . . . . . . . 12 ⊢ +_𝑒 = (+_g‘ℝ^*_𝑠)
23		imasdsf1o.w	. . . . . . . . . . . 12 ⊢ 𝑊 = (ℝ^_𝑠 ↾_s (ℝ^ ∖ {-∞}))
24		xrsex 20953	. . . . . . . . . . . . 13 ⊢ ℝ^*_𝑠 ∈ V
25	24	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ℝ^*_𝑠 ∈ V)
26		fzfid 13935	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1...𝑛) ∈ Fin)
27		difss 4131	. . . . . . . . . . . . 13 ⊢ (ℝ^* ∖ {-∞}) ⊆ ℝ^*
28	27	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ^* ∖ {-∞}) ⊆ ℝ^*)
29		imasdsf1o.m	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸 ∈ (∞Met‘𝑉))
30		xmetf 23827	. . . . . . . . . . . . . . . 16 ⊢ (𝐸 ∈ (∞Met‘𝑉) → 𝐸:(𝑉 × 𝑉)⟶ℝ^*)
31		ffn 6715	. . . . . . . . . . . . . . . 16 ⊢ (𝐸:(𝑉 × 𝑉)⟶ℝ^* → 𝐸 Fn (𝑉 × 𝑉))
32	29, 30, 31	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐸 Fn (𝑉 × 𝑉))
33		xmetcl 23829	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉) → (𝑓𝐸𝑔) ∈ ℝ^*)
34		xmetge0 23842	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉) → 0 ≤ (𝑓𝐸𝑔))
35		ge0nemnf 13149	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓𝐸𝑔) ∈ ℝ^* ∧ 0 ≤ (𝑓𝐸𝑔)) → (𝑓𝐸𝑔) ≠ -∞)
36	33, 34, 35	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉) → (𝑓𝐸𝑔) ≠ -∞)
37		eldifsn 4790	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓𝐸𝑔) ∈ (ℝ^* ∖ {-∞}) ↔ ((𝑓𝐸𝑔) ∈ ℝ^* ∧ (𝑓𝐸𝑔) ≠ -∞))
38	33, 36, 37	sylanbrc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉) → (𝑓𝐸𝑔) ∈ (ℝ^* ∖ {-∞}))
39	38	3expb 1121	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉)) → (𝑓𝐸𝑔) ∈ (ℝ^* ∖ {-∞}))
40	29, 39	sylan 581	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉)) → (𝑓𝐸𝑔) ∈ (ℝ^* ∖ {-∞}))
41	40	ralrimivva 3201	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑓 ∈ 𝑉 ∀𝑔 ∈ 𝑉 (𝑓𝐸𝑔) ∈ (ℝ^* ∖ {-∞}))
42		ffnov 7532	. . . . . . . . . . . . . . 15 ⊢ (𝐸:(𝑉 × 𝑉)⟶(ℝ^* ∖ {-∞}) ↔ (𝐸 Fn (𝑉 × 𝑉) ∧ ∀𝑓 ∈ 𝑉 ∀𝑔 ∈ 𝑉 (𝑓𝐸𝑔) ∈ (ℝ^* ∖ {-∞})))
43	32, 41, 42	sylanbrc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸:(𝑉 × 𝑉)⟶(ℝ^* ∖ {-∞}))
44	43	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐸:(𝑉 × 𝑉)⟶(ℝ^* ∖ {-∞}))
45	15	ssrab3 4080	. . . . . . . . . . . . . . . 16 ⊢ 𝑆 ⊆ ((𝑉 × 𝑉) ↑_m (1...𝑛))
46	45	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑆 ⊆ ((𝑉 × 𝑉) ↑_m (1...𝑛)))
47	46	sselda 3982	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑔 ∈ ((𝑉 × 𝑉) ↑_m (1...𝑛)))
48		elmapi 8840	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ ((𝑉 × 𝑉) ↑_m (1...𝑛)) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
49	47, 48	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
50		fco 6739	. . . . . . . . . . . . 13 ⊢ ((𝐸:(𝑉 × 𝑉)⟶(ℝ^* ∖ {-∞}) ∧ 𝑔:(1...𝑛)⟶(𝑉 × 𝑉)) → (𝐸 ∘ 𝑔):(1...𝑛)⟶(ℝ^* ∖ {-∞}))
51	44, 49, 50	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸 ∘ 𝑔):(1...𝑛)⟶(ℝ^* ∖ {-∞}))
52		0re 11213	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
53		rexr 11257	. . . . . . . . . . . . . 14 ⊢ (0 ∈ ℝ → 0 ∈ ℝ^*)
54		renemnf 11260	. . . . . . . . . . . . . 14 ⊢ (0 ∈ ℝ → 0 ≠ -∞)
55		eldifsn 4790	. . . . . . . . . . . . . 14 ⊢ (0 ∈ (ℝ^* ∖ {-∞}) ↔ (0 ∈ ℝ^* ∧ 0 ≠ -∞))
56	53, 54, 55	sylanbrc 584	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℝ → 0 ∈ (ℝ^* ∖ {-∞}))
57	52, 56	mp1i 13	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 0 ∈ (ℝ^* ∖ {-∞}))
58		xaddlid 13218	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ^* → (0 +_𝑒 𝑥) = 𝑥)
59		xaddrid 13217	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ^* → (𝑥 +_𝑒 0) = 𝑥)
60	58, 59	jca 513	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ^* → ((0 +_𝑒 𝑥) = 𝑥 ∧ (𝑥 +_𝑒 0) = 𝑥))
61	60	adantl 483	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ 𝑥 ∈ ℝ^*) → ((0 +_𝑒 𝑥) = 𝑥 ∧ (𝑥 +_𝑒 0) = 𝑥))
62	21, 22, 23, 25, 26, 28, 51, 57, 61	gsumress 18598	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ^*_𝑠 Σ_g (𝐸 ∘ 𝑔)) = (𝑊 Σ_g (𝐸 ∘ 𝑔)))
63	23, 21	ressbas2 17179	. . . . . . . . . . . . 13 ⊢ ((ℝ^* ∖ {-∞}) ⊆ ℝ^* → (ℝ^* ∖ {-∞}) = (Base‘𝑊))
64	27, 63	ax-mp 5	. . . . . . . . . . . 12 ⊢ (ℝ^* ∖ {-∞}) = (Base‘𝑊)
65	23	xrs10 20977	. . . . . . . . . . . 12 ⊢ 0 = (0_g‘𝑊)
66	23	xrs1cmn 20978	. . . . . . . . . . . . 13 ⊢ 𝑊 ∈ CMnd
67	66	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑊 ∈ CMnd)
68		c0ex 11205	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
69	68	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 0 ∈ V)
70	51, 26, 69	fdmfifsupp 9370	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸 ∘ 𝑔) finSupp 0)
71	64, 65, 67, 26, 51, 70	gsumcl 19778	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σ_g (𝐸 ∘ 𝑔)) ∈ (ℝ^* ∖ {-∞}))
72	62, 71	eqeltrd 2834	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔)) ∈ (ℝ^ ∖ {-∞}))
73	72	eldifad 3960	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔)) ∈ ℝ^)
74	73	fmpttd 7112	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑔 ∈ 𝑆 ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))):𝑆⟶ℝ^)
75	74	frnd 6723	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝑔 ∈ 𝑆 ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))) ⊆ ℝ^)
76	75	ralrimiva 3147	. . . . . 6 ⊢ (𝜑 → ∀𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))) ⊆ ℝ^)
77		iunss 5048	. . . . . 6 ⊢ (∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))) ⊆ ℝ^ ↔ ∀𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))) ⊆ ℝ^)
78	76, 77	sylibr 233	. . . . 5 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))) ⊆ ℝ^)
79	18, 78	eqsstrid 4030	. . . 4 ⊢ (𝜑 → 𝑇 ⊆ ℝ^*)
80		infxrcl 13309	. . . 4 ⊢ (𝑇 ⊆ ℝ^* → inf(𝑇, ℝ^, < ) ∈ ℝ^)
81	79, 80	syl 17	. . 3 ⊢ (𝜑 → inf(𝑇, ℝ^, < ) ∈ ℝ^)
82		xmetcl 23829	. . . 4 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋𝐸𝑌) ∈ ℝ^*)
83	29, 11, 13, 82	syl3anc 1372	. . 3 ⊢ (𝜑 → (𝑋𝐸𝑌) ∈ ℝ^*)
84		1nn 12220	. . . . . . 7 ⊢ 1 ∈ ℕ
85		1ex 11207	. . . . . . . . . . . 12 ⊢ 1 ∈ V
86		opex 5464	. . . . . . . . . . . 12 ⊢ ⟨𝑋, 𝑌⟩ ∈ V
87	85, 86	f1osn 6871	. . . . . . . . . . 11 ⊢ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}–1-1-onto→{⟨𝑋, 𝑌⟩}
88		f1of 6831	. . . . . . . . . . 11 ⊢ ({⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}–1-1-onto→{⟨𝑋, 𝑌⟩} → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩})
89	87, 88	ax-mp 5	. . . . . . . . . 10 ⊢ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩}
90	11, 13	opelxpd 5714	. . . . . . . . . . 11 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉))
91	90	snssd 4812	. . . . . . . . . 10 ⊢ (𝜑 → {⟨𝑋, 𝑌⟩} ⊆ (𝑉 × 𝑉))
92		fss 6732	. . . . . . . . . 10 ⊢ (({⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩} ∧ {⟨𝑋, 𝑌⟩} ⊆ (𝑉 × 𝑉)) → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉))
93	89, 91, 92	sylancr 588	. . . . . . . . 9 ⊢ (𝜑 → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉))
94	29	elfvexd 6928	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ∈ V)
95	94, 94	xpexd 7735	. . . . . . . . . 10 ⊢ (𝜑 → (𝑉 × 𝑉) ∈ V)
96		snex 5431	. . . . . . . . . 10 ⊢ {1} ∈ V
97		elmapg 8830	. . . . . . . . . 10 ⊢ (((𝑉 × 𝑉) ∈ V ∧ {1} ∈ V) → ({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑_m {1}) ↔ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉)))
98	95, 96, 97	sylancl 587	. . . . . . . . 9 ⊢ (𝜑 → ({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑_m {1}) ↔ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉)))
99	93, 98	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → {⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑_m {1}))
100		op1stg 7984	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (1^st ‘⟨𝑋, 𝑌⟩) = 𝑋)
101	11, 13, 100	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘⟨𝑋, 𝑌⟩) = 𝑋)
102	101	fveq2d 6893	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(1^st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋))
103		op2ndg 7985	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (2^nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
104	11, 13, 103	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → (2^nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
105	104	fveq2d 6893	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌))
106	102, 105	jca 513	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌)))
107	24	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ^*_𝑠 ∈ V)
108		snfi 9041	. . . . . . . . . . 11 ⊢ {1} ∈ Fin
109	108	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → {1} ∈ Fin)
110	27	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ^* ∖ {-∞}) ⊆ ℝ^*)
111		xmetge0 23842	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → 0 ≤ (𝑋𝐸𝑌))
112	29, 11, 13, 111	syl3anc 1372	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ≤ (𝑋𝐸𝑌))
113		ge0nemnf 13149	. . . . . . . . . . . . . 14 ⊢ (((𝑋𝐸𝑌) ∈ ℝ^* ∧ 0 ≤ (𝑋𝐸𝑌)) → (𝑋𝐸𝑌) ≠ -∞)
114	83, 112, 113	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋𝐸𝑌) ≠ -∞)
115		eldifsn 4790	. . . . . . . . . . . . 13 ⊢ ((𝑋𝐸𝑌) ∈ (ℝ^* ∖ {-∞}) ↔ ((𝑋𝐸𝑌) ∈ ℝ^* ∧ (𝑋𝐸𝑌) ≠ -∞))
116	83, 114, 115	sylanbrc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋𝐸𝑌) ∈ (ℝ^* ∖ {-∞}))
117		fconst6g 6778	. . . . . . . . . . . 12 ⊢ ((𝑋𝐸𝑌) ∈ (ℝ^* ∖ {-∞}) → ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ^* ∖ {-∞}))
118	116, 117	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ^* ∖ {-∞}))
119		fcoconst 7129	. . . . . . . . . . . . . 14 ⊢ ((𝐸 Fn (𝑉 × 𝑉) ∧ ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉)) → (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}))
120	32, 90, 119	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}))
121	85, 86	xpsn 7136	. . . . . . . . . . . . . 14 ⊢ ({1} × {⟨𝑋, 𝑌⟩}) = {⟨1, ⟨𝑋, 𝑌⟩⟩}
122	121	coeq2i 5859	. . . . . . . . . . . . 13 ⊢ (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})
123		df-ov 7409	. . . . . . . . . . . . . . . 16 ⊢ (𝑋𝐸𝑌) = (𝐸‘⟨𝑋, 𝑌⟩)
124	123	eqcomi 2742	. . . . . . . . . . . . . . 15 ⊢ (𝐸‘⟨𝑋, 𝑌⟩) = (𝑋𝐸𝑌)
125	124	sneqi 4639	. . . . . . . . . . . . . 14 ⊢ {(𝐸‘⟨𝑋, 𝑌⟩)} = {(𝑋𝐸𝑌)}
126	125	xpeq2i 5703	. . . . . . . . . . . . 13 ⊢ ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}) = ({1} × {(𝑋𝐸𝑌)})
127	120, 122, 126	3eqtr3g 2796	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}) = ({1} × {(𝑋𝐸𝑌)}))
128	127	feq1d 6700	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}):{1}⟶(ℝ^* ∖ {-∞}) ↔ ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ^* ∖ {-∞})))
129	118, 128	mpbird 257	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}):{1}⟶(ℝ^* ∖ {-∞}))
130	52, 56	mp1i 13	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ (ℝ^* ∖ {-∞}))
131	60	adantl 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ^*) → ((0 +_𝑒 𝑥) = 𝑥 ∧ (𝑥 +_𝑒 0) = 𝑥))
132	21, 22, 23, 107, 109, 110, 129, 130, 131	gsumress 18598	. . . . . . . . 9 ⊢ (𝜑 → (ℝ^*_𝑠 Σ_g (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})) = (𝑊 Σ_g (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
133		fconstmpt 5737	. . . . . . . . . . 11 ⊢ ({1} × {(𝑋𝐸𝑌)}) = (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))
134	127, 133	eqtrdi 2789	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}) = (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌)))
135	134	oveq2d 7422	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 Σ_g (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})) = (𝑊 Σ_g (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))))
136		cmnmnd 19660	. . . . . . . . . . 11 ⊢ (𝑊 ∈ CMnd → 𝑊 ∈ Mnd)
137	66, 136	mp1i 13	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ Mnd)
138	84	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℕ)
139		eqidd 2734	. . . . . . . . . . 11 ⊢ (𝑗 = 1 → (𝑋𝐸𝑌) = (𝑋𝐸𝑌))
140	64, 139	gsumsn 19817	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Mnd ∧ 1 ∈ ℕ ∧ (𝑋𝐸𝑌) ∈ (ℝ^* ∖ {-∞})) → (𝑊 Σ_g (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))) = (𝑋𝐸𝑌))
141	137, 138, 116, 140	syl3anc 1372	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 Σ_g (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))) = (𝑋𝐸𝑌))
142	132, 135, 141	3eqtrrd 2778	. . . . . . . 8 ⊢ (𝜑 → (𝑋𝐸𝑌) = (ℝ^*_𝑠 Σ_g (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
143		fveq1 6888	. . . . . . . . . . . . . 14 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝑔‘1) = ({⟨1, ⟨𝑋, 𝑌⟩⟩}‘1))
144	85, 86	fvsn 7176	. . . . . . . . . . . . . 14 ⊢ ({⟨1, ⟨𝑋, 𝑌⟩⟩}‘1) = ⟨𝑋, 𝑌⟩
145	143, 144	eqtrdi 2789	. . . . . . . . . . . . 13 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝑔‘1) = ⟨𝑋, 𝑌⟩)
146	145	fveq2d 6893	. . . . . . . . . . . 12 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (1^st ‘(𝑔‘1)) = (1^st ‘⟨𝑋, 𝑌⟩))
147	146	fveqeq2d 6897	. . . . . . . . . . 11 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ↔ (𝐹‘(1^st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋)))
148	145	fveq2d 6893	. . . . . . . . . . . 12 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (2^nd ‘(𝑔‘1)) = (2^nd ‘⟨𝑋, 𝑌⟩))
149	148	fveqeq2d 6897	. . . . . . . . . . 11 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝐹‘(2^nd ‘(𝑔‘1))) = (𝐹‘𝑌) ↔ (𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌)))
150	147, 149	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ↔ ((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌))))
151		coeq2 5857	. . . . . . . . . . . 12 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝐸 ∘ 𝑔) = (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}))
152	151	oveq2d 7422	. . . . . . . . . . 11 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔)) = (ℝ^_𝑠 Σ_g (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
153	152	eqeq2d 2744	. . . . . . . . . 10 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝑋𝐸𝑌) = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔)) ↔ (𝑋𝐸𝑌) = (ℝ^_𝑠 Σ_g (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}))))
154	150, 153	anbi12d 632	. . . . . . . . 9 ⊢ (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))) ↔ (((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ^_𝑠 Σ_g (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))))
155	154	rspcev 3613	. . . . . . . 8 ⊢ (({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑_m {1}) ∧ (((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ^_𝑠 Σ_g (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))) → ∃𝑔 ∈ ((𝑉 × 𝑉) ↑_m {1})(((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))))
156	99, 106, 142, 155	syl12anc 836	. . . . . . 7 ⊢ (𝜑 → ∃𝑔 ∈ ((𝑉 × 𝑉) ↑_m {1})(((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ^*_𝑠 Σ_g (𝐸 ∘ 𝑔))))
157		ovex 7439	. . . . . . . . . 10 ⊢ (𝑋𝐸𝑌) ∈ V
158		eqid 2733	. . . . . . . . . . 11 ⊢ (𝑔 ∈ 𝑆 ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))) = (𝑔 ∈ 𝑆 ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔)))
159	158	elrnmpt 5954	. . . . . . . . . 10 ⊢ ((𝑋𝐸𝑌) ∈ V → ((𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))))
160	157, 159	ax-mp 5	. . . . . . . . 9 ⊢ ((𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔)))
161	15	rexeqi 3325	. . . . . . . . . . 11 ⊢ (∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔)) ↔ ∃𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑_m (1...𝑛)) ∣ ((𝐹‘(1^st ‘(ℎ‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(ℎ‘𝑖))) = (𝐹‘(1^st ‘(ℎ‘(𝑖 + 1)))))} (𝑋𝐸𝑌) = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔)))
162		fveq1 6888	. . . . . . . . . . . . . . 15 ⊢ (ℎ = 𝑔 → (ℎ‘1) = (𝑔‘1))
163	162	fveq2d 6893	. . . . . . . . . . . . . 14 ⊢ (ℎ = 𝑔 → (1^st ‘(ℎ‘1)) = (1^st ‘(𝑔‘1)))
164	163	fveqeq2d 6897	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑔 → ((𝐹‘(1^st ‘(ℎ‘1))) = (𝐹‘𝑋) ↔ (𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋)))
165		fveq1 6888	. . . . . . . . . . . . . . 15 ⊢ (ℎ = 𝑔 → (ℎ‘𝑛) = (𝑔‘𝑛))
166	165	fveq2d 6893	. . . . . . . . . . . . . 14 ⊢ (ℎ = 𝑔 → (2^nd ‘(ℎ‘𝑛)) = (2^nd ‘(𝑔‘𝑛)))
167	166	fveqeq2d 6897	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑔 → ((𝐹‘(2^nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ↔ (𝐹‘(2^nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)))
168		fveq1 6888	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = 𝑔 → (ℎ‘𝑖) = (𝑔‘𝑖))
169	168	fveq2d 6893	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = 𝑔 → (2^nd ‘(ℎ‘𝑖)) = (2^nd ‘(𝑔‘𝑖)))
170	169	fveq2d 6893	. . . . . . . . . . . . . . 15 ⊢ (ℎ = 𝑔 → (𝐹‘(2^nd ‘(ℎ‘𝑖))) = (𝐹‘(2^nd ‘(𝑔‘𝑖))))
171		fveq1 6888	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = 𝑔 → (ℎ‘(𝑖 + 1)) = (𝑔‘(𝑖 + 1)))
172	171	fveq2d 6893	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = 𝑔 → (1^st ‘(ℎ‘(𝑖 + 1))) = (1^st ‘(𝑔‘(𝑖 + 1))))
173	172	fveq2d 6893	. . . . . . . . . . . . . . 15 ⊢ (ℎ = 𝑔 → (𝐹‘(1^st ‘(ℎ‘(𝑖 + 1)))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1)))))
174	170, 173	eqeq12d 2749	. . . . . . . . . . . . . 14 ⊢ (ℎ = 𝑔 → ((𝐹‘(2^nd ‘(ℎ‘𝑖))) = (𝐹‘(1^st ‘(ℎ‘(𝑖 + 1)))) ↔ (𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1))))))
175	174	ralbidv 3178	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑔 → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(ℎ‘𝑖))) = (𝐹‘(1^st ‘(ℎ‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1))))))
176	164, 167, 175	3anbi123d 1437	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑔 → (((𝐹‘(1^st ‘(ℎ‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(ℎ‘𝑖))) = (𝐹‘(1^st ‘(ℎ‘(𝑖 + 1))))) ↔ ((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1)))))))
177	176	rexrab 3692	. . . . . . . . . . 11 ⊢ (∃𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑_m (1...𝑛)) ∣ ((𝐹‘(1^st ‘(ℎ‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(ℎ‘𝑖))) = (𝐹‘(1^st ‘(ℎ‘(𝑖 + 1)))))} (𝑋𝐸𝑌) = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑_m (1...𝑛))(((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))))
178	161, 177	bitri 275	. . . . . . . . . 10 ⊢ (∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑_m (1...𝑛))(((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))))
179		oveq2 7414	. . . . . . . . . . . . 13 ⊢ (𝑛 = 1 → (1...𝑛) = (1...1))
180		1z 12589	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℤ
181		fzsn 13540	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℤ → (1...1) = {1})
182	180, 181	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (1...1) = {1}
183	179, 182	eqtrdi 2789	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (1...𝑛) = {1})
184	183	oveq2d 7422	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → ((𝑉 × 𝑉) ↑_m (1...𝑛)) = ((𝑉 × 𝑉) ↑_m {1}))
185		df-3an 1090	. . . . . . . . . . . . 13 ⊢ (((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1))))) ↔ (((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1))))))
186		ral0 4512	. . . . . . . . . . . . . . . 16 ⊢ ∀𝑖 ∈ ∅ (𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1))))
187		oveq1 7413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 1 → (𝑛 − 1) = (1 − 1))
188		1m1e0 12281	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 − 1) = 0
189	187, 188	eqtrdi 2789	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 1 → (𝑛 − 1) = 0)
190	189	oveq2d 7422	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 1 → (1...(𝑛 − 1)) = (1...0))
191		fz10 13519	. . . . . . . . . . . . . . . . . 18 ⊢ (1...0) = ∅
192	190, 191	eqtrdi 2789	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 1 → (1...(𝑛 − 1)) = ∅)
193	192	raleqdv 3326	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1 → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ ∅ (𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1))))))
194	186, 193	mpbiri 258	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1 → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1)))))
195	194	biantrud 533	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 1 → (((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ↔ (((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1)))))))
196		2fveq3 6894	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1 → (2^nd ‘(𝑔‘𝑛)) = (2^nd ‘(𝑔‘1)))
197	196	fveqeq2d 6897	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1 → ((𝐹‘(2^nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ↔ (𝐹‘(2^nd ‘(𝑔‘1))) = (𝐹‘𝑌)))
198	197	anbi2d 630	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 1 → (((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ↔ ((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘1))) = (𝐹‘𝑌))))
199	195, 198	bitr3d 281	. . . . . . . . . . . . 13 ⊢ (𝑛 = 1 → ((((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1))))) ↔ ((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘1))) = (𝐹‘𝑌))))
200	185, 199	bitrid 283	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1))))) ↔ ((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘1))) = (𝐹‘𝑌))))
201	200	anbi1d 631	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → ((((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))) ↔ (((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔)))))
202	184, 201	rexeqbidv 3344	. . . . . . . . . 10 ⊢ (𝑛 = 1 → (∃𝑔 ∈ ((𝑉 × 𝑉) ↑_m (1...𝑛))(((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑_m {1})(((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔)))))
203	178, 202	bitrid 283	. . . . . . . . 9 ⊢ (𝑛 = 1 → (∃𝑔 ∈ 𝑆 (𝑋𝐸𝑌) = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑_m {1})(((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔)))))
204	160, 203	bitrid 283	. . . . . . . 8 ⊢ (𝑛 = 1 → ((𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑_m {1})(((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔)))))
205	204	rspcev 3613	. . . . . . 7 ⊢ ((1 ∈ ℕ ∧ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑_m {1})(((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘1))) = (𝐹‘𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔)))) → ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))))
206	84, 156, 205	sylancr 588	. . . . . 6 ⊢ (𝜑 → ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ^*_𝑠 Σ_g (𝐸 ∘ 𝑔))))
207		eliun 5001	. . . . . 6 ⊢ ((𝑋𝐸𝑌) ∈ ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))) ↔ ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))))
208	206, 207	sylibr 233	. . . . 5 ⊢ (𝜑 → (𝑋𝐸𝑌) ∈ ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ^*_𝑠 Σ_g (𝐸 ∘ 𝑔))))
209	208, 18	eleqtrrdi 2845	. . . 4 ⊢ (𝜑 → (𝑋𝐸𝑌) ∈ 𝑇)
210		infxrlb 13310	. . . 4 ⊢ ((𝑇 ⊆ ℝ^* ∧ (𝑋𝐸𝑌) ∈ 𝑇) → inf(𝑇, ℝ^*, < ) ≤ (𝑋𝐸𝑌))
211	79, 209, 210	syl2anc 585	. . 3 ⊢ (𝜑 → inf(𝑇, ℝ^*, < ) ≤ (𝑋𝐸𝑌))
212	18	eleq2i 2826	. . . . . . 7 ⊢ (𝑝 ∈ 𝑇 ↔ 𝑝 ∈ ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ^*_𝑠 Σ_g (𝐸 ∘ 𝑔))))
213		eliun 5001	. . . . . . 7 ⊢ (𝑝 ∈ ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))) ↔ ∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))))
214	212, 213	bitri 275	. . . . . 6 ⊢ (𝑝 ∈ 𝑇 ↔ ∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ^*_𝑠 Σ_g (𝐸 ∘ 𝑔))))
215	158	elrnmpt 5954	. . . . . . . . 9 ⊢ (𝑝 ∈ V → (𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ 𝑆 𝑝 = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))))
216	215	elv 3481	. . . . . . . 8 ⊢ (𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))) ↔ ∃𝑔 ∈ 𝑆 𝑝 = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔)))
217	176, 15	elrab2 3686	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∈ 𝑆 ↔ (𝑔 ∈ ((𝑉 × 𝑉) ↑_m (1...𝑛)) ∧ ((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1)))))))
218	217	simprbi 498	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 ∈ 𝑆 → ((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1))))))
219	218	adantl 483	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2^nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1))))))
220	219	simp2d 1144	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐹‘(2^nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌))
221	3	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐹:𝑉–1-1-onto→𝐵)
222		f1of1 6830	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹:𝑉–1-1→𝐵)
223	221, 222	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐹:𝑉–1-1→𝐵)
224		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑛 ∈ ℕ)
225		elfz1end 13528	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (1...𝑛))
226	224, 225	sylib 217	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑛 ∈ (1...𝑛))
227	49, 226	ffvelcdmd 7085	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑔‘𝑛) ∈ (𝑉 × 𝑉))
228		xp2nd 8005	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔‘𝑛) ∈ (𝑉 × 𝑉) → (2^nd ‘(𝑔‘𝑛)) ∈ 𝑉)
229	227, 228	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (2^nd ‘(𝑔‘𝑛)) ∈ 𝑉)
230	13	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑌 ∈ 𝑉)
231		f1fveq 7258	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ ((2^nd ‘(𝑔‘𝑛)) ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ((𝐹‘(2^nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ↔ (2^nd ‘(𝑔‘𝑛)) = 𝑌))
232	223, 229, 230, 231	syl12anc 836	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐹‘(2^nd ‘(𝑔‘𝑛))) = (𝐹‘𝑌) ↔ (2^nd ‘(𝑔‘𝑛)) = 𝑌))
233	220, 232	mpbid 231	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (2^nd ‘(𝑔‘𝑛)) = 𝑌)
234	233	oveq2d 7422	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2^nd ‘(𝑔‘𝑛))) = (𝑋𝐸𝑌))
235		eleq1 2822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 1 → (𝑚 ∈ (1...𝑛) ↔ 1 ∈ (1...𝑛)))
236		2fveq3 6894	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 1 → (2^nd ‘(𝑔‘𝑚)) = (2^nd ‘(𝑔‘1)))
237	236	oveq2d 7422	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 1 → (𝑋𝐸(2^nd ‘(𝑔‘𝑚))) = (𝑋𝐸(2^nd ‘(𝑔‘1))))
238		oveq2 7414	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 1 → (1...𝑚) = (1...1))
239	238, 182	eqtrdi 2789	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 1 → (1...𝑚) = {1})
240	239	reseq2d 5980	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 1 → ((𝐸 ∘ 𝑔) ↾ (1...𝑚)) = ((𝐸 ∘ 𝑔) ↾ {1}))
241	240	oveq2d 7422	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 1 → (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) = (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ {1})))
242	237, 241	breq12d 5161	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 1 → ((𝑋𝐸(2^nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2^nd ‘(𝑔‘1))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ {1}))))
243	235, 242	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 1 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑚)))) ↔ (1 ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘1))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ {1})))))
244	243	imbi2d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 1 → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑚))))) ↔ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1 ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘1))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ {1}))))))
245		eleq1 2822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑥 → (𝑚 ∈ (1...𝑛) ↔ 𝑥 ∈ (1...𝑛)))
246		2fveq3 6894	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑥 → (2^nd ‘(𝑔‘𝑚)) = (2^nd ‘(𝑔‘𝑥)))
247	246	oveq2d 7422	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑥 → (𝑋𝐸(2^nd ‘(𝑔‘𝑚))) = (𝑋𝐸(2^nd ‘(𝑔‘𝑥))))
248		oveq2 7414	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑥 → (1...𝑚) = (1...𝑥))
249	248	reseq2d 5980	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑥 → ((𝐸 ∘ 𝑔) ↾ (1...𝑚)) = ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))
250	249	oveq2d 7422	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑥 → (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) = (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))))
251	247, 250	breq12d 5161	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑥 → ((𝑋𝐸(2^nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2^nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))))
252	245, 251	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑥 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑚)))) ↔ (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))))))
253	252	imbi2d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑥 → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑚))))) ↔ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))))))
254		eleq1 2822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑥 + 1) → (𝑚 ∈ (1...𝑛) ↔ (𝑥 + 1) ∈ (1...𝑛)))
255		2fveq3 6894	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = (𝑥 + 1) → (2^nd ‘(𝑔‘𝑚)) = (2^nd ‘(𝑔‘(𝑥 + 1))))
256	255	oveq2d 7422	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = (𝑥 + 1) → (𝑋𝐸(2^nd ‘(𝑔‘𝑚))) = (𝑋𝐸(2^nd ‘(𝑔‘(𝑥 + 1)))))
257		oveq2 7414	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = (𝑥 + 1) → (1...𝑚) = (1...(𝑥 + 1)))
258	257	reseq2d 5980	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = (𝑥 + 1) → ((𝐸 ∘ 𝑔) ↾ (1...𝑚)) = ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))
259	258	oveq2d 7422	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = (𝑥 + 1) → (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) = (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))))
260	256, 259	breq12d 5161	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑥 + 1) → ((𝑋𝐸(2^nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2^nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))))
261	254, 260	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝑥 + 1) → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑚)))) ↔ ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))))))
262	261	imbi2d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝑥 + 1) → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑚))))) ↔ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))))))
263		eleq1 2822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ (1...𝑛) ↔ 𝑛 ∈ (1...𝑛)))
264		2fveq3 6894	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → (2^nd ‘(𝑔‘𝑚)) = (2^nd ‘(𝑔‘𝑛)))
265	264	oveq2d 7422	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → (𝑋𝐸(2^nd ‘(𝑔‘𝑚))) = (𝑋𝐸(2^nd ‘(𝑔‘𝑛))))
266		oveq2 7414	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
267	266	reseq2d 5980	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → ((𝐸 ∘ 𝑔) ↾ (1...𝑚)) = ((𝐸 ∘ 𝑔) ↾ (1...𝑛)))
268	267	oveq2d 7422	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) = (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))
269	265, 268	breq12d 5161	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → ((𝑋𝐸(2^nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2^nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑛)))))
270	263, 269	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑛 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑚)))) ↔ (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))))
271	270	imbi2d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑛 → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘𝑚))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑚))))) ↔ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑛)))))))
272	29	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐸 ∈ (∞Met‘𝑉))
273	11	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑋 ∈ 𝑉)
274		nnuz 12862	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℕ = (ℤ_≥‘1)
275	224, 274	eleqtrdi 2844	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑛 ∈ (ℤ_≥‘1))
276		eluzfz1 13505	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (ℤ_≥‘1) → 1 ∈ (1...𝑛))
277	275, 276	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 1 ∈ (1...𝑛))
278	49, 277	ffvelcdmd 7085	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑔‘1) ∈ (𝑉 × 𝑉))
279		xp2nd 8005	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔‘1) ∈ (𝑉 × 𝑉) → (2^nd ‘(𝑔‘1)) ∈ 𝑉)
280	278, 279	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (2^nd ‘(𝑔‘1)) ∈ 𝑉)
281		xmetcl 23829	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ (2^nd ‘(𝑔‘1)) ∈ 𝑉) → (𝑋𝐸(2^nd ‘(𝑔‘1))) ∈ ℝ^*)
282	272, 273, 280, 281	syl3anc 1372	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2^nd ‘(𝑔‘1))) ∈ ℝ^*)
283	282	xrleidd 13128	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2^nd ‘(𝑔‘1))) ≤ (𝑋𝐸(2^nd ‘(𝑔‘1))))
284	137	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝑊 ∈ Mnd)
285	84	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 1 ∈ ℕ)
286	44, 278	ffvelcdmd 7085	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸‘(𝑔‘1)) ∈ (ℝ^* ∖ {-∞}))
287		2fveq3 6894	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 1 → (𝐸‘(𝑔‘𝑗)) = (𝐸‘(𝑔‘1)))
288	64, 287	gsumsn 19817	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Mnd ∧ 1 ∈ ℕ ∧ (𝐸‘(𝑔‘1)) ∈ (ℝ^* ∖ {-∞})) → (𝑊 Σ_g (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗)))) = (𝐸‘(𝑔‘1)))
289	284, 285, 286, 288	syl3anc 1372	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σ_g (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗)))) = (𝐸‘(𝑔‘1)))
290	272, 30	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → 𝐸:(𝑉 × 𝑉)⟶ℝ^*)
291		fcompt 7128	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐸:(𝑉 × 𝑉)⟶ℝ^* ∧ 𝑔:(1...𝑛)⟶(𝑉 × 𝑉)) → (𝐸 ∘ 𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))))
292	290, 49, 291	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸 ∘ 𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))))
293	292	reseq1d 5979	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐸 ∘ 𝑔) ↾ {1}) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ {1}))
294	277	snssd 4812	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → {1} ⊆ (1...𝑛))
295	294	resmptd 6039	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ {1}) = (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗))))
296	293, 295	eqtrd 2773	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐸 ∘ 𝑔) ↾ {1}) = (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗))))
297	296	oveq2d 7422	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ {1})) = (𝑊 Σ_g (𝑗 ∈ {1} ↦ (𝐸‘(𝑔‘𝑗)))))
298		df-ov 7409	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋𝐸(2^nd ‘(𝑔‘1))) = (𝐸‘⟨𝑋, (2^nd ‘(𝑔‘1))⟩)
299		1st2nd2 8011	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔‘1) ∈ (𝑉 × 𝑉) → (𝑔‘1) = ⟨(1^st ‘(𝑔‘1)), (2^nd ‘(𝑔‘1))⟩)
300	278, 299	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑔‘1) = ⟨(1^st ‘(𝑔‘1)), (2^nd ‘(𝑔‘1))⟩)
301	219	simp1d 1143	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋))
302		xp1st 8004	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔‘1) ∈ (𝑉 × 𝑉) → (1^st ‘(𝑔‘1)) ∈ 𝑉)
303	278, 302	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1^st ‘(𝑔‘1)) ∈ 𝑉)
304		f1fveq 7258	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ ((1^st ‘(𝑔‘1)) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ↔ (1^st ‘(𝑔‘1)) = 𝑋))
305	223, 303, 273, 304	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐹‘(1^st ‘(𝑔‘1))) = (𝐹‘𝑋) ↔ (1^st ‘(𝑔‘1)) = 𝑋))
306	301, 305	mpbid 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1^st ‘(𝑔‘1)) = 𝑋)
307	306	opeq1d 4879	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ⟨(1^st ‘(𝑔‘1)), (2^nd ‘(𝑔‘1))⟩ = ⟨𝑋, (2^nd ‘(𝑔‘1))⟩)
308	300, 307	eqtr2d 2774	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ⟨𝑋, (2^nd ‘(𝑔‘1))⟩ = (𝑔‘1))
309	308	fveq2d 6893	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝐸‘⟨𝑋, (2^nd ‘(𝑔‘1))⟩) = (𝐸‘(𝑔‘1)))
310	298, 309	eqtrid 2785	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2^nd ‘(𝑔‘1))) = (𝐸‘(𝑔‘1)))
311	289, 297, 310	3eqtr4d 2783	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ {1})) = (𝑋𝐸(2^nd ‘(𝑔‘1))))
312	283, 311	breqtrrd 5176	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2^nd ‘(𝑔‘1))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ {1})))
313	312	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (1 ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘1))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ {1}))))
314		simprl 770	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ ℕ)
315	314, 274	eleqtrdi 2844	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (ℤ_≥‘1))
316		simprr 772	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑥 + 1) ∈ (1...𝑛))
317		peano2fzr 13511	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (ℤ_≥‘1) ∧ (𝑥 + 1) ∈ (1...𝑛)) → 𝑥 ∈ (1...𝑛))
318	315, 316, 317	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (1...𝑛))
319	318	expr 458	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 + 1) ∈ (1...𝑛) → 𝑥 ∈ (1...𝑛)))
320	319	imim1d 82	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))))))
321	272	adantr 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸 ∈ (∞Met‘𝑉))
322	273	adantr 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑋 ∈ 𝑉)
323	49	adantr 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
324	323, 318	ffvelcdmd 7085	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘𝑥) ∈ (𝑉 × 𝑉))
325		xp2nd 8005	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔‘𝑥) ∈ (𝑉 × 𝑉) → (2^nd ‘(𝑔‘𝑥)) ∈ 𝑉)
326	324, 325	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2^nd ‘(𝑔‘𝑥)) ∈ 𝑉)
327		xmetcl 23829	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ (2^nd ‘(𝑔‘𝑥)) ∈ 𝑉) → (𝑋𝐸(2^nd ‘(𝑔‘𝑥))) ∈ ℝ^*)
328	321, 322, 326, 327	syl3anc 1372	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2^nd ‘(𝑔‘𝑥))) ∈ ℝ^*)
329	66	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑊 ∈ CMnd)
330		fzfid 13935	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...𝑥) ∈ Fin)
331	51	adantr 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸 ∘ 𝑔):(1...𝑛)⟶(ℝ^* ∖ {-∞}))
332		fzsuc 13545	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (ℤ_≥‘1) → (1...(𝑥 + 1)) = ((1...𝑥) ∪ {(𝑥 + 1)}))
333	315, 332	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...(𝑥 + 1)) = ((1...𝑥) ∪ {(𝑥 + 1)}))
334		elfzuz3 13495	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 + 1) ∈ (1...𝑛) → 𝑛 ∈ (ℤ_≥‘(𝑥 + 1)))
335	334	ad2antll 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑛 ∈ (ℤ_≥‘(𝑥 + 1)))
336		fzss2 13538	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ (ℤ_≥‘(𝑥 + 1)) → (1...(𝑥 + 1)) ⊆ (1...𝑛))
337	335, 336	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...(𝑥 + 1)) ⊆ (1...𝑛))
338	333, 337	eqsstrrd 4021	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((1...𝑥) ∪ {(𝑥 + 1)}) ⊆ (1...𝑛))
339	338	unssad 4187	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...𝑥) ⊆ (1...𝑛))
340	331, 339	fssresd 6756	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...𝑥)):(1...𝑥)⟶(ℝ^* ∖ {-∞}))
341	68	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 0 ∈ V)
342	340, 330, 341	fdmfifsupp 9370	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...𝑥)) finSupp 0)
343	64, 65, 329, 330, 340, 342	gsumcl 19778	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) ∈ (ℝ^* ∖ {-∞}))
344	343	eldifad 3960	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) ∈ ℝ^*)
345	321, 30	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸:(𝑉 × 𝑉)⟶ℝ^*)
346	323, 316	ffvelcdmd 7085	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉))
347	345, 346	ffvelcdmd 7085	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ^*)
348		xleadd1a 13229	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑋𝐸(2^nd ‘(𝑔‘𝑥))) ∈ ℝ^* ∧ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) ∈ ℝ^* ∧ (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ^*) ∧ (𝑋𝐸(2^nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥)))) → ((𝑋𝐸(2^nd ‘(𝑔‘𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
349	348	ex 414	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑋𝐸(2^nd ‘(𝑔‘𝑥))) ∈ ℝ^* ∧ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) ∈ ℝ^* ∧ (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ^*) → ((𝑋𝐸(2^nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) → ((𝑋𝐸(2^nd ‘(𝑔‘𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
350	328, 344, 347, 349	syl3anc 1372	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2^nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) → ((𝑋𝐸(2^nd ‘(𝑔‘𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
351		xp2nd 8005	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (2^nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
352	346, 351	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2^nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
353		xmettri 23849	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑋 ∈ 𝑉 ∧ (2^nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉 ∧ (2^nd ‘(𝑔‘𝑥)) ∈ 𝑉)) → (𝑋𝐸(2^nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2^nd ‘(𝑔‘𝑥))) +_𝑒 ((2^nd ‘(𝑔‘𝑥))𝐸(2^nd ‘(𝑔‘(𝑥 + 1))))))
354	321, 322, 352, 326, 353	syl13anc 1373	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2^nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2^nd ‘(𝑔‘𝑥))) +_𝑒 ((2^nd ‘(𝑔‘𝑥))𝐸(2^nd ‘(𝑔‘(𝑥 + 1))))))
355		1st2nd2 8011	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (𝑔‘(𝑥 + 1)) = ⟨(1^st ‘(𝑔‘(𝑥 + 1))), (2^nd ‘(𝑔‘(𝑥 + 1)))⟩)
356	346, 355	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) = ⟨(1^st ‘(𝑔‘(𝑥 + 1))), (2^nd ‘(𝑔‘(𝑥 + 1)))⟩)
357		2fveq3 6894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 = 𝑥 → (2^nd ‘(𝑔‘𝑖)) = (2^nd ‘(𝑔‘𝑥)))
358	357	fveq2d 6893	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝑥 → (𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(2^nd ‘(𝑔‘𝑥))))
359		fvoveq1 7429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = 𝑥 → (𝑔‘(𝑖 + 1)) = (𝑔‘(𝑥 + 1)))
360	359	fveq2d 6893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 = 𝑥 → (1^st ‘(𝑔‘(𝑖 + 1))) = (1^st ‘(𝑔‘(𝑥 + 1))))
361	360	fveq2d 6893	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝑥 → (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1)))) = (𝐹‘(1^st ‘(𝑔‘(𝑥 + 1)))))
362	358, 361	eqeq12d 2749	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 = 𝑥 → ((𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1)))) ↔ (𝐹‘(2^nd ‘(𝑔‘𝑥))) = (𝐹‘(1^st ‘(𝑔‘(𝑥 + 1))))))
363	219	simp3d 1145	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1)))))
364	363	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(𝑔‘𝑖))) = (𝐹‘(1^st ‘(𝑔‘(𝑖 + 1)))))
365		nnz 12576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℤ)
366	365	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ ℤ)
367		eluzp1m1 12845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ (ℤ_≥‘(𝑥 + 1))) → (𝑛 − 1) ∈ (ℤ_≥‘𝑥))
368	366, 335, 367	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑛 − 1) ∈ (ℤ_≥‘𝑥))
369		elfzuzb 13492	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ (1...(𝑛 − 1)) ↔ (𝑥 ∈ (ℤ_≥‘1) ∧ (𝑛 − 1) ∈ (ℤ_≥‘𝑥)))
370	315, 368, 369	sylanbrc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (1...(𝑛 − 1)))
371	362, 364, 370	rspcdva 3614	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐹‘(2^nd ‘(𝑔‘𝑥))) = (𝐹‘(1^st ‘(𝑔‘(𝑥 + 1)))))
372	223	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐹:𝑉–1-1→𝐵)
373		xp1st 8004	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (1^st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
374	346, 373	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1^st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
375		f1fveq 7258	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ ((2^nd ‘(𝑔‘𝑥)) ∈ 𝑉 ∧ (1^st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)) → ((𝐹‘(2^nd ‘(𝑔‘𝑥))) = (𝐹‘(1^st ‘(𝑔‘(𝑥 + 1)))) ↔ (2^nd ‘(𝑔‘𝑥)) = (1^st ‘(𝑔‘(𝑥 + 1)))))
376	372, 326, 374, 375	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐹‘(2^nd ‘(𝑔‘𝑥))) = (𝐹‘(1^st ‘(𝑔‘(𝑥 + 1)))) ↔ (2^nd ‘(𝑔‘𝑥)) = (1^st ‘(𝑔‘(𝑥 + 1)))))
377	371, 376	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2^nd ‘(𝑔‘𝑥)) = (1^st ‘(𝑔‘(𝑥 + 1))))
378	377	opeq1d 4879	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ⟨(2^nd ‘(𝑔‘𝑥)), (2^nd ‘(𝑔‘(𝑥 + 1)))⟩ = ⟨(1^st ‘(𝑔‘(𝑥 + 1))), (2^nd ‘(𝑔‘(𝑥 + 1)))⟩)
379	356, 378	eqtr4d 2776	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) = ⟨(2^nd ‘(𝑔‘𝑥)), (2^nd ‘(𝑔‘(𝑥 + 1)))⟩)
380	379	fveq2d 6893	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) = (𝐸‘⟨(2^nd ‘(𝑔‘𝑥)), (2^nd ‘(𝑔‘(𝑥 + 1)))⟩))
381		df-ov 7409	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2^nd ‘(𝑔‘𝑥))𝐸(2^nd ‘(𝑔‘(𝑥 + 1)))) = (𝐸‘⟨(2^nd ‘(𝑔‘𝑥)), (2^nd ‘(𝑔‘(𝑥 + 1)))⟩)
382	380, 381	eqtr4di 2791	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) = ((2^nd ‘(𝑔‘𝑥))𝐸(2^nd ‘(𝑔‘(𝑥 + 1)))))
383	382	oveq2d 7422	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2^nd ‘(𝑔‘𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) = ((𝑋𝐸(2^nd ‘(𝑔‘𝑥))) +_𝑒 ((2^nd ‘(𝑔‘𝑥))𝐸(2^nd ‘(𝑔‘(𝑥 + 1))))))
384	354, 383	breqtrrd 5176	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2^nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2^nd ‘(𝑔‘𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
385		xmetcl 23829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋 ∈ 𝑉 ∧ (2^nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉) → (𝑋𝐸(2^nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ^*)
386	321, 322, 352, 385	syl3anc 1372	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2^nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ^*)
387	328, 347	xaddcld 13277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2^nd ‘(𝑔‘𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ^*)
388	344, 347	xaddcld 13277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ^*)
389		xrletr 13134	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑋𝐸(2^nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ^* ∧ ((𝑋𝐸(2^nd ‘(𝑔‘𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ^* ∧ ((𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ^*) → (((𝑋𝐸(2^nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2^nd ‘(𝑔‘𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∧ ((𝑋𝐸(2^nd ‘(𝑔‘𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))) → (𝑋𝐸(2^nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
390	386, 387, 388, 389	syl3anc 1372	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (((𝑋𝐸(2^nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2^nd ‘(𝑔‘𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∧ ((𝑋𝐸(2^nd ‘(𝑔‘𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))) → (𝑋𝐸(2^nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
391	384, 390	mpand 694	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (((𝑋𝐸(2^nd ‘(𝑔‘𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) → (𝑋𝐸(2^nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
392	350, 391	syld 47	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2^nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) → (𝑋𝐸(2^nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
393		xrex 12968	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℝ^* ∈ V
394	393	difexi 5328	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℝ^* ∖ {-∞}) ∈ V
395	23, 22	ressplusg 17232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℝ^* ∖ {-∞}) ∈ V → +_𝑒 = (+_g‘𝑊))
396	394, 395	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ +_𝑒 = (+_g‘𝑊)
397	44	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → 𝐸:(𝑉 × 𝑉)⟶(ℝ^* ∖ {-∞}))
398		fzelp1 13550	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (1...𝑥) → 𝑗 ∈ (1...(𝑥 + 1)))
399	49	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
400	337	sselda 3982	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → 𝑗 ∈ (1...𝑛))
401	399, 400	ffvelcdmd 7085	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → (𝑔‘𝑗) ∈ (𝑉 × 𝑉))
402	398, 401	sylan2 594	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → (𝑔‘𝑗) ∈ (𝑉 × 𝑉))
403	397, 402	ffvelcdmd 7085	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → (𝐸‘(𝑔‘𝑗)) ∈ (ℝ^* ∖ {-∞}))
404		fzp1disj 13557	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1...𝑥) ∩ {(𝑥 + 1)}) = ∅
405	404	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((1...𝑥) ∩ {(𝑥 + 1)}) = ∅)
406		disjsn 4715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1...𝑥) ∩ {(𝑥 + 1)}) = ∅ ↔ ¬ (𝑥 + 1) ∈ (1...𝑥))
407	405, 406	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ¬ (𝑥 + 1) ∈ (1...𝑥))
408	44	adantr 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸:(𝑉 × 𝑉)⟶(ℝ^* ∖ {-∞}))
409	408, 346	ffvelcdmd 7085	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) ∈ (ℝ^* ∖ {-∞}))
410		2fveq3 6894	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑥 + 1) → (𝐸‘(𝑔‘𝑗)) = (𝐸‘(𝑔‘(𝑥 + 1))))
411	64, 396, 329, 330, 403, 316, 407, 409, 410	gsumunsn 19823	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σ_g (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔‘𝑗)))) = ((𝑊 Σ_g (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗)))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
412	292	adantr 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸 ∘ 𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))))
413	412, 333	reseq12d 5981	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ ((1...𝑥) ∪ {(𝑥 + 1)})))
414	338	resmptd 6039	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ ((1...𝑥) ∪ {(𝑥 + 1)})) = (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔‘𝑗))))
415	413, 414	eqtrd 2773	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))) = (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔‘𝑗))))
416	415	oveq2d 7422	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))) = (𝑊 Σ_g (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔‘𝑗)))))
417	412	reseq1d 5979	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...𝑥)) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ (1...𝑥)))
418	339	resmptd 6039	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔‘𝑗))) ↾ (1...𝑥)) = (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗))))
419	417, 418	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸 ∘ 𝑔) ↾ (1...𝑥)) = (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗))))
420	419	oveq2d 7422	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) = (𝑊 Σ_g (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗)))))
421	420	oveq1d 7421	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) = ((𝑊 Σ_g (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔‘𝑗)))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
422	411, 416, 421	3eqtr4d 2783	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))) = ((𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
423	422	breq2d 5160	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2^nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1)))) ↔ (𝑋𝐸(2^nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) +_𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
424	392, 423	sylibrd 259	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2^nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))) → (𝑋𝐸(2^nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))))
425	320, 424	animpimp2impd 845	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℕ → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘𝑥))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑥))))) → (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...(𝑥 + 1))))))))
426	244, 253, 262, 271, 313, 425	nnind 12227	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))))
427	224, 426	mpcom 38	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2^nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑛)))))
428	226, 427	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸(2^nd ‘(𝑔‘𝑛))) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))
429	234, 428	eqbrtrrd 5172	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸𝑌) ≤ (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))
430		ffn 6715	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∘ 𝑔):(1...𝑛)⟶(ℝ^* ∖ {-∞}) → (𝐸 ∘ 𝑔) Fn (1...𝑛))
431		fnresdm 6667	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∘ 𝑔) Fn (1...𝑛) → ((𝐸 ∘ 𝑔) ↾ (1...𝑛)) = (𝐸 ∘ 𝑔))
432	51, 430, 431	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → ((𝐸 ∘ 𝑔) ↾ (1...𝑛)) = (𝐸 ∘ 𝑔))
433	432	oveq2d 7422	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑛))) = (𝑊 Σ_g (𝐸 ∘ 𝑔)))
434	62, 433	eqtr4d 2776	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (ℝ^*_𝑠 Σ_g (𝐸 ∘ 𝑔)) = (𝑊 Σ_g ((𝐸 ∘ 𝑔) ↾ (1...𝑛))))
435	429, 434	breqtrrd 5176	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑋𝐸𝑌) ≤ (ℝ^*_𝑠 Σ_g (𝐸 ∘ 𝑔)))
436		breq2 5152	. . . . . . . . . 10 ⊢ (𝑝 = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔)) → ((𝑋𝐸𝑌) ≤ 𝑝 ↔ (𝑋𝐸𝑌) ≤ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))))
437	435, 436	syl5ibrcom 246	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑔 ∈ 𝑆) → (𝑝 = (ℝ^*_𝑠 Σ_g (𝐸 ∘ 𝑔)) → (𝑋𝐸𝑌) ≤ 𝑝))
438	437	rexlimdva 3156	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∃𝑔 ∈ 𝑆 𝑝 = (ℝ^*_𝑠 Σ_g (𝐸 ∘ 𝑔)) → (𝑋𝐸𝑌) ≤ 𝑝))
439	216, 438	biimtrid 241	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ^*_𝑠 Σ_g (𝐸 ∘ 𝑔))) → (𝑋𝐸𝑌) ≤ 𝑝))
440	439	rexlimdva 3156	. . . . . 6 ⊢ (𝜑 → (∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔 ∈ 𝑆 ↦ (ℝ^*_𝑠 Σ_g (𝐸 ∘ 𝑔))) → (𝑋𝐸𝑌) ≤ 𝑝))
441	214, 440	biimtrid 241	. . . . 5 ⊢ (𝜑 → (𝑝 ∈ 𝑇 → (𝑋𝐸𝑌) ≤ 𝑝))
442	441	ralrimiv 3146	. . . 4 ⊢ (𝜑 → ∀𝑝 ∈ 𝑇 (𝑋𝐸𝑌) ≤ 𝑝)
443		infxrgelb 13311	. . . . 5 ⊢ ((𝑇 ⊆ ℝ^* ∧ (𝑋𝐸𝑌) ∈ ℝ^) → ((𝑋𝐸𝑌) ≤ inf(𝑇, ℝ^, < ) ↔ ∀𝑝 ∈ 𝑇 (𝑋𝐸𝑌) ≤ 𝑝))
444	79, 83, 443	syl2anc 585	. . . 4 ⊢ (𝜑 → ((𝑋𝐸𝑌) ≤ inf(𝑇, ℝ^*, < ) ↔ ∀𝑝 ∈ 𝑇 (𝑋𝐸𝑌) ≤ 𝑝))
445	442, 444	mpbird 257	. . 3 ⊢ (𝜑 → (𝑋𝐸𝑌) ≤ inf(𝑇, ℝ^*, < ))
446	81, 83, 211, 445	xrletrid 13131	. 2 ⊢ (𝜑 → inf(𝑇, ℝ^*, < ) = (𝑋𝐸𝑌))
447	20, 446	eqtrd 2773	1 ⊢ (𝜑 → ((𝐹‘𝑋)𝐷(𝐹‘𝑌)) = (𝑋𝐸𝑌))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ≠ wne 2941 ∀wral 3062 ∃wrex 3071 {crab 3433 Vcvv 3475 ∖ cdif 3945 ∪ cun 3946 ∩ cin 3947 ⊆ wss 3948 ∅c0 4322 {csn 4628 ⟨cop 4634 ∪ ciun 4997 class class class wbr 5148 ↦ cmpt 5231 × cxp 5674 ran crn 5677 ↾ cres 5678 ∘ ccom 5680 Fn wfn 6536 ⟶wf 6537 –1-1→wf1 6538 –onto→wfo 6539 –1-1-onto→wf1o 6540 ‘cfv 6541 (class class class)co 7406 1^st c1st 7970 2^nd c2nd 7971 ↑_m cmap 8817 Fincfn 8936 infcinf 9433 ℝcr 11106 0cc0 11107 1c1 11108 + caddc 11110 -∞cmnf 11243 ℝ^*cxr 11244 < clt 11245 ≤ cle 11246 − cmin 11441 ℕcn 12209 ℤcz 12555 ℤ_≥cuz 12819 +_𝑒 cxad 13087 ...cfz 13481 Basecbs 17141 ↾_s cress 17170 +_gcplusg 17194 distcds 17203 Σ_g cgsu 17383 ℝ^*_𝑠cxrs 17443 “_s cimas 17447 Mndcmnd 18622 CMndccmn 19643 ∞Metcxmet 20922

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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-cnex 11163 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-addrcl 11168 ax-mulcl 11169 ax-mulrcl 11170 ax-mulcom 11171 ax-addass 11172 ax-mulass 11173 ax-distr 11174 ax-i2m1 11175 ax-1ne0 11176 ax-1rid 11177 ax-rnegex 11178 ax-rrecex 11179 ax-cnre 11180 ax-pre-lttri 11181 ax-pre-lttrn 11182 ax-pre-ltadd 11183 ax-pre-mulgt0 11184 ax-pre-sup 11185

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-iin 5000 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6298 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7362 df-ov 7409 df-oprab 7410 df-mpo 7411 df-of 7667 df-om 7853 df-1st 7972 df-2nd 7973 df-supp 8144 df-frecs 8263 df-wrecs 8294 df-recs 8368 df-rdg 8407 df-1o 8463 df-er 8700 df-map 8819 df-en 8937 df-dom 8938 df-sdom 8939 df-fin 8940 df-fsupp 9359 df-sup 9434 df-inf 9435 df-oi 9502 df-card 9931 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-div 11869 df-nn 12210 df-2 12272 df-3 12273 df-4 12274 df-5 12275 df-6 12276 df-7 12277 df-8 12278 df-9 12279 df-n0 12470 df-z 12556 df-dec 12675 df-uz 12820 df-rp 12972 df-xneg 13089 df-xadd 13090 df-xmul 13091 df-fz 13482 df-fzo 13625 df-seq 13964 df-hash 14288 df-struct 17077 df-sets 17094 df-slot 17112 df-ndx 17124 df-base 17142 df-ress 17171 df-plusg 17207 df-mulr 17208 df-sca 17210 df-vsca 17211 df-ip 17212 df-tset 17213 df-ple 17214 df-ds 17216 df-0g 17384 df-gsum 17385 df-xrs 17445 df-imas 17451 df-mre 17527 df-mrc 17528 df-acs 17530 df-mgm 18558 df-sgrp 18607 df-mnd 18623 df-submnd 18669 df-mulg 18946 df-cntz 19176 df-cmn 19645 df-xmet 20930

This theorem is referenced by: imasdsf1o 23872

W3C validator