mmtheorems169 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17500 176 17501-17600 177 17601-17700 178 17701-17800 179 17801-17900 180 17901-18000 181 18001-18100 182 18101-18200 183 18201-18300 184 18301-18400 185 18401-18500 186 18501-18600 187 18601-18700 188 18701-18800 189 18801-18900 190 18901-19000 191 19001-19026

Statement List for Metamath Proof Explorer - 16801-16900 - Page 169 of 191

Type	Label	Description
Statement
Theorem	heiborlem23 16801	Lemma for heibor 16821. If a set has no finite subcover, then there exists a ball of any given radius whose intersection with the set also has no finite subcover. This lemma relies on the totally bounded condition to show that S can be covered by finitely many balls. [Auxiliary lemma - not displayed.]
Theorem	heiborlem24 16802	Lemma for heibor 16821. The set B consists of ordered pairs of centers and radii of balls which have no finite subcover. [Auxiliary lemma - not displayed.]
Theorem	heiborlem25 16803	Lemma for heibor 16821. The value of the function G, which takes a ball and a natural number and gives the set of all balls of the form given in heiborlem22 16800. This is part of the setup for the use of the Axiom of Dependent Choice acdc2 9157 in heiborlem41 16819. [Auxiliary lemma - not displayed.]
Theorem	heiborlem26 16804	Lemma for heibor 16821. The value of the function G. [Auxiliary lemma - not displayed.]
Theorem	heiborlem27 16805	Lemma for heibor 16821. The value of G is a subset of B. [Auxiliary lemma - not displayed.]
Theorem	heiborlem28 16806	Lemma for heibor 16821. The value of G is nonempty, due to the existence proven in heiborlem23 16801. [Auxiliary lemma - not displayed.]
Theorem	heiborlem29 16807	Lemma for heibor 16821. Property of G required for the application of acdc2 9157. [Auxiliary lemma - not displayed.]
Theorem	heiborlem30 16808	Lemma for heibor 16821. The first in a series of lemmas giving properties of the function H which will be constructed by acdc2 9157. H is a sequence of balls with radii in a decreasing geometric progression. [Auxiliary lemma - not displayed.]
Theorem	heiborlem31 16809	Lemma for heibor 16821. Consecutive balls in the sequence H have nonzero intersection. [Auxiliary lemma - not displayed.]
Theorem	heiborlem32 16810	Lemma for heibor 16821. Bound on the distance between centers of consecutive balls in H. [Auxiliary lemma - not displayed.]
Theorem	heiborlem33 16811	Lemma for heibor 16821. The centers of the balls in H form a Cauchy sequence. [Auxiliary lemma - not displayed.]
Theorem	heiborlem34 16812	Lemma for heibor 16821. If Y is the limit of the Cauchy sequence from heiborlem33 16811, then bound the distance between Y and the center of a ball in H. [Auxiliary lemma - not displayed.]
Theorem	heiborlem35 16813	Lemma for heibor 16821. Bound the distance between a point in a ball in H and the ball's center. [Auxiliary lemma - not displayed.]
Theorem	heiborlem36 16814	Lemma for heibor 16821. Combine the two bounds in heiborlem34 16812 and heiborlem35 16813 to get a ball in H lying completely within a ball of arbitrary radius about Y. [Auxiliary lemma - not displayed.]
Theorem	heiborlem37 16815	Lemma for heibor 16821. Since U is an open cover of X, there is an element of U containing a ball around Y, and thus containing a ball in H. [Auxiliary lemma - not displayed.]
Theorem	heiborlem38 16816	Lemma for heibor 16821. The ball which is contained in an element of U has a finite subcover, namely the single element containing it. [Auxiliary lemma - not displayed.]
Theorem	heiborlem39 16817	Lemma for heibor 16821. The conclusion of heiborlem38 16816 contradicts the construction of H, whose elements do not have finite subcovers. [Auxiliary lemma - not displayed.]
Theorem	heiborlem40 16818	Lemma for heibor 16821. If B were non-empty, then we could apply the Axiom of Dependent Choice acdc2 9157 to arrive at a contradiction heiborlem39 16817. [Auxiliary lemma - not displayed.]
Theorem	heiborlem41 16819	Lemma for heibor 16821. Apply the previous result to the entire metric space M, which is equal to a ball since it is totally bounded hence bounded by totbndbnd 16768. [Auxiliary lemma - not displayed.]
Theorem	heiborlem42 16820	Lemma for heibor 16821. Use the deduction theorem. Since every open cover has a finite subcover, J is compact. [Auxiliary lemma - not displayed.]
Theorem	heibor 16821	Generalized Heine-Borel Theorem. A metric space is compact iff it is complete and totally bounded.
|- J = (MetOpen` M)   &   |- X = dom dom M   =>   |- (M e. Met -> (J e. Comp <-> (M e. CMet /\ M e. TotBnd)))
Banach Fixed Point Theorem
Theorem	bfplem1 16822	Lemma for bfp 16833. We construct a sequence G by repeatedly applying F to a starting value Y. [Auxiliary lemma - not displayed.]
Theorem	bfplem2 16823	Lemma for bfp 16833. The first element in the sequence is Y. [Auxiliary lemma - not displayed.]
Theorem	bfplem3 16824	Lemma for bfp 16833. The next element in the sequence is obtained by applying F to the previous element. [Auxiliary lemma - not displayed.]
Theorem	bfplem4 16825	Lemma for bfp 16833. Define the initial distance D. [Auxiliary lemma - not displayed.]
Theorem	bfplem5 16826	Lemma for bfp 16833. Recursively bound the distance between consecutive elements of the sequence G based on the contraction property. [Auxiliary lemma - not displayed.]
Theorem	bfplem6 16827	Lemma for bfp 16833. Bound the distance between consecutive elements of the sequence G by applying bfplem5 16826 inductively. [Auxiliary lemma - not displayed.]
Theorem	bfplem7 16828	Lemma for bfp 16833. Use geomcau 16673 to show that G is a Cauchy sequence, which then converges as M is complete. [Auxiliary lemma - not displayed.]
Theorem	bfplem8 16829	Lemma for bfp 16833. The limit of G is a fixed point of F. [Auxiliary lemma - not displayed.]
Theorem	bfplem9 16830	Lemma for bfp 16833. The fixed point is unique. [Auxiliary lemma - not displayed.]
Theorem	bfplem10 16831	Lemma for bfp 16833. F has exactly one fixed point. [Auxiliary lemma - not displayed.]
Theorem	bfplem11 16832	Lemma for bfp 16833. Apply the deduction theorem. [Auxiliary lemma - not displayed.]
Theorem	bfp 16833	Banach fixed point theorem, also known as contraction mapping theorem. A contraction on a complete metric space has a unique fixed point.
|- X = dom dom M   =>   |- (((M e. CMet /\ X =/= (/)) /\ (K e. RR+ /\ K < 1) /\ (F:X-->X /\ A.x e. X A.y e. X ((F` x)M(F` y)) <_ (K x. (xMy)))) -> E!z e. X (F` z) = z)
Euclidean space
Theorem	recms 16834	The real numbers are a complete metric space.
|- ((abs o. - ) |` (RR X. RR)) e. CMet
Syntax	crrn 16835	Extend class notation with the n-dimensional Euclidean space.
class RRn
Definition	df-rrn 16836	Define n-dimensional Euclidean space as a metric space with the standard Euclidean norm given by the quadratic mean.
|- RRn = {<.n, r>. | (n e. NN /\ r = {<.<.x, y>., d>. | ((x e. (RR ^m (1...n)) /\ y e. (RR ^m (1...n))) /\ d = (sqr` sum_k e. (1...n)(((x` k) - (y` k))^2)))})}
Theorem	rrnval 16837	The n-dimensional Euclidean space.
|- (N e. NN -> (RRn` N) = {<.<.x, y>., d>. | ((x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N))) /\ d = (sqr` sum_k e. (1...N)(((x` k) - (y` k))^2)))})
Theorem	rrnmval 16838	The value of the Euclidean metric.
|- ((N e. NN /\ X e. (RR ^m (1...N)) /\ Y e. (RR ^m (1...N))) -> (X(RRn` N)Y) = (sqr` sum_k e. (1...N)(((X` k) - (Y` k))^2)))
Theorem	rrndm 16839	The underlying set of Euclidean space.
|- (N e. NN -> dom dom (RRn` N) = (RR ^m (1...N)))
Theorem	rrnmet 16840	Euclidean space is a metric space.
|- (N e. NN -> (RRn` N) e. Met)
Theorem	rrndstprj1 16841	The distance between two points in Euclidean space is greater than the distance between the projections onto one coordinate.
|- M = ((abs o. - ) |` (RR X. RR))   &   |- X = (RR ^m (1...N))   =>   |- (((N e. NN /\ A e. (1...N)) /\ (F e. X /\ G e. X)) -> ((F` A)M(G` A)) <_ (F(RRn` N)G))
Theorem	rrndstprj2 16842	Bound on the distance between two points in Euclidean space given bounds on the distances in each coordinate. This theorem and rrndstprj1 16841 can be used to show that the supremum norm and Euclidean norm are equivalent.
|- M = ((abs o. - ) |` (RR X. RR))   &   |- X = (RR ^m (1...N))   =>   |- (((N e. NN /\ F e. X /\ G e. X) /\ (R e. RR+ /\ A.n e. (1...N)((F` n)M(G` n)) < R)) -> (F(RRn` N)G) < (R x. (sqr` N)))
Theorem	rrncms 16843	Euclidean space is complete.
|- (N e. NN -> (RRn` N) e. CMet)
Theorem	rrntotbndlem1 16844	Lemma for rrntotbnd 16846. [Auxiliary lemma - not displayed.]
Theorem	rrntotbndlem2 16845	Lemma for rrntotbnd 16846. [Auxiliary lemma - not displayed.]
Theorem	rrntotbnd 16846	A set in Euclidean space is totally bounded iff its is bounded.
|- X = (RR ^m (1...N))   &   |- M = ((RRn` N) |` (Y X. Y))   =>   |- ((N e. NN /\ Y C_ X) -> (M e. TotBnd <-> M e. Bnd))
Theorem	rrnheibor 16847	Heine-Borel theorem for Euclidean space. A subset of Euclidean space is compact iff it is closed and bounded.
|- X = (RR ^m (1...N))   &   |- M = ((RRn` N) |` (Y X. Y))   &   |- T = (MetOpen` M)   &   |- U = (MetOpen` (RRn` N))   =>   |- ((N e. NN /\ Y C_ X) -> (T e. Comp <-> (Y e. (Clsd` U) /\ M e. Bnd)))
Intervals (continued)
Theorem	ismrer1 16848	An isometry between RR and RR^1.
|- R = ((abs o. - ) |` (RR X. RR))   &   |- F = {<.x, y>. | (x e. RR /\ y = ({1} X. {x}))}   =>   |- F e. (RIsmty(RRn` 1))
Theorem	reheibor 16849	Heine-Borel theorem for real numbers. A subset of RR is compact iff it is closed and bounded.
|- R = ((abs o. - ) |` (RR X. RR))   &   |- M = (R |` (Y X. Y))   &   |- T = (MetOpen` M)   &   |- U = (MetOpen` R)   =>   |- (Y C_ RR -> (T e. Comp <-> (Y e. (Clsd` U) /\ M e. Bnd)))
Theorem	iccbnd 16850	A closed interval in RR is bounded.
|- J = (A[,]B)   &   |- M = ((abs o. - ) |` (J X. J))   =>   |- ((A e. RR /\ B e. RR) -> M e. Bnd)
Theorem	icccmp 16851	A closed interval in RR is compact.
|- J = (A[,]B)   &   |- M = ((abs o. - ) |` (J X. J))   &   |- T = (MetOpen` M)   =>   |- ((A e. RR /\ B e. RR) -> T e. Comp)
Theorem	iicmp 16852	The unit interval is compact.
|- II e. Comp
Groups and related structures
Theorem	exidcl 16853	Closure of the binary operation of a magma with identity.
|- X = ran G   =>   |- ((G e. (Magma i^i ExId ) /\ A e. X /\ B e. X) -> (AGB) e. X)
Theorem	exidreslem 16854	Lemma for exidres 16855 and exidresid 16856. [Auxiliary lemma - not displayed.]
Theorem	exidres 16855	The restriction of a binary operation with identity to a subset containing the identity has an identity element.
|- X = ran G   &   |- U = (Id` G)   &   |- H = (G |` (Y X. Y))   =>   |- ((G e. (Magma i^i ExId ) /\ Y C_ X /\ U e. Y) -> H e. ExId )
Theorem	exidresid 16856	The restriction of a binary operation with identity to a subset containing the identity has the same identity element.
|- X = ran G   &   |- U = (Id` G)   &   |- H = (G |` (Y X. Y))   =>   |- (((G e. (Magma i^i ExId ) /\ Y C_ X /\ U e. Y) /\ H e. Magma) -> (Id` H) = U)
Theorem	isgrpda 16857	Properties that determine a group operation.
|- (ph -> X e. _V)   &   |- (ph -> G:(X X. X)-->X)   &   |- ((ph /\ (x e. X /\ y e. X /\ z e. X)) -> ((xGy)Gz) = (xG(yGz)))   &   |- (ph -> U e. X)   &   |- ((ph /\ x e. X) -> (UGx) = x)   &   |- ((ph /\ x e. X) -> E.n e. X (nGx) = U)   =>   |- (ph -> G e. GrpOp)
Theorem	isgrpd 16858	Properties that determine a group operation.
|- (ph -> X e. _V)   &   |- (ph -> G:(X X. X)-->X)   &   |- ((ph /\ (x e. X /\ y e. X /\ z e. X)) -> ((xGy)Gz) = (xG(yGz)))   &   |- (ph -> U e. X)   &   |- ((ph /\ x e. X) -> (UGx) = x)   &   |- ((ph /\ x e. X) -> N e. X)   &   |- ((ph /\ x e. X) -> (NGx) = U)   =>   |- (ph -> G e. GrpOp)
Theorem	isablda 16859	Properties that determine an Abelian group operation.
|- (ph -> X e. _V)   &   |- (ph -> G:(X X. X)-->X)   &   |- ((ph /\ (x e. X /\ y e. X /\ z e. X)) -> ((xGy)Gz) = (xG(yGz)))   &   |- (ph -> U e. X)   &   |- ((ph /\ x e. X) -> (UGx) = x)   &   |- ((ph /\ x e. X) -> E.n e. X (nGx) = U)   &   |- ((ph /\ (x e. X /\ y e. X)) -> (xGy) = (yGx))   =>   |- (ph -> G e. AbelOp)
Theorem	isabld 16860	Properties that determine an Abelian group operation.
|- (ph -> X e. _V)   &   |- (ph -> G:(X X. X)-->X)   &   |- ((ph /\ (x e. X /\ y e. X /\ z e. X)) -> ((xGy)Gz) = (xG(yGz)))   &   |- (ph -> U e. X)   &   |- ((ph /\ x e. X) -> (UGx) = x)   &   |- ((ph /\ x e. X) -> N e. X)   &   |- ((ph /\ x e. X) -> (NGx) = U)   &   |- ((ph /\ (x e. X /\ y e. X)) -> (xGy) = (yGx))   =>   |- (ph -> G e. AbelOp)
Theorem	abl4pnp 16861	A commutative/associative law for Abelian groups.
|- X = ran G   &   |- D = ( /g ` G)   =>   |- ((G e. AbelOp /\ ((A e. X /\ B e. X) /\ (C e. X /\ F e. X))) -> ((AGB)D(CGF)) = ((ADC)G(BDF)))
Theorem	grpeqdivid 16862	Two group elements are equal iff their quotient is the identity.
|- X = ran G   &   |- U = (Id` G)   &   |- D = ( /g ` G)   =>   |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (A = B <-> (ADB) = U))
Theorem	ghomf 16863	Mapping property of a group homomorphism.
|- X = ran G   &   |- W = ran H   =>   |- ((G e. GrpOp /\ H e. GrpOp /\ F e. (G GrpHom H)) -> F:X-->W)
Theorem	ghomco 16864	The composition of two group homomorphisms is a group homomorphism.
|- (((G e. GrpOp /\ H e. GrpOp /\ K e. GrpOp) /\ (S e. (G GrpHom H) /\ T e. (H GrpHom K))) -> (T o. S) e. (G GrpHom K))
Theorem	ghomdiv 16865	Group homomorphisms preserve division.
|- X = ran G   &   |- D = ( /g ` G)   &   |- C = ( /g ` H)   =>   |- (((G e. GrpOp /\ H e. GrpOp /\ F e. (G GrpHom H)) /\ (A e. X /\ B e. X)) -> (F` (ADB)) = ((F` A)C(F` B)))
Theorem	grpkerinj 16866	A group homomorphism is injective if and only if its kernel is zero.
|- X = ran G   &   |- W = (Id` G)   &   |- Y = ran H   &   |- U = (Id` H)   =>   |- ((G e. GrpOp /\ H e. GrpOp /\ F e. (G GrpHom H)) -> (F:X-1-1->Y <-> (`'F"{U}) = {W}))
Path homotopy
Syntax	cphtpy 16867	Extend class notation with the class of path homotopies between two continuous functions.
class PHtpy
Syntax	cphtpc 16868	Extend class notation with the path homotopy relation.
class ~=ph
Definition	df-phtpy 16869	Define the function which takes a topological space X and two continuous functions F:II-->X and G:II-->X and returns the class of path homotopies from F to G. Definition of [Hatcher] p. 25.
|- PHtpy = {<.x, y>. | (x e. Top /\ y = {<.<.f, g>., z>. | (((f e. (II Cn x) /\ g e. (II Cn x)) /\ ((f` 0) = (g` 0) /\ (f` 1) = (g` 1))) /\ z = {h e. ((II X.t II) Cn x) | A.s e. (0[,]1)(((sh0) = (f` s) /\ (sh1) = (g` s)) /\ ((0hs) = (f` 0) /\ (1hs) = (f` 1)))})})}
Theorem	phtpyfval 16870	Value of the path homotopy function on a topology.
|- (J e. Top -> (PHtpy` J) = {<.<.f, g>., z>. | (((f e. (II Cn J) /\ g e. (II Cn J)) /\ ((f` 0) = (g` 0) /\ (f` 1) = (g` 1))) /\ z = {h e. ((II X.t II) Cn J) | A.s e. (0[,]1)(((sh0) = (f` s) /\ (sh1) = (g` s)) /\ ((0hs) = (f` 0) /\ (1hs) = (f` 1)))})})
Theorem	phtpyval 16871	The class of path homotopies between two continuous functions.
|- (((J e. Top /\ F e. (II Cn J) /\ G e. (II Cn J)) /\ ((F` 0) = (G` 0) /\ (F` 1) = (G` 1))) -> (F(PHtpy` J)G) = {h e. ((II X.t II) Cn J) | A.s e. (0[,]1)(((sh0) = (F` s) /\ (sh1) = (G` s)) /\ ((0hs) = (F` 0) /\ (1hs) = (F` 1)))})
Theorem	isphtpy 16872	Membership in the class of path homotopies between two continuous functions.
|- (((J e. Top /\ F e. (II Cn J) /\ G e. (II Cn J)) /\ ((F` 0) = (G` 0) /\ (F` 1) = (G` 1))) -> (H e. (F(PHtpy` J)G) <-> (H e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sH0) = (F` s) /\ (sH1) = (G` s)) /\ ((0Hs) = (F` 0) /\ (1Hs) = (F` 1))))))
Theorem	phtpyid 16873	A homotopy from a path to itself.
|- H = {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` x))}   =>   |- ((J e. Top /\ F e. (II Cn J)) -> H e. (F(PHtpy` J)F))
Theorem	phtpycom 16874	Given a homotopy from F to G, produce a homotopy from G to F.
|- K = {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (xH(1 - y)))}   =>   |- (((J e. Top /\ F e. (II Cn J) /\ G e. (II Cn J)) /\ ((F` 0) = (G` 0) /\ (F` 1) = (G` 1))) -> (H e. (F(PHtpy` J)G) -> K e. (G(PHtpy` J)F)))
Theorem	phtpycolem1 16875	Lemma for phtpyco 16880. [Auxiliary lemma - not displayed.]
Theorem	phtpycolem2 16876	Lemma for phtpyco 16880. [Auxiliary lemma - not displayed.]
Theorem	phtpycolem3 16877	Lemma for phtpyco 16880. [Auxiliary lemma - not displayed.]
Theorem	phtpycolem4 16878	Lemma for phtpyco 16880. [Auxiliary lemma - not displayed.]
Theorem	phtpycolem5 16879	Lemma for phtpyco 16880. [Auxiliary lemma - not displayed.]
Theorem	phtpyco 16880	Concatenate two path homotopies.
|- M = {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(y <_ (1 / 2), (xK(2 x. y)), (xL((2 x. y) - 1))))}   =>   |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J)) /\ (((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1)))) -> ((K e. (F(PHtpy` J)G) /\ L e. (G(PHtpy` J)H)) -> M e. (F(PHtpy` J)H)))
Definition	df-phtpc 16881	Define the function which takes a topology and returns the path homotopy relation on that topology. Definition of [Hatcher] p. 25.
|- ~=ph = {<.x, y>. | (x e. Top /\ y = {<.f, g>. | (((f e. (II Cn x) /\ g e. (II Cn x)) /\ ((f` 0) = (g` 0) /\ (f` 1) = (g` 1))) /\ (f(PHtpy` x)g) =/= (/))})}
Theorem	phtpcval 16882	The value of the path homotopy relation.
|- (J e. Top -> (~=ph` J) = {<.f, g>. | (((f e. (II Cn J) /\ g e. (II Cn J)) /\ ((f` 0) = (g` 0) /\ (f` 1) = (g` 1))) /\ (f(PHtpy` J)g) =/= (/))})
Theorem	isphtpc 16883	The relation "is path homotopic to".
|- ((J e. Top /\ F e. A /\ G e. B) -> (F(~=ph` J)G <-> (((F e. (II Cn J) /\ G e. (II Cn J)) /\ ((F` 0) = (G` 0) /\ (F` 1) = (G` 1))) /\ (F(PHtpy` J)G) =/= (/))))
Theorem	isphtpc2 16884	The relation "is path homotopic to".
|- ((J e. Top /\ G e. A) -> (F(~=ph` J)G <-> (((F e. (II Cn J) /\ G e. (II Cn J)) /\ ((F` 0) = (G` 0) /\ (F` 1) = (G` 1))) /\ (F(PHtpy` J)G) =/= (/))))
Theorem	phtpcdm 16885	The domain of the path homotopy relation.
|- (J e. Top -> dom (~=ph` J) = (II Cn J))
Theorem	phtpcer 16886	Path homotopy is an equivalence relation. Proposition 1.2 of [Hatcher] p. 26.
|- (J e. Top -> Er (~=ph` J))
Theorem	reparphtlem1 16887	Lemma for reparpht 16889. [Auxiliary lemma - not displayed.]
Theorem	reparphtlem2 16888	Lemma for reparpht 16889. [Auxiliary lemma - not displayed.]
Theorem	reparpht 16889	Reparametrization lemma. The reparametrization of a path by any continuous map G:II-->II with G(0) = 0 and G(1) = 1 is path-homotopic to the original path.
|- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> (F o. G)(~=ph` J)F)
The fundamental group
Syntax	cpi1b 16890	Extend class notation with the base set of the fundamental group.
class pi1b
Syntax	cpco 16891	Extend class notation with the concatenation operation for paths in a topological space.
class *p
Syntax	cpi1 16892	Extend class notation with the fundamental group.
class pi1
Definition	df-pco 16893	Define the concatenation of two paths in a topological space J whose endpoints line up. Definition of [Hatcher] p. 26. Hatcher denotes path concatenation with a square dot; other authors, such as Munkres, use a star.
|- *p = {<.j, z>. | (j e. Top /\ z = {<.<.f, g>., h>. | (((f e. (II Cn j) /\ g e. (II Cn j)) /\ (f` 1) = (g` 0)) /\ h = {<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), (f` (2 x. x)), (g` ((2 x. x) - 1))))})})}
Definition	df-pi1b 16894	Define the base set of the fundamental group of J at Y as the set of equivalence classes of loops in J based at Y. The group structure is defined in df-pi1 16895.
|- pi1b = {<.<.j, y>., p>. | ((j e. Top /\ y e. U.j) /\ p = {g | E.f e. (II Cn j)(((f` 0) = y /\ (f` 1) = y) /\ g = [f](~=ph` j))})}
Definition	df-pi1 16895	Define the fundamental group, whose operation is given by concatenation of homotopy classes of loops. Definition of [Hatcher] p. 26.
|- pi1 = {<.<.j, y>., p>. | ((j e. Top /\ y e. U.j) /\ p = {<.<.f, g>., h>. | E.m e. {t e. (II Cn j) | ((t` 0) = y /\ (t` 1) = y)}E.n e. {t e. (II Cn j) | ((t` 0) = y /\ (t` 1) = y)} ((f = [m](~=ph` j) /\ g = [n](~=ph` j)) /\ h = [(m(*p` j)n)](~=ph` j))})}
Theorem	pcofval 16896	The value of the path concatenation function on a topological space.
|- (J e. Top -> (*p` J) = {<.<.f, g>., h>. | (((f e. (II Cn J) /\ g e. (II Cn J)) /\ (f` 1) = (g` 0)) /\ h = {<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), (f` (2 x. x)), (g` ((2 x. x) - 1))))})})
Theorem	pcoval 16897	The concatenation of two paths.
|- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> (F(*p` J)G) = {<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), (F` (2 x. x)), (G` ((2 x. x) - 1))))})
Theorem	pcoval1 16898	Evaluate the concatenation of two paths on the first half.
|- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ X e. (0[,](1 / 2))) -> ((F(*p` J)G)` X) = (F` (2 x. X)))
Theorem	pcoval2 16899	Evaluate the concatenation of two paths on the second half.
|- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ X e. ((1 / 2)[,]1)) -> ((F(*p` J)G)` X) = (G` ((2 x. X) - 1)))
Theorem	pcocn 16900	The concatenation of two paths is a path.
|- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> (F(*p` J)G) e. (II Cn J))