Metamath Proof Explorer

Theorem imasdsf1olem

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

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

Proof

Step Hyp Ref Expression
1 imasdsf1o.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2 imasdsf1o.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3 imasdsf1o.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
4 imasdsf1o.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
5 imasdsf1o.e ⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
6 imasdsf1o.d ⊢ 𝐷 = ( dist ‘ 𝑈 )
7 imasdsf1o.m ⊢ ( 𝜑 → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
8 imasdsf1o.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
9 imasdsf1o.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
10 imasdsf1o.w ⊢ 𝑊 = ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) )
11 imasdsf1o.s ⊢ 𝑆 = { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) }
12 imasdsf1o.t ⊢ 𝑇 = ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) )
13 f1ofo ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 → 𝐹 : 𝑉 –onto→ 𝐵 )
14 3 13 syl ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
15 eqid ⊢ ( dist ‘ 𝑅 ) = ( dist ‘ 𝑅 )
16 f1of ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 → 𝐹 : 𝑉 ⟶ 𝐵 )
17 3 16 syl ⊢ ( 𝜑 → 𝐹 : 𝑉 ⟶ 𝐵 )
18 17 8 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
19 17 9 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) ∈ 𝐵 )
20 1 2 14 4 15 6 18 19 11 5 imasdsval2 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) 𝐷 ( 𝐹 ‘ 𝑌 ) ) = inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) , ℝ* , < ) )
21 12 infeq1i ⊢ inf ( 𝑇 , ℝ* , < ) = inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) , ℝ* , < )
22 20 21 eqtr4di ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) 𝐷 ( 𝐹 ‘ 𝑌 ) ) = inf ( 𝑇 , ℝ* , < ) )
23 xrsbas ⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
24 xrsadd ⊢ +e = ( +g ‘ ℝ*𝑠 )
25 xrsex ⊢ ℝ*𝑠 ∈ V
26 25 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ℝ*𝑠 ∈ V )
27 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 1 ... 𝑛 ) ∈ Fin )
28 difss ⊢ ( ℝ* ∖ { -∞ } ) ⊆ ℝ*
29 28 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( ℝ* ∖ { -∞ } ) ⊆ ℝ* )
30 xmetf ⊢ ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) → 𝐸 : ( 𝑉 × 𝑉 ) ⟶ ℝ* )
31 ffn ⊢ ( 𝐸 : ( 𝑉 × 𝑉 ) ⟶ ℝ* → 𝐸 Fn ( 𝑉 × 𝑉 ) )
32 7 30 31 3syl ⊢ ( 𝜑 → 𝐸 Fn ( 𝑉 × 𝑉 ) )
33 xmetcl ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉 ) → ( 𝑓 𝐸 𝑔 ) ∈ ℝ* )
34 xmetge0 ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉 ) → 0 ≤ ( 𝑓 𝐸 𝑔 ) )
35 ge0nemnf ⊢ ( ( ( 𝑓 𝐸 𝑔 ) ∈ ℝ* ∧ 0 ≤ ( 𝑓 𝐸 𝑔 ) ) → ( 𝑓 𝐸 𝑔 ) ≠ -∞ )
36 33 34 35 syl2anc ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉 ) → ( 𝑓 𝐸 𝑔 ) ≠ -∞ )
37 eldifsn ⊢ ( ( 𝑓 𝐸 𝑔 ) ∈ ( ℝ* ∖ { -∞ } ) ↔ ( ( 𝑓 𝐸 𝑔 ) ∈ ℝ* ∧ ( 𝑓 𝐸 𝑔 ) ≠ -∞ ) )
38 33 36 37 sylanbrc ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉 ) → ( 𝑓 𝐸 𝑔 ) ∈ ( ℝ* ∖ { -∞ } ) )
39 38 3expb ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ ( 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉 ) ) → ( 𝑓 𝐸 𝑔 ) ∈ ( ℝ* ∖ { -∞ } ) )
40 7 39 sylan ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑉 ∧ 𝑔 ∈ 𝑉 ) ) → ( 𝑓 𝐸 𝑔 ) ∈ ( ℝ* ∖ { -∞ } ) )
41 40 ralrimivva ⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝑉 ∀ 𝑔 ∈ 𝑉 ( 𝑓 𝐸 𝑔 ) ∈ ( ℝ* ∖ { -∞ } ) )
42 ffnov ⊢ ( 𝐸 : ( 𝑉 × 𝑉 ) ⟶ ( ℝ* ∖ { -∞ } ) ↔ ( 𝐸 Fn ( 𝑉 × 𝑉 ) ∧ ∀ 𝑓 ∈ 𝑉 ∀ 𝑔 ∈ 𝑉 ( 𝑓 𝐸 𝑔 ) ∈ ( ℝ* ∖ { -∞ } ) ) )
43 32 41 42 sylanbrc ⊢ ( 𝜑 → 𝐸 : ( 𝑉 × 𝑉 ) ⟶ ( ℝ* ∖ { -∞ } ) )
44 43 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → 𝐸 : ( 𝑉 × 𝑉 ) ⟶ ( ℝ* ∖ { -∞ } ) )
45 11 ssrab3 ⊢ 𝑆 ⊆ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) )
46 45 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑆 ⊆ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) )
47 46 sselda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → 𝑔 ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) )
48 elmapi ⊢ ( 𝑔 ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) → 𝑔 : ( 1 ... 𝑛 ) ⟶ ( 𝑉 × 𝑉 ) )
49 47 48 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → 𝑔 : ( 1 ... 𝑛 ) ⟶ ( 𝑉 × 𝑉 ) )
50 fco ⊢ ( ( 𝐸 : ( 𝑉 × 𝑉 ) ⟶ ( ℝ* ∖ { -∞ } ) ∧ 𝑔 : ( 1 ... 𝑛 ) ⟶ ( 𝑉 × 𝑉 ) ) → ( 𝐸 ∘ 𝑔 ) : ( 1 ... 𝑛 ) ⟶ ( ℝ* ∖ { -∞ } ) )
51 44 49 50 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝐸 ∘ 𝑔 ) : ( 1 ... 𝑛 ) ⟶ ( ℝ* ∖ { -∞ } ) )
52 0re ⊢ 0 ∈ ℝ
53 rexr ⊢ ( 0 ∈ ℝ → 0 ∈ ℝ* )
54 renemnf ⊢ ( 0 ∈ ℝ → 0 ≠ -∞ )
55 eldifsn ⊢ ( 0 ∈ ( ℝ* ∖ { -∞ } ) ↔ ( 0 ∈ ℝ* ∧ 0 ≠ -∞ ) )
56 53 54 55 sylanbrc ⊢ ( 0 ∈ ℝ → 0 ∈ ( ℝ* ∖ { -∞ } ) )
57 52 56 mp1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → 0 ∈ ( ℝ* ∖ { -∞ } ) )
58 xaddlid ⊢ ( 𝑥 ∈ ℝ* → ( 0 +e 𝑥 ) = 𝑥 )
59 xaddrid ⊢ ( 𝑥 ∈ ℝ* → ( 𝑥 +e 0 ) = 𝑥 )
60 58 59 jca ⊢ ( 𝑥 ∈ ℝ* → ( ( 0 +e 𝑥 ) = 𝑥 ∧ ( 𝑥 +e 0 ) = 𝑥 ) )
61 60 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ 𝑥 ∈ ℝ* ) → ( ( 0 +e 𝑥 ) = 𝑥 ∧ ( 𝑥 +e 0 ) = 𝑥 ) )
62 23 24 10 26 27 29 51 57 61 gsumress ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) = ( 𝑊 Σg ( 𝐸 ∘ 𝑔 ) ) )
63 10 23 ressbas2 ⊢ ( ( ℝ* ∖ { -∞ } ) ⊆ ℝ* → ( ℝ* ∖ { -∞ } ) = ( Base ‘ 𝑊 ) )
64 28 63 ax-mp ⊢ ( ℝ* ∖ { -∞ } ) = ( Base ‘ 𝑊 )
65 10 xrs10 ⊢ 0 = ( 0g ‘ 𝑊 )
66 10 xrs1cmn ⊢ 𝑊 ∈ CMnd
67 66 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → 𝑊 ∈ CMnd )
68 c0ex ⊢ 0 ∈ V
69 68 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → 0 ∈ V )
70 51 27 69 fdmfifsupp ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝐸 ∘ 𝑔 ) finSupp 0 )
71 64 65 67 27 51 70 gsumcl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑊 Σg ( 𝐸 ∘ 𝑔 ) ) ∈ ( ℝ* ∖ { -∞ } ) )
72 62 71 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ∈ ( ℝ* ∖ { -∞ } ) )
73 72 eldifad ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ∈ ℝ* )
74 73 fmpttd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) : 𝑆 ⟶ ℝ* )
75 74 frnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) ⊆ ℝ* )
76 75 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) ⊆ ℝ* )
77 iunss ⊢ ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) ⊆ ℝ* ↔ ∀ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) ⊆ ℝ* )
78 76 77 sylibr ⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) ⊆ ℝ* )
79 12 78 eqsstrid ⊢ ( 𝜑 → 𝑇 ⊆ ℝ* )
80 infxrcl ⊢ ( 𝑇 ⊆ ℝ* → inf ( 𝑇 , ℝ* , < ) ∈ ℝ* )
81 79 80 syl ⊢ ( 𝜑 → inf ( 𝑇 , ℝ* , < ) ∈ ℝ* )
82 xmetcl ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 𝐸 𝑌 ) ∈ ℝ* )
83 7 8 9 82 syl3anc ⊢ ( 𝜑 → ( 𝑋 𝐸 𝑌 ) ∈ ℝ* )
84 1nn ⊢ 1 ∈ ℕ
85 1ex ⊢ 1 ∈ V
86 opex ⊢ ⟨ 𝑋 , 𝑌 ⟩ ∈ V
87 85 86 f1osn ⊢ { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } : { 1 } –1-1-onto→ { ⟨ 𝑋 , 𝑌 ⟩ }
88 f1of ⊢ ( { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } : { 1 } –1-1-onto→ { ⟨ 𝑋 , 𝑌 ⟩ } → { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } : { 1 } ⟶ { ⟨ 𝑋 , 𝑌 ⟩ } )
89 87 88 ax-mp ⊢ { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } : { 1 } ⟶ { ⟨ 𝑋 , 𝑌 ⟩ }
90 8 9 opelxpd ⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝑉 × 𝑉 ) )
91 90 snssd ⊢ ( 𝜑 → { ⟨ 𝑋 , 𝑌 ⟩ } ⊆ ( 𝑉 × 𝑉 ) )
92 fss ⊢ ( ( { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } : { 1 } ⟶ { ⟨ 𝑋 , 𝑌 ⟩ } ∧ { ⟨ 𝑋 , 𝑌 ⟩ } ⊆ ( 𝑉 × 𝑉 ) ) → { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } : { 1 } ⟶ ( 𝑉 × 𝑉 ) )
93 89 91 92 sylancr ⊢ ( 𝜑 → { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } : { 1 } ⟶ ( 𝑉 × 𝑉 ) )
94 7 elfvexd ⊢ ( 𝜑 → 𝑉 ∈ V )
95 94 94 xpexd ⊢ ( 𝜑 → ( 𝑉 × 𝑉 ) ∈ V )
96 snex ⊢ { 1 } ∈ V
97 elmapg ⊢ ( ( ( 𝑉 × 𝑉 ) ∈ V ∧ { 1 } ∈ V ) → ( { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } ∈ ( ( 𝑉 × 𝑉 ) ↑m { 1 } ) ↔ { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } : { 1 } ⟶ ( 𝑉 × 𝑉 ) ) )
98 95 96 97 sylancl ⊢ ( 𝜑 → ( { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } ∈ ( ( 𝑉 × 𝑉 ) ↑m { 1 } ) ↔ { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } : { 1 } ⟶ ( 𝑉 × 𝑉 ) ) )
99 93 98 mpbird ⊢ ( 𝜑 → { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } ∈ ( ( 𝑉 × 𝑉 ) ↑m { 1 } ) )
100 op1stg ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
101 8 9 100 syl2anc ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
102 101 fveq2d ⊢ ( 𝜑 → ( 𝐹 ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝐹 ‘ 𝑋 ) )
103 op2ndg ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
104 8 9 103 syl2anc ⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
105 104 fveq2d ⊢ ( 𝜑 → ( 𝐹 ‘ ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝐹 ‘ 𝑌 ) )
106 102 105 jca ⊢ ( 𝜑 → ( ( 𝐹 ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝐹 ‘ 𝑌 ) ) )
107 25 a1i ⊢ ( 𝜑 → ℝ*𝑠 ∈ V )
108 snfi ⊢ { 1 } ∈ Fin
109 108 a1i ⊢ ( 𝜑 → { 1 } ∈ Fin )
110 28 a1i ⊢ ( 𝜑 → ( ℝ* ∖ { -∞ } ) ⊆ ℝ* )
111 xmetge0 ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 0 ≤ ( 𝑋 𝐸 𝑌 ) )
112 7 8 9 111 syl3anc ⊢ ( 𝜑 → 0 ≤ ( 𝑋 𝐸 𝑌 ) )
113 ge0nemnf ⊢ ( ( ( 𝑋 𝐸 𝑌 ) ∈ ℝ* ∧ 0 ≤ ( 𝑋 𝐸 𝑌 ) ) → ( 𝑋 𝐸 𝑌 ) ≠ -∞ )
114 83 112 113 syl2anc ⊢ ( 𝜑 → ( 𝑋 𝐸 𝑌 ) ≠ -∞ )
115 eldifsn ⊢ ( ( 𝑋 𝐸 𝑌 ) ∈ ( ℝ* ∖ { -∞ } ) ↔ ( ( 𝑋 𝐸 𝑌 ) ∈ ℝ* ∧ ( 𝑋 𝐸 𝑌 ) ≠ -∞ ) )
116 83 114 115 sylanbrc ⊢ ( 𝜑 → ( 𝑋 𝐸 𝑌 ) ∈ ( ℝ* ∖ { -∞ } ) )
117 fconst6g ⊢ ( ( 𝑋 𝐸 𝑌 ) ∈ ( ℝ* ∖ { -∞ } ) → ( { 1 } × { ( 𝑋 𝐸 𝑌 ) } ) : { 1 } ⟶ ( ℝ* ∖ { -∞ } ) )
118 116 117 syl ⊢ ( 𝜑 → ( { 1 } × { ( 𝑋 𝐸 𝑌 ) } ) : { 1 } ⟶ ( ℝ* ∖ { -∞ } ) )
119 fcoconst ⊢ ( ( 𝐸 Fn ( 𝑉 × 𝑉 ) ∧ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝑉 × 𝑉 ) ) → ( 𝐸 ∘ ( { 1 } × { ⟨ 𝑋 , 𝑌 ⟩ } ) ) = ( { 1 } × { ( 𝐸 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) } ) )
120 32 90 119 syl2anc ⊢ ( 𝜑 → ( 𝐸 ∘ ( { 1 } × { ⟨ 𝑋 , 𝑌 ⟩ } ) ) = ( { 1 } × { ( 𝐸 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) } ) )
121 85 86 xpsn ⊢ ( { 1 } × { ⟨ 𝑋 , 𝑌 ⟩ } ) = { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ }
122 121 coeq2i ⊢ ( 𝐸 ∘ ( { 1 } × { ⟨ 𝑋 , 𝑌 ⟩ } ) ) = ( 𝐸 ∘ { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } )
123 df-ov ⊢ ( 𝑋 𝐸 𝑌 ) = ( 𝐸 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
124 123 eqcomi ⊢ ( 𝐸 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( 𝑋 𝐸 𝑌 )
125 124 sneqi ⊢ { ( 𝐸 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) } = { ( 𝑋 𝐸 𝑌 ) }
126 125 xpeq2i ⊢ ( { 1 } × { ( 𝐸 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) } ) = ( { 1 } × { ( 𝑋 𝐸 𝑌 ) } )
127 120 122 126 3eqtr3g ⊢ ( 𝜑 → ( 𝐸 ∘ { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } ) = ( { 1 } × { ( 𝑋 𝐸 𝑌 ) } ) )
128 127 feq1d ⊢ ( 𝜑 → ( ( 𝐸 ∘ { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } ) : { 1 } ⟶ ( ℝ* ∖ { -∞ } ) ↔ ( { 1 } × { ( 𝑋 𝐸 𝑌 ) } ) : { 1 } ⟶ ( ℝ* ∖ { -∞ } ) ) )
129 118 128 mpbird ⊢ ( 𝜑 → ( 𝐸 ∘ { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } ) : { 1 } ⟶ ( ℝ* ∖ { -∞ } ) )
130 52 56 mp1i ⊢ ( 𝜑 → 0 ∈ ( ℝ* ∖ { -∞ } ) )
131 60 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ* ) → ( ( 0 +e 𝑥 ) = 𝑥 ∧ ( 𝑥 +e 0 ) = 𝑥 ) )
132 23 24 10 107 109 110 129 130 131 gsumress ⊢ ( 𝜑 → ( ℝ*𝑠 Σg ( 𝐸 ∘ { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } ) ) = ( 𝑊 Σg ( 𝐸 ∘ { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } ) ) )
133 fconstmpt ⊢ ( { 1 } × { ( 𝑋 𝐸 𝑌 ) } ) = ( 𝑗 ∈ { 1 } ↦ ( 𝑋 𝐸 𝑌 ) )
134 127 133 eqtrdi ⊢ ( 𝜑 → ( 𝐸 ∘ { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } ) = ( 𝑗 ∈ { 1 } ↦ ( 𝑋 𝐸 𝑌 ) ) )
135 134 oveq2d ⊢ ( 𝜑 → ( 𝑊 Σg ( 𝐸 ∘ { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } ) ) = ( 𝑊 Σg ( 𝑗 ∈ { 1 } ↦ ( 𝑋 𝐸 𝑌 ) ) ) )
136 cmnmnd ⊢ ( 𝑊 ∈ CMnd → 𝑊 ∈ Mnd )
137 66 136 mp1i ⊢ ( 𝜑 → 𝑊 ∈ Mnd )
138 84 a1i ⊢ ( 𝜑 → 1 ∈ ℕ )
139 eqidd ⊢ ( 𝑗 = 1 → ( 𝑋 𝐸 𝑌 ) = ( 𝑋 𝐸 𝑌 ) )
140 64 139 gsumsn ⊢ ( ( 𝑊 ∈ Mnd ∧ 1 ∈ ℕ ∧ ( 𝑋 𝐸 𝑌 ) ∈ ( ℝ* ∖ { -∞ } ) ) → ( 𝑊 Σg ( 𝑗 ∈ { 1 } ↦ ( 𝑋 𝐸 𝑌 ) ) ) = ( 𝑋 𝐸 𝑌 ) )
141 137 138 116 140 syl3anc ⊢ ( 𝜑 → ( 𝑊 Σg ( 𝑗 ∈ { 1 } ↦ ( 𝑋 𝐸 𝑌 ) ) ) = ( 𝑋 𝐸 𝑌 ) )
142 132 135 141 3eqtrrd ⊢ ( 𝜑 → ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } ) ) )
143 fveq1 ⊢ ( 𝑔 = { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } → ( 𝑔 ‘ 1 ) = ( { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } ‘ 1 ) )
144 85 86 fvsn ⊢ ( { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } ‘ 1 ) = ⟨ 𝑋 , 𝑌 ⟩
145 143 144 eqtrdi ⊢ ( 𝑔 = { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } → ( 𝑔 ‘ 1 ) = ⟨ 𝑋 , 𝑌 ⟩ )
146 145 fveq2d ⊢ ( 𝑔 = { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } → ( 1st ‘ ( 𝑔 ‘ 1 ) ) = ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
147 146 fveqeq2d ⊢ ( 𝑔 = { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } → ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝐹 ‘ 𝑋 ) ) )
148 145 fveq2d ⊢ ( 𝑔 = { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } → ( 2nd ‘ ( 𝑔 ‘ 1 ) ) = ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
149 148 fveqeq2d ⊢ ( 𝑔 = { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } → ( ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑌 ) ↔ ( 𝐹 ‘ ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝐹 ‘ 𝑌 ) ) )
150 147 149 anbi12d ⊢ ( 𝑔 = { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } → ( ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑌 ) ) ↔ ( ( 𝐹 ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝐹 ‘ 𝑌 ) ) ) )
151 coeq2 ⊢ ( 𝑔 = { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } → ( 𝐸 ∘ 𝑔 ) = ( 𝐸 ∘ { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } ) )
152 151 oveq2d ⊢ ( 𝑔 = { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } → ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } ) ) )
153 152 eqeq2d ⊢ ( 𝑔 = { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } → ( ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ↔ ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } ) ) ) )
154 150 153 anbi12d ⊢ ( 𝑔 = { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } → ( ( ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑌 ) ) ∧ ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) ↔ ( ( ( 𝐹 ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝐹 ‘ 𝑌 ) ) ∧ ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } ) ) ) ) )
155 154 rspcev ⊢ ( ( { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } ∈ ( ( 𝑉 × 𝑉 ) ↑m { 1 } ) ∧ ( ( ( 𝐹 ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝐹 ‘ 𝑌 ) ) ∧ ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ { ⟨ 1 , ⟨ 𝑋 , 𝑌 ⟩ ⟩ } ) ) ) ) → ∃ 𝑔 ∈ ( ( 𝑉 × 𝑉 ) ↑m { 1 } ) ( ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑌 ) ) ∧ ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) )
156 99 106 142 155 syl12anc ⊢ ( 𝜑 → ∃ 𝑔 ∈ ( ( 𝑉 × 𝑉 ) ↑m { 1 } ) ( ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑌 ) ) ∧ ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) )
157 ovex ⊢ ( 𝑋 𝐸 𝑌 ) ∈ V
158 eqid ⊢ ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) = ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) )
159 158 elrnmpt ⊢ ( ( 𝑋 𝐸 𝑌 ) ∈ V → ( ( 𝑋 𝐸 𝑌 ) ∈ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) ↔ ∃ 𝑔 ∈ 𝑆 ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) )
160 157 159 ax-mp ⊢ ( ( 𝑋 𝐸 𝑌 ) ∈ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) ↔ ∃ 𝑔 ∈ 𝑆 ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) )
161 11 rexeqi ⊢ ( ∃ 𝑔 ∈ 𝑆 ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ↔ ∃ 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) )
162 fveq1 ⊢ ( ℎ = 𝑔 → ( ℎ ‘ 1 ) = ( 𝑔 ‘ 1 ) )
163 162 fveq2d ⊢ ( ℎ = 𝑔 → ( 1st ‘ ( ℎ ‘ 1 ) ) = ( 1st ‘ ( 𝑔 ‘ 1 ) ) )
164 163 fveqeq2d ⊢ ( ℎ = 𝑔 → ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ) )
165 fveq1 ⊢ ( ℎ = 𝑔 → ( ℎ ‘ 𝑛 ) = ( 𝑔 ‘ 𝑛 ) )
166 165 fveq2d ⊢ ( ℎ = 𝑔 → ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) = ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) )
167 166 fveqeq2d ⊢ ( ℎ = 𝑔 → ( ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ↔ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ) )
168 fveq1 ⊢ ( ℎ = 𝑔 → ( ℎ ‘ 𝑖 ) = ( 𝑔 ‘ 𝑖 ) )
169 168 fveq2d ⊢ ( ℎ = 𝑔 → ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) = ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) )
170 169 fveq2d ⊢ ( ℎ = 𝑔 → ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
171 fveq1 ⊢ ( ℎ = 𝑔 → ( ℎ ‘ ( 𝑖 + 1 ) ) = ( 𝑔 ‘ ( 𝑖 + 1 ) ) )
172 171 fveq2d ⊢ ( ℎ = 𝑔 → ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) = ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) )
173 172 fveq2d ⊢ ( ℎ = 𝑔 → ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) )
174 170 173 eqeq12d ⊢ ( ℎ = 𝑔 → ( ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ↔ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) ) )
175 174 ralbidv ⊢ ( ℎ = 𝑔 → ( ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) ) )
176 164 167 175 3anbi123d ⊢ ( ℎ = 𝑔 → ( ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) ↔ ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
177 176 rexrab ⊢ ( ∃ 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ↔ ∃ 𝑔 ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ( ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) ) ∧ ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) )
178 161 177 bitri ⊢ ( ∃ 𝑔 ∈ 𝑆 ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ↔ ∃ 𝑔 ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ( ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) ) ∧ ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) )
179 oveq2 ⊢ ( 𝑛 = 1 → ( 1 ... 𝑛 ) = ( 1 ... 1 ) )
180 1z ⊢ 1 ∈ ℤ
181 fzsn ⊢ ( 1 ∈ ℤ → ( 1 ... 1 ) = { 1 } )
182 180 181 ax-mp ⊢ ( 1 ... 1 ) = { 1 }
183 179 182 eqtrdi ⊢ ( 𝑛 = 1 → ( 1 ... 𝑛 ) = { 1 } )
184 183 oveq2d ⊢ ( 𝑛 = 1 → ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) = ( ( 𝑉 × 𝑉 ) ↑m { 1 } ) )
185 df-3an ⊢ ( ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) ) ↔ ( ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ) ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) ) )
186 ral0 ⊢ ∀ 𝑖 ∈ ∅ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) )
187 oveq1 ⊢ ( 𝑛 = 1 → ( 𝑛 − 1 ) = ( 1 − 1 ) )
188 1m1e0 ⊢ ( 1 − 1 ) = 0
189 187 188 eqtrdi ⊢ ( 𝑛 = 1 → ( 𝑛 − 1 ) = 0 )
190 189 oveq2d ⊢ ( 𝑛 = 1 → ( 1 ... ( 𝑛 − 1 ) ) = ( 1 ... 0 ) )
191 fz10 ⊢ ( 1 ... 0 ) = ∅
192 190 191 eqtrdi ⊢ ( 𝑛 = 1 → ( 1 ... ( 𝑛 − 1 ) ) = ∅ )
193 192 raleqdv ⊢ ( 𝑛 = 1 → ( ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) ↔ ∀ 𝑖 ∈ ∅ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) ) )
194 186 193 mpbiri ⊢ ( 𝑛 = 1 → ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) )
195 194 biantrud ⊢ ( 𝑛 = 1 → ( ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ) ↔ ( ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ) ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
196 2fveq3 ⊢ ( 𝑛 = 1 → ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) = ( 2nd ‘ ( 𝑔 ‘ 1 ) ) )
197 196 fveqeq2d ⊢ ( 𝑛 = 1 → ( ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ↔ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑌 ) ) )
198 197 anbi2d ⊢ ( 𝑛 = 1 → ( ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ) ↔ ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑌 ) ) ) )
199 195 198 bitr3d ⊢ ( 𝑛 = 1 → ( ( ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ) ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) ) ↔ ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑌 ) ) ) )
200 185 199 bitrid ⊢ ( 𝑛 = 1 → ( ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) ) ↔ ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑌 ) ) ) )
201 200 anbi1d ⊢ ( 𝑛 = 1 → ( ( ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) ) ∧ ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) ↔ ( ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑌 ) ) ∧ ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) ) )
202 184 201 rexeqbidv ⊢ ( 𝑛 = 1 → ( ∃ 𝑔 ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ( ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) ) ∧ ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) ↔ ∃ 𝑔 ∈ ( ( 𝑉 × 𝑉 ) ↑m { 1 } ) ( ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑌 ) ) ∧ ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) ) )
203 178 202 bitrid ⊢ ( 𝑛 = 1 → ( ∃ 𝑔 ∈ 𝑆 ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ↔ ∃ 𝑔 ∈ ( ( 𝑉 × 𝑉 ) ↑m { 1 } ) ( ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑌 ) ) ∧ ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) ) )
204 160 203 bitrid ⊢ ( 𝑛 = 1 → ( ( 𝑋 𝐸 𝑌 ) ∈ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) ↔ ∃ 𝑔 ∈ ( ( 𝑉 × 𝑉 ) ↑m { 1 } ) ( ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑌 ) ) ∧ ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) ) )
205 204 rspcev ⊢ ( ( 1 ∈ ℕ ∧ ∃ 𝑔 ∈ ( ( 𝑉 × 𝑉 ) ↑m { 1 } ) ( ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑌 ) ) ∧ ( 𝑋 𝐸 𝑌 ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) ) → ∃ 𝑛 ∈ ℕ ( 𝑋 𝐸 𝑌 ) ∈ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) )
206 84 156 205 sylancr ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ ( 𝑋 𝐸 𝑌 ) ∈ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) )
207 eliun ⊢ ( ( 𝑋 𝐸 𝑌 ) ∈ ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) ↔ ∃ 𝑛 ∈ ℕ ( 𝑋 𝐸 𝑌 ) ∈ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) )
208 206 207 sylibr ⊢ ( 𝜑 → ( 𝑋 𝐸 𝑌 ) ∈ ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) )
209 208 12 eleqtrrdi ⊢ ( 𝜑 → ( 𝑋 𝐸 𝑌 ) ∈ 𝑇 )
210 infxrlb ⊢ ( ( 𝑇 ⊆ ℝ* ∧ ( 𝑋 𝐸 𝑌 ) ∈ 𝑇 ) → inf ( 𝑇 , ℝ* , < ) ≤ ( 𝑋 𝐸 𝑌 ) )
211 79 209 210 syl2anc ⊢ ( 𝜑 → inf ( 𝑇 , ℝ* , < ) ≤ ( 𝑋 𝐸 𝑌 ) )
212 12 eleq2i ⊢ ( 𝑝 ∈ 𝑇 ↔ 𝑝 ∈ ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) )
213 eliun ⊢ ( 𝑝 ∈ ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) ↔ ∃ 𝑛 ∈ ℕ 𝑝 ∈ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) )
214 212 213 bitri ⊢ ( 𝑝 ∈ 𝑇 ↔ ∃ 𝑛 ∈ ℕ 𝑝 ∈ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) )
215 158 elrnmpt ⊢ ( 𝑝 ∈ V → ( 𝑝 ∈ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) ↔ ∃ 𝑔 ∈ 𝑆 𝑝 = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) )
216 215 elv ⊢ ( 𝑝 ∈ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) ↔ ∃ 𝑔 ∈ 𝑆 𝑝 = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) )
217 176 11 elrab2 ⊢ ( 𝑔 ∈ 𝑆 ↔ ( 𝑔 ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∧ ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
218 217 simprbi ⊢ ( 𝑔 ∈ 𝑆 → ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) ) )
219 218 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) ) )
220 219 simp2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) )
221 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
222 f1of1 ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 → 𝐹 : 𝑉 –1-1→ 𝐵 )
223 221 222 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → 𝐹 : 𝑉 –1-1→ 𝐵 )
224 simplr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → 𝑛 ∈ ℕ )
225 elfz1end ⊢ ( 𝑛 ∈ ℕ ↔ 𝑛 ∈ ( 1 ... 𝑛 ) )
226 224 225 sylib ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → 𝑛 ∈ ( 1 ... 𝑛 ) )
227 49 226 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑔 ‘ 𝑛 ) ∈ ( 𝑉 × 𝑉 ) )
228 xp2nd ⊢ ( ( 𝑔 ‘ 𝑛 ) ∈ ( 𝑉 × 𝑉 ) → ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ∈ 𝑉 )
229 227 228 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ∈ 𝑉 )
230 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → 𝑌 ∈ 𝑉 )
231 f1fveq ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝐵 ∧ ( ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ↔ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) = 𝑌 ) )
232 223 229 230 231 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ↔ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) = 𝑌 ) )
233 220 232 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) = 𝑌 )
234 233 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝑋 𝐸 𝑌 ) )
235 eleq1 ⊢ ( 𝑚 = 1 → ( 𝑚 ∈ ( 1 ... 𝑛 ) ↔ 1 ∈ ( 1 ... 𝑛 ) ) )
236 2fveq3 ⊢ ( 𝑚 = 1 → ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) = ( 2nd ‘ ( 𝑔 ‘ 1 ) ) )
237 236 oveq2d ⊢ ( 𝑚 = 1 → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ) = ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) )
238 oveq2 ⊢ ( 𝑚 = 1 → ( 1 ... 𝑚 ) = ( 1 ... 1 ) )
239 238 182 eqtrdi ⊢ ( 𝑚 = 1 → ( 1 ... 𝑚 ) = { 1 } )
240 239 reseq2d ⊢ ( 𝑚 = 1 → ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑚 ) ) = ( ( 𝐸 ∘ 𝑔 ) ↾ { 1 } ) )
241 240 oveq2d ⊢ ( 𝑚 = 1 → ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑚 ) ) ) = ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ { 1 } ) ) )
242 237 241 breq12d ⊢ ( 𝑚 = 1 → ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑚 ) ) ) ↔ ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ { 1 } ) ) ) )
243 235 242 imbi12d ⊢ ( 𝑚 = 1 → ( ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑚 ) ) ) ) ↔ ( 1 ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ { 1 } ) ) ) ) )
244 243 imbi2d ⊢ ( 𝑚 = 1 → ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑚 ) ) ) ) ) ↔ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 1 ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ { 1 } ) ) ) ) ) )
245 eleq1 ⊢ ( 𝑚 = 𝑥 → ( 𝑚 ∈ ( 1 ... 𝑛 ) ↔ 𝑥 ∈ ( 1 ... 𝑛 ) ) )
246 2fveq3 ⊢ ( 𝑚 = 𝑥 → ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) = ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) )
247 246 oveq2d ⊢ ( 𝑚 = 𝑥 → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ) = ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) )
248 oveq2 ⊢ ( 𝑚 = 𝑥 → ( 1 ... 𝑚 ) = ( 1 ... 𝑥 ) )
249 248 reseq2d ⊢ ( 𝑚 = 𝑥 → ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑚 ) ) = ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) )
250 249 oveq2d ⊢ ( 𝑚 = 𝑥 → ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑚 ) ) ) = ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) )
251 247 250 breq12d ⊢ ( 𝑚 = 𝑥 → ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑚 ) ) ) ↔ ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) ) )
252 245 251 imbi12d ⊢ ( 𝑚 = 𝑥 → ( ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑚 ) ) ) ) ↔ ( 𝑥 ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) ) ) )
253 252 imbi2d ⊢ ( 𝑚 = 𝑥 → ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑚 ) ) ) ) ) ↔ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑥 ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) ) ) ) )
254 eleq1 ⊢ ( 𝑚 = ( 𝑥 + 1 ) → ( 𝑚 ∈ ( 1 ... 𝑛 ) ↔ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) )
255 2fveq3 ⊢ ( 𝑚 = ( 𝑥 + 1 ) → ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) = ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) )
256 255 oveq2d ⊢ ( 𝑚 = ( 𝑥 + 1 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ) = ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) )
257 oveq2 ⊢ ( 𝑚 = ( 𝑥 + 1 ) → ( 1 ... 𝑚 ) = ( 1 ... ( 𝑥 + 1 ) ) )
258 257 reseq2d ⊢ ( 𝑚 = ( 𝑥 + 1 ) → ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑚 ) ) = ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... ( 𝑥 + 1 ) ) ) )
259 258 oveq2d ⊢ ( 𝑚 = ( 𝑥 + 1 ) → ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑚 ) ) ) = ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... ( 𝑥 + 1 ) ) ) ) )
260 256 259 breq12d ⊢ ( 𝑚 = ( 𝑥 + 1 ) → ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑚 ) ) ) ↔ ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... ( 𝑥 + 1 ) ) ) ) ) )
261 254 260 imbi12d ⊢ ( 𝑚 = ( 𝑥 + 1 ) → ( ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑚 ) ) ) ) ↔ ( ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... ( 𝑥 + 1 ) ) ) ) ) ) )
262 261 imbi2d ⊢ ( 𝑚 = ( 𝑥 + 1 ) → ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑚 ) ) ) ) ) ↔ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... ( 𝑥 + 1 ) ) ) ) ) ) ) )
263 eleq1 ⊢ ( 𝑚 = 𝑛 → ( 𝑚 ∈ ( 1 ... 𝑛 ) ↔ 𝑛 ∈ ( 1 ... 𝑛 ) ) )
264 2fveq3 ⊢ ( 𝑚 = 𝑛 → ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) = ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) )
265 264 oveq2d ⊢ ( 𝑚 = 𝑛 → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ) = ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) )
266 oveq2 ⊢ ( 𝑚 = 𝑛 → ( 1 ... 𝑚 ) = ( 1 ... 𝑛 ) )
267 266 reseq2d ⊢ ( 𝑚 = 𝑛 → ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑚 ) ) = ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑛 ) ) )
268 267 oveq2d ⊢ ( 𝑚 = 𝑛 → ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑚 ) ) ) = ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑛 ) ) ) )
269 265 268 breq12d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑚 ) ) ) ↔ ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑛 ) ) ) ) )
270 263 269 imbi12d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑚 ) ) ) ) ↔ ( 𝑛 ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑛 ) ) ) ) ) )
271 270 imbi2d ⊢ ( 𝑚 = 𝑛 → ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑚 ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑚 ) ) ) ) ) ↔ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑛 ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑛 ) ) ) ) ) ) )
272 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
273 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → 𝑋 ∈ 𝑉 )
274 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
275 224 274 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
276 eluzfz1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... 𝑛 ) )
277 275 276 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → 1 ∈ ( 1 ... 𝑛 ) )
278 49 277 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑔 ‘ 1 ) ∈ ( 𝑉 × 𝑉 ) )
279 xp2nd ⊢ ( ( 𝑔 ‘ 1 ) ∈ ( 𝑉 × 𝑉 ) → ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ∈ 𝑉 )
280 278 279 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ∈ 𝑉 )
281 xmetcl ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ 𝑋 ∈ 𝑉 ∧ ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ∈ 𝑉 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) ∈ ℝ* )
282 272 273 280 281 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) ∈ ℝ* )
283 282 xrleidd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) ≤ ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) )
284 137 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → 𝑊 ∈ Mnd )
285 84 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → 1 ∈ ℕ )
286 44 278 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝐸 ‘ ( 𝑔 ‘ 1 ) ) ∈ ( ℝ* ∖ { -∞ } ) )
287 2fveq3 ⊢ ( 𝑗 = 1 → ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐸 ‘ ( 𝑔 ‘ 1 ) ) )
288 64 287 gsumsn ⊢ ( ( 𝑊 ∈ Mnd ∧ 1 ∈ ℕ ∧ ( 𝐸 ‘ ( 𝑔 ‘ 1 ) ) ∈ ( ℝ* ∖ { -∞ } ) ) → ( 𝑊 Σg ( 𝑗 ∈ { 1 } ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) ) = ( 𝐸 ‘ ( 𝑔 ‘ 1 ) ) )
289 284 285 286 288 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑊 Σg ( 𝑗 ∈ { 1 } ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) ) = ( 𝐸 ‘ ( 𝑔 ‘ 1 ) ) )
290 272 30 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → 𝐸 : ( 𝑉 × 𝑉 ) ⟶ ℝ* )
291 fcompt ⊢ ( ( 𝐸 : ( 𝑉 × 𝑉 ) ⟶ ℝ* ∧ 𝑔 : ( 1 ... 𝑛 ) ⟶ ( 𝑉 × 𝑉 ) ) → ( 𝐸 ∘ 𝑔 ) = ( 𝑗 ∈ ( 1 ... 𝑛 ) ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) )
292 290 49 291 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝐸 ∘ 𝑔 ) = ( 𝑗 ∈ ( 1 ... 𝑛 ) ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) )
293 292 reseq1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( ( 𝐸 ∘ 𝑔 ) ↾ { 1 } ) = ( ( 𝑗 ∈ ( 1 ... 𝑛 ) ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) ↾ { 1 } ) )
294 277 snssd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → { 1 } ⊆ ( 1 ... 𝑛 ) )
295 294 resmptd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( ( 𝑗 ∈ ( 1 ... 𝑛 ) ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) ↾ { 1 } ) = ( 𝑗 ∈ { 1 } ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) )
296 293 295 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( ( 𝐸 ∘ 𝑔 ) ↾ { 1 } ) = ( 𝑗 ∈ { 1 } ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) )
297 296 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ { 1 } ) ) = ( 𝑊 Σg ( 𝑗 ∈ { 1 } ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) ) )
298 df-ov ⊢ ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐸 ‘ ⟨ 𝑋 , ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ⟩ )
299 1st2nd2 ⊢ ( ( 𝑔 ‘ 1 ) ∈ ( 𝑉 × 𝑉 ) → ( 𝑔 ‘ 1 ) = ⟨ ( 1st ‘ ( 𝑔 ‘ 1 ) ) , ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ⟩ )
300 278 299 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑔 ‘ 1 ) = ⟨ ( 1st ‘ ( 𝑔 ‘ 1 ) ) , ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ⟩ )
301 219 simp1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) )
302 xp1st ⊢ ( ( 𝑔 ‘ 1 ) ∈ ( 𝑉 × 𝑉 ) → ( 1st ‘ ( 𝑔 ‘ 1 ) ) ∈ 𝑉 )
303 278 302 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 1st ‘ ( 𝑔 ‘ 1 ) ) ∈ 𝑉 )
304 f1fveq ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝐵 ∧ ( ( 1st ‘ ( 𝑔 ‘ 1 ) ) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ↔ ( 1st ‘ ( 𝑔 ‘ 1 ) ) = 𝑋 ) )
305 223 303 273 304 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ↔ ( 1st ‘ ( 𝑔 ‘ 1 ) ) = 𝑋 ) )
306 301 305 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 1st ‘ ( 𝑔 ‘ 1 ) ) = 𝑋 )
307 306 opeq1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ⟨ ( 1st ‘ ( 𝑔 ‘ 1 ) ) , ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ⟩ = ⟨ 𝑋 , ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ⟩ )
308 300 307 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ⟨ 𝑋 , ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ⟩ = ( 𝑔 ‘ 1 ) )
309 308 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝐸 ‘ ⟨ 𝑋 , ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ⟩ ) = ( 𝐸 ‘ ( 𝑔 ‘ 1 ) ) )
310 298 309 eqtrid ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) = ( 𝐸 ‘ ( 𝑔 ‘ 1 ) ) )
311 289 297 310 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ { 1 } ) ) = ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) )
312 283 311 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ { 1 } ) ) )
313 312 a1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 1 ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 1 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ { 1 } ) ) ) )
314 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → 𝑥 ∈ ℕ )
315 314 274 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → 𝑥 ∈ ( ℤ≥ ‘ 1 ) )
316 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) )
317 peano2fzr ⊢ ( ( 𝑥 ∈ ( ℤ≥ ‘ 1 ) ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) → 𝑥 ∈ ( 1 ... 𝑛 ) )
318 315 316 317 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → 𝑥 ∈ ( 1 ... 𝑛 ) )
319 318 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) → 𝑥 ∈ ( 1 ... 𝑛 ) ) )
320 319 imim1d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝑥 ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) ) → ( ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) ) ) )
321 272 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
322 273 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → 𝑋 ∈ 𝑉 )
323 49 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → 𝑔 : ( 1 ... 𝑛 ) ⟶ ( 𝑉 × 𝑉 ) )
324 323 318 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑉 × 𝑉 ) )
325 xp2nd ⊢ ( ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑉 × 𝑉 ) → ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ∈ 𝑉 )
326 324 325 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ∈ 𝑉 )
327 xmetcl ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ 𝑋 ∈ 𝑉 ∧ ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ∈ 𝑉 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) ∈ ℝ* )
328 321 322 326 327 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) ∈ ℝ* )
329 66 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → 𝑊 ∈ CMnd )
330 fzfid ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 1 ... 𝑥 ) ∈ Fin )
331 51 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝐸 ∘ 𝑔 ) : ( 1 ... 𝑛 ) ⟶ ( ℝ* ∖ { -∞ } ) )
332 fzsuc ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 1 ) → ( 1 ... ( 𝑥 + 1 ) ) = ( ( 1 ... 𝑥 ) ∪ { ( 𝑥 + 1 ) } ) )
333 315 332 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 1 ... ( 𝑥 + 1 ) ) = ( ( 1 ... 𝑥 ) ∪ { ( 𝑥 + 1 ) } ) )
334 elfzuz3 ⊢ ( ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) → 𝑛 ∈ ( ℤ≥ ‘ ( 𝑥 + 1 ) ) )
335 334 ad2antll ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ ( 𝑥 + 1 ) ) )
336 fzss2 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑥 + 1 ) ) → ( 1 ... ( 𝑥 + 1 ) ) ⊆ ( 1 ... 𝑛 ) )
337 335 336 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 1 ... ( 𝑥 + 1 ) ) ⊆ ( 1 ... 𝑛 ) )
338 333 337 eqsstrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( ( 1 ... 𝑥 ) ∪ { ( 𝑥 + 1 ) } ) ⊆ ( 1 ... 𝑛 ) )
339 338 unssad ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 1 ... 𝑥 ) ⊆ ( 1 ... 𝑛 ) )
340 331 339 fssresd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) : ( 1 ... 𝑥 ) ⟶ ( ℝ* ∖ { -∞ } ) )
341 68 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → 0 ∈ V )
342 340 330 341 fdmfifsupp ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) finSupp 0 )
343 64 65 329 330 340 342 gsumcl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) ∈ ( ℝ* ∖ { -∞ } ) )
344 343 eldifad ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) ∈ ℝ* )
345 321 30 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → 𝐸 : ( 𝑉 × 𝑉 ) ⟶ ℝ* )
346 323 316 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝑔 ‘ ( 𝑥 + 1 ) ) ∈ ( 𝑉 × 𝑉 ) )
347 345 346 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ∈ ℝ* )
348 xleadd1a ⊢ ( ( ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) ∈ ℝ* ∧ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) ∈ ℝ* ∧ ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ∈ ℝ* ) ∧ ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) ) → ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) )
349 348 ex ⊢ ( ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) ∈ ℝ* ∧ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) ∈ ℝ* ∧ ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ∈ ℝ* ) → ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) → ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ) )
350 328 344 347 349 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) → ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ) )
351 xp2nd ⊢ ( ( 𝑔 ‘ ( 𝑥 + 1 ) ) ∈ ( 𝑉 × 𝑉 ) → ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ∈ 𝑉 )
352 346 351 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ∈ 𝑉 )
353 xmettri ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ∈ 𝑉 ∧ ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ∈ 𝑉 ) ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) +e ( ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ) )
354 321 322 352 326 353 syl13anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) +e ( ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ) )
355 1st2nd2 ⊢ ( ( 𝑔 ‘ ( 𝑥 + 1 ) ) ∈ ( 𝑉 × 𝑉 ) → ( 𝑔 ‘ ( 𝑥 + 1 ) ) = ⟨ ( 1st ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) , ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ⟩ )
356 346 355 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝑔 ‘ ( 𝑥 + 1 ) ) = ⟨ ( 1st ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) , ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ⟩ )
357 2fveq3 ⊢ ( 𝑖 = 𝑥 → ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) )
358 357 fveq2d ⊢ ( 𝑖 = 𝑥 → ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) )
359 fvoveq1 ⊢ ( 𝑖 = 𝑥 → ( 𝑔 ‘ ( 𝑖 + 1 ) ) = ( 𝑔 ‘ ( 𝑥 + 1 ) ) )
360 359 fveq2d ⊢ ( 𝑖 = 𝑥 → ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) = ( 1st ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) )
361 360 fveq2d ⊢ ( 𝑖 = 𝑥 → ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) )
362 358 361 eqeq12d ⊢ ( 𝑖 = 𝑥 → ( ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) ↔ ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ) )
363 219 simp3d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) )
364 363 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑖 + 1 ) ) ) ) )
365 nnz ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℤ )
366 365 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → 𝑥 ∈ ℤ )
367 eluzp1m1 ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑥 + 1 ) ) ) → ( 𝑛 − 1 ) ∈ ( ℤ≥ ‘ 𝑥 ) )
368 366 335 367 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝑛 − 1 ) ∈ ( ℤ≥ ‘ 𝑥 ) )
369 elfzuzb ⊢ ( 𝑥 ∈ ( 1 ... ( 𝑛 − 1 ) ) ↔ ( 𝑥 ∈ ( ℤ≥ ‘ 1 ) ∧ ( 𝑛 − 1 ) ∈ ( ℤ≥ ‘ 𝑥 ) ) )
370 315 368 369 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → 𝑥 ∈ ( 1 ... ( 𝑛 − 1 ) ) )
371 362 364 370 rspcdva ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) )
372 223 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → 𝐹 : 𝑉 –1-1→ 𝐵 )
373 xp1st ⊢ ( ( 𝑔 ‘ ( 𝑥 + 1 ) ) ∈ ( 𝑉 × 𝑉 ) → ( 1st ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ∈ 𝑉 )
374 346 373 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 1st ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ∈ 𝑉 )
375 f1fveq ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝐵 ∧ ( ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ∈ 𝑉 ∧ ( 1st ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ∈ 𝑉 ) ) → ( ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ↔ ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) = ( 1st ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) )
376 372 326 374 375 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( ( 𝐹 ‘ ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ↔ ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) = ( 1st ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) )
377 371 376 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) = ( 1st ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) )
378 377 opeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ⟨ ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) , ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ⟩ = ⟨ ( 1st ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) , ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ⟩ )
379 356 378 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝑔 ‘ ( 𝑥 + 1 ) ) = ⟨ ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) , ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ⟩ )
380 379 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) = ( 𝐸 ‘ ⟨ ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) , ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) )
381 df-ov ⊢ ( ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) = ( 𝐸 ‘ ⟨ ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) , ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ⟩ )
382 380 381 eqtr4di ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) = ( ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) )
383 382 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) = ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) +e ( ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ) )
384 354 383 breqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) )
385 xmetcl ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ 𝑋 ∈ 𝑉 ∧ ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ∈ 𝑉 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ∈ ℝ* )
386 321 322 352 385 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ∈ ℝ* )
387 328 347 xaddcld ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ∈ ℝ* )
388 344 347 xaddcld ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ∈ ℝ* )
389 xrletr ⊢ ( ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ∈ ℝ* ∧ ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ∈ ℝ* ∧ ( ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ∈ ℝ* ) → ( ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ∧ ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ) )
390 386 387 388 389 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ∧ ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ) )
391 384 390 mpand ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ) )
392 350 391 syld ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ) )
393 xrex ⊢ ℝ* ∈ V
394 393 difexi ⊢ ( ℝ* ∖ { -∞ } ) ∈ V
395 10 24 ressplusg ⊢ ( ( ℝ* ∖ { -∞ } ) ∈ V → +e = ( +g ‘ 𝑊 ) )
396 394 395 ax-mp ⊢ +e = ( +g ‘ 𝑊 )
397 44 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑥 ) ) → 𝐸 : ( 𝑉 × 𝑉 ) ⟶ ( ℝ* ∖ { -∞ } ) )
398 fzelp1 ⊢ ( 𝑗 ∈ ( 1 ... 𝑥 ) → 𝑗 ∈ ( 1 ... ( 𝑥 + 1 ) ) )
399 49 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑥 + 1 ) ) ) → 𝑔 : ( 1 ... 𝑛 ) ⟶ ( 𝑉 × 𝑉 ) )
400 337 sselda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑥 + 1 ) ) ) → 𝑗 ∈ ( 1 ... 𝑛 ) )
401 399 400 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑥 + 1 ) ) ) → ( 𝑔 ‘ 𝑗 ) ∈ ( 𝑉 × 𝑉 ) )
402 398 401 sylan2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑥 ) ) → ( 𝑔 ‘ 𝑗 ) ∈ ( 𝑉 × 𝑉 ) )
403 397 402 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑥 ) ) → ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ∈ ( ℝ* ∖ { -∞ } ) )
404 fzp1disj ⊢ ( ( 1 ... 𝑥 ) ∩ { ( 𝑥 + 1 ) } ) = ∅
405 404 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( ( 1 ... 𝑥 ) ∩ { ( 𝑥 + 1 ) } ) = ∅ )
406 disjsn ⊢ ( ( ( 1 ... 𝑥 ) ∩ { ( 𝑥 + 1 ) } ) = ∅ ↔ ¬ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑥 ) )
407 405 406 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ¬ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑥 ) )
408 44 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → 𝐸 : ( 𝑉 × 𝑉 ) ⟶ ( ℝ* ∖ { -∞ } ) )
409 408 346 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ∈ ( ℝ* ∖ { -∞ } ) )
410 2fveq3 ⊢ ( 𝑗 = ( 𝑥 + 1 ) → ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) )
411 64 396 329 330 403 316 407 409 410 gsumunsn ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝑊 Σg ( 𝑗 ∈ ( ( 1 ... 𝑥 ) ∪ { ( 𝑥 + 1 ) } ) ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) ) = ( ( 𝑊 Σg ( 𝑗 ∈ ( 1 ... 𝑥 ) ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) )
412 292 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝐸 ∘ 𝑔 ) = ( 𝑗 ∈ ( 1 ... 𝑛 ) ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) )
413 412 333 reseq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... ( 𝑥 + 1 ) ) ) = ( ( 𝑗 ∈ ( 1 ... 𝑛 ) ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) ↾ ( ( 1 ... 𝑥 ) ∪ { ( 𝑥 + 1 ) } ) ) )
414 338 resmptd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( ( 𝑗 ∈ ( 1 ... 𝑛 ) ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) ↾ ( ( 1 ... 𝑥 ) ∪ { ( 𝑥 + 1 ) } ) ) = ( 𝑗 ∈ ( ( 1 ... 𝑥 ) ∪ { ( 𝑥 + 1 ) } ) ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) )
415 413 414 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... ( 𝑥 + 1 ) ) ) = ( 𝑗 ∈ ( ( 1 ... 𝑥 ) ∪ { ( 𝑥 + 1 ) } ) ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) )
416 415 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... ( 𝑥 + 1 ) ) ) ) = ( 𝑊 Σg ( 𝑗 ∈ ( ( 1 ... 𝑥 ) ∪ { ( 𝑥 + 1 ) } ) ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) ) )
417 412 reseq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) = ( ( 𝑗 ∈ ( 1 ... 𝑛 ) ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) ↾ ( 1 ... 𝑥 ) ) )
418 339 resmptd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( ( 𝑗 ∈ ( 1 ... 𝑛 ) ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) ↾ ( 1 ... 𝑥 ) ) = ( 𝑗 ∈ ( 1 ... 𝑥 ) ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) )
419 417 418 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) = ( 𝑗 ∈ ( 1 ... 𝑥 ) ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) )
420 419 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) = ( 𝑊 Σg ( 𝑗 ∈ ( 1 ... 𝑥 ) ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) ) )
421 420 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) = ( ( 𝑊 Σg ( 𝑗 ∈ ( 1 ... 𝑥 ) ↦ ( 𝐸 ‘ ( 𝑔 ‘ 𝑗 ) ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) )
422 411 416 421 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... ( 𝑥 + 1 ) ) ) ) = ( ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) )
423 422 breq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... ( 𝑥 + 1 ) ) ) ) ↔ ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) +e ( 𝐸 ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ) )
424 392 423 sylibrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ℕ ∧ ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) ) ) → ( ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... ( 𝑥 + 1 ) ) ) ) ) )
425 320 424 animpimp2impd ⊢ ( 𝑥 ∈ ℕ → ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑥 ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑥 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑥 ) ) ) ) ) → ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( ( 𝑥 + 1 ) ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... ( 𝑥 + 1 ) ) ) ) ) ) ) )
426 244 253 262 271 313 425 nnind ⊢ ( 𝑛 ∈ ℕ → ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑛 ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑛 ) ) ) ) ) )
427 224 426 mpcom ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑛 ∈ ( 1 ... 𝑛 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑛 ) ) ) ) )
428 226 427 mpd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑋 𝐸 ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑛 ) ) ) )
429 234 428 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑋 𝐸 𝑌 ) ≤ ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑛 ) ) ) )
430 ffn ⊢ ( ( 𝐸 ∘ 𝑔 ) : ( 1 ... 𝑛 ) ⟶ ( ℝ* ∖ { -∞ } ) → ( 𝐸 ∘ 𝑔 ) Fn ( 1 ... 𝑛 ) )
431 fnresdm ⊢ ( ( 𝐸 ∘ 𝑔 ) Fn ( 1 ... 𝑛 ) → ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑛 ) ) = ( 𝐸 ∘ 𝑔 ) )
432 51 430 431 3syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑛 ) ) = ( 𝐸 ∘ 𝑔 ) )
433 432 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑛 ) ) ) = ( 𝑊 Σg ( 𝐸 ∘ 𝑔 ) ) )
434 62 433 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) = ( 𝑊 Σg ( ( 𝐸 ∘ 𝑔 ) ↾ ( 1 ... 𝑛 ) ) ) )
435 429 434 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑋 𝐸 𝑌 ) ≤ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) )
436 breq2 ⊢ ( 𝑝 = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) → ( ( 𝑋 𝐸 𝑌 ) ≤ 𝑝 ↔ ( 𝑋 𝐸 𝑌 ) ≤ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) )
437 435 436 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑝 = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) → ( 𝑋 𝐸 𝑌 ) ≤ 𝑝 ) )
438 437 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∃ 𝑔 ∈ 𝑆 𝑝 = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) → ( 𝑋 𝐸 𝑌 ) ≤ 𝑝 ) )
439 216 438 biimtrid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑝 ∈ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) → ( 𝑋 𝐸 𝑌 ) ≤ 𝑝 ) )
440 439 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℕ 𝑝 ∈ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) → ( 𝑋 𝐸 𝑌 ) ≤ 𝑝 ) )
441 214 440 biimtrid ⊢ ( 𝜑 → ( 𝑝 ∈ 𝑇 → ( 𝑋 𝐸 𝑌 ) ≤ 𝑝 ) )
442 441 ralrimiv ⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝑇 ( 𝑋 𝐸 𝑌 ) ≤ 𝑝 )
443 infxrgelb ⊢ ( ( 𝑇 ⊆ ℝ* ∧ ( 𝑋 𝐸 𝑌 ) ∈ ℝ* ) → ( ( 𝑋 𝐸 𝑌 ) ≤ inf ( 𝑇 , ℝ* , < ) ↔ ∀ 𝑝 ∈ 𝑇 ( 𝑋 𝐸 𝑌 ) ≤ 𝑝 ) )
444 79 83 443 syl2anc ⊢ ( 𝜑 → ( ( 𝑋 𝐸 𝑌 ) ≤ inf ( 𝑇 , ℝ* , < ) ↔ ∀ 𝑝 ∈ 𝑇 ( 𝑋 𝐸 𝑌 ) ≤ 𝑝 ) )
445 442 444 mpbird ⊢ ( 𝜑 → ( 𝑋 𝐸 𝑌 ) ≤ inf ( 𝑇 , ℝ* , < ) )
446 81 83 211 445 xrletrid ⊢ ( 𝜑 → inf ( 𝑇 , ℝ* , < ) = ( 𝑋 𝐸 𝑌 ) )
447 22 446 eqtrd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) 𝐷 ( 𝐹 ‘ 𝑌 ) ) = ( 𝑋 𝐸 𝑌 ) )