Metamath Proof Explorer Home Metamath Proof Explorer
Most Recent Proofs
 
Mirrors  >  Home  >  MPE Home  >  Th. List  >  Recent Other  >  MM 100

Most recent proofs    These are the 10 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the set.mm database for the Metamath Proof Explorer (and the Hilbert Space Explorer). The set.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from develop commit 8ef0caf, also available here: set.mm (32MB) or set.mm.bz2 (compressed, 9MB).

The original proofs of theorems with recently shortened proofs can often be found by appending "OLD" to the theorem name, for example 19.43OLD for 19.43.

Other links    Email: Norm Megill.    Mailing list: Metamath Google Group Updated 12-Apr-2018 .    Syndication: RSS feed (courtesy of Dan Getz).    Related wikis: Wikiproofs (JHilbert) (Recent Changes); Ghilbert site; Ghilbert Google Group.

Recent news items    (11-Apr-2018) Benoît Jubin solved an open problem about the "Axiom of Twoness", showing that it is necessary for completeness. See item 14 on the "Open problems and miscellany" page.

(30-Mar-2018) Filip Cernatescu's Milpgame has been updated to version 0.6, which reduces the set.mm load time to about 40 seconds. A new how-to has also been added to its web page.

(25-Mar-2018) Giovanni Mascellani has announced mmpp, a new proof editing environment for the Metamath language.

(27-Feb-2018) Bill Hale has released an app for the Apple iPad and desktop computer that allows you to browse Metamath theorems and their proofs.

(17-Jan-2018) Dylan Houlihan has kindly provided a new mirror site. He has also provided an rsync server; type "rsync uk.metamath.org::" in a bash shell to check its status (it should return "metamath metamath").

(15-Jan-2018) The metamath program, version 0.157, has been updated to implement the file inclusion conventions described in the 21-Dec-2017 entry of mmnotes.txt.

(11-Dec-2017) I added a paragraph, suggested by Gérard Lang, to the distinct variable description here.

(10-Dec-2017) Per FL's request, his mathbox will be removed from set.mm. If you wish to export any of his theorems, today's version (master commit 1024a3a) is the last one that will contain it.

(11-Nov-2017) Alan Sare updated his completeusersproof program.

(3-Oct-2017) Sean B. Palmer created a web page that runs the metamath program under emulated Linux in JavaScript. He also wrote some programs to work with our shortest known proofs of the PM propositional calculus theorems.

(28-Sep-2017) Ivan Kuckir wrote a tutorial blog entry, Introduction to Metamath, that summarizes the language syntax. (It may have been written some time ago, but I was not aware of it before.)

(26-Sep-2017) The default directory for the Metamath Proof Explorer (MPE) has been changed from the GIF version (mpegif) to the Unicode version (mpeuni) throughout the site. Please let me know if you find broken links or other issues.

(24-Sep-2017) Saveliy Skresanov added a new proof to the 100 theorem list, Ceva's Theorem cevath, bringing the Metamath total to 67.

(3-Sep-2017) Brendan Leahy added a new proof to the 100 theorem list, Area of a Circle areacirc, bringing the Metamath total to 66.

(7-Aug-2017) Mario Carneiro added a new proof to the 100 theorem list, Principle of Inclusion/Exclusion incexc, bringing the Metamath total to 65.

(1-Jul-2017) Glauco Siliprandi added a new proof to the 100 theorem list, Stirling's Formula stirling, bringing the Metamath total to 64. Related theorems include 2 versions of Wallis' formula for π (wallispi and wallispi2).

(7-May-2017) Thierry Arnoux added a new proof to the 100 theorem list, Betrand's Ballot Problem ballotth, bringing the Metamath total to 63.

(20-Apr-2017) Glauco Siliprandi added a new proof in the supplementary list on the 100 theorem list, Stone-Weierstrass Theorem stowei.

(28-Feb-2017) David Moews added a new proof to the 100 theorem list, Product of Segments of Chords chordthm, bringing the Metamath total to 62.    Older news...

Color key:   Metamath Proof Explorer  Metamath Proof Explorer   Hilbert Space Explorer  Hilbert Space Explorer   User Mathboxes  User Mathboxes  

Last updated on 16-Apr-2018 at 7:25 PM ET.
Recent Additions to the Metamath Proof Explorer   Notes (last updated 1-Jan-2018 )
DateLabelDescription
Theorem
 
15-Apr-2018equveli 2042 A variable elimination law for equality with no distinct variable requirements. (Compare equvini 2040.) (Contributed by NM, 1-Mar-2013.) (Proof shortened by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 15-Apr-2018.)
 |-  ( A. z ( z  =  x  <->  z  =  y
 )  ->  x  =  y )
 
7-Apr-2018swrd0swrd0 28014 A prefix of a prefix. (Contributed by Alexander van der Vekens, 7-Apr-2018.)
 |-  (
 ( W  e. Word  V  /\  N  e.  ( 0
 ... ( # `  W ) )  /\  L  e.  ( 0 ... N ) )  ->  ( ( W substr  <. 0 ,  N >. ) substr  <. 0 ,  L >. )  =  ( W substr  <. 0 ,  L >. ) )
 
7-Apr-20182elfz3nn0 27984 If there are two elements in a finite set of sequential integers from 0, these two elements as well as the upper bound are nonnegative integers. (Contributed by Alexander van der Vekens, 7-Apr-2018.)
 |-  (
 ( A  e.  (
 0 ... N )  /\  B  e.  ( 0 ... N ) )  ->  ( A  e.  NN0  /\  B  e.  NN0  /\  N  e.  NN0 ) )
 
7-Apr-2018equvini 2040 A variable introduction law for equality. Lemma 15 of [Monk2] p. 109, however we do not require  z to be distinct from  x and  y (making the proof longer). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 7-Apr-2018.)
 |-  ( x  =  y 
 ->  E. z ( x  =  z  /\  z  =  y ) )
 
6-Apr-2018swrdswrd0 28013 A subword of a prefix. (Contributed by Alexander van der Vekens, 6-Apr-2018.)
 |-  (
 ( W  e. Word  V  /\  N  e.  ( 0
 ... ( # `  W ) ) )  ->  ( ( K  e.  ( 0 ... N )  /\  L  e.  ( K ... N ) ) 
 ->  ( ( W substr  <. 0 ,  N >. ) substr  <. K ,  L >. )  =  ( W substr  <. K ,  L >. ) ) )
 
6-Apr-20180elfz 27983 0 is an element of a finite set of sequential integers from 0 to a nonnegative integer. (Contributed by Alexander van der Vekens, 6-Apr-2018.)
 |-  ( N  e.  NN0  ->  0  e.  ( 0 ... N ) )
 
6-Apr-2018nn0resubcl 27975 Closure law for subtraction of reals, restricted to nonnnegative integers. (Contributed by Alexander van der Vekens, 6-Apr-2018.)
 |-  (
 ( A  e.  NN0  /\  B  e.  NN0 )  ->  ( A  -  B )  e.  RR )
 
6-Apr-2018nn0readdcl 27974 Closure law for addition of reals, restricted to nonnnegative integers. (Contributed by Alexander van der Vekens, 6-Apr-2018.)
 |-  (
 ( A  e.  NN0  /\  B  e.  NN0 )  ->  ( A  +  B )  e.  RR )
 
6-Apr-2018ltsubnn0 27973 Subtracting a nonnegative integer from a nonnegative integer which is greater than the first one results in a nonnegative integer. (Contributed by Alexander van der Vekens, 6-Apr-2018.)
 |-  (
 ( A  e.  NN0  /\  B  e.  NN0 )  ->  ( B  <  A  ->  ( A  -  B )  e.  NN0 ) )
 
6-Apr-2018lesubnn0 27972 Subtracting a nonnegative integer from a nonnegative integer which is greater than or equal to the first one results in a nonnegative integer. (Contributed by Alexander van der Vekens, 6-Apr-2018.)
 |-  (
 ( A  e.  NN0  /\  B  e.  NN0 )  ->  ( B  <_  A  ->  ( A  -  B )  e.  NN0 ) )
 
5-Apr-2018swrdccatin12c 28028 The subword of a concatenation of two words within both of the concatenated words. REMARK: Maybe this can be proven directly, without using swrdccatin12 28026 (this would be a special case of the current theorem) and swrdccatin12b 28027 (this would be obsolete then). (Contributed by Alexander van der Vekens, 5-Apr-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( V  e.  X  /\  A  e. Word  V  /\  B  e. Word  V )  ->  ( ( M  e.  ( 0 ... L )  /\  N  e.  ( L ... ( L  +  ( # `  B ) ) ) )  ->  ( ( A concat  B ) substr 
 <. M ,  N >. )  =  ( ( A substr  <. M ,  L >. ) concat 
 ( B substr  <. 0 ,  ( N  -  L ) >. ) ) ) )
 
5-Apr-2018swrdccatin12b 28027 The subword of a concatenation of two words within both of the concatenated words. REMARK: If swrdccatin12c 28028 is proven directly, this theorem would be obsolete then). (Contributed by Alexander van der Vekens, 5-Apr-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( V  e.  X  /\  A  e. Word  V  /\  B  e. Word  V )  ->  ( ( M  e.  ( 0 ... L )  /\  N  e.  (
 ( L  +  1 ) ... ( L  +  ( # `  B ) ) ) ) 
 ->  ( ( A concat  B ) substr 
 <. M ,  N >. )  =  ( ( A substr  <. M ,  L >. ) concat 
 ( B substr  <. 0 ,  ( N  -  L ) >. ) ) ) )
 
5-Apr-2018swrd0swrdid 28012 A prefix of a prefix with the same length is the prefix. (Contributed by Alexander van der Vekens, 5-Apr-2018.)
 |-  (
 ( W  e. Word  V  /\  N  e.  ( 0
 ... ( # `  W ) ) )  ->  ( ( W substr  <. 0 ,  N >. ) substr  <. 0 ,  N >. )  =  ( W substr  <. 0 ,  N >. ) )
 
5-Apr-2018swrdrlen 28003 Length of a right-anchored subword. (Contributed by Alexander van der Vekens, 5-Apr-2018.)
 |-  (
 ( S  e. Word  A  /\  F  e.  ( 0
 ... ( # `  S ) ) )  ->  ( # `  ( S substr  <. F ,  ( # `  S ) >. ) )  =  ( ( # `  S )  -  F ) )
 
4-Apr-2018swrdswrd 28011 A subword of a subword. (Contributed by Alexander van der Vekens, 4-Apr-2018.)
 |-  (
 ( W  e. Word  V  /\  N  e.  ( 0
 ... ( # `  W ) )  /\  M  e.  ( 0 ... N ) )  ->  ( ( K  e.  ( 0
 ... ( N  -  M ) )  /\  L  e.  ( K ... ( N  -  M ) ) )  ->  ( ( W substr  <. M ,  N >. ) substr  <. K ,  L >. )  =  ( W substr  <. ( M  +  K ) ,  ( M  +  L ) >. ) ) )
 
4-Apr-2018swrdswrdlem 28010 Lemma for swrdswrd 28011. (Contributed by Alexander van der Vekens, 4-Apr-2018.)
 |-  (
 ( ( W  e. Word  V 
 /\  N  e.  (
 0 ... ( # `  W ) )  /\  M  e.  ( 0 ... N ) )  /\  ( K  e.  ( 0 ... ( N  -  M ) )  /\  L  e.  ( K ... ( N  -  M ) ) ) )  ->  ( W  e. Word  V  /\  ( M  +  K )  e.  ( 0 ... ( M  +  L )
 )  /\  ( M  +  L )  e.  (
 0 ... ( # `  W ) ) ) )
 
4-Apr-2018cnambfre 26154 A real-valued, a.e. continuous function is measurable. (Contributed by Brendan Leahy, 4-Apr-2018.)
 |-  (
 ( F : A --> RR  /\  A  e.  dom  vol  /\  ( vol * `  ( A  \  ( ( `' ( ( ( topGen `  ran  (,) )t  A )  CnP  ( topGen `
  ran  (,) ) )  o.  _E  ) " { F } ) ) )  =  0 ) 
 ->  F  e. MblFn )
 
3-Apr-2018elfzelfzelfz 27981 En element of a finite set of sequential integers is an element of a finite set of sequential integers with the upper bound being an element of the finite set of sequential integers with the same lower bound as for the first interval and the element under consideration as upper bound. (Contributed by Alexander van der Vekens, 3-Apr-2018.)
 |-  (
 ( K  e.  (
 0 ... N )  /\  L  e.  ( K ... N ) )  ->  K  e.  ( 0 ... L ) )
 
3-Apr-2018zletr 27980 Transitive law of ordering for integers. (Contributed by Alexander van der Vekens, 3-Apr-2018.)
 |-  (
 ( J  e.  ZZ  /\  K  e.  ZZ  /\  L  e.  ZZ )  ->  ( ( J  <_  K 
 /\  K  <_  L )  ->  J  <_  L ) )
 
3-Apr-2018itgaddnclem2 26163 Lemma for itgaddnc 26164; cf. itgaddlem2 19668. (Contributed by Brendan Leahy, 10-Nov-2017.) (Revised by Brendan Leahy, 3-Apr-2018.)
 |-  (
 ( ph  /\  x  e.  A )  ->  B  e.  V )   &    |-  ( ph  ->  ( x  e.  A  |->  B )  e.  L ^1 )   &    |-  ( ( ph  /\  x  e.  A ) 
 ->  C  e.  V )   &    |-  ( ph  ->  ( x  e.  A  |->  C )  e.  L ^1 )   &    |-  ( ph  ->  ( x  e.  A  |->  ( B  +  C ) )  e. MblFn
 )   &    |-  ( ( ph  /\  x  e.  A )  ->  B  e.  RR )   &    |-  ( ( ph  /\  x  e.  A ) 
 ->  C  e.  RR )   =>    |-  ( ph  ->  S. A ( B  +  C )  _d x  =  ( S. A B  _d x  +  S. A C  _d x ) )
 
2-Apr-2018swrd0swrd 28009 A prefix of a subword. (Contributed by Alexander van der Vekens, 2-Apr-2018.)
 |-  (
 ( W  e. Word  V  /\  N  e.  ( 0
 ... ( # `  W ) )  /\  M  e.  ( 0 ... N ) )  ->  ( L  e.  ( 0 ... ( N  -  M ) )  ->  ( ( W substr  <. M ,  N >. ) substr  <. 0 ,  L >. )  =  ( W substr  <. M ,  ( M  +  L ) >. ) ) )
 
2-Apr-2018nn0fz0 27979 Nonnegative integers expressed in terms of finite sets of sequential integers with lower bound 0. (Contributed by Alexander van der Vekens, 2-Apr-2018.)
 |-  ( N  e.  NN0  <->  N  e.  (
 0 ... N ) )
 
2-Apr-2018mbfposadd 26153 If the sum of two measurable functions is measurable, the sum of their nonnegative parts is measurable. (Contributed by Brendan Leahy, 2-Apr-2018.)
 |-  ( ph  ->  ( x  e.  A  |->  B )  e. MblFn
 )   &    |-  ( ( ph  /\  x  e.  A )  ->  B  e.  RR )   &    |-  ( ph  ->  ( x  e.  A  |->  C )  e. MblFn )   &    |-  ( ( ph  /\  x  e.  A ) 
 ->  C  e.  RR )   &    |-  ( ph  ->  ( x  e.  A  |->  ( B  +  C ) )  e. MblFn
 )   =>    |-  ( ph  ->  ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0 
 <_  C ,  C , 
 0 ) ) )  e. MblFn )
 
1-Apr-2018lenrevcctswrd 28005 The length of two reversely concatenated parts of a word is the length of the word. (Contributed by Alexander van der Vekens, 1-Apr-2018.)
 |-  (
 ( W  e. Word  V  /\  M  e.  ( 0
 ... ( # `  W ) ) )  ->  ( # `  ( ( W substr  <. M ,  ( # `
  W ) >. ) concat 
 ( W substr  <. 0 ,  M >. ) ) )  =  ( # `  W ) )
 
1-Apr-2018addlenrevswrd 28004 The sum of the lengths of two parts of a word is the length of the word. (Contributed by Alexander van der Vekens, 1-Apr-2018.)
 |-  (
 ( W  e. Word  V  /\  M  e.  ( 0
 ... ( # `  W ) ) )  ->  ( ( # `  ( W substr 
 <. M ,  ( # `  W ) >. ) )  +  ( # `  ( W substr 
 <. 0 ,  M >. ) ) )  =  ( # `  W ) )
 
31-Mar-2018swrdccat3b 28031 A suffix of a concatenation is either a suffix of the second concatenated word or a concatenation of a suffix of the first word with the second word. (Contributed by Alexander van der Vekens, 31-Mar-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( V  e.  X  /\  A  e. Word  V  /\  B  e. Word  V )  ->  ( M  e.  (
 0 ... ( L  +  ( # `  B ) ) )  ->  (
 ( A concat  B ) substr  <. M ,  ( L  +  ( # `  B ) ) >. )  =  if ( L  <_  M ,  ( B substr  <. ( M  -  L ) ,  ( # `  B ) >. ) ,  (
 ( A substr  <. M ,  L >. ) concat  B )
 ) ) )
 
31-Mar-2018swrdccat3a 28030 A prefix of a concatenation is either a prefix of the first concatenated word or a concatenation of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 31-Mar-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( V  e.  X  /\  A  e. Word  V  /\  B  e. Word  V )  ->  ( N  e.  (
 0 ... ( L  +  ( # `  B ) ) )  ->  (
 ( A concat  B ) substr  <.
 0 ,  N >. )  =  if ( N 
 <_  L ,  ( A substr  <. 0 ,  N >. ) ,  ( A concat  ( B substr 
 <. 0 ,  ( N  -  L ) >. ) ) ) ) )
 
31-Mar-2018swrd0 28002 A subword of an empty set is always the empty set. REMARK: The antecedent  ( F  e.  ZZ  /\  L  e.  ZZ ) should not be necessary! (Contributed by Alexander van der Vekens, 31-Mar-2018.)
 |-  (
 ( F  e.  ZZ  /\  L  e.  ZZ )  ->  ( (/) substr  <. F ,  L >. )  =  (/) )
 
31-Mar-2018mbfresfi 26152 Measurability of a piecewise function across arbitrarily many subsets. (Contributed by Brendan Leahy, 31-Mar-2018.)
 |-  ( ph  ->  F : A --> CC )   &    |-  ( ph  ->  S  e.  Fin )   &    |-  ( ph  ->  A. s  e.  S  ( F  |`  s )  e. MblFn )   &    |-  ( ph  ->  U. S  =  A )   =>    |-  ( ph  ->  F  e. MblFn )
 
30-Mar-2018swrdccat3 28029 The subword of a concatenation is either a subword of the first concatenated word or a subword of the second concatenated word or a concatenation of a suffix of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 30-Mar-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( V  e.  X  /\  A  e. Word  V  /\  B  e. Word  V )  ->  ( ( M  e.  ( 0 ... N )  /\  N  e.  (
 0 ... ( L  +  ( # `  B ) ) ) )  ->  ( ( A concat  B ) substr 
 <. M ,  N >. )  =  if ( N 
 <_  L ,  ( A substr  <. M ,  N >. ) ,  if ( L 
 <_  M ,  ( B substr  <. ( M  -  L ) ,  ( N  -  L ) >. ) ,  ( ( A substr  <. M ,  L >. ) concat  ( B substr  <.
 0 ,  ( N  -  L ) >. ) ) ) ) ) )
 
30-Mar-2018swrdccatin12 28026 The subword of a concatenation of two words within both of the concatenated words. REMARK: If swrdccatin12c 28028 is proven directly, this theorem would be special case of swrdccatin12c 28028). (Contributed by Alexander van der Vekens, 30-Mar-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( V  e.  X  /\  A  e. Word  V  /\  B  e. Word  V )  ->  ( ( M  e.  ( 0..^ L )  /\  N  e.  ( ( L  +  1 ) ... ( L  +  ( # `
  B ) ) ) )  ->  (
 ( A concat  B ) substr  <. M ,  N >. )  =  ( ( A substr  <. M ,  L >. ) concat 
 ( B substr  <. 0 ,  ( N  -  L ) >. ) ) ) )
 
30-Mar-2018swrdccatin12lem4 28025 Lemma 4 for swrdccatin12 28026. (Contributed by Alexander van der Vekens, 30-Mar-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( ( V  e.  X  /\  A  e. Word  V  /\  B  e. Word  V )  /\  ( M  e.  ( 0..^ L )  /\  N  e.  (
 ( L  +  1 ) ... ( L  +  ( # `  B ) ) ) ) )  ->  ( ( K  e.  ( 0..^ ( N  -  M ) )  /\  K  e.  ( 0..^ ( L  -  M ) ) ) 
 ->  ( ( ( A concat  B ) substr  <. M ,  N >. ) `  K )  =  ( ( A substr 
 <. M ,  L >. ) `
  K ) ) )
 
30-Mar-2018swrdccatin12lem3 28024 Lemma 3 for swrdccatin12 28026. (Contributed by Alexander van der Vekens, 30-Mar-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( ( V  e.  X  /\  A  e. Word  V  /\  B  e. Word  V )  /\  ( M  e.  ( 0..^ L )  /\  N  e.  (
 ( L  +  1 ) ... ( L  +  ( # `  B ) ) ) ) )  ->  ( ( K  e.  ( 0..^ ( N  -  M ) )  /\  -.  K  e.  ( 0..^ ( L  -  M ) ) )  ->  ( (
 ( A concat  B ) substr  <. M ,  N >. ) `
  K )  =  ( ( B substr  <. 0 ,  ( N  -  L ) >. ) `  ( K  -  ( # `  ( A substr 
 <. M ,  L >. ) ) ) ) ) )
 
30-Mar-2018swrdccatin12lem3c 28023 Lemma for swrdccatin12lem3 28024 and swrdccatin12lem4 28025. (Contributed by Alexander van der Vekens, 30-Mar-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( ( V  e.  X  /\  A  e. Word  V  /\  B  e. Word  V )  /\  ( M  e.  ( 0..^ L )  /\  N  e.  (
 ( L  +  1 ) ... ( L  +  ( # `  B ) ) ) ) )  ->  ( ( A concat  B )  e. Word  V  /\  M  e.  ( 0
 ... N )  /\  N  e.  ( 0 ... ( # `  ( A concat  B ) ) ) ) )
 
30-Mar-2018swrdccatin12lem3b 28022 Lemma 2 for swrdccatin12lem3 28024. (Contributed by Alexander van der Vekens, 30-Mar-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( B  e.  NN0  /\  M  e.  ( 0..^ L )  /\  N  e.  ( ( L  +  1 ) ... ( L  +  B )
 ) )  ->  (
 ( K  e.  (
 0..^ ( N  -  M ) )  /\  -.  K  e.  ( 0..^ ( L  -  M ) ) )  ->  ( K  -  ( L  -  M ) )  e.  ( 0..^ ( ( N  -  L )  -  0 ) ) ) )
 
30-Mar-2018swrdccatin12lem3a 28021 Lemma 1 for swrdccatin12lem3 28024. (Contributed by Alexander van der Vekens, 30-Mar-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( B  e.  NN0  /\  M  e.  ( 0..^ L )  /\  N  e.  ( ( L  +  1 ) ... ( L  +  B )
 ) )  ->  (
 ( K  e.  (
 0..^ ( N  -  M ) )  /\  -.  K  e.  ( 0..^ ( L  -  M ) ) )  ->  ( K  +  M )  e.  ( L..^ ( L  +  B ) ) ) )
 
30-Mar-2018swrdccatin12lem2 28020 Lemma 2 for swrdccatin12 28026. (Contributed by Alexander van der Vekens, 30-Mar-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( L  e.  NN0  /\  M  e.  NN0  /\  N  e.  ZZ )  ->  (
 ( K  e.  (
 0..^ ( N  -  M ) )  /\  -.  K  e.  ( 0..^ ( L  -  M ) ) )  ->  K  e.  ( ( L  -  M )..^ ( ( L  -  M )  +  ( N  -  L ) ) ) ) )
 
30-Mar-2018ccatvalfn 28008 The concatenation of two words is a function over the half-open interval of integers having the sum of the lengths of the word as length. (Contributed by Alexander van der Vekens, 30-Mar-2018.)
 |-  (
 ( A  e. Word  V  /\  B  e. Word  V )  ->  ( A concat  B )  Fn  ( 0..^ ( ( # `  A )  +  ( # `  B ) ) ) )
 
30-Mar-2018elfzonelfzo 27992 If an element of a half-open range of integers is not contained in the lower subrange, it must be in the upper subrange. (Contributed by Alexander van der Vekens, 30-Mar-2018.)
 |-  ( N  e.  ZZ  ->  ( ( K  e.  ( M..^ R )  /\  -.  K  e.  ( M..^ N ) )  ->  K  e.  ( N..^ R ) ) )
 
30-Mar-2018elfzomelpfzo 27989 An integer increased by another interger is an element of a half-open range of integers if and only if the integer is contained in the half-open range of integers with bounds decreased by the other integer. (Contributed by Alexander van der Vekens, 30-Mar-2018.)
 |-  (
 ( ( M  e.  ZZ  /\  N  e.  ZZ )  /\  ( K  e.  ZZ  /\  L  e.  ZZ ) )  ->  ( K  e.  ( ( M  -  L )..^ ( N  -  L ) )  <->  ( K  +  L )  e.  ( M..^ N ) ) )
 
29-Mar-2018swrdccatin2lem1 28017 Lemma for swrdccatin2 28018. (Contributed by Alexander van der Vekens, 29-Mar-2018.)
 |-  (
 ( ( A  e.  NN0  /\  B  e.  NN0 )  /\  ( M  e.  ( A ... N )  /\  N  e.  ( ( A  +  1 ) ... ( A  +  B ) )  /\  K  e.  ( 0..^ ( N  -  M ) ) ) )  ->  ( K  +  M )  e.  ( A..^ ( A  +  B ) ) )
 
29-Mar-2018elfzmlbp 27978 Subtracting the lower bound of a finite sets of sequential integers from an element of this set. (Contributed by Alexander van der Vekens, 29-Mar-2018.)
 |-  (
 ( N  e.  ZZ  /\  K  e.  ( M
 ... ( M  +  N ) ) ) 
 ->  ( K  -  M )  e.  ( 0 ... N ) )
 
29-Mar-2018elfzmlbm 27977 Subtracting the left border of a finite sets of sequential integers from an element of this set. (Contributed by Alexander van der Vekens, 29-Mar-2018.)
 |-  ( K  e.  ( M ... N )  ->  ( K  -  M )  e.  ( 0 ... ( N  -  M ) ) )
 
28-Mar-2018swrdccatin12lem1 28019 Lemma 1 for swrdccatin12 28026. (Contributed by Alexander van der Vekens, 28-Mar-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( ( V  e.  X  /\  A  e. Word  V  /\  B  e. Word  V )  /\  ( M  e.  ( 0..^ L )  /\  N  e.  (
 ( L  +  1 ) ... ( L  +  ( # `  B ) ) ) ) )  ->  ( A  e. Word  V  /\  M  e.  ( 0 ... L )  /\  L  e.  (
 0 ... ( # `  A ) ) ) )
 
28-Mar-2018swrdccatin2 28018 The subword of a concatenation of two words within the second of the concatenated words. (Contributed by Alexander van der Vekens, 28-Mar-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( V  e.  X  /\  A  e. Word  V  /\  B  e. Word  V )  ->  ( ( M  e.  ( L ... N ) 
 /\  N  e.  (
 ( L  +  1 ) ... ( L  +  ( # `  B ) ) ) ) 
 ->  ( ( A concat  B ) substr 
 <. M ,  N >. )  =  ( B substr  <. ( M  -  L ) ,  ( N  -  L ) >. ) ) )
 
28-Mar-2018swrdccatin1 28016 The subword of a concatenation of two words within the first of the concatenated words. (Contributed by Alexander van der Vekens, 28-Mar-2018.)
 |-  (
 ( A  e. Word  V  /\  B  e. Word  V )  ->  ( ( M  e.  ( 0 ... N )  /\  N  e.  (
 0 ... ( # `  A ) ) )  ->  ( ( A concat  B ) substr 
 <. M ,  N >. )  =  ( A substr  <. M ,  N >. ) ) )
 
28-Mar-2018swrdvalfn 28007 Value of the subword extractor as function with domain. (Contributed by Alexander van der Vekens, 28-Mar-2018.)
 |-  (
 ( S  e. Word  A  /\  F  e.  ( 0
 ... L )  /\  L  e.  ( 0 ... ( # `  S ) ) )  ->  ( S substr  <. F ,  L >. )  Fn  (
 0..^ ( L  -  F ) ) )
 
28-Mar-2018elfzelfzccat 28006 An element of a finite set of sequential integers up to the length of a word is an element of an extended finite set of sequential integers up to the length of a concatenation of this word with another word. (Contributed by Alexander van der Vekens, 28-Mar-2018.)
 |-  (
 ( A  e. Word  V  /\  B  e. Word  V )  ->  ( N  e.  (
 0 ... ( # `  A ) )  ->  N  e.  ( 0 ... ( # `
  ( A concat  B ) ) ) ) )
 
28-Mar-2018elfzelfzadd 27982 An element of a finite set of sequential integers is an element of an extended finite set of sequential integers. (Contributed by Alexander van der Vekens, 28-Mar-2018.)
 |-  (
 ( A  e.  NN0  /\  B  e.  NN0 )  ->  ( N  e.  (
 0 ... A )  ->  N  e.  ( 0 ... ( A  +  B ) ) ) )
 
28-Mar-20180mbf 26151 The empty function is measurable. (Contributed by Brendan Leahy, 28-Mar-2018.)
 |-  (/)  e. MblFn
 
28-Mar-2018ismblfin 26146 Measurability in terms of inner and outer measure. Proposition 7 of [Viaclovsky8] p. 3. (Contributed by Brendan Leahy, 4-Mar-2018.) (Revised by Brendan Leahy, 28-Mar-2018.)
 |-  (
 ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  ->  ( A  e.  dom 
 vol 
 <->  ( vol * `  A )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
 ) ( b  C_  A  /\  y  =  ( vol `  b )
 ) } ,  RR ,  <  ) ) )
 
28-Mar-2018mblfinlem3 26145 Backward direction of ismblfin 26146. (Contributed by Brendan Leahy, 28-Mar-2018.)
 |-  (
 ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  ->  ( vol * `
  A )  = 
 sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
 C_  A  /\  y  =  ( vol `  b
 ) ) } ,  RR ,  <  ) )
 
27-Mar-2018swrdccat3a0 28015 The subword of a concatenation of an empty word with another word is the subword of the second concatenated word. (Contributed by Alexander van der Vekens, 27-Mar-2018.)
 |-  (
 ( A  e.  Y  /\  B  e. Word  V )  ->  ( ( # `  A )  =  0  ->  ( ( A concat  B ) substr  <. M ,  N >. )  =  ( B substr  <. M ,  N >. ) ) )
 
27-Mar-20182if2 27941 Resolve two nested conditionals. (Contributed by Alexander van der Vekens, 27-Mar-2018.)
 |-  (
 ( ph  /\  ps )  ->  D  =  A )   &    |-  ( ( ph  /\  -.  ps 
 /\  th )  ->  D  =  B )   &    |-  ( ( ph  /\ 
 -.  ps  /\  -.  th )  ->  D  =  C )   =>    |-  ( ph  ->  D  =  if ( ps ,  A ,  if ( th ,  B ,  C ) ) )
 
25-Mar-2018fseq0hash 27993 The value of the size function on a finite 0-based sequence. (Contributed by Alexander van der Vekens, 25-Mar-2018.)
 |-  (
 ( N  e.  NN0  /\  F  Fn  ( 0..^ N ) )  ->  ( # `  F )  =  N )
 
25-Mar-2018mblfinlem2 26144 The difference between two sets measurable by the criterion in ismblfin 26146 is itself measurable by the same. Proposition 0.3 of [Viaclovsky7] p. 3. (Contributed by Brendan Leahy, 25-Mar-2018.)
 |-  (
 ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B )  e.  RR )  /\  ( ( vol
 * `  A )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
 C_  A  /\  y  =  ( vol `  b
 ) ) } ,  RR ,  <  )  /\  ( vol * `  B )  =  sup ( {
 y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
 C_  B  /\  y  =  ( vol `  b
 ) ) } ,  RR ,  <  ) ) )  ->  sup ( {
 y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
 C_  ( A  \  B )  /\  y  =  ( vol `  b
 ) ) } ,  RR ,  <  )  =  ( vol * `  ( A  \  B ) ) )
 
23-Mar-2018fzosplitsnm1 27991 Removing a singleton from a half-open range at the end. (Contributed by Alexander van der Vekens, 23-Mar-2018.)
 |-  (
 ( A  e.  ZZ  /\  B  e.  ( ZZ>= `  ( A  +  1
 ) ) )  ->  ( A..^ B )  =  ( ( A..^ ( B  -  1 ) )  u.  { ( B  -  1 ) }
 ) )
 
23-Mar-2018ubmelm1fzo 27987 If an integer between 0 and an upper bound of a half open interval of integers minus 1 is subtracted from this upper bound, the result is contained in this half open interval. (Contributed by Alexander van der Vekens, 23-Mar-2018.)
 |-  ( K  e.  ( 1..^ N )  ->  ( ( N  -  K )  -  1 )  e.  ( 0..^ N ) )
 
22-Mar-2018axbnd 2384 Axiom of Bundling (intuitionistic logic axiom ax-bnd).

In classical logic, this and axi12 2383 are fairly straightforward consequences of ax12o 1976. But in intuitionistic logic, it is not easy to add the extra  A. x to axi12 2383 and so we treat the two as separate axioms.

(Contributed by Jim Kingdon, 22-Mar-2018.)

 |-  ( A. z  z  =  x  \/  ( A. z  z  =  y  \/  A. x A. z ( x  =  y  ->  A. z  x  =  y ) ) )
 
21-Mar-2018fzo1fzo0n0 27988 An integer between 1 and an upper bound of a half open interval of integers is not 0 and between 0 and the upper bound of a half open interval of integers. (Contributed by Alexander van der Vekens, 21-Mar-2018.)
 |-  ( K  e.  ( 1..^ N )  <->  ( K  e.  ( 0..^ N )  /\  K  =/=  0 ) )
 
20-Mar-2018usgranloop 21352 In an undirected simple graph without loops, there is no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Proof shortened by Alexander van der Vekens, 20-Mar-2018.)
 |-  ( V USGrph  E  ->  ( E. x  e.  dom  E ( E `  x )  =  { M ,  N }  ->  M  =/=  N ) )
 
20-Mar-2018usisuslgra 21340 An undirected simple graph without loops is an undirected simple graph with loops. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Proof shortened by Alexander van der Vekens, 20-Mar-2018.)
 |-  ( V USGrph  E  ->  V USLGrph  E )
 
20-Mar-2018eqlei2 9140 Equality implies 'less than or equal to'. (Contributed by Alexander van der Vekens, 20-Mar-2018.)
 |-  A  e.  RR   =>    |-  ( B  =  A  ->  B  <_  A )
 
20-Mar-2018eqlei 9139 Equality implies 'less than or equal to'. (Contributed by NM, 23-May-1999.) (Revised by Alexander van der Vekens, 20-Mar-2018.)
 |-  A  e.  RR   =>    |-  ( A  =  B  ->  A  <_  B )
 
19-Mar-20180mnnnnn0 27971 The result of subtracting a positive integer from 0 is not a nonnegative integer. (Contributed by Alexander van der Vekens, 19-Mar-2018.)
 |-  ( N  e.  NN  ->  ( 0  -  N ) 
 e/  NN0 )
 
18-Mar-2018ubmelfzo 27986 If an integer between 0 and an upper bound of a half open interval of integers is subtracted from this upper bound, the result is contained in this half open interval. (Contributed by Alexander van der Vekens, 18-Mar-2018.)
 |-  ( K  e.  ( 1..^ N )  ->  ( N  -  K )  e.  ( 0..^ N ) )
 
18-Mar-2018fzo0ss1 27985 Subset relationship for half-open sequences of integers with lower bounds 0 and 1. (Contributed by Alexander van der Vekens, 18-Mar-2018.)
 |-  (
 1..^ N )  C_  ( 0..^ N )
 
18-Mar-2018leaddsuble 27970 Addition and subtraction on one side of 'less or equal'. (Contributed by Alexander van der Vekens, 18-Mar-2018.)
 |-  (
 ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( B  <_  C  <->  ( ( A  +  B )  -  C )  <_  A ) )
 
18-Mar-2018cnm1cn 27968 A complex number minus 1 is a complex number. (Contributed by Alexander van der Vekens, 18-Mar-2018.)
 |-  ( N  e.  CC  ->  ( N  -  1 )  e.  CC )
 
16-Mar-2018swrdnd 28001 The value of the subword extractor is the empty set (undefined) if the range is not valid. (Contributed by Alexander van der Vekens, 16-Mar-2018.)
 |-  (
 ( W  e. Word  V  /\  F  e.  ZZ  /\  L  e.  ZZ )  ->  ( ( F  <  0  \/  L  <_  F  \/  ( # `  W )  <  L )  ->  ( W substr  <. F ,  L >. )  =  (/) ) )
 
16-Mar-2018swrdltnd 28000 The value of the subword extractor is the empty set (undefined) if the range is not valid. (Contributed by Alexander van der Vekens, 16-Mar-2018.)
 |-  (
 ( W  e. Word  V  /\  F  e.  ZZ  /\  L  e.  ZZ )  ->  ( L  <_  F  ->  ( W substr  <. F ,  L >. )  =  (/) ) )
 
16-Mar-2018ssfzo12 27990 Subset relationship for half-open integer ranges. (Contributed by Alexander van der Vekens, 16-Mar-2018.)
 |-  (
 ( K  e.  ZZ  /\  L  e.  ZZ  /\  K  <  L )  ->  ( ( K..^ L )  C_  ( M..^ N )  ->  ( M  <_  K 
 /\  L  <_  N ) ) )
 
16-Mar-2018ssfz12 27976 Subset relationship for finite sets of sequential integers. (Contributed by Alexander van der Vekens, 16-Mar-2018.)
 |-  (
 ( K  e.  ZZ  /\  L  e.  ZZ  /\  K  <_  L )  ->  ( ( K ... L )  C_  ( M ... N )  ->  ( M  <_  K  /\  L  <_  N ) ) )
 
16-Mar-2018binomrisefac 25309 A version of the binomial theorem using rising factorials instead of exponentials. (Contributed by Scott Fenton, 16-Mar-2018.)
 |-  (
 ( A  e.  CC  /\  B  e.  CC  /\  N  e.  NN0 )  ->  ( ( A  +  B ) RiseFac  N )  = 
 sum_ k  e.  (
 0 ... N ) ( ( N  _C  k
 )  x.  ( ( A RiseFac  ( N  -  k ) )  x.  ( B RiseFac  k )
 ) ) )
 
15-Mar-2018hashfzdm 27997 The size of a function with a finite set of sequential integers, starting with 0, as domain equals the right border of this range increased by 1. (Contributed by Alexander van der Vekens, 15-Mar-2018.)
 |-  (
 ( N  e.  NN0  /\  F : ( 0
 ... N ) --> B ) 
 ->  ( # `  F )  =  ( N  +  1 ) )
 
13-Mar-2018itg2addnc 26158 Alternate proof of itg2add 19604 using the "buffer zone" definition from the first lemma, in which every simple function in the set is divided into to by dividing its buffer by a third and finding the largest allowable function locked to a grid laid out in increments of the new, smaller buffer up to the original simple function. The measurability of this function follows from that of the augend, and subtracting it from the original simple function yields another simple function by i1fsub 19553, which is allowable by the fact that the grid must have a mark between one third and two thirds the original buffer. This has two advantages over the current approach: first, eliminating ax-cc 8271, and second, weakening the measurability hypothesis to only the augend. (Contributed by Brendan Leahy, 31-Oct-2017.) (Revised by Brendan Leahy, 13-Mar-2018.)
 |-  ( ph  ->  F  e. MblFn )   &    |-  ( ph  ->  F : RR --> ( 0 [,)  +oo ) )   &    |-  ( ph  ->  (
 S.2 `  F )  e.  RR )   &    |-  ( ph  ->  G : RR --> ( 0 [,)  +oo ) )   &    |-  ( ph  ->  ( S.2 `  G )  e.  RR )   =>    |-  ( ph  ->  ( S.2 `  ( F  o F  +  G ) )  =  (
 ( S.2 `  F )  +  ( S.2 `  G ) ) )
 
13-Mar-2018binomfallfac 25308 A version of the binomial theorem using falling factorials instead of exponentials. (Contributed by Scott Fenton, 13-Mar-2018.)
 |-  (
 ( A  e.  CC  /\  B  e.  CC  /\  N  e.  NN0 )  ->  ( ( A  +  B ) FallFac  N )  = 
 sum_ k  e.  (
 0 ... N ) ( ( N  _C  k
 )  x.  ( ( A FallFac  ( N  -  k ) )  x.  ( B FallFac  k )
 ) ) )
 
13-Mar-2018binomfallfaclem2 25307 Lemma for binomfallfac 25308. Inductive step. (Contributed by Scott Fenton, 13-Mar-2018.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  N  e.  NN0 )   &    |-  ( ps  ->  ( ( A  +  B ) FallFac  N )  =  sum_ k  e.  ( 0 ...
 N ) ( ( N  _C  k )  x.  ( ( A FallFac  ( N  -  k
 ) )  x.  ( B FallFac  k ) ) ) )   =>    |-  ( ( ph  /\  ps )  ->  ( ( A  +  B ) FallFac  ( N  +  1 )
 )  =  sum_ k  e.  ( 0 ... ( N  +  1 )
 ) ( ( ( N  +  1 )  _C  k )  x.  ( ( A FallFac  (
 ( N  +  1 )  -  k ) )  x.  ( B FallFac  k ) ) ) )
 
13-Mar-2018binomfallfaclem1 25306 Lemma for binomfallfac 25308. Closure law. (Contributed by Scott Fenton, 13-Mar-2018.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  N  e.  NN0 )   =>    |-  ( ( ph  /\  K  e.  ( 0 ... N ) )  ->  ( ( N  _C  K )  x.  ( ( A FallFac  ( N  -  K ) )  x.  ( B FallFac  ( K  +  1 ) ) ) )  e.  CC )
 
12-Mar-2018sibfof 24607 Applying function operations on simple functions results in simple functions with regard to the the destination space, provided the operation fulfills a simple condition. (Contributed by Thierry Arnoux, 12-Mar-2018.)
 |-  B  =  ( Base `  W )   &    |-  J  =  ( TopOpen `  W )   &    |-  S  =  (sigaGen `  J )   &    |-  .0.  =  ( 0g `  W )   &    |- 
 .x.  =  ( .s `  W )   &    |-  H  =  (RRHom `  (Scalar `  W )
 )   &    |-  ( ph  ->  W  e.  V )   &    |-  ( ph  ->  M  e.  U. ran measures )   &    |-  ( ph  ->  F  e.  dom  ( Wsitg M ) )   &    |-  C  =  ( Base `  K )   &    |-  ( ph  ->  W  e.  TopSp )   &    |-  ( ph  ->  .+ 
 : ( B  X.  B ) --> C )   &    |-  ( ph  ->  G  e.  dom  ( Wsitg M ) )   &    |-  ( ph  ->  K  e.  TopSp )   &    |-  ( ph  ->  J  e.  Fre )   &    |-  ( ph  ->  (  .0.  .+  .0.  )  =  ( 0g
 `  K ) )   =>    |-  ( ph  ->  ( F  o F  .+  G )  e.  dom  ( Ksitg M ) )
 
11-Mar-2018frgregordn0 28173 If a nonempty friendship graph is k-regular, its order is k(k-1)+1. This corresponds to the third claim in the proof of the friendship theorem in [Huneke] p. 2: "Next we claim that the number n of vertices in G is exactly k(k-1)+1.". (Contributed by Alexander van der Vekens, 11-Mar-2018.)
 |-  (
 ( V FriendGrph  E  /\  V  e.  Fin  /\  V  =/=  (/) )  ->  ( A. v  e.  V  (
 ( V VDeg  E ) `  v )  =  K  ->  ( # `  V )  =  ( ( K  x.  ( K  -  1 ) )  +  1 ) ) )
 
11-Mar-2018usgreghash2spot 28172 In a finite k-regular graph with N vertices there are N times " k choose 2 " paths with length 2, according to the proof of the third claim in the proof of the friendship theorem in [Huneke] p. 2: "... giving n * ( k 2 ) total paths of length two.", if the direction of traversing the path is not respected. For simple paths of length 2 represented by ordered triples, however, we have again n*k*(k-1) such paths. (Contributed by Alexander van der Vekens, 11-Mar-2018.)
 |-  (
 ( V USGrph  E  /\  V  e.  Fin  /\  V  =/= 
 (/) )  ->  ( A. v  e.  V  ( ( V VDeg  E ) `  v )  =  K  ->  ( # `  ( V 2SPathOnOt  E ) )  =  ( ( # `  V )  x.  ( K  x.  ( K  -  1
 ) ) ) ) )
 
11-Mar-20182spotmdisj 28171 The sets of paths of length 2 with a given vertex in the middle are distinct for different vertices in the middle. (Contributed by Alexander van der Vekens, 11-Mar-2018.)
 |-  M  =  ( a  e.  V  |->  { t  e.  ( ( V  X.  V )  X.  V )  |  ( t  e.  ( V 2SPathOnOt  E )  /\  ( 2nd `  ( 1st `  t
 ) )  =  a ) } )   =>    |-  ( V  e.  _V 
 -> Disj 
 x  e.  V ( M `  x ) )
 
11-Mar-20182spot0 28167 If there are no vertices, then there are no paths (of length 2), too. (Contributed by Alexander van der Vekens, 11-Mar-2018.)
 |-  (
 ( V  =  (/)  /\  E  e.  X ) 
 ->  ( V 2SPathOnOt  E )  =  (/) )
 
11-Mar-2018kcnktkm1cn 27969 k times k minus 1 is a complex number if k is a complex number. (Contributed by Alexander van der Vekens, 11-Mar-2018.)
 |-  ( K  e.  CC  ->  ( K  x.  ( K  -  1 ) )  e.  CC )
 
11-Mar-20183xpfi 27967 The cross product of three finite sets is a finite set. (Contributed by Alexander van der Vekens, 11-Mar-2018.)
 |-  ( V  e.  Fin  ->  (
 ( V  X.  V )  X.  V )  e. 
 Fin )
 
11-Mar-2018itg2addnclem3 26157 Lemma incomprehensible in isolation split off to shorten proof of itg2addnc 26158. (Contributed by Brendan Leahy, 11-Mar-2018.)
 |-  ( ph  ->  F  e. MblFn )   &    |-  ( ph  ->  F : RR --> ( 0 [,)  +oo ) )   &    |-  ( ph  ->  (
 S.2 `  F )  e.  RR )   &    |-  ( ph  ->  G : RR --> ( 0 [,)  +oo ) )   &    |-  ( ph  ->  ( S.2 `  G )  e.  RR )   =>    |-  ( ph  ->  ( E. h  e.  dom  S.1 ( E. y  e.  RR+  ( z  e. 
 RR  |->  if ( ( h `
  z )  =  0 ,  0 ,  ( ( h `  z )  +  y
 ) ) )  o R  <_  ( F  o F  +  G )  /\  s  =  (
 S.1 `  h )
 )  ->  E. t E. u ( E. f  e.  dom  S.1 E. g  e. 
 dom  S.1 ( ( E. c  e.  RR+  ( z  e.  RR  |->  if (
 ( f `  z
 )  =  0 ,  0 ,  ( ( f `  z )  +  c ) ) )  o R  <_  F 
 /\  t  =  (
 S.1 `  f )
 )  /\  ( E. d  e.  RR+  ( z  e.  RR  |->  if (
 ( g `  z
 )  =  0 ,  0 ,  ( ( g `  z )  +  d ) ) )  o R  <_  G 
 /\  u  =  (
 S.1 `  g )
 ) )  /\  s  =  ( t  +  u ) ) ) )
 
11-Mar-2018cnflduss 19263 The uniform structure of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.)
 |-  U  =  (UnifSt ` fld )   =>    |-  U  =  (metUnif `  ( abs  o.  -  ) )
 
11-Mar-2018xmetutop 18567 The topology induced by a uniform structure generated by an extended metric  D is that metric's open sets. (Contributed by Thierry Arnoux, 11-Mar-2018.)
 |-  ( ( X  =/=  (/)  /\  D  e.  ( * Met `  X ) ) 
 ->  (unifTop `  (metUnif `  D ) )  =  ( MetOpen `  D ) )
 
11-Mar-2018psmetutop 18566 The topology induced by a uniform structure generated by a metric  D is generated by that metric's open balls. (Contributed by Thierry Arnoux, 6-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.)
 |-  ( ( X  =/=  (/)  /\  D  e.  (PsMet `  X ) )  ->  (unifTop `  (metUnif `  D ) )  =  ( topGen `
  ran  ( ball `  D ) ) )
 
11-Mar-2018elbl4 18559 Membership in a ball, alternative definition. (Contributed by Thierry Arnoux, 26-Jan-2018.) (Revised by Thierry Arnoux, 11-Mar-2018.)
 |-  ( ( ( D  e.  (PsMet `  X )  /\  R  e.  RR+ )  /\  ( A  e.  X  /\  B  e.  X ) )  ->  ( B  e.  ( A (
 ball `  D ) R )  <->  B ( `' D " ( 0 [,) R ) ) A ) )
 
11-Mar-2018blval2 18558 The ball around a point  P, alternative definition. (Contributed by Thierry Arnoux, 7-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.)
 |-  ( ( D  e.  (PsMet `  X )  /\  P  e.  X  /\  R  e.  RR+ )  ->  ( P ( ball `  D ) R )  =  ( ( `' D "
 ( 0 [,) R ) ) " { P } ) )
 
11-Mar-2018blssexps 18409 Two ways to express the existence of a ball subset. (Contributed by NM, 5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.)
 |-  ( ( D  e.  (PsMet `  X )  /\  P  e.  X )  ->  ( E. x  e. 
 ran  ( ball `  D ) ( P  e.  x  /\  x  C_  A ) 
 <-> 
 E. r  e.  RR+  ( P ( ball `  D ) r )  C_  A ) )
 
11-Mar-2018blssps 18407 Any point  P in a ball  B can be centered in another ball that is a subset of  B. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.)
 |-  ( ( D  e.  (PsMet `  X )  /\  B  e.  ran  ( ball `  D )  /\  P  e.  B )  ->  E. x  e.  RR+  ( P (
 ball `  D ) x )  C_  B )
 
11-Mar-2018ssblps 18405 The size of a ball increases monotonically with its radius. (Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro, 24-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.)
 |-  ( ( ( D  e.  (PsMet `  X )  /\  P  e.  X )  /\  ( R  e.  RR*  /\  S  e.  RR* )  /\  R  <_  S )  ->  ( P ( ball `  D ) R ) 
 C_  ( P (
 ball `  D ) S ) )
 
11-Mar-2018unirnblps 18402 The union of the set of balls of a metric space is its base set. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.)
 |-  ( D  e.  (PsMet `  X )  ->  U. ran  ( ball `  D )  =  X )
 
11-Mar-2018blelrnps 18399 A ball belongs to the set of balls of a metric space. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.)
 |-  ( ( D  e.  (PsMet `  X )  /\  P  e.  X  /\  R  e.  RR* )  ->  ( P ( ball `  D ) R )  e.  ran  ( ball `  D )
 )
 
11-Mar-2018blcntrps 18395 A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.)
 |-  ( ( D  e.  (PsMet `  X )  /\  P  e.  X  /\  R  e.  RR+ )  ->  P  e.  ( P ( ball `  D ) R ) )
 
11-Mar-2018xblcntrps 18393 A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.)
 |-  ( ( D  e.  (PsMet `  X )  /\  P  e.  X  /\  ( R  e.  RR*  /\  0  <  R ) )  ->  P  e.  ( P ( ball `  D ) R ) )
 
11-Mar-2018blrnps 18391 Membership in the range of the ball function. Note that  ran  ( ball `  D ) is the collection of all balls for metric 
D. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.)
 |-  ( D  e.  (PsMet `  X )  ->  ( A  e.  ran  ( ball `  D )  <->  E. x  e.  X  E. r  e.  RR*  A  =  ( x ( ball `  D ) r ) ) )
 
11-Mar-2018blfps 18389 Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.)
 |-  ( D  e.  (PsMet `  X )  ->  ( ball `  D ) : ( X  X.  RR* )
 --> ~P X )
 
11-Mar-2018blss2ps 18386 One ball is contained in another if the center-to-center distance is less than the difference of the radii. (Contributed by Mario Carneiro, 15-Jan-2014.) (Revised by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.)
 |-  ( ( ( D  e.  (PsMet `  X )  /\  P  e.  X  /\  Q  e.  X ) 
 /\  ( R  e.  RR  /\  S  e.  RR  /\  ( P D Q )  <_  ( S  -  R ) ) ) 
 ->  ( P ( ball `  D ) R ) 
 C_  ( Q (
 ball `  D ) S ) )
 
11-Mar-2018xblss2ps 18384 One ball is contained in another if the center-to-center distance is less than the difference of the radii. In this version of blss2 18387 for extended metrics, we have to assume the balls are a finite distance apart, or else  P will not even be in the infinity ball around  Q. (Contributed by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.)
 |-  ( ph  ->  D  e.  (PsMet `  X )
 )   &    |-  ( ph  ->  P  e.  X )   &    |-  ( ph  ->  Q  e.  X )   &    |-  ( ph  ->  R  e.  RR* )   &    |-  ( ph  ->  S  e.  RR* )   &    |-  ( ph  ->  ( P D Q )  e.  RR )   &    |-  ( ph  ->  ( P D Q )  <_  ( S + e  - e R ) )   =>    |-  ( ph  ->  ( P ( ball `  D ) R )  C_  ( Q ( ball `  D ) S ) )
 
11-Mar-2018xblpnfps 18378 The infinity ball in an extended metric is the set of all points that are a finite distance from the center. (Contributed by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.)
 |-  ( ( D  e.  (PsMet `  X )  /\  P  e.  X )  ->  ( A  e.  ( P ( ball `  D )  +oo )  <->  ( A  e.  X  /\  ( P D A )  e.  RR ) ) )
 
11-Mar-2018blcomps 18376 Commute the arguments to the ball function. (Contributed by Mario Carneiro, 22-Jan-2014.) (Revised by Thierry Arnoux, 11-Mar-2018.)
 |-  ( ( ( D  e.  (PsMet `  X )  /\  R  e.  RR* )  /\  ( P  e.  X  /\  A  e.  X ) )  ->  ( A  e.  ( P (
 ball `  D ) R )  <->  P  e.  ( A ( ball `  D ) R ) ) )
 
11-Mar-2018elbl2ps 18372 Membership in a ball. (Contributed by NM, 9-Mar-2007.) (Revised by Thierry Arnoux, 11-Mar-2018.)
 |-  ( ( ( D  e.  (PsMet `  X )  /\  R  e.  RR* )  /\  ( P  e.  X  /\  A  e.  X ) )  ->  ( A  e.  ( P (
 ball `  D ) R )  <->  ( P D A )  <  R ) )
 
11-Mar-2018elblps 18370 Membership in a ball. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.)
 |-  ( ( D  e.  (PsMet `  X )  /\  P  e.  X  /\  R  e.  RR* )  ->  ( A  e.  ( P ( ball `  D ) R )  <->  ( A  e.  X  /\  ( P D A )  <  R ) ) )
 
11-Mar-2018blvalps 18368 The ball around a point  P is the set of all points whose distance from  P is less than the ball's radius  R. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.)
 |-  ( ( D  e.  (PsMet `  X )  /\  P  e.  X  /\  R  e.  RR* )  ->  ( P ( ball `  D ) R )  =  { x  e.  X  |  ( P D x )  <  R } )
 
11-Mar-2018psmetlecl 18299 Real closure of an extended metric value that is upper bounded by a real. (Contributed by Thierry Arnoux, 11-Mar-2018.)
 |-  ( ( D  e.  (PsMet `  X )  /\  ( A  e.  X  /\  B  e.  X ) 
 /\  ( C  e.  RR  /\  ( A D B )  <_  C ) )  ->  ( A D B )  e.  RR )
 
10-Mar-2018usgreg2spot 28170 In a finite k-regular graph the set of all paths of length two is the union of all the paths of length 2 over the vertices which are in the the middle of such a path. (Contributed by Alexander van der Vekens, 10-Mar-2018.)
 |-  M  =  ( a  e.  V  |->  { t  e.  ( ( V  X.  V )  X.  V )  |  ( t  e.  ( V 2SPathOnOt  E )  /\  ( 2nd `  ( 1st `  t
 ) )  =  a ) } )   =>    |-  ( ( V USGrph  E  /\  V  e.  Fin )  ->  ( A. v  e.  V  ( ( V VDeg 
 E ) `  v
 )  =  K  ->  ( V 2SPathOnOt  E )  =  U_ x  e.  V  ( M `  x ) ) )
 
10-Mar-2018usgreghash2spotv 28169 According to the proof of the third claim in the proof of the friendship theorem in [Huneke] p. 2: "For each vertex v, there are exactly ( k 2 ) paths with length two having v in the middle, ..." in a finite k-regular graph. For simple paths of length 2 represented by ordered triples, we have again k*(k-1) such paths. (Contributed by Alexander van der Vekens, 10-Mar-2018.)
 |-  M  =  ( a  e.  V  |->  { t  e.  ( ( V  X.  V )  X.  V )  |  ( t  e.  ( V 2SPathOnOt  E )  /\  ( 2nd `  ( 1st `  t
 ) )  =  a ) } )   =>    |-  ( ( V USGrph  E  /\  V  e.  Fin )  ->  A. v  e.  V  ( ( ( V VDeg 
 E ) `  v
 )  =  K  ->  ( # `  ( M `  v ) )  =  ( K  x.  ( K  -  1 ) ) ) )
 
10-Mar-2018usgfidegfi 28090 In a finite graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 10-Mar-2018.)
 |-  (
 ( V USGrph  E  /\  V  e.  Fin )  ->  A. v  e.  V  ( ( V VDeg  E ) `  v )  e. 
 NN0 )
 
10-Mar-2018otiunsndisjX 27955 The union of singletons consisting of ordered triples which have distinct first and third components are disjunct. (Contributed by Alexander van der Vekens, 10-Mar-2018.)
 |-  ( B  e.  X  -> Disj  a  e.  V U_ c  e.  W  { <. a ,  B ,  c >. } )
 
10-Mar-2018otiunsndisj 27954 The union of singletons consisting of ordered triples which have distinct first and third components are disjunct. (Contributed by Alexander van der Vekens, 10-Mar-2018.)
 |-  ( B  e.  X  -> Disj  a  e.  V U_ c  e.  ( W  \  {
 a } ) { <. a ,  B ,  c >. } )
 
10-Mar-2018otsndisj 27953 The singletons consisting of ordered triples which have distinct third components are disjunct. (Contributed by Alexander van der Vekens, 10-Mar-2018.)
 |-  (
 ( A  e.  X  /\  B  e.  Y ) 
 -> Disj  c  e.  V { <. A ,  B ,  c >. } )
 
10-Mar-2018otthg 27952 Ordered triple theorem, closed form. (Contributed by Alexander van der Vekens, 10-Mar-2018.)
 |-  (
 ( A  e.  U  /\  B  e.  V  /\  C  e.  W )  ->  ( <. A ,  B ,  C >.  =  <. D ,  E ,  F >.  <-> 
 ( A  =  D  /\  B  =  E  /\  C  =  F )
 ) )
 
10-Mar-2018itg2addnclem 26155 An alternate expression for the 
S.2 integral that includes an arbitrarily small but strictly positive "buffer zone" wherever the simple function is nonzero. (Contributed by Brendan Leahy, 10-Oct-2017.) (Revised by Brendan Leahy, 10-Mar-2018.)
 |-  L  =  { x  |  E. g  e.  dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if (
 ( g `  z
 )  =  0 ,  0 ,  ( ( g `  z )  +  y ) ) )  o R  <_  F 
 /\  x  =  (
 S.1 `  g )
 ) }   =>    |-  ( F : RR --> ( 0 [,]  +oo )  ->  ( S.2 `  F )  =  sup ( L ,  RR* ,  <  )
 )
 
9-Mar-2018usg2spot2nb 28168 The set of paths of length 2 with a given vertex in the middle for a finite graph is the union of all paths of length 2 from one neighbor to another neighbor of this vertex via this vertex. (Contributed by Alexander van der Vekens, 9-Mar-2018.)
 |-  M  =  ( a  e.  V  |->  { t  e.  ( ( V  X.  V )  X.  V )  |  ( t  e.  ( V 2SPathOnOt  E )  /\  ( 2nd `  ( 1st `  t
 ) )  =  a ) } )   =>    |-  ( ( V USGrph  E  /\  V  e.  Fin  /\  N  e.  V ) 
 ->  ( M `  N )  =  U_ x  e.  ( <. V ,  E >. Neighbors  N ) U_ y  e.  ( ( <. V ,  E >. Neighbors  N )  \  { x } ) { <. x ,  N ,  y >. } )
 
9-Mar-2018usg2spthonot1 28087 A simple path of length 2 between two vertices as ordered triple corresponds to two adjacent edges in an undirected simple graph. (Contributed by Alexander van der Vekens, 9-Mar-2018.)
 |-  (
 ( V USGrph  E  /\  ( A  e.  V  /\  C  e.  V ) )  ->  ( T  e.  ( A ( V 2SPathOnOt  E ) C )  <->  E. b  e.  V  ( ( T  =  <. A ,  b ,  C >.  /\  A  =/=  C )  /\  ( { A ,  b }  e.  ran  E  /\  {
 b ,  C }  e.  ran  E ) ) ) )
 
9-Mar-2018el2spthonot0 28068 A simple path of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 9-Mar-2018.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  C  e.  V ) )  ->  ( T  e.  ( A ( V 2SPathOnOt  E ) C )  <->  E. b  e.  V  ( T  =  <. A ,  b ,  C >.  /\  <. A ,  b ,  C >.  e.  ( A ( V 2SPathOnOt  E ) C ) ) ) )
 
9-Mar-2018measge0 24514 A measure is non negative. (Contributed by Thierry Arnoux, 9-Mar-2018.)
 |-  (
 ( M  e.  (measures `  S )  /\  A  e.  S )  ->  0  <_  ( M `  A ) )
 
9-Mar-2018disjxpin 23981 Derive a disjunction over a cross product from the disjunctions over its first and second elements. (Contributed by Thierry Arnoux, 9-Mar-2018.)
 |-  ( x  =  ( 1st `  p )  ->  C  =  E )   &    |-  ( y  =  ( 2nd `  p )  ->  D  =  F )   &    |-  ( ph  -> Disj  x  e.  A C )   &    |-  ( ph  -> Disj  y  e.  B D )   =>    |-  ( ph  -> Disj  p  e.  ( A  X.  B ) ( E  i^i  F ) )
 
9-Mar-2018isspthonpth 21537 Properties of a pair of functions to be a simple path between two given vertices(in an undirected graph). (Contributed by Alexander van der Vekens, 9-Mar-2018.)
 |-  ( ( ( V  e.  X  /\  E  e.  Y )  /\  ( F  e.  W  /\  P  e.  Z )  /\  ( A  e.  V  /\  B  e.  V ) )  ->  ( F ( A ( V SPathOn  E ) B ) P  <->  ( F ( V SPaths  E ) P  /\  ( P `  0 )  =  A  /\  ( P `  ( # `  F ) )  =  B ) ) )
 
8-Mar-2018usg2spthonot0 28086 A simple path of length 2 between two vertices as ordered triple corresponds to two adjacent edges in an undirected simple graph. (Contributed by Alexander van der Vekens, 8-Mar-2018.)
 |-  (
 ( V USGrph  E  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )
 )  ->  ( <. S ,  B ,  T >.  e.  ( A ( V 2SPathOnOt  E ) C )  <-> 
 ( ( S  =  A  /\  T  =  C  /\  A  =/=  C ) 
 /\  ( { A ,  B }  e.  ran  E 
 /\  { B ,  C }  e.  ran  E ) ) ) )
 
8-Mar-2018usg2spthonot 28085 A simple path of length 2 between two vertices as ordered triple corresponds to two adjacent edges in an undirected simple graph. (Contributed by Alexander van der Vekens, 8-Mar-2018.)
 |-  (
 ( V USGrph  E  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )
 )  ->  ( <. A ,  B ,  C >.  e.  ( A ( V 2SPathOnOt  E ) C )  <-> 
 ( A  =/=  C  /\  { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E ) ) )
 
8-Mar-2018el2wlkonotot1 28071 A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 8-Mar-2018.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  ( R  e.  V  /\  S  e.  V ) )  ->  ( <. A ,  B ,  C >.  e.  ( R ( V 2WalksOnOt  E ) S )  <-> 
 ( A  =  R  /\  C  =  S  /\  <. A ,  B ,  C >.  e.  ( A ( V 2WalksOnOt  E ) C ) ) ) )
 
8-Mar-2018ofpreima 24034 Express the preimage of a function operation as a union of preimages. (Contributed by Thierry Arnoux, 8-Mar-2018.)
 |-  ( ph  ->  F : A --> B )   &    |-  ( ph  ->  G : A --> C )   &    |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  R  Fn  ( B  X.  C ) )   =>    |-  ( ph  ->  ( `' ( F  o F R G ) " D )  =  U_ p  e.  ( `' R " D ) ( ( `' F " { ( 1st `  p ) }
 )  i^i  ( `' G " { ( 2nd `  p ) } )
 ) )
 
7-Mar-2018nbfiusgrafi 28034 The class of neighbors of a vertex in a finite graph is a finite set. (Contributed by Alexander van der Vekens, 7-Mar-2018.)
 |-  (
 ( V USGrph  E  /\  V  e.  Fin  /\  N  e.  V )  ->  ( <. V ,  E >. Neighbors  N )  e.  Fin )
 
6-Mar-2018frghash2spot 28166 The number of simple paths of length 2 is n*(n-1) in a friendship graph with  n vertices. This corresponds to the proof of the third claim in the proof of the friendship theorem in [Huneke] p. 2: "... the paths of length two in G: by assumption there are ( n 2 ) such paths.". However, the order of vertices is not respected by Huneke, so he only counts half of the paths which are existing when respecting the order as it is the case for simple paths represented by orderes triples. (Contributed by Alexander van der Vekens, 6-Mar-2018.)
 |-  (
 ( V FriendGrph  E  /\  ( V  e.  Fin  /\  V  =/= 
 (/) ) )  ->  ( # `  ( V 2SPathOnOt  E ) )  =  ( ( # `  V )  x.  ( ( # `  V )  -  1
 ) ) )
 
6-Mar-2018usgfiregdegfi 28091 In a finite graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 6-Mar-2018.)
 |-  (
 ( V USGrph  E  /\  V  e.  Fin  /\  V  =/= 
 (/) )  ->  ( A. v  e.  V  ( ( V VDeg  E ) `  v )  =  K  ->  K  e.  NN0 ) )
 
6-Mar-2018ax10 1991 Derive set.mm's original ax-10 2190 from others. (Contributed by NM, 25-Jul-2015.) (Revised by NM, 7-Nov-2015.) (Proof shortened by Wolf Lammen, 6-Mar-2018.)
 |-  ( A. x  x  =  y  ->  A. y  y  =  x )
 
6-Mar-2018spime 1960 Existential introduction, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Mar-2018.)
 |- 
 F/ x ph   &    |-  ( x  =  y  ->  ( ph  ->  ps ) )   =>    |-  ( ph  ->  E. x ps )
 
5-Mar-20182spotiundisj 28165 All simple paths of length 2 as ordered triple from a fixed vertex to another vertex are disjunct. (Contributed by Alexander van der Vekens, 5-Mar-2018.)
 |-  (
 ( V  e.  X  /\  E  e.  Y ) 
 -> Disj  a  e.  V U_ b  e.  ( V  \  { a } )
 ( a ( V 2SPathOnOt  E ) b ) )
 
5-Mar-2018df-hcmp 24294 Definition of the Hausdorff completion. In this definition, a structure  w is a Hausdorff completion of a uniform structure  u if  w is a complete uniform space, in which  u is dense, and which admits the same uniform structure. Theorem 3 of [BourbakiTop1] p. II.21. states the existence and unicity of such a completion. (Contributed by Thierry Arnoux, 5-Mar-2018.)
 |- HCmp  =  { <. u ,  w >.  |  ( ( u  e. 
 U. ran UnifOn  /\  w  e. CUnifSp )  /\  (UnifSt `  w )  =  u  /\  ( ( cls `  ( TopOpen `  w ) ) `  dom  U. u )  =  ( Base `  w )
 ) }
 
4-Mar-20182spotdisj 28164 All simple paths of length 2 as ordered triple from a fixed vertex to another vertex are disjunct. (Contributed by Alexander van der Vekens, 4-Mar-2018.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  A  e.  V )  -> Disj  b  e.  ( V 
 \  { A }
 ) ( A ( V 2SPathOnOt  E ) b ) )
 
4-Mar-20182spotfi 28089 In a finite graph, the set of simple paths of length 2 between two vertices (as ordered triples) is finite. (Contributed by Alexander van der Vekens, 4-Mar-2018.)
 |-  (
 ( ( V  e.  Fin  /\  E  e.  X ) 
 /\  ( A  e.  V  /\  B  e.  V ) )  ->  ( A ( V 2SPathOnOt  E ) B )  e.  Fin )
 
4-Mar-2018sibf0 24602 The constant zero function is a simple function. (Contributed by Thierry Arnoux, 4-Mar-2018.)
 |-  B  =  ( Base `  W )   &    |-  J  =  ( TopOpen `  W )   &    |-  S  =  (sigaGen `  J )   &    |-  .0.  =  ( 0g `  W )   &    |- 
 .x.  =  ( .s `  W )   &    |-  H  =  (RRHom `  (Scalar `  W )
 )   &    |-  ( ph  ->  W  e.  V )   &    |-  ( ph  ->  M  e.  U. ran measures )   &    |-  ( ph  ->  W  e.  TopSp )   &    |-  ( ph  ->  W  e.  Grp )   =>    |-  ( ph  ->  ( U. dom  M  X.  {  .0.  } )  e.  dom  ( Wsitg M ) )
 
4-Mar-2018dral1 2022 Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 24-Nov-1994.) (Proof shortened by Wolf Lammen, 4-Mar-2018.)
 |-  ( A. x  x  =  y  ->  ( ph 
 <->  ps ) )   =>    |-  ( A. x  x  =  y  ->  (
 A. x ph  <->  A. y ps )
 )
 
4-Mar-2018dral2 2020 Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 27-Feb-2005.) (Revised by Wolf Lammen, 4-Mar-2018.)
 |-  ( A. x  x  =  y  ->  ( ph 
 <->  ps ) )   =>    |-  ( A. x  x  =  y  ->  (
 A. z ph  <->  A. z ps )
 )
 
4-Mar-2018dvelimh 2015 Version of dvelim 2066 without any variable restrictions. (Contributed by NM, 1-Oct-2002.) (Proof shortened by Wolf Lammen, 4-Mar-2018.)
 |-  ( ph  ->  A. x ph )   &    |-  ( ps  ->  A. z ps )   &    |-  (
 z  =  y  ->  ( ph  <->  ps ) )   =>    |-  ( -.  A. x  x  =  y  ->  ( ps  ->  A. x ps ) )
 
3-Mar-2018frg2spot1 28161 In a friendship graph, there is exactly one simple path of length 2 between two different vertices as ordered triple. (Contributed by Alexander van der Vekens, 3-Mar-2018.)
 |-  (
 ( V FriendGrph  E  /\  ( A  e.  V  /\  B  e.  V )  /\  A  =/=  B ) 
 ->  ( # `  ( A ( V 2SPathOnOt  E ) B ) )  =  1 )
 
3-Mar-20182spot2iun2spont 28088 The set of simple paths of length 2 (in a graph) is the double union of the simple paths of length 2 between different vertices. (Contributed by Alexander van der Vekens, 3-Mar-2018.)
 |-  (
 ( V  e.  _V  /\  E  e.  _V )  ->  ( V 2SPathOnOt  E )  =  U_ x  e.  V  U_ y  e.  ( V 
 \  { x }
 ) ( x ( V 2SPathOnOt  E ) y ) )
 
3-Mar-20182spontn0vne 28084 If the set of simple paths of length 2 between two vertices (in a graph) is not empty, the two vertices must be not equal. (Contributed by Alexander van der Vekens, 3-Mar-2018.)
 |-  (
 ( X ( V 2SPathOnOt  E ) Y )  =/=  (/)  ->  X  =/=  Y )
 
3-Mar-2018dvelimhw 1872 Proof of dvelimh 2015 without using ax-12 1946 but with additional distinct variable conditions. (Contributed by Andrew Salmon, 21-Jul-2011.) (Revised by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 3-Mar-2018.)
 |-  ( ph  ->  A. x ph )   &    |-  ( ps  ->  A. z ps )   &    |-  (
 z  =  y  ->  ( ph  <->  ps ) )   &    |-  ( -.  A. x  x  =  y  ->  ( y  =  z  ->  A. x  y  =  z )
 )   =>    |-  ( -.  A. x  x  =  y  ->  ( ps  ->  A. x ps ) )
 
3-Mar-2018hbnt 1795 Closed theorem version of bound-variable hypothesis builder hbn 1797. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Mar-2018.)
 |-  ( A. x (
 ph  ->  A. x ph )  ->  ( -.  ph  ->  A. x  -.  ph )
 )
 
3-Mar-201819.9ht 1788 A closed version of 19.9 1793. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Mar-2018.)
 |-  ( A. x (
 ph  ->  A. x ph )  ->  ( E. x ph  -> 
 ph ) )
 
2-Mar-20182pthwlkonot 28082 For two different vertices, a walk of length 2 between these vertices as ordered triple is a simple path of length 2 between these vertices as ordered triple in an undirected simple graph. (Contributed by Alexander van der Vekens, 2-Mar-2018.)
 |-  (
 ( V USGrph  E  /\  ( A  e.  V  /\  B  e.  V ) 
 /\  A  =/=  B )  ->  ( A ( V 2SPathOnOt  E ) B )  =  ( A ( V 2WalksOnOt  E ) B ) )
 
2-Mar-2018el2spthonot 28067 A simple path of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  C  e.  V ) )  ->  ( T  e.  ( A ( V 2SPathOnOt  E ) C )  <->  E. b  e.  V  ( T  =  <. A ,  b ,  C >.  /\  E. f E. p ( f ( V SPaths  E ) p  /\  ( # `  f )  =  2  /\  ( A  =  ( p `  0 )  /\  b  =  ( p `  1
 )  /\  C  =  ( p `  2 ) ) ) ) ) )
 
2-Mar-2018usgra2wlkspth 28038 In a undirected simple graph, any walk of length 2 between two different vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.)
 |-  (
 ( V USGrph  E  /\  ( # `  F )  =  2  /\  A  =/=  B )  ->  ( F ( A ( V WalkOn  E ) B ) P  <->  F ( A ( V SPathOn  E ) B ) P ) )
 
2-Mar-2018usgra2wlkspthlem2 28037 Lemma 2 for usgra2wlkspth 28038. (Contributed by Alexander van der Vekens, 2-Mar-2018.)
 |-  (
 ( ( F  e. Word  dom 
 E  /\  ( # `  F )  =  2 )  /\  ( V USGrph  E  /\  P : ( 0 ... ( # `  F ) ) --> V ) )  ->  ( (
 ( ( P `  0 )  =  A  /\  ( P `  ( # `
  F ) )  =  B  /\  A  =/=  B )  /\  A. i  e.  ( 0..^ ( # `  F ) ) ( E `  ( F `  i ) )  =  { ( P `  i ) ,  ( P `  (
 i  +  1 ) ) } )  ->  Fun  `' P ) )
 
2-Mar-2018usgra2wlkspthlem1 28036 Lemma 1 for usgra2wlkspth 28038. (Contributed by Alexander van der Vekens, 2-Mar-2018.)
 |-  (
 ( F  e. Word  dom  E 
 /\  E : dom  E
 -1-1-> ran  E  /\  ( # `
  F )  =  2 )  ->  (
 ( ( ( P `
  0 )  =  A  /\  ( P `
  ( # `  F ) )  =  B  /\  A  =/=  B ) 
 /\  A. i  e.  (
 0..^ ( # `  F ) ) ( E `
  ( F `  i ) )  =  { ( P `  i ) ,  ( P `  ( i  +  1 ) ) }
 )  ->  Fun  `' F ) )
 
2-Mar-2018f12dfv 27961 A one-to-one function with a pair as domain in terms of function values. (Contributed by Alexander van der Vekens, 2-Mar-2018.)
 |-  A  =  { X ,  Y }   =>    |-  ( ( ( X  e.  U  /\  Y  e.  V )  /\  X  =/=  Y )  ->  ( F : A -1-1-> B  <->  ( F : A
 --> B  /\  ( F `
  X )  =/=  ( F `  Y ) ) ) )
 
2-Mar-2018oteqimp 27951 The components of an ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018.)
 |-  ( T  =  <. A ,  B ,  C >.  ->  ( ( A  e.  X  /\  B  e.  Y  /\  C  e.  Z ) 
 ->  ( ( 1st `  ( 1st `  T ) )  =  A  /\  ( 2nd `  ( 1st `  T ) )  =  B  /\  ( 2nd `  T )  =  C )
 ) )
 
2-Mar-2018spthonisspth 21539 A simple path between to vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.)
 |-  ( F ( A ( V SPathOn  E ) B ) P  ->  F ( V SPaths  E ) P )
 
1-Mar-2018el2spthsoton 28076 A simple path of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 1-Mar-2018.)
 |-  (
 ( V  e.  X  /\  E  e.  Y ) 
 ->  ( T  e.  ( V 2SPathOnOt  E )  <->  E. a  e.  V  E. b  e.  V  T  e.  ( a
 ( V 2SPathOnOt  E ) b ) ) )
 
1-Mar-20182spthonot3v 28073 If an ordered triple represents a simple path of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.)
 |-  ( T  e.  ( A ( V 2SPathOnOt  E ) C )  ->  ( ( V  e.  _V  /\  E  e.  _V )  /\  ( A  e.  V  /\  C  e.  V )  /\  T  e.  ( ( V  X.  V )  X.  V ) ) )
 
1-Mar-20182spthonot 28063 The set of simple paths of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 1-Mar-2018.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  B  e.  V ) )  ->  ( A ( V 2SPathOnOt  E ) B )  =  {
 t  e.  ( ( V  X.  V )  X.  V )  | 
 E. f E. p ( f ( A ( V SPathOn  E ) B ) p  /\  ( # `  f )  =  2  /\  (
 ( 1st `  ( 1st `  t ) )  =  A  /\  ( 2nd `  ( 1st `  t
 ) )  =  ( p `  1 ) 
 /\  ( 2nd `  t
 )  =  B ) ) } )
 
1-Mar-2018is2spthonot 28061 The set of simple paths of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 1-Mar-2018.)
 |-  (
 ( V  e.  X  /\  E  e.  Y ) 
 ->  ( V 2SPathOnOt  E )  =  ( a  e.  V ,  b  e.  V  |->  { t  e.  ( ( V  X.  V )  X.  V )  | 
 E. f E. p ( f ( a ( V SPathOn  E )
 b ) p  /\  ( # `  f )  =  2  /\  (
 ( 1st `  ( 1st `  t ) )  =  a  /\  ( 2nd `  ( 1st `  t
 ) )  =  ( p `  1 ) 
 /\  ( 2nd `  t
 )  =  b ) ) } ) )
 
1-Mar-2018df-2spthsot 28058 Define the collection of all simple paths of length 2 as ordered triple. (in a graph) (Contributed by Alexander van der Vekens, 1-Mar-2018.)
 |- 2SPathOnOt  =  ( v  e.  _V ,  e  e.  _V  |->  { t  e.  ( ( v  X.  v )  X.  v
 )  |  E. a  e.  v  E. b  e.  v  t  e.  ( a ( v 2SPathOnOt  e ) b ) } )
 
1-Mar-2018df-2spthonot 28057 Define the collection of simple paths of length 2 with particular endpoints as ordered triple (in a graph) . (Contributed by Alexander van der Vekens, 1-Mar-2018.)
 |- 2SPathOnOt  =  ( v  e.  _V ,  e  e.  _V  |->  ( a  e.  v ,  b  e.  v  |->  { t  e.  ( ( v  X.  v )  X.  v
 )  |  E. f E. p ( f ( a ( v SPathOn  e
 ) b ) p 
 /\  ( # `  f
 )  =  2  /\  ( ( 1st `  ( 1st `  t ) )  =  a  /\  ( 2nd `  ( 1st `  t
 ) )  =  ( p `  1 ) 
 /\  ( 2nd `  t
 )  =  b ) ) } ) )
 
1-Mar-2018spthonepeq 21540 The endpoints of a simple path between two vertices are equal if and only if the path is of length 0 (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.)
 |-  ( F ( A ( V SPathOn  E ) B ) P  ->  ( A  =  B  <->  ( # `  F )  =  0 )
 )
 
1-Mar-2018spthonprp 21538 Properties of a simple path between two vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.)
 |-  ( F ( A ( V SPathOn  E ) B ) P  ->  ( ( ( V  e.  _V 
 /\  E  e.  _V )  /\  ( F  e.  _V 
 /\  P  e.  _V )  /\  ( A  e.  V  /\  B  e.  V ) )  /\  ( F ( A ( V WalkOn  E ) B ) P  /\  F ( V SPaths  E ) P ) ) )
 
1-Mar-2018isspthon 21536 Properties of a pair of functions to be a simple path between two given vertices(in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.)
 |-  ( ( ( V  e.  X  /\  E  e.  Y )  /\  ( F  e.  W  /\  P  e.  Z )  /\  ( A  e.  V  /\  B  e.  V ) )  ->  ( F ( A ( V SPathOn  E ) B ) P  <->  ( F ( A ( V WalkOn  E ) B ) P  /\  F ( V SPaths  E ) P ) ) )
 
1-Mar-2018spthon 21535 The set of simple paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.)
 |-  ( ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  B  e.  V )
 )  ->  ( A ( V SPathOn  E ) B )  =  { <. f ,  p >.  |  ( f ( A ( V WalkOn  E ) B ) p  /\  f ( V SPaths  E ) p ) } )
 
1-Mar-2018df-spthon 21478 Define the collection of simple paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.)
 |- SPathOn  =  ( v  e.  _V ,  e  e.  _V  |->  ( a  e.  v ,  b  e.  v  |->  { <. f ,  p >.  |  ( f ( a ( v WalkOn  e
 ) b ) p 
 /\  f ( v SPaths 
 e ) p ) } ) )
 
28-Feb-2018el2pthsot 28078 A simple path of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 28-Feb-2018.)
 |-  (
 ( V  e.  X  /\  E  e.  Y ) 
 ->  ( T  e.  ( V 2SPathOnOt  E )  <->  E. a  e.  V  E. b  e.  V  E. c  e.  V  ( T  =  <. a ,  b ,  c >.  /\  E. f E. p ( f ( V SPaths  E ) p  /\  ( # `  f )  =  2  /\  (
 a  =  ( p `
  0 )  /\  b  =  ( p `  1 )  /\  c  =  ( p `  2
 ) ) ) ) ) )
 
28-Feb-20182spthsot 28065 The set of simple paths of length 2 (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 28-Feb-2018.)
 |-  (
 ( V  e.  X  /\  E  e.  Y ) 
 ->  ( V 2SPathOnOt  E )  =  { t  e.  (
 ( V  X.  V )  X.  V )  | 
 E. a  e.  V  E. b  e.  V  t  e.  ( a
 ( V 2SPathOnOt  E ) b ) } )
 
28-Feb-2018hbn1fw 1715 Weak version of ax-6 1740 from which we can prove any ax-6 1740 instance not involving wff variables or bundling. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.) (Proof shortened by Wolf Lammen, 28-Feb-2018.)
 |-  ( A. x ph  ->  A. y A. x ph )   &    |-  ( -.  ps  ->  A. x  -.  ps )   &    |-  ( A. y ps 
 ->  A. x A. y ps )   &    |-  ( -.  ph  ->  A. y  -.  ph )   &    |-  ( -.  A. y ps  ->  A. x  -.  A. y ps )   &    |-  ( x  =  y  ->  ( ph  <->  ps ) )   =>    |-  ( -.  A. x ph 
 ->  A. x  -.  A. x ph )
 
28-Feb-2018cbvalvw 1711 Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 28-Feb-2018.)
 |-  ( x  =  y 
 ->  ( ph  <->  ps ) )   =>    |-  ( A. x ph  <->  A. y ps )
 
27-Feb-20182wot2wont 28083 The set of (simple) paths of length 2 (in a graph) is the set of (simple) paths of length 2 between any two different vertices. (Contributed by Alexander van der Vekens, 27-Feb-2018.)
 |-  (
 ( V  e.  X  /\  E  e.  Y ) 
 ->  ( V 2WalksOt  E )  =  U_ x  e.  V  U_ y  e.  V  ( x ( V 2WalksOnOt  E ) y ) )
 
27-Feb-2018dveeq1 1987 Quantifier introduction when one pair of variables is distinct. Revised to be independent of dvelimv 2017. (Contributed by NM, 2-Jan-2002.) (Revised by Wolf Lammen, 27-Feb-2018.)
 |-  ( -.  A. x  x  =  y  ->  ( y  =  z  ->  A. x  y  =  z ) )
 
27-Feb-2018spw 1702 Weak version of specialization scheme sp 1759. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 1759 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 1759 having no wff metavariables and mutually distinct set variables (see ax11wdemo 1734 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 1759 are spfw 1699 (minimal distinct variable requirements), spnfw 1678 (when  x is not free in  -.  ph), spvw 1674 (when  x does not appear in  ph), sptruw 1679 (when  ph is true), and spfalw 1680 (when  ph is false). (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 27-Feb-2018.)
 |-  ( x  =  y 
 ->  ( ph  <->  ps ) )   =>    |-  ( A. x ph 
 ->  ph )
 
26-Feb-2018el2wlksotot 28079 A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 26-Feb-2018.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V ) )  ->  ( <. A ,  B ,  C >.  e.  ( V 2WalksOt  E )  <->  E. f E. p ( f ( V Walks  E ) p  /\  ( # `  f )  =  2 
 /\  ( A  =  ( p `  0 ) 
 /\  B  =  ( p `  1 ) 
 /\  C  =  ( p `  2 ) ) ) ) )
 
26-Feb-2018otel3xp 27950 An ordered triple is an element of a doubled cross product. (Contributed by Alexander van der Vekens, 26-Feb-2018.)
 |-  (
 ( T  =  <. A ,  B ,  C >.  /\  ( A  e.  X  /\  B  e.  Y  /\  C  e.  Z ) )  ->  T  e.  ( ( X  X.  Y )  X.  Z ) )
 
26-Feb-2018ax12b 1697 Two equivalent ways of expressing ax-12 1946. See the comment for ax-12 1946. (Contributed by NM, 2-May-2017.) (Proof shortened by Wolf Lammen, 26-Feb-2018.)
 |-  ( ( -.  x  =  y  ->  ( y  =  z  ->  A. x  y  =  z )
 ) 
 <->  ( -.  x  =  y  ->  ( -.  x  =  z  ->  ( y  =  z  ->  A. x  y  =  z ) ) ) )
 
25-Feb-2018cnzh 24307 The  ZZ-module of  CC is a normed module. (Contributed by Thierry Arnoux, 25-Feb-2018.)
 |-  ( ZMod ` fld )  e. NrmMod
 
25-Feb-2018dvelimv 2017 Similar to dvelim 2066 with first hypothesis replaced by distinct variable condition. (Contributed by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 25-Feb-2018.)
 |-  ( z  =  y 
 ->  ( ph  <->  ps ) )   =>    |-  ( -.  A. x  x  =  y  ->  ( ps  ->  A. x ps ) )
 
25-Feb-2018a9e 1948 At least one individual exists. This is not a theorem of free logic, which is sound in empty domains. For such a logic, we would add this theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10). In the system consisting of ax-5 1563 through ax-14 1725 and ax-17 1623, all axioms other than ax-9 1662 are believed to be theorems of free logic, although the system without ax-9 1662 is probably not complete in free logic. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen, 25-Feb-2018.)
 |- 
 E. x  x  =  y
 
25-Feb-2018sbequ2 1657 An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Feb-2018.)
 |-  ( x  =  y 
 ->  ( [ y  /  x ] ph  ->  ph )
 )
 
24-Feb-2018sitgclre 24612 Closure of the Bochner integral on a simple function. This version is specific to Banach spaces on the real numbers. (Contributed by Thierry Arnoux, 24-Feb-2018.)
 |-  B  =  ( Base `  W )   &    |-  J  =  ( TopOpen `  W )   &    |-  S  =  (sigaGen `  J )   &    |-  .0.  =  ( 0g `  W )   &    |- 
 .x.  =  ( .s `  W )   &    |-  H  =  (RRHom `  (Scalar `  W )
 )   &    |-  ( ph  ->  W  e.  V )   &    |-  ( ph  ->  M  e.  U. ran measures )   &    |-  ( ph  ->  F  e.  dom  ( Wsitg M ) )   &    |-  ( ph  ->  W  e. Ban )   &    |-  ( ph  ->  (Scalar `  W )  =  (flds  RR ) )   =>    |-  ( ph  ->  ( ( Wsitg M ) `
  F )  e.  B )
 
24-Feb-2018sitgclcn 24611 Closure of the Bochner integral on a simple function. This version is specific to Banach spaces on the complex numbers. (Contributed by Thierry Arnoux, 24-Feb-2018.)
 |-  B  =  ( Base `  W )   &    |-  J  =  ( TopOpen `  W )   &    |-  S  =  (sigaGen `  J )   &    |-  .0.  =  ( 0g `  W )   &    |- 
 .x.  =  ( .s `  W )   &    |-  H  =  (RRHom `  (Scalar `  W )
 )   &    |-  ( ph  ->  W  e.  V )   &    |-  ( ph  ->  M  e.  U. ran measures )   &    |-  ( ph  ->  F  e.  dom  ( Wsitg M ) )   &    |-  ( ph  ->  W  e. Ban )   &    |-  ( ph  ->  (Scalar `  W )  =fld )   =>    |-  ( ph  ->  (
 ( Wsitg M ) `
  F )  e.  B )
 
24-Feb-2018sitgclbn 24610 Closure of the Bochner integral on a simple function. This version is specific to Banach spaces, with additional conditions on its scalar field. (Contributed by Thierry Arnoux, 24-Feb-2018.)
 |-  B  =  ( Base `  W )   &    |-  J  =  ( TopOpen `  W )   &    |-  S  =  (sigaGen `  J )   &    |-  .0.  =  ( 0g `  W )   &    |- 
 .x.  =  ( .s `  W )   &    |-  H  =  (RRHom `  (Scalar `  W )
 )   &    |-  ( ph  ->  W  e.  V )   &    |-  ( ph  ->  M  e.  U. ran measures )   &    |-  ( ph  ->  F  e.  dom  ( Wsitg M ) )   &    |-  G  =  (Scalar `  W )   &    |-  D  =  ( (
 dist `  G )  |`  ( ( Base `  G )  X.  ( Base `  G ) ) )   &    |-  ( ph  ->  W  e. Ban )   &    |-  ( ph  ->  G  e. CUnifSp )   &    |-  ( ph  ->  ( TopOpen `  G )  e.  Haus )   &    |-  ( ph  ->  (UnifSt `  G )  =  (metUnif `  D )
 )   &    |-  ( ph  ->  ( ZMod `  G )  e. NrmMod )   &    |-  ( ph  ->  (chr `  G )  =  0 )   =>    |-  ( ph  ->  (
 ( Wsitg M ) `
  F )  e.  B )
 
24-Feb-2018sitgclg 24609 Closure of the Bochner integral on a simple functions. This version is very generic, thus the many hypothesis. See sitgclbn 24610 for the version for Banach spaces. (Contributed by Thierry Arnoux, 24-Feb-2018.)
 |-  B  =  ( Base `  W )   &    |-  J  =  ( TopOpen `  W )   &    |-  S  =  (sigaGen `  J )   &    |-  .0.  =  ( 0g `  W )   &    |- 
 .x.  =  ( .s `  W )   &    |-  H  =  (RRHom `  (Scalar `  W )
 )   &    |-  ( ph  ->  W  e.  V )   &    |-  ( ph  ->  M  e.  U. ran measures )   &    |-  ( ph  ->  F  e.  dom  ( Wsitg M ) )   &    |-  G  =  (Scalar `  W )   &    |-  D  =  ( (
 dist `  G )  |`  ( ( Base `  G )  X.  ( Base `  G ) ) )   &    |-  ( ph  ->  W  e.  TopSp )   &    |-  ( ph  ->  W  e. CMnd )   &    |-  ( ph  ->  G  e.  DivRing )   &    |-  ( ph  ->  G  e. NrmRing )   &    |-  ( ph  ->  ( ZMod `  G )  e. NrmMod )   &    |-  ( ph  ->  (chr `  G )  =  0 )   &    |-  ( ph  ->  G  e.  TopSp )   &    |-  ( ph  ->  G  e. CUnifSp )   &    |-  ( ph  ->  (
 TopOpen `  G )  e. 
 Haus )   &    |-  ( ph  ->  (UnifSt `  G )  =  (metUnif `  D ) )   &    |-  (
 ( ph  /\  m  e.  ( H " (
 0 [,)  +oo ) ) 
 /\  x  e.  B )  ->  ( m  .x.  x )  e.  B )   =>    |-  ( ph  ->  (
 ( Wsitg M ) `
  F )  e.  B )
 
24-Feb-2018subrgchr 24183 If  A is a subring of  R, then they have the same characteristic. (Contributed by Thierry Arnoux, 24-Feb-2018.)
 |-  ( A  e.  (SubRing `  R )  ->  (chr `  ( Rs  A ) )  =  (chr `  R )
 )
 
24-Feb-2018psmetxrge0 18297 The distance function of a pseudometric space is a function into the nonnegative extended real numbers. (Contributed by Thierry Arnoux, 24-Feb-2018.)
 |-  ( D  e.  (PsMet `  X )  ->  D : ( X  X.  X ) --> ( 0 [,]  +oo ) )
 
24-Feb-2018spimt 1953 Closed theorem form of spim 1955. (Contributed by NM, 15-Jan-2008.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Feb-2018.)
 |-  ( ( F/ x ps  /\  A. x ( x  =  y  ->  ( ph  ->  ps )
 ) )  ->  ( A. x ph  ->  ps )
 )
 
23-Feb-2018spei 1964 Inference from existential specialization, using implicit substitution. Revised to remove a distinct variable constraint. (Contributed by NM, 19-Aug-1993.) (Revised by Wolf Lammen, 23-Feb-2018.)
 |-  ( x  =  y 
 ->  ( ph  <->  ps ) )   &    |-  ps   =>    |-  E. x ph
 
21-Feb-2018el2wlksot 28077 A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 21-Feb-2018.)
 |-  (
 ( V  e.  X  /\  E  e.  Y ) 
 ->  ( T  e.  ( V 2WalksOt  E )  <->  E. a  e.  V  E. b  e.  V  E. c  e.  V  ( T  =  <. a ,  b ,  c >.  /\  E. f E. p ( f ( V Walks  E ) p 
 /\  ( # `  f
 )  =  2  /\  ( a  =  ( p `  0 )  /\  b  =  ( p `  1 )  /\  c  =  ( p `  2
 ) ) ) ) ) )
 
21-Feb-2018el2wlksoton 28075 A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 21-Feb-2018.)
 |-  (
 ( V  e.  X  /\  E  e.  Y ) 
 ->  ( T  e.  ( V 2WalksOt  E )  <->  E. a  e.  V  E. b  e.  V  T  e.  ( a
 ( V 2WalksOnOt  E ) b ) ) )
 
21-Feb-20182wlksot 28064 The set of walks of length 2 (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 21-Feb-2018.)
 |-  (
 ( V  e.  X  /\  E  e.  Y ) 
 ->  ( V 2WalksOt  E )  =  { t  e.  (
 ( V  X.  V )  X.  V )  | 
 E. a  e.  V  E. b  e.  V  t  e.  ( a
 ( V 2WalksOnOt  E ) b ) } )
 
21-Feb-20183xpexg 27942 The cross product of three sets is a set. (Contributed by Alexander van der Vekens, 21-Feb-2018.)
 |-  ( V  e.  W  ->  ( ( V  X.  V )  X.  V )  e. 
 _V )
 
21-Feb-2018mblfinlem 26143 Lemma for ismblfin 26146, effectively one direction of the same fact for open sets, made necessary by Viaclovsky's slightly different defintion of outer measure. Note that unlike the main theorem, this holds for sets of infinite measure. (Contributed by Brendan Leahy, 21-Feb-2018.)
 |-  (
 ( A  e.  ( topGen `
  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol * `  A ) )  ->  E. s  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( s 
 C_  A  /\  M  <  ( vol * `  s ) ) )
 
20-Feb-2018frg2woteqm 28162 There is a (simple) path of length 2 from one vertex to another vertex in a friendship graph if and only if there is a (simple) path of length 2 from the other vertex back to the first vertex. (Contributed by Alexander van der Vekens, 20-Feb-2018.)
 |-  (
 ( V FriendGrph  E  /\  A  =/=  B )  ->  (
 ( <. A ,  P ,  B >.  e.  ( A ( V 2WalksOnOt  E ) B )  /\  <. B ,  Q ,  A >.  e.  ( B ( V 2WalksOnOt  E ) A ) )  ->  Q  =  P ) )
 
19-Feb-2018frg2wot1 28160 In a friendship graph, there is exactly one walk of length 2 between two different vertices as ordered triple. (Contributed by Alexander van der Vekens, 19-Feb-2018.)
 |-  (
 ( V FriendGrph  E  /\  ( A  e.  V  /\  B  e.  V )  /\  A  =/=  B ) 
 ->  ( # `  ( A ( V 2WalksOnOt  E ) B ) )  =  1 )
 
19-Feb-20182wlkonotv 28074 If an ordered tripple represents a walk of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018.)
 |-  ( <. A ,  B ,  C >.  e.  ( A ( V 2WalksOnOt  E ) C )  ->  ( ( V  e.  _V  /\  E  e.  _V )  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )
 ) )
 
19-Feb-20182wlkonot3v 28072 If an ordered triple represents a walk of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018.)
 |-  ( T  e.  ( A ( V 2WalksOnOt  E ) C )  ->  ( ( V  e.  _V  /\  E  e.  _V )  /\  ( A  e.  V  /\  C  e.  V )  /\  T  e.  ( ( V  X.  V )  X.  V ) ) )
 
19-Feb-2018sibfima 24606 Any preimage of a singleton by a simple function is measurable. (Contributed by Thierry Arnoux, 19-Feb-2018.)
 |-  B  =  ( Base `  W )   &    |-  J  =  ( TopOpen `  W )   &    |-  S  =  (sigaGen `  J )   &    |-  .0.  =  ( 0g `  W )   &    |- 
 .x.  =  ( .s `  W )   &    |-  H  =  (RRHom `  (Scalar `  W )
 )   &    |-  ( ph  ->  W  e.  V )   &    |-  ( ph  ->  M  e.  U. ran measures )   &    |-  ( ph  ->  F  e.  dom  ( Wsitg M ) )   =>    |-  ( ( ph  /\  A  e.  ( ran  F  \  {  .0.  } ) ) 
 ->  ( M `  ( `' F " { A } ) )  e.  ( 0 [,)  +oo ) )
 
19-Feb-2018sibfrn 24605 A simple function has finite range. (Contributed by Thierry Arnoux, 19-Feb-2018.)
 |-  B  =  ( Base `  W )   &    |-  J  =  ( TopOpen `  W )   &    |-  S  =  (sigaGen `  J )   &    |-  .0.  =  ( 0g `  W )   &    |- 
 .x.  =  ( .s `  W )   &    |-  H  =  (RRHom `  (Scalar `  W )
 )   &    |-  ( ph  ->  W  e.  V )   &    |-  ( ph  ->  M  e.  U. ran measures )   &    |-  ( ph  ->  F  e.  dom  ( Wsitg M ) )   =>    |-  ( ph  ->  ran  F  e.  Fin )
 
19-Feb-2018sibff 24604 A simple function is a function. (Contributed by Thierry Arnoux, 19-Feb-2018.)
 |-  B  =  ( Base `  W )   &    |-  J  =  ( TopOpen `  W )   &    |-  S  =  (sigaGen `  J )   &    |-  .0.  =  ( 0g `  W )   &    |- 
 .x.  =  ( .s `  W )   &    |-  H  =  (RRHom `  (Scalar `  W )
 )   &    |-  ( ph  ->  W  e.  V )   &    |-  ( ph  ->  M  e.  U. ran measures )   &    |-  ( ph  ->  F  e.  dom  ( Wsitg M ) )   =>    |-  ( ph  ->  F : U. dom  M --> U. J )
 
19-Feb-2018sibfmbl 24603 A simple function is measurable. (Contributed by Thierry Arnoux, 19-Feb-2018.)
 |-  B  =  ( Base `  W )   &    |-  J  =  ( TopOpen `  W )   &    |-  S  =  (sigaGen `  J )   &    |-  .0.  =  ( 0g `  W )   &    |- 
 .x.  =  ( .s `  W )   &    |-  H  =  (RRHom `  (Scalar `  W )
 )   &    |-  ( ph  ->  W  e.  V )   &    |-  ( ph  ->  M  e.  U. ran measures )   &    |-  ( ph  ->  F  e.  dom  ( Wsitg M ) )   =>    |-  ( ph  ->  F  e.  ( dom  MMblFnM S ) )
 
19-Feb-2018issibf 24601 The predicate " F is a simple function" relative to the Bochner integral. (Contributed by Thierry Arnoux, 19-Feb-2018.)
 |-  B  =  ( Base `  W )   &    |-  J  =  ( TopOpen `  W )   &    |-  S  =  (sigaGen `  J )   &    |-  .0.  =  ( 0g `  W )   &    |- 
 .x.  =  ( .s `  W )   &    |-  H  =  (RRHom `  (Scalar `  W )
 )   &    |-  ( ph  ->  W  e.  V )   &    |-  ( ph  ->  M  e.  U. ran measures )   =>    |-  ( ph  ->  ( F  e.  dom  ( Wsitg M )  <->  ( F  e.  ( dom  MMblFnM S )  /\  ran 
 F  e.  Fin  /\  A. x  e.  ( ran 
 F  \  {  .0.  } ) ( M `  ( `' F " { x } ) )  e.  ( 0 [,)  +oo ) ) ) )
 
19-Feb-2018dmmeas 24508 The domain of a measure is a sigma algebra. (Contributed by Thierry Arnoux, 19-Feb-2018.)
 |-  ( M  e.  U. ran measures  ->  dom  M  e.  U. ran sigAlgebra )
 
19-Feb-2018xrhval 24337 The value of the embedding from the extended real numbers into a complete lattice. (Contributed by Thierry Arnoux, 19-Feb-2018.)
 |-  B  =  ( (RRHom `  R ) " RR )   &    |-  L  =  ( glb `  R )   &    |-  U  =  ( lub `  R )   =>    |-  ( R  e.  V  ->  (RR*Hom `  R )  =  ( x  e.  RR*  |->  if ( x  e.  RR ,  ( (RRHom `  R ) `  x ) ,  if ( x  = 
 +oo ,  ( U `  B ) ,  ( L `  B ) ) ) ) )
 
19-Feb-2018df-xrh 24336 Define an embedding from the extended real number into a complete lattice. (Contributed by Thierry Arnoux, 19-Feb-2018.)
 |- RR*Hom  =  (
 r  e.  _V  |->  ( x  e.  RR*  |->  if ( x  e.  RR ,  (
 (RRHom `  r ) `  x ) ,  if ( x  =  +oo ,  ( ( lub `  r
 ) `  ( (RRHom `  r ) " RR ) ) ,  (
 ( glb `  r ) `  ( (RRHom `  r
 ) " RR ) ) ) ) ) )
 
19-Feb-2018spimed 1958 Deduction version of spime 1960. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 19-Feb-2018.)
 |-  ( ch  ->  F/ x ph )   &    |-  ( x  =  y  ->  ( ph  ->  ps ) )   =>    |-  ( ch  ->  (
 ph  ->  E. x ps )
 )
 
18-Feb-2018frg2wotn0 28159 In a friendship graph, there is always a path/walk of length 2 between two different vertices as ordered triple. (Contributed by Alexander van der Vekens, 18-Feb-2018.)
 |-  (
 ( V FriendGrph  E  /\  ( A  e.  V  /\  B  e.  V )  /\  A  =/=  B ) 
 ->  ( A ( V 2WalksOnOt  E ) B )  =/=  (/) )
 
18-Feb-2018frg2woteu 28158 For two different vertices in a friendship graph, there is exactly one third vertex being the middle vertex of a (simple) path/walk of length 2 between the two vertices as ordered triple. (Contributed by Alexander van der Vekens, 18-Feb-2018.)
 |-  (
 ( V FriendGrph  E  /\  ( A  e.  V  /\  B  e.  V )  /\  A  =/=  B ) 
 ->  E! c  e.  V  <. A ,  c ,  B >.  e.  ( A ( V 2WalksOnOt  E ) B ) )
 
18-Feb-2018frgraeu 28157 Any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 18-Feb-2018.)
 |-  ( V FriendGrph  E  ->  ( ( A  e.  V  /\  C  e.  V  /\  A  =/=  C )  ->  E! b ( { A ,  b }  e.  ran  E 
 /\  { b ,  C }  e.  ran  E ) ) )
 
18-Feb-2018usg2wlkonot 28080 A walk of length 2 between two vertices as ordered triple in an undirected simple graph. This theorem would also hold for undirected multigraphs, but to proof this the cases  A  =  B and/or  B  =  C must be considered separately. (Contributed by Alexander van der Vekens, 18-Feb-2018.)
 |-  (
 ( V USGrph  E  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )
 )  ->  ( <. A ,  B ,  C >.  e.  ( A ( V 2WalksOnOt  E ) C )  <-> 
 ( { A ,  B }  e.  ran  E 
 /\  { B ,  C }  e.  ran  E ) ) )
 
18-Feb-2018usg2wlkon 28050 In an undirected simple graph, two adjacent edges form a walk between two (different) vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.)
 |-  ( V USGrph  E  ->  ( ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E )  ->  E. f E. p  f ( A ( V WalkOn  E ) C ) p ) )
 
18-Feb-2018usg2wlk 28049 In an undirected simple graph, two adjacent edges form a walk between two (different) vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.)
 |-  (
 ( V USGrph  E  /\  { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E )  ->  E. f E. p ( f ( V Walks  E ) p  /\  ( # `  f )  =  2 
 /\  ( A  =  ( p `  0 ) 
 /\  B  =  ( p `  1 ) 
 /\  C  =  ( p `  2 ) ) ) )
 
18-Feb-2018usgra2adedgwlkon 28047 In an undirected simple graph, two adjacent edges form a walk between two (different) vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.)
 |-  F  =  { <. 0 ,  ( `' E `  { A ,  B } ) >. , 
 <. 1 ,  ( `' E `  { B ,  C } ) >. }   &    |-  P  =  { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. }   =>    |-  ( V USGrph  E  ->  ( ( { A ,  B }  e.  ran  E 
 /\  { B ,  C }  e.  ran  E ) 
 ->  F ( A ( V WalkOn  E ) C ) P ) )
 
18-Feb-2018usgra2adedgwlk 28046 In an undirected simple graph, two adjacent edges form a walk between two (different) vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.)
 |-  F  =  { <. 0 ,  ( `' E `  { A ,  B } ) >. , 
 <. 1 ,  ( `' E `  { B ,  C } ) >. }   &    |-  P  =  { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. }   =>    |-  ( V USGrph  E  ->  ( ( { A ,  B }  e.  ran  E 
 /\  { B ,  C }  e.  ran  E ) 
 ->  ( F ( V Walks  E ) P  /\  ( # `  F )  =  2  /\  ( A  =  ( P `  0 )  /\  B  =  ( P `  1
 )  /\  C  =  ( P `  2 ) ) ) ) )
 
18-Feb-2018uhgraedgrnv 28032 An edge of an undirected hypergraph contains only vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.)
 |-  (
 ( V UHGrph  E  /\  F  e.  ran  E  /\  N  e.  F )  ->  N  e.  V )
 
18-Feb-2018xrsp1 24157 The poset 1 of the extended real numbers is plus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.)
 |-  +oo  =  ( 1. `  RR* s )
 
18-Feb-2018xrsp0 24156 The poset 0 of the extended real numbers is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.)
 |-  -oo  =  ( 0. `  RR* s )
 
18-Feb-2018xrinfm 24074 The extended real numbers are unbounded below. (Contributed by Thierry Arnoux, 18-Feb-2018.)
 |-  sup ( RR* ,  RR* ,  `'  <  )  =  -oo
 
18-Feb-2018infxrmnf 24073 The infinimum of a set of extended reals containing minus infnity is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.)
 |-  (
 ( A  C_  RR*  /\  -oo  e.  A )  ->  sup ( A ,  RR* ,  `'  <  )  =  -oo )
 
18-Feb-2018xlemnf 24070 An extended real which is less than minus infinity is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.)
 |-  ( A  e.  RR*  ->  ( A  <_  -oo  <->  A  =  -oo ) )
 
18-Feb-20182pthlem2 21549 Lemma 2 for constr2pth 21554. (Contributed by Alexander van der Vekens, 5-Dec-2017.) (Revised by Alexander van der Vekens, 18-Feb-2018.)
 |-  P  =  { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. }   =>    |-  ( ( ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  B  =/=  C ) )  ->  ( ( P " { 0 ,  2 } )  i^i  ( P " (
 1..^ 2 ) ) )  =  (/) )
 
18-Feb-20182wlklemC 21509 Lemma for constr2wlk 21551. (Contributed by Alexander van der Vekens, 18-Feb-2018.)
 |-  P  =  { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. }   =>    |-  ( C  e.  V  ->  ( P `  2 )  =  C )
 
18-Feb-20182wlklemB 21508 Lemma for constr2wlk 21551. (Contributed by Alexander van der Vekens, 18-Feb-2018.)
 |-  P  =  { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. }   =>    |-  ( B  e.  V  ->  ( P `  1 )  =  B )
 
18-Feb-20182wlklemA 21507 Lemma for constr2wlk 21551. (Contributed by Alexander van der Vekens, 18-Feb-2018.)
 |-  P  =  { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. }   =>    |-  ( A  e.  V  ->  ( P `  0 )  =  A )
 
18-Feb-2018a16g 2012 Generalization of ax16 2094. (Contributed by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 18-Feb-2018.)
 |-  ( A. x  x  =  y  ->  ( ph  ->  A. z ph )
 )
 
18-Feb-2018spim 1955 Specialization, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. The spim 1955 series of theorems requires that only one direction of the substitution hypothesis hold. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 18-Feb-2018.)
 |- 
 F/ x ps   &    |-  ( x  =  y  ->  (
 ph  ->  ps ) )   =>    |-  ( A. x ph 
 ->  ps )
 
17-Feb-20180risefac 25305 The value of the zero rising factorial at natural  N. (Contributed by Scott Fenton, 17-Feb-2018.)
 |-  ( N  e.  NN  ->  ( 0 RiseFac  N )  =  0 )
 
17-Feb-20180fallfac 25304 The value of the zero falling factorial at natural  N. (Contributed by Scott Fenton, 17-Feb-2018.)
 |-  ( N  e.  NN  ->  ( 0 FallFac  N )  =  0 )
 
17-Feb-2018clatp1ex 24147 The poset one of a complete lattice belongs to its base. (Contributed by Thierry Arnoux, 17-Feb-2018.)
 |-  B  =  ( Base `  W )   &    |-  .1.  =  ( 1. `  W )   =>    |-  ( W  e.  CLat  ->  .1.  e.  B )
 
17-Feb-2018clatp0ex 24146 The poset zero of a complete lattice belongs to its base. (Contributed by Thierry Arnoux, 17-Feb-2018.)
 |-  B  =  ( Base `  W )   &    |-  .0.  =  ( 0. `  W )   =>    |-  ( W  e.  CLat  ->  .0.  e.  B )
 
17-Feb-2018tosglb 24145 Same theorem as toslub 24144, for infinimum. (Contributed by Thierry Arnoux, 17-Feb-2018.)
 |-  B  =  ( Base `  K )   &    |-  .<  =  ( lt `  K )   &    |-  ( ph  ->  K  e. Toset )   &    |-  ( ph  ->  A 
 C_  B )   &    |-  ( ph  ->  E. a  e.  B  ( A. b  e.  A  -.  b  .<  a  /\  A. b  e.  B  ( a  .<  b  ->  E. d  e.  A  d 
 .<  b ) ) )   =>    |-  ( ph  ->  ( ( glb `  K ) `  A )  =  sup ( A ,  B ,  `'  .<  ) )
 
17-Feb-2018aevlem1 2010 Lemma for aev 2011 and a16g 2012. Change free and bound variables. (Contributed by NM, 22-Jul-2015.) (Proof shortened by Wolf Lammen, 17-Feb-2018.)
 |-  ( A. z  z  =  w  ->  A. y  y  =  x )
 
17-Feb-2018ax10lem2 1989 Lemma for ax10 1991. Change bound variable. (Contributed by NM, 8-Jul-2016.) (Proof shortened by Wolf Lammen, 17-Feb-2018.)
 |-  ( A. x  x  =  w  ->  A. y  y  =  x )
 
16-Feb-2018usg2wotspth 28081 A walk of length 2 between two different vertices as ordered triple corresponds to a simple path of length 2 in an undirected simple graph. (Contributed by Alexander van der Vekens, 16-Feb-2018.)
 |-  (
 ( V USGrph  E  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  A  =/=  C ) 
 ->  ( <. A ,  B ,  C >.  e.  ( A ( V 2WalksOnOt  E ) C )  <->  E. f E. p ( f ( V SPaths  E ) p  /\  ( # `  f )  =  2  /\  ( A  =  ( p `  0 )  /\  B  =  ( p `  1
 )  /\  C  =  ( p `  2 ) ) ) ) )
 
16-Feb-2018is2wlk 21518 Properties of a pair of functions to be a walk of length 2 (in an undirected graph). (Contributed by Alexander van der Vekens, 16-Feb-2018.)
 |-  ( ( ( V  e.  X  /\  E  e.  Y )  /\  ( F  e.  W  /\  P  e.  Z )
 )  ->  ( ( F ( V Walks  E ) P  /\  ( # `  F )  =  2 )  <->  ( F :
 ( 0..^ 2 ) --> dom  E  /\  P : ( 0 ... 2 ) --> V  /\  ( ( E `  ( F `  0 ) )  =  { ( P `  0 ) ,  ( P `  1
 ) }  /\  ( E `  ( F `  1 ) )  =  { ( P `  1 ) ,  ( P `  2 ) }
 ) ) ) )
 
15-Feb-2018el2wlkonotot 28070 A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  C  e.  V ) )  ->  ( <. A ,  B ,  C >.  e.  ( A ( V 2WalksOnOt  E ) C )  <->  E. f E. p ( f ( V Walks  E ) p  /\  ( # `  f )  =  2 
 /\  ( A  =  ( p `  0 ) 
 /\  B  =  ( p `  1 ) 
 /\  C  =  ( p `  2 ) ) ) ) )
 
15-Feb-2018el2wlkonotot0 28069 A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  ( R  e.  V  /\  S  e.  V ) )  ->  ( <. A ,  B ,  C >.  e.  ( R ( V 2WalksOnOt  E ) S )  <-> 
 ( A  =  R  /\  C  =  S  /\  E. f E. p ( f ( V Walks  E ) p  /\  ( # `  f )  =  2 
 /\  ( A  =  ( p `  0 ) 
 /\  B  =  ( p `  1 ) 
 /\  C  =  ( p `  2 ) ) ) ) ) )
 
15-Feb-2018el2wlkonot 28066 A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  C  e.  V ) )  ->  ( T  e.  ( A ( V 2WalksOnOt  E ) C )  <->  E. b  e.  V  ( T  =  <. A ,  b ,  C >.  /\  E. f E. p ( f ( V Walks  E ) p 
 /\  ( # `  f
 )  =  2  /\  ( A  =  ( p `  0 )  /\  b  =  ( p `  1 )  /\  C  =  ( p `  2
 ) ) ) ) ) )
 
15-Feb-20182wlkonot 28062 The set of walks of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  B  e.  V ) )  ->  ( A ( V 2WalksOnOt  E ) B )  =  {
 t  e.  ( ( V  X.  V )  X.  V )  | 
 E. f E. p ( f ( A ( V WalkOn  E ) B ) p  /\  ( # `  f )  =  2  /\  (
 ( 1st `  ( 1st `  t ) )  =  A  /\  ( 2nd `  ( 1st `  t
 ) )  =  ( p `  1 ) 
 /\  ( 2nd `  t
 )  =  B ) ) } )
 
15-Feb-2018is2wlkonot 28060 The set of walks of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.)
 |-  (
 ( V  e.  X  /\  E  e.  Y ) 
 ->  ( V 2WalksOnOt  E )  =  ( a  e.  V ,  b  e.  V  |->  { t  e.  ( ( V  X.  V )  X.  V )  | 
 E. f E. p ( f ( a ( V WalkOn  E )
 b ) p  /\  ( # `  f )  =  2  /\  (
 ( 1st `  ( 1st `  t ) )  =  a  /\  ( 2nd `  ( 1st `  t
 ) )  =  ( p `  1 ) 
 /\  ( 2nd `  t
 )  =  b ) ) } ) )
 
15-Feb-2018el2wlkonotlem 28059 Lemma for el2wlkonot 28066. (Contributed by Alexander van der Vekens, 15-Feb-2018.)
 |-  (
 ( f ( V Walks  E ) p  /\  ( # `  f )  =  2 )  ->  ( p `  1 )  e.  V )
 
15-Feb-2018df-2wlksot 28056 Define the collection of all walks of length 2 as ordered triple (in a graph). (Contributed by Alexander van der Vekens, 15-Feb-2018.)
 |- 2WalksOt  =  ( v  e.  _V ,  e  e.  _V  |->  { t  e.  ( ( v  X.  v )  X.  v
 )  |  E. a  e.  v  E. b  e.  v  t  e.  ( a ( v 2WalksOnOt  e ) b ) } )
 
15-Feb-2018df-2wlkonot 28055 Define the collection of walks of length 2 with particular endpoints as ordered triple (in a graph). (Contributed by Alexander van der Vekens, 15-Feb-2018.)
 |- 2WalksOnOt  =  ( v  e.  _V ,  e  e.  _V  |->  ( a  e.  v ,  b  e.  v  |->  { t  e.  ( ( v  X.  v )  X.  v
 )  |  E. f E. p ( f ( a ( v WalkOn  e
 ) b ) p 
 /\  ( # `  f
 )  =  2  /\  ( ( 1st `  ( 1st `  t ) )  =  a  /\  ( 2nd `  ( 1st `  t
 ) )  =  ( p `  1 ) 
 /\  ( 2nd `  t
 )  =  b ) ) } ) )
 
15-Feb-2018el2xptp0 27949 A member of a nested cross product is an ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.)
 |-  (
 ( X  e.  U  /\  Y  e.  V  /\  Z  e.  W )  ->  ( ( A  e.  ( ( U  X.  V )  X.  W ) 
 /\  ( ( 1st `  ( 1st `  A ) )  =  X  /\  ( 2nd `  ( 1st `  A ) )  =  Y  /\  ( 2nd `  A )  =  Z ) )  <->  A  =  <. X ,  Y ,  Z >. ) )
 
15-Feb-2018el2xptp 27948 A member of a nested cross product is an ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.)
 |-  ( A  e.  ( ( B  X.  C )  X.  D )  <->  E. x  e.  B  E. y  e.  C  E. z  e.  D  A  =  <. x ,  y ,  z >. )
 
15-Feb-2018xrsclat 24155 The extended real numbers form a complete lattice. (Contributed by Thierry Arnoux, 15-Feb-2018.)
 |-  RR* s  e.  CLat
 
15-Feb-2018xrstos 24154 The extended real numbers form a toset. (Contributed by Thierry Arnoux, 15-Feb-2018.)
 |-  RR* s  e. Toset
 
15-Feb-2018toslub 24144 In a toset, the lowest upper bound 
lub, defined for partial orders is the supremum,  sup ( A ,  B ,  .<  ), defined for total orders, if this supremum exists (these are the set.mm definition: lowest upper bound and supremum are normally synonymous) Note that the two definitions do not have the same value when there is no such supremum. In that case,  sup ( A ,  B ,  .<  ) will take the value  (/), but  ( ( lub `  K ) `  A ) takes the value  ( Undef `  B
), therefore, we restrict this theorem only to the case where this supremum exists, which is expressed by the last assumption. (Contributed by Thierry Arnoux, 15-Feb-2018.)
 |-  B  =  ( Base `  K )   &    |-  .<  =  ( lt `  K )   &    |-  ( ph  ->  K  e. Toset )   &    |-  ( ph  ->  A 
 C_  B )   &    |-  ( ph  ->  E. a  e.  B  ( A. b  e.  A  -.  a  .<  b  /\  A. b  e.  B  ( b  .<  a  ->  E. d  e.  A  b 
 .<  d ) ) )   =>    |-  ( ph  ->  ( ( lub `  K ) `  A )  =  sup ( A ,  B ,  .<  ) )
 
14-Feb-2018frg2woteq 28163 There is a (simple) path of length 2 from one vertex to another vertex in a friendship graph if and only if there is a (simple) path of length 2 from the other vertex back to the first vertex. (Contributed by Alexander van der Vekens, 14-Feb-2018.)
 |-  (
 ( V FriendGrph  E  /\  A  =/=  B )  ->  (
 ( P  e.  ( A ( V 2WalksOnOt  E ) B )  /\  Q  e.  ( B ( V 2WalksOnOt  E ) A ) )  ->  ( ( 1st `  ( 1st `  P ) )  =  ( 2nd `  Q )  /\  ( 2nd `  ( 1st `  P ) )  =  ( 2nd `  ( 1st `  P ) ) 
 /\  ( 1st `  ( 1st `  Q ) )  =  ( 2nd `  P ) ) ) )
 
14-Feb-2018rezh 24308 The  ZZ-module of  RR is a normed module. (Contributed by Thierry Arnoux, 14-Feb-2018.)
 |-  R  =  (flds  RR )   =>    |-  ( ZMod `  R )  e. NrmMod
 
14-Feb-2018reust 24297 The Uniform structure of the real numbers. (Contributed by Thierry Arnoux, 14-Feb-2018.)
 |-  R  =  (flds  RR )   =>    |-  (UnifSt `  R )  =  (metUnif `  ( ( dist `  R )  |`  ( RR  X.  RR )
 ) )
 
14-Feb-2018ofresid 24008 Applying an operation restricted to the range of the functions does not change the function operation. (Contributed by Thierry Arnoux, 14-Feb-2018.)
 |-  ( ph  ->  F : A --> B )   &    |-  ( ph  ->  G : A --> B )   &    |-  ( ph  ->  A  e.  V )   =>    |-  ( ph  ->  ( F  o F R G )  =  ( F  o F ( R  |`  ( B  X.  B ) ) G ) )
 
13-Feb-2018df-itgm 24617 Define the Bochner integral as the extension by continuity of the Bochnel integral for simple functions.

Bogachev first defines 'fundamental in the mean' sequences, in definition 2.3.1 of [Bogachev] p. 116, and notes that those are actually Cauchy sequences for the pseudometric  ( wsitm m ).

He then defines the Bochner integral in chapter 2.4.4 in [Bogachev] p. 118. The definition of the Lebesgue integral, df-itg 19469.

(Contributed by Thierry Arnoux, 13-Feb-2018.)

 |- itgm  =  ( w  e.  _V ,  m  e.  U. ran measures  |->  ( ( (metUnif `  ( wsitm m ) )CnExt (UnifSt `  w ) ) `  ( wsitg m ) ) )
 
13-Feb-2018sitmcl 24616 Closure of the integral distance between two simple functions, for an extended metric space. (Contributed by Thierry Arnoux, 13-Feb-2018.)
 |-  ( ph  ->  W  e.  Mnd )   &    |-  ( ph  ->  W  e.  * MetSp )   &    |-  ( ph  ->  M  e.  U. ran measures )   &    |-  ( ph  ->  F  e.  dom  ( Wsitg M ) )   &    |-  ( ph  ->  G  e.  dom  ( Wsitg M ) )   =>    |-  ( ph  ->  ( F ( Wsitm M ) G )  e.  (
 0 [,]  +oo ) )
 
13-Feb-2018sitgf 24613 The integral for simple functions is itself a function. (Contributed by Thierry Arnoux, 13-Feb-2018.)
 |-  B  =  ( Base `  W )   &    |-  J  =  ( TopOpen `  W )   &    |-  S  =  (sigaGen `  J )   &    |-  .0.  =  ( 0g `  W )   &    |- 
 .x.  =  ( .s `  W )   &    |-  H  =  (RRHom `  (Scalar `  W )
 )   &    |-  ( ph  ->  W  e.  V )   &    |-  ( ph  ->  M  e.  U. ran measures )   &    |-  (
 ( ph  /\  f  e. 
 dom  ( Wsitg M ) )  ->  ( ( Wsitg M ) `  f )  e.  B )   =>    |-  ( ph  ->  ( Wsitg M ) : dom  ( Wsitg M ) --> B )
 
12-Feb-2018iprodgam 25272 An infinite product version of Euler's gamma function. (Contributed by Scott Fenton, 12-Feb-2018.)
 |-  ( ph  ->  A  e.  ( CC  \  ( ZZ  \  NN ) ) )   =>    |-  ( ph  ->  (
 _G `  A )  =  ( prod_ k  e.  NN ( ( ( 1  +  ( 1  /  k ) )  ^ c  A )  /  (
 1  +  ( A 
 /  k ) ) )  /  A ) )
 
11-Feb-2018iprodefisum 25271 Applying the exponential function to an infinite sum yields an infinite product. (Contributed by Scott Fenton, 11-Feb-2018.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  =  B )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  B  e.  CC )   &    |-  ( ph  ->  seq  M (  +  ,  F )  e.  dom  ~~>  )   =>    |-  ( ph  ->  prod_ k  e.  Z ( exp `  B )  =  ( exp ` 
 sum_ k  e.  Z  B ) )
 
11-Feb-2018iprodefisumlem 25270 Lemma for iprodefisum 25271. (Contributed by Scott Fenton, 11-Feb-2018.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F : Z --> CC )   =>    |-  ( ph  ->  seq 
 M (  x.  ,  ( exp  o.  F ) )  =  ( exp 
 o.  seq  M (  +  ,  F )
 ) )
 
11-Feb-2018pstmxmet 24245 The metric induced by a pseudometric is a full-fledged metric on the equivalence classes of the metric identification. (Contributed by Thierry Arnoux, 11-Feb-2018.)
 |-  .~  =  (~Met `  D )   =>    |-  ( D  e.  (PsMet `  X )  ->  (pstoMet `  D )  e.  ( * Met `  ( X /.  .~  ) ) )
 
11-Feb-2018pstmfval 24244 Function value of the metric induced by a pseudometric  D (Contributed by Thierry Arnoux, 11-Feb-2018.)
 |-  .~  =  (~Met `  D )   =>    |-  (
 ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  ->  ( [ A ]  .~  (pstoMet `  D ) [ B ]  .~  )  =  ( A D B ) )
 
11-Feb-2018metider 24242 The metric identification is an equivalence relation. (Contributed by Thierry Arnoux, 11-Feb-2018.)
 |-  ( D  e.  (PsMet `  X )  ->  (~Met `  D )  Er  X )
 
11-Feb-2018tltnle 24143 In a Toset, less-than is equivalent to not inverse less-than-or-equal see pltnle 14378. (Contributed by Thierry Arnoux, 11-Feb-2018.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .<  =  ( lt `  K )   =>    |-  ( ( K  e. Toset