P. 217 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21601-21700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	htpycom 21601*	Given a homotopy from F to G, produce a homotopy from G to F. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F e. ( J Cn K ) )   &    |- ( ph -> G e. ( J Cn K ) )   &    |- M = ( x e. X , y e. ( 0 [,] 1 ) |-> ( x H ( 1 - y ) ) )   &    |- ( ph -> H e. ( F ( J Htpy K ) G ) )   =>    |- ( ph -> M e. ( G ( J Htpy K ) F ) )
Theorem	htpyid 21602*	A homotopy from a function to itself. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- G = ( x e. X , y e. ( 0 [,] 1 ) |-> ( F ` x ) )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F e. ( J Cn K ) )   =>    |- ( ph -> G e. ( F ( J Htpy K ) F ) )
Theorem	htpyco1 21603*	Compose a homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.)
|- N = ( x e. X , y e. ( 0 [,] 1 ) |-> ( ( P ` x ) H y ) )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> P e. ( J Cn K ) )   &    |- ( ph -> F e. ( K Cn L ) )   &    |- ( ph -> G e. ( K Cn L ) )   &    |- ( ph -> H e. ( F ( K Htpy L ) G ) )   =>    |- ( ph -> N e. ( ( F o. P ) ( J Htpy L ) ( G o. P ) ) )
Theorem	htpyco2 21604	Compose a homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.)
|- ( ph -> F e. ( J Cn K ) )   &    |- ( ph -> G e. ( J Cn K ) )   &    |- ( ph -> P e. ( K Cn L ) )   &    |- ( ph -> H e. ( F ( J Htpy K ) G ) )   =>    |- ( ph -> ( P o. H ) e. ( ( P o. F ) ( J Htpy L ) ( P o. G ) ) )
Theorem	htpycc 21605*	Concatenate two homotopies. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.)
|- N = ( x e. X , y e. ( 0 [,] 1 ) |-> if ( y <_ ( 1 / 2 ) , ( x L ( 2 x. y ) ) , ( x M ( ( 2 x. y ) - 1 ) ) ) )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F e. ( J Cn K ) )   &    |- ( ph -> G e. ( J Cn K ) )   &    |- ( ph -> H e. ( J Cn K ) )   &    |- ( ph -> L e. ( F ( J Htpy K ) G ) )   &    |- ( ph -> M e. ( G ( J Htpy K ) H ) )   =>    |- ( ph -> N e. ( F ( J Htpy K ) H ) )
Theorem	isphtpy 21606*	Membership in the class of path homotopies between two continuous functions. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   =>    |- ( ph -> ( H e. ( F ( PHtpy ` J ) G ) <-> ( H e. ( F ( II Htpy J ) G ) /\ A. s e. ( 0 [,] 1 ) ( ( 0 H s ) = ( F ` 0 ) /\ ( 1 H s ) = ( F ` 1 ) ) ) ) )
Theorem	phtpyhtpy 21607	A path homotopy is a homotopy. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   =>    |- ( ph -> ( F ( PHtpy ` J ) G ) C_ ( F ( II Htpy J ) G ) )
Theorem	phtpycn 21608	A path homotopy is a continuous function. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   =>    |- ( ph -> ( F ( PHtpy ` J ) G ) C_ ( ( II tX II ) Cn J ) )
Theorem	phtpyi 21609	Membership in the class of path homotopies between two continuous functions. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   &    |- ( ph -> H e. ( F ( PHtpy ` J ) G ) )   =>    |- ( ( ph /\ A e. ( 0 [,] 1 ) ) -> ( ( 0 H A ) = ( F ` 0 ) /\ ( 1 H A ) = ( F ` 1 ) ) )
Theorem	phtpy01 21610	Two path-homotopic paths have the same start and end point. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   &    |- ( ph -> H e. ( F ( PHtpy ` J ) G ) )   =>    |- ( ph -> ( ( F ` 0 ) = ( G ` 0 ) /\ ( F ` 1 ) = ( G ` 1 ) ) )
Theorem	isphtpyd 21611*	Deduction for membership in the class of path homotopies. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   &    |- ( ph -> H e. ( F ( II Htpy J ) G ) )   &    |- ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 0 H s ) = ( F ` 0 ) )   &    |- ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 1 H s ) = ( F ` 1 ) )   =>    |- ( ph -> H e. ( F ( PHtpy ` J ) G ) )
Theorem	isphtpy2d 21612*	Deduction for membership in the class of path homotopies. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   &    |- ( ph -> H e. ( ( II tX II ) Cn J ) )   &    |- ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( s H 0 ) = ( F ` s ) )   &    |- ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( s H 1 ) = ( G ` s ) )   &    |- ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 0 H s ) = ( F ` 0 ) )   &    |- ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 1 H s ) = ( F ` 1 ) )   =>    |- ( ph -> H e. ( F ( PHtpy ` J ) G ) )
Theorem	phtpycom 21613*	Given a homotopy from F to G, produce a homotopy from G to F. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   &    |- K = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x H ( 1 - y ) ) )   &    |- ( ph -> H e. ( F ( PHtpy ` J ) G ) )   =>    |- ( ph -> K e. ( G ( PHtpy ` J ) F ) )
Theorem	phtpyid 21614*	A homotopy from a path to itself. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.)
|- G = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( F ` x ) )   &    |- ( ph -> F e. ( II Cn J ) )   =>    |- ( ph -> G e. ( F ( PHtpy ` J ) F ) )
Theorem	phtpyco2 21615	Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   &    |- ( ph -> P e. ( J Cn K ) )   &    |- ( ph -> H e. ( F ( PHtpy ` J ) G ) )   =>    |- ( ph -> ( P o. H ) e. ( ( P o. F ) ( PHtpy ` K ) ( P o. G ) ) )
Theorem	phtpycc 21616*	Concatenate two path homotopies. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 7-Jun-2014.)
|- M = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> if ( y <_ ( 1 / 2 ) , ( x K ( 2 x. y ) ) , ( x L ( ( 2 x. y ) - 1 ) ) ) )   &    |- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   &    |- ( ph -> H e. ( II Cn J ) )   &    |- ( ph -> K e. ( F ( PHtpy ` J ) G ) )   &    |- ( ph -> L e. ( G ( PHtpy ` J ) H ) )   =>    |- ( ph -> M e. ( F ( PHtpy ` J ) H ) )
Definition	df-phtpc 21617*	Define the function which takes a topology and returns the path homotopy relation on that topology. Definition of [Hatcher] p. 25. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Jun-2014.)
|- ~=ph = ( x e. Top |-> { <. f , g >. | ( { f , g } C_ ( II Cn x ) /\ ( f ( PHtpy ` x ) g ) =/= (/) ) } )
Theorem	phtpcrel 21618	The path homotopy relation is a relation. (Contributed by Mario Carneiro, 7-Jun-2014.) (Revised by Mario Carneiro, 7-Aug-2014.)
|- Rel ( ~=ph ` J )
Theorem	isphtpc 21619	The relation "is path homotopic to". (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Sep-2015.)
|- ( F ( ~=ph ` J ) G <-> ( F e. ( II Cn J ) /\ G e. ( II Cn J ) /\ ( F ( PHtpy ` J ) G ) =/= (/) ) )
Theorem	phtpcer 21620	Path homotopy is an equivalence relation. Proposition 1.2 of [Hatcher] p. 26. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 6-Jul-2015.)
|- ( ~=ph ` J ) Er ( II Cn J )
Theorem	phtpc01 21621	Path homotopic paths have the same endpoints. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( F ( ~=ph ` J ) G -> ( ( F ` 0 ) = ( G ` 0 ) /\ ( F ` 1 ) = ( G ` 1 ) ) )
Theorem	reparphti 21622*	Lemma for reparpht 21623. (Contributed by NM, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn II ) )   &    |- ( ph -> ( G ` 0 ) = 0 )   &    |- ( ph -> ( G ` 1 ) = 1 )   &    |- H = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( F ` ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) )   =>    |- ( ph -> H e. ( ( F o. G ) ( PHtpy ` J ) F ) )
Theorem	reparpht 21623	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. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn II ) )   &    |- ( ph -> ( G ` 0 ) = 0 )   &    |- ( ph -> ( G ` 1 ) = 1 )   =>    |- ( ph -> ( F o. G ) ( ~=ph ` J ) F )
Theorem	phtpcco2 21624	Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 6-Jul-2015.)
|- ( ph -> F ( ~=ph ` J ) G )   &    |- ( ph -> P e. ( J Cn K ) )   =>    |- ( ph -> ( P o. F ) ( ~=ph ` K ) ( P o. G ) )
12.4.13  The fundamental group
Syntax	cpco 21625	Extend class notation with the concatenation operation for paths in a topological space.
class *p
Syntax	comi 21626	Extend class notation with the loop space.
class Om1
Syntax	comn 21627	Extend class notation with the higher loop spaces.
class OmN
Syntax	cpi1 21628	Extend class notation with the fundamental group.
class pi1
Syntax	cpin 21629	Extend class notation with the higher homotopy groups.
class piN
Definition	df-pco 21630*	Define the concatenation of two paths in a topological space J. For simplicity of definition, we define it on all paths, not just those 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. (Contributed by Jeff Madsen, 15-Jun-2010.)
|- *p = ( j e. Top |-> ( f e. ( II Cn j ) , g e. ( II Cn j ) |-> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( f ` ( 2 x. x ) ) , ( g ` ( ( 2 x. x ) - 1 ) ) ) ) ) )
Definition	df-om1 21631*	Define the loop space of a topological space, with a magma structure on it given by concatenation of loops. This structure is not a group, but the operation is compatible with homotopy, which allows the homotopy groups to be defined based on this operation. (Contributed by Mario Carneiro, 10-Jul-2015.)
|- Om1 = ( j e. Top , y e. U. j |-> { <. ( Base ` ndx ) , { f e. ( II Cn j ) | ( ( f ` 0 ) = y /\ ( f ` 1 ) = y ) } >. , <. ( +g ` ndx ) , ( *p ` j ) >. , <. (TopSet ` ndx ) , ( j ^ko II ) >. } )
Definition	df-omn 21632*	Define the n-th iterated loop space of a topological space. Unlike Om1 this is actually a pointed topological space, which is to say a tuple of a topological space (a member of TopSp, not Top) and a point in the space. Higher loop spaces select the constant loop at the point from the lower loop space for the distinguished point. (Contributed by Mario Carneiro, 10-Jul-2015.)
|- OmN = ( j e. Top , y e. U. j |-> seq 0 ( ( ( x e. _V , p e. _V |-> <. ( ( TopOpen ` ( 1st ` x ) ) Om1 ( 2nd ` x ) ) , ( ( 0 [,] 1 ) X. { ( 2nd ` x ) } ) >. ) o. 1st ) , <. { <. ( Base ` ndx ) , U. j >. , <. (TopSet ` ndx ) , j >. } , y >. ) )
Definition	df-pi1 21633*	Define the fundamental group, whose operation is given by concatenation of homotopy classes of loops. Definition of [Hatcher] p. 26. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- pi1 = ( j e. Top , y e. U. j |-> ( ( j Om1 y ) /.s ( ~=ph ` j ) ) )
Definition	df-pin 21634*	Define the n-th homotopy group, which is formed by taking the n-th loop space and forming the quotient under the relation of path homotopy equivalence in the base space of the n-th loop space, which is the n - 1-th loop space. For n = 0, since this is not well-defined we replace this relation with the path-connectedness relation, so that the 0-th homotopy group is the set of path components of X. (Since the 0-th loop space does not have a group operation, neither does the 0-th homotopy group, but the rest are genuine groups.) (Contributed by Mario Carneiro, 11-Feb-2015.)
|- piN = ( j e. Top , p e. U. j |-> ( n e. NN0 |-> ( ( 1st ` ( ( j OmN p ) ` n ) ) /.s if ( n = 0 , { <. x , y >. | E. f e. ( II Cn j ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } , ( ~=ph ` ( TopOpen ` ( 1st ` ( ( j OmN p ) ` ( n - 1 ) ) ) ) ) ) ) ) )
Theorem	pcofval 21635*	The value of the path concatenation function on a topological space. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.)
|- ( *p ` J ) = ( f e. ( II Cn J ) , g e. ( II Cn J ) |-> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( f ` ( 2 x. x ) ) , ( g ` ( ( 2 x. x ) - 1 ) ) ) ) )
Theorem	pcoval 21636*	The concatenation of two paths. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   =>    |- ( ph -> ( F ( *p ` J ) G ) = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) ) )
Theorem	pcovalg 21637	Evaluate the concatenation of two paths. (Contributed by Mario Carneiro, 7-Jun-2014.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   =>    |- ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( ( F ( *p ` J ) G ) ` X ) = if ( X <_ ( 1 / 2 ) , ( F ` ( 2 x. X ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) )
Theorem	pcoval1 21638	Evaluate the concatenation of two paths on the first half. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   =>    |- ( ( ph /\ X e. ( 0 [,] ( 1 / 2 ) ) ) -> ( ( F ( *p ` J ) G ) ` X ) = ( F ` ( 2 x. X ) ) )
Theorem	pco0 21639	The starting point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   =>    |- ( ph -> ( ( F ( *p ` J ) G ) ` 0 ) = ( F ` 0 ) )
Theorem	pco1 21640	The ending point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   =>    |- ( ph -> ( ( F ( *p ` J ) G ) ` 1 ) = ( G ` 1 ) )
Theorem	pcoval2 21641	Evaluate the concatenation of two paths on the second half. (Contributed by Jeff Madsen, 15-Jun-2010.) (Proof shortened by Mario Carneiro, 7-Jun-2014.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   &    |- ( ph -> ( F ` 1 ) = ( G ` 0 ) )   =>    |- ( ( ph /\ X e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( F ( *p ` J ) G ) ` X ) = ( G ` ( ( 2 x. X ) - 1 ) ) )
Theorem	pcocn 21642	The concatenation of two paths is a path. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof shortened by Mario Carneiro, 7-Jun-2014.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   &    |- ( ph -> ( F ` 1 ) = ( G ` 0 ) )   =>    |- ( ph -> ( F ( *p ` J ) G ) e. ( II Cn J ) )
Theorem	copco 21643	The composition of a concatenation of paths with a continuous function. (Contributed by Mario Carneiro, 9-Jul-2015.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   &    |- ( ph -> ( F ` 1 ) = ( G ` 0 ) )   &    |- ( ph -> H e. ( J Cn K ) )   =>    |- ( ph -> ( H o. ( F ( *p ` J ) G ) ) = ( ( H o. F ) ( *p ` K ) ( H o. G ) ) )
Theorem	pcohtpylem 21644*	Lemma for pcohtpy 21645. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> ( F ` 1 ) = ( G ` 0 ) )   &    |- ( ph -> F ( ~=ph ` J ) H )   &    |- ( ph -> G ( ~=ph ` J ) K )   &    |- P = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( ( 2 x. x ) M y ) , ( ( ( 2 x. x ) - 1 ) N y ) ) )   &    |- ( ph -> M e. ( F ( PHtpy ` J ) H ) )   &    |- ( ph -> N e. ( G ( PHtpy ` J ) K ) )   =>    |- ( ph -> P e. ( ( F ( *p ` J ) G ) ( PHtpy ` J ) ( H ( *p ` J ) K ) ) )
Theorem	pcohtpy 21645	Homotopy invariance of path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> ( F ` 1 ) = ( G ` 0 ) )   &    |- ( ph -> F ( ~=ph ` J ) H )   &    |- ( ph -> G ( ~=ph ` J ) K )   =>    |- ( ph -> ( F ( *p ` J ) G ) ( ~=ph ` J ) ( H ( *p ` J ) K ) )
Theorem	pcoptcl 21646	A constant function is a path from Y to itself. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 19-Mar-2015.)
|- P = ( ( 0 [,] 1 ) X. { Y } )   =>    |- ( ( J e. (TopOn ` X ) /\ Y e. X ) -> ( P e. ( II Cn J ) /\ ( P ` 0 ) = Y /\ ( P ` 1 ) = Y ) )
Theorem	pcopt 21647	Concatenation with a point does not affect homotopy class. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
|- P = ( ( 0 [,] 1 ) X. { Y } )   =>    |- ( ( F e. ( II Cn J ) /\ ( F ` 0 ) = Y ) -> ( P ( *p ` J ) F ) ( ~=ph ` J ) F )
Theorem	pcopt2 21648	Concatenation with a point does not affect homotopy class. (Contributed by Mario Carneiro, 12-Feb-2015.)
|- P = ( ( 0 [,] 1 ) X. { Y } )   =>    |- ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( F ( *p ` J ) P ) ( ~=ph ` J ) F )
Theorem	pcoass 21649*	Order of concatenation does not affect homotopy class. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof shortened by Mario Carneiro, 8-Jun-2014.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   &    |- ( ph -> H e. ( II Cn J ) )   &    |- ( ph -> ( F ` 1 ) = ( G ` 0 ) )   &    |- ( ph -> ( G ` 1 ) = ( H ` 0 ) )   &    |- P = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) )   =>    |- ( ph -> ( ( F ( *p ` J ) G ) ( *p ` J ) H ) ( ~=ph ` J ) ( F ( *p ` J ) ( G ( *p ` J ) H ) ) )
Theorem	pcorevcl 21650*	Closure for a reversed path. (Contributed by Mario Carneiro, 12-Feb-2015.)
|- G = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )   =>    |- ( F e. ( II Cn J ) -> ( G e. ( II Cn J ) /\ ( G ` 0 ) = ( F ` 1 ) /\ ( G ` 1 ) = ( F ` 0 ) ) )
Theorem	pcorevlem 21651*	Lemma for pcorev 21652. Prove continuity of the homotopy function. (Contributed by Jeff Madsen, 11-Jun-2010.) (Proof shortened by Mario Carneiro, 8-Jun-2014.)
|- G = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )   &    |- P = ( ( 0 [,] 1 ) X. { ( F ` 1 ) } )   &    |- H = ( s e. ( 0 [,] 1 ) , t e. ( 0 [,] 1 ) |-> ( F ` if ( s <_ ( 1 / 2 ) , ( 1 - ( ( 1 - t ) x. ( 2 x. s ) ) ) , ( 1 - ( ( 1 - t ) x. ( 1 - ( ( 2 x. s ) - 1 ) ) ) ) ) ) )   =>    |- ( F e. ( II Cn J ) -> ( H e. ( ( G ( *p ` J ) F ) ( PHtpy ` J ) P ) /\ ( G ( *p ` J ) F ) ( ~=ph ` J ) P ) )
Theorem	pcorev 21652*	Concatenation with the reverse path. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
|- G = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )   &    |- P = ( ( 0 [,] 1 ) X. { ( F ` 1 ) } )   =>    |- ( F e. ( II Cn J ) -> ( G ( *p ` J ) F ) ( ~=ph ` J ) P )
Theorem	pcorev2 21653*	Concatenation with the reverse path. (Contributed by Mario Carneiro, 12-Feb-2015.)
|- G = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )   &    |- P = ( ( 0 [,] 1 ) X. { ( F ` 0 ) } )   =>    |- ( F e. ( II Cn J ) -> ( F ( *p ` J ) G ) ( ~=ph ` J ) P )
Theorem	pcophtb 21654*	The path homotopy equivalence relation on two paths F , G with the same start and end point can be written in terms of the loop F - G formed by concatenating F with the inverse of G. Thus, all the homotopy information in ~=ph ` J is available if we restrict our attention to closed loops, as in the definition of the fundamental group. (Contributed by Mario Carneiro, 12-Feb-2015.)
|- H = ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) )   &    |- P = ( ( 0 [,] 1 ) X. { ( F ` 0 ) } )   &    |- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   &    |- ( ph -> ( F ` 0 ) = ( G ` 0 ) )   &    |- ( ph -> ( F ` 1 ) = ( G ` 1 ) )   =>    |- ( ph -> ( ( F ( *p ` J ) H ) ( ~=ph ` J ) P <-> F ( ~=ph ` J ) G ) )
Theorem	om1val 21655*	The definition of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.)
|- O = ( J Om1 Y )   &    |- ( ph -> B = { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } )   &    |- ( ph -> .+ = ( *p ` J ) )   &    |- ( ph -> K = ( J ^ko II ) )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y e. X )   =>    |- ( ph -> O = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (TopSet ` ndx ) , K >. } )
Theorem	om1bas 21656*	The base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.)
|- O = ( J Om1 Y )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y e. X )   &    |- ( ph -> B = ( Base ` O ) )   =>    |- ( ph -> B = { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } )
Theorem	om1elbas 21657	Elementhood in the base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.)
|- O = ( J Om1 Y )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y e. X )   &    |- ( ph -> B = ( Base ` O ) )   =>    |- ( ph -> ( F e. B <-> ( F e. ( II Cn J ) /\ ( F ` 0 ) = Y /\ ( F ` 1 ) = Y ) ) )
Theorem	om1addcl 21658	Closure of the group operation of the loop space. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 5-Sep-2015.)
|- O = ( J Om1 Y )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y e. X )   &    |- ( ph -> B = ( Base ` O ) )   &    |- ( ph -> H e. B )   &    |- ( ph -> K e. B )   =>    |- ( ph -> ( H ( *p ` J ) K ) e. B )
Theorem	om1plusg 21659	The group operation (which isn't much more than a magma) of the loop space. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- O = ( J Om1 Y )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y e. X )   =>    |- ( ph -> ( *p ` J ) = ( +g ` O ) )
Theorem	om1tset 21660	The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.)
|- O = ( J Om1 Y )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y e. X )   =>    |- ( ph -> ( J ^ko II ) = (TopSet ` O ) )
Theorem	om1opn 21661	The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.)
|- O = ( J Om1 Y )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y e. X )   &    |- K = ( TopOpen ` O )   &    |- ( ph -> B = ( Base ` O ) )   =>    |- ( ph -> K = ( ( J ^ko II ) ↾t B ) )
Theorem	pi1val 21662	The definition of the fundamental group. (Contributed by Mario Carneiro, 11-Feb-2015.) (Revised by Mario Carneiro, 10-Jul-2015.)
|- G = ( J pi1 Y )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y e. X )   &    |- O = ( J Om1 Y )   =>    |- ( ph -> G = ( O /.s ( ~=ph ` J ) ) )
Theorem	pi1bas 21663	The base set of the fundamental group of a topological space at a given base point. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.)
|- G = ( J pi1 Y )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y e. X )   &    |- O = ( J Om1 Y )   &    |- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> K = ( Base ` O ) )   =>    |- ( ph -> B = ( K /. ( ~=ph ` J ) ) )
Theorem	pi1blem 21664	Lemma for pi1buni 21665. (Contributed by Mario Carneiro, 10-Jul-2015.)
|- G = ( J pi1 Y )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y e. X )   &    |- O = ( J Om1 Y )   &    |- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> K = ( Base ` O ) )   =>    |- ( ph -> ( ( ( ~=ph ` J ) " K ) C_ K /\ K C_ ( II Cn J ) ) )
Theorem	pi1buni 21665	Another way to write the loop space base in terms of the base of the fundamental group. (Contributed by Mario Carneiro, 10-Jul-2015.)
|- G = ( J pi1 Y )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y e. X )   &    |- O = ( J Om1 Y )   &    |- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> K = ( Base ` O ) )   =>    |- ( ph -> U. B = K )
Theorem	pi1bas2 21666	The base set of the fundamental group, written self-referentially. (Contributed by Mario Carneiro, 10-Jul-2015.)
|- G = ( J pi1 Y )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y e. X )   &    |- ( ph -> B = ( Base ` G ) )   =>    |- ( ph -> B = ( U. B /. ( ~=ph ` J ) ) )
Theorem	pi1eluni 21667	Elementhood in the base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.)
|- G = ( J pi1 Y )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y e. X )   &    |- ( ph -> B = ( Base ` G ) )   =>    |- ( ph -> ( F e. U. B <-> ( F e. ( II Cn J ) /\ ( F ` 0 ) = Y /\ ( F ` 1 ) = Y ) ) )
Theorem	pi1bas3 21668	The base set of the fundamental group. (Contributed by Mario Carneiro, 10-Jul-2015.)
|- G = ( J pi1 Y )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y e. X )   &    |- ( ph -> B = ( Base ` G ) )   &    |- R = ( ( ~=ph ` J ) i^i ( U. B X. U. B ) )   =>    |- ( ph -> B = ( U. B /. R ) )
Theorem	pi1cpbl 21669	The group operation, loop concatenation, is compatible with homotopy equivalence. (Contributed by Mario Carneiro, 10-Jul-2015.)
|- G = ( J pi1 Y )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y e. X )   &    |- ( ph -> B = ( Base ` G ) )   &    |- R = ( ( ~=ph ` J ) i^i ( U. B X. U. B ) )   &    |- O = ( J Om1 Y )   &    |- .+ = ( +g ` O )   =>    |- ( ph -> ( ( M R N /\ P R Q ) -> ( M .+ P ) R ( N .+ Q ) ) )
Theorem	elpi1 21670*	The elements of the fundamental group. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.)
|- G = ( J pi1 Y )   &    |- B = ( Base ` G )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y e. X )   =>    |- ( ph -> ( F e. B <-> E. f e. ( II Cn J ) ( ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) /\ F = [ f ] ( ~=ph ` J ) ) ) )
Theorem	elpi1i 21671	The elements of the fundamental group. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.)
|- G = ( J pi1 Y )   &    |- B = ( Base ` G )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y e. X )   &    |- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> ( F ` 0 ) = Y )   &    |- ( ph -> ( F ` 1 ) = Y )   =>    |- ( ph -> [ F ] ( ~=ph ` J ) e. B )
Theorem	pi1addf 21672	The group operation of pi1 is a binary operation. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.)
|- G = ( J pi1 Y )   &    |- B = ( Base ` G )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y e. X )   &    |- .+ = ( +g ` G )   =>    |- ( ph -> .+ : ( B X. B ) --> B )
Theorem	pi1addval 21673	The concatenation of two path-homotopy classes in the fundamental group. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.)
|- G = ( J pi1 Y )   &    |- B = ( Base ` G )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y e. X )   &    |- .+ = ( +g ` G )   &    |- ( ph -> M e. U. B )   &    |- ( ph -> N e. U. B )   =>    |- ( ph -> ( [ M ] ( ~=ph ` J ) .+ [ N ] ( ~=ph ` J ) ) = [ ( M ( *p ` J ) N ) ] ( ~=ph ` J ) )
Theorem	pi1grplem 21674	Lemma for pi1grp 21675. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 10-Aug-2015.)
|- G = ( J pi1 Y )   &    |- B = ( Base ` G )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y e. X )   &    |- .0. = ( ( 0 [,] 1 ) X. { Y } )   =>    |- ( ph -> ( G e. Grp /\ [ .0. ] ( ~=ph ` J ) = ( 0g ` G ) ) )
Theorem	pi1grp 21675	The fundamental group is a group. Proposition 1.3 of [Hatcher] p. 26. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof shortened by Mario Carneiro, 8-Jun-2014.) (Revised by Mario Carneiro, 10-Aug-2015.)
|- G = ( J pi1 Y )   =>    |- ( ( J e. (TopOn ` X ) /\ Y e. X ) -> G e. Grp )
Theorem	pi1id 21676	The identity element of the fundamental group. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 10-Aug-2015.)
|- G = ( J pi1 Y )   &    |- .0. = ( ( 0 [,] 1 ) X. { Y } )   =>    |- ( ( J e. (TopOn ` X ) /\ Y e. X ) -> [ .0. ] ( ~=ph ` J ) = ( 0g ` G ) )
Theorem	pi1inv 21677*	An inverse in the fundamental group. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 10-Aug-2015.)
|- G = ( J pi1 Y )   &    |- N = ( invg ` G )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y e. X )   &    |- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> ( F ` 0 ) = Y )   &    |- ( ph -> ( F ` 1 ) = Y )   &    |- I = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )   =>    |- ( ph -> ( N ` [ F ] ( ~=ph ` J ) ) = [ I ] ( ~=ph ` J ) )
Theorem	pi1xfrf 21678*	Functionality of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- P = ( J pi1 ( F ` 0 ) )   &    |- Q = ( J pi1 ( F ` 1 ) )   &    |- B = ( Base ` P )   &    |- G = ran ( g e. U. B |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) >. )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> I e. ( II Cn J ) )   &    |- ( ph -> ( F ` 1 ) = ( I ` 0 ) )   &    |- ( ph -> ( I ` 1 ) = ( F ` 0 ) )   =>    |- ( ph -> G : B --> ( Base ` Q ) )
Theorem	pi1xfrval 21679*	The value of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 23-Dec-2016.)
|- P = ( J pi1 ( F ` 0 ) )   &    |- Q = ( J pi1 ( F ` 1 ) )   &    |- B = ( Base ` P )   &    |- G = ran ( g e. U. B |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) >. )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> I e. ( II Cn J ) )   &    |- ( ph -> ( F ` 1 ) = ( I ` 0 ) )   &    |- ( ph -> ( I ` 1 ) = ( F ` 0 ) )   &    |- ( ph -> A e. U. B )   =>    |- ( ph -> ( G ` [ A ] ( ~=ph ` J ) ) = [ ( I ( *p ` J ) ( A ( *p ` J ) F ) ) ] ( ~=ph ` J ) )
Theorem	pi1xfr 21680*	Given a path F and its inverse I between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015.)
|- P = ( J pi1 ( F ` 0 ) )   &    |- Q = ( J pi1 ( F ` 1 ) )   &    |- B = ( Base ` P )   &    |- G = ran ( g e. U. B |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) >. )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F e. ( II Cn J ) )   &    |- I = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )   =>    |- ( ph -> G e. ( P GrpHom Q ) )
Theorem	pi1xfrcnvlem 21681*	Given a path F between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
|- P = ( J pi1 ( F ` 0 ) )   &    |- Q = ( J pi1 ( F ` 1 ) )   &    |- B = ( Base ` P )   &    |- G = ran ( g e. U. B |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) >. )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F e. ( II Cn J ) )   &    |- I = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )   &    |- H = ran ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. )   =>    |- ( ph -> `' G C_ H )
Theorem	pi1xfrcnv 21682*	Given a path F between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
|- P = ( J pi1 ( F ` 0 ) )   &    |- Q = ( J pi1 ( F ` 1 ) )   &    |- B = ( Base ` P )   &    |- G = ran ( g e. U. B |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) >. )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F e. ( II Cn J ) )   &    |- I = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )   &    |- H = ran ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. )   =>    |- ( ph -> ( `' G = H /\ `' G e. ( Q GrpHom P ) ) )
Theorem	pi1xfrgim 21683*	The mapping G between fundamental groups is an isomorphism. (Contributed by Mario Carneiro, 12-Feb-2015.)
|- P = ( J pi1 ( F ` 0 ) )   &    |- Q = ( J pi1 ( F ` 1 ) )   &    |- B = ( Base ` P )   &    |- G = ran ( g e. U. B |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) >. )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F e. ( II Cn J ) )   &    |- I = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )   =>    |- ( ph -> G e. ( P GrpIso Q ) )
Theorem	pi1cof 21684*	Functionality of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- P = ( J pi1 A )   &    |- Q = ( K pi1 B )   &    |- V = ( Base ` P )   &    |- G = ran ( g e. U. V |-> <. [ g ] ( ~=ph ` J ) , [ ( F o. g ) ] ( ~=ph ` K ) >. )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F e. ( J Cn K ) )   &    |- ( ph -> A e. X )   &    |- ( ph -> ( F ` A ) = B )   =>    |- ( ph -> G : V --> ( Base ` Q ) )
Theorem	pi1coval 21685*	The value of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 10-Aug-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
|- P = ( J pi1 A )   &    |- Q = ( K pi1 B )   &    |- V = ( Base ` P )   &    |- G = ran ( g e. U. V |-> <. [ g ] ( ~=ph ` J ) , [ ( F o. g ) ] ( ~=ph ` K ) >. )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F e. ( J Cn K ) )   &    |- ( ph -> A e. X )   &    |- ( ph -> ( F ` A ) = B )   =>    |- ( ( ph /\ T e. U. V ) -> ( G ` [ T ] ( ~=ph ` J ) ) = [ ( F o. T ) ] ( ~=ph ` K ) )
Theorem	pi1coghm 21686*	The mapping G between fundamental groups is a group homomorphism. (Contributed by Mario Carneiro, 10-Aug-2015.) (Revised by Mario Carneiro, 23-Dec-2016.)
|- P = ( J pi1 A )   &    |- Q = ( K pi1 B )   &    |- V = ( Base ` P )   &    |- G = ran ( g e. U. V |-> <. [ g ] ( ~=ph ` J ) , [ ( F o. g ) ] ( ~=ph ` K ) >. )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F e. ( J Cn K ) )   &    |- ( ph -> A e. X )   &    |- ( ph -> ( F ` A ) = B )   =>    |- ( ph -> G e. ( P GrpHom Q ) )
12.5  Complex metric vector spaces
12.5.1  Complex left modules
Syntax	cclm 21687	Complex module.
class CMod
Definition	df-clm 21688*	Define a complex module, which is just a left module over a subring of CC, which allows us to use conventional addition, multiplication, etc. in the left module theorems. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- CMod = { w e. LMod | [. (Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = (ℂfld ↾s k ) /\ k e. (SubRing ` ℂfld ) ) }
Theorem	isclm 21689	A complex module is a left module over a subring of the complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CMod <-> ( W e. LMod /\ F = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) )
Theorem	clmsca 21690	A complex module is a left module over a subring of the complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CMod -> F = (ℂfld ↾s K ) )
Theorem	clmsubrg 21691	A complex module is a left module over a subring of the complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CMod -> K e. (SubRing ` ℂfld ) )
Theorem	clmlmod 21692	A complex module is a left module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ( W e. CMod -> W e. LMod )
Theorem	clmgrp 21693	A complex module is an additive group. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ( W e. CMod -> W e. Grp )
Theorem	clmabl 21694	A complex module is an abelian group. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ( W e. CMod -> W e. Abel )
Theorem	clmring 21695	The scalar ring of a complex module is a ring. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. CMod -> F e. Ring )
Theorem	clmfgrp 21696	The scalar ring of a complex module is a group. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. CMod -> F e. Grp )
Theorem	clm0 21697	The zero of the scalar ring of a complex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. CMod -> 0 = ( 0g ` F ) )
Theorem	clm1 21698	The identity of the scalar ring of a complex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. CMod -> 1 = ( 1r ` F ) )
Theorem	clmadd 21699	The addition of the scalar ring of a complex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. CMod -> + = ( +g ` F ) )
Theorem	clmmul 21700	The multiplication of the scalar ring of a complex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. CMod -> x. = ( .r ` F ) )