# 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 ${⊢}{\phi }\to {U}={F}{“}_{𝑠}{R}$
imasdsf1o.v ${⊢}{\phi }\to {V}={\mathrm{Base}}_{{R}}$
imasdsf1o.f ${⊢}{\phi }\to {F}:{V}\underset{1-1 onto}{⟶}{B}$
imasdsf1o.r ${⊢}{\phi }\to {R}\in {Z}$
imasdsf1o.e ${⊢}{E}={\mathrm{dist}\left({R}\right)↾}_{\left({V}×{V}\right)}$
imasdsf1o.d ${⊢}{D}=\mathrm{dist}\left({U}\right)$
imasdsf1o.m ${⊢}{\phi }\to {E}\in \mathrm{\infty Met}\left({V}\right)$
imasdsf1o.x ${⊢}{\phi }\to {X}\in {V}$
imasdsf1o.y ${⊢}{\phi }\to {Y}\in {V}$
imasdsf1o.w ${⊢}{W}={ℝ}_{𝑠}^{*}{↾}_{𝑠}\left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)$
imasdsf1o.s ${⊢}{S}=\left\{{h}\in \left({\left({V}×{V}\right)}^{\left(1\dots {n}\right)}\right)|\left({F}\left({1}^{st}\left({h}\left(1\right)\right)\right)={F}\left({X}\right)\wedge {F}\left({2}^{nd}\left({h}\left({n}\right)\right)\right)={F}\left({Y}\right)\wedge \forall {i}\in \left(1\dots {n}-1\right)\phantom{\rule{.4em}{0ex}}{F}\left({2}^{nd}\left({h}\left({i}\right)\right)\right)={F}\left({1}^{st}\left({h}\left({i}+1\right)\right)\right)\right)\right\}$
imasdsf1o.t ${⊢}{T}=\bigcup _{{n}\in ℕ}\mathrm{ran}\left({g}\in {S}⟼{\sum }_{{ℝ}_{𝑠}^{*}}\left({E}\circ {g}\right)\right)$
Assertion imasdsf1olem ${⊢}{\phi }\to {F}\left({X}\right){D}{F}\left({Y}\right)={X}{E}{Y}$

### Proof

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