P. 229 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22801-22900   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	comi 22801	Extend class notation with the loop space.
class Om1
Syntax	comn 22802	Extend class notation with the higher loop spaces.
class OmN
Syntax	cpi1 22803	Extend class notation with the fundamental group.
class pi1
Syntax	cpin 22804	Extend class notation with the higher homotopy groups.
class piN
Definition	df-pco 22805*	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 22806*	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 22807*	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 22808*	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 22809*	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 22810*	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 22811*	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 22812	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 22813	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 22814	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 22815	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 22816	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 22817	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 22818	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 22819*	Lemma for pcohtpy 22820. (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 22820	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 22821	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 22822	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 22823	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 22824*	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 22825*	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 22826*	Lemma for pcorev 22827. 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 22827*	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 22828*	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 22829*	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 22830*	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 22831*	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 22832	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 22833	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 22834	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 22835	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 22836	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 22837	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 22838	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 22839	Lemma for pi1buni 22840. (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 22840	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 22841	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 22842	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 22843	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 22844	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 22845*	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 22846	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 22847	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 22848	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 22849	Lemma for pi1grp 22850. (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 22850	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 22851	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 22852*	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 22853*	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 22854*	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 22855*	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 22856*	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 22857*	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 22858*	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 22859*	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 22860*	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 22861*	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  Metric subcomplex vector spaces
12.5.1  Subcomplex modules
Syntax	cclm 22862	Syntax for the class of subcomplex modules.
class CMod
Definition	df-clm 22863*	Define the class of subcomplex modules, which are left modules over a subring of the field of complex numbers ℂfld, which allows us to use the complex addition, multiplication, etc. in theorems about subcomplex modules. Since the field of complex numbers is commutative and so are its subrings (see subrgcrng 18784), left modules over such subrings are the same as right modules, see rmodislmod 18931. Therefore, we drop the word "left" from "subcomplex left module". (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 22864	A subcomplex module is a left module over a subring of the field of 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 22865	The ring of scalars F of a subcomplex module is the restriction of the field of complex numbers to the base set of F. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CMod -> F = (ℂfld ↾s K ) )
Theorem	clmsubrg 22866	The base set of the ring of scalars of a subcomplex module is the base set of a subring of the field of complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CMod -> K e. (SubRing ` ℂfld ) )
Theorem	clmlmod 22867	A subcomplex module is a left module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ( W e. CMod -> W e. LMod )
Theorem	clmgrp 22868	A subcomplex module is an additive group. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ( W e. CMod -> W e. Grp )
Theorem	clmabl 22869	A subcomplex module is an abelian group. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ( W e. CMod -> W e. Abel )
Theorem	clmring 22870	The scalar ring of a subcomplex module is a ring. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. CMod -> F e. Ring )
Theorem	clmfgrp 22871	The scalar ring of a subcomplex module is a group. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. CMod -> F e. Grp )
Theorem	clm0 22872	The zero of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. CMod -> 0 = ( 0g ` F ) )
Theorem	clm1 22873	The identity of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. CMod -> 1 = ( 1r ` F ) )
Theorem	clmadd 22874	The addition of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. CMod -> + = ( +g ` F ) )
Theorem	clmmul 22875	The multiplication of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. CMod -> x. = ( .r ` F ) )
Theorem	clmcj 22876	The conjugation of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. CMod -> * = ( *r ` F ) )
Theorem	isclmi 22877	Reverse direction of isclm 22864. (Contributed by Mario Carneiro, 30-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( ( W e. LMod /\ F = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> W e. CMod )
Theorem	clmzss 22878	The scalar ring of a subcomplex module contains the integers. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CMod -> ZZ C_ K )
Theorem	clmsscn 22879	The scalar ring of a subcomplex module is a subset of the complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CMod -> K C_ CC )
Theorem	clmsub 22880	Subtraction in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CMod /\ A e. K /\ B e. K ) -> ( A - B ) = ( A ( -g ` F ) B ) )
Theorem	clmneg 22881	Negation in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CMod /\ A e. K ) -> -u A = ( ( invg ` F ) ` A ) )
Theorem	clmneg1 22882	Minus one is in the scalar ring of a subcomplex module. (Contributed by AV, 28-Sep-2021.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CMod -> -u 1 e. K )
Theorem	clmabs 22883	Norm in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CMod /\ A e. K ) -> ( abs ` A ) = ( ( norm ` F ) ` A ) )
Theorem	clmacl 22884	Closure of ring addition for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CMod /\ X e. K /\ Y e. K ) -> ( X + Y ) e. K )
Theorem	clmmcl 22885	Closure of ring multiplication for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CMod /\ X e. K /\ Y e. K ) -> ( X x. Y ) e. K )
Theorem	clmsubcl 22886	Closure of ring subtraction for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CMod /\ X e. K /\ Y e. K ) -> ( X - Y ) e. K )
Theorem	lmhmclm 22887	The domain of a linear operator is a subcomplex module iff the range is. (Contributed by Mario Carneiro, 21-Oct-2015.)
|- ( F e. ( S LMHom T ) -> ( S e. CMod <-> T e. CMod ) )
Theorem	clmvscl 22888	Closure of scalar product for a subcomplex module. Analogue of lmodvscl 18880. (Contributed by NM, 3-Nov-2006.) (Revised by AV, 28-Sep-2021.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CMod /\ Q e. K /\ X e. V ) -> ( Q .x. X ) e. V )
Theorem	clmvsass 22889	Associative law for scalar product. Analogue of lmodvsass 18888. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( ( Q x. R ) .x. X ) = ( Q .x. ( R .x. X ) ) )
Theorem	clmvscom 22890	Commutative law for the scalar product. (Contributed by NM, 14-Feb-2008.) (Revised by AV, 7-Oct-2021.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( Q .x. ( R .x. X ) ) = ( R .x. ( Q .x. X ) ) )
Theorem	clmvsdir 22891	Distributive law for scalar product (right-distributivity). (lmodvsdir 18887 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   &    |- .+ = ( +g ` W )   =>    |- ( ( W e. CMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( ( Q + R ) .x. X ) = ( ( Q .x. X ) .+ ( R .x. X ) ) )
Theorem	clmvsdi 22892	Distributive law for scalar product (left-distributivity). (lmodvsdi 18886 analog.) (Contributed by NM, 3-Nov-2006.) (Revised by AV, 28-Sep-2021.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   &    |- .+ = ( +g ` W )   =>    |- ( ( W e. CMod /\ ( A e. K /\ X e. V /\ Y e. V ) ) -> ( A .x. ( X .+ Y ) ) = ( ( A .x. X ) .+ ( A .x. Y ) ) )
Theorem	clmvs1 22893	Scalar product with ring unit. (lmodvs1 18891 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
|- V = ( Base ` W )   &    |- .x. = ( .s ` W )   =>    |- ( ( W e. CMod /\ X e. V ) -> ( 1 .x. X ) = X )
Theorem	clmvs2 22894	A vector plus itself is two times the vector. (Contributed by NM, 1-Feb-2007.) (Revised by AV, 21-Sep-2021.)
|- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- .+ = ( +g ` W )   =>    |- ( ( W e. CMod /\ A e. V ) -> ( A .+ A ) = ( 2 .x. A ) )
Theorem	clm0vs 22895	Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (lmod0vs 18896 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- .0. = ( 0g ` W )   =>    |- ( ( W e. CMod /\ X e. V ) -> ( 0 .x. X ) = .0. )
Theorem	clmopfne 22896	The (functionalized) operations of addition and multiplication by a scalar of a subcomplex module cannot be identical. (Contributed by NM, 31-May-2008.) (Revised by AV, 3-Oct-2021.)
|- .x. = ( .sf ` W )   &    |- .+ = ( +f ` W )   =>    |- ( W e. CMod -> .+ =/= .x. )
Theorem	isclmp 22897*	The predicate "is a subcomplex module." (Contributed by NM, 31-May-2008.) (Revised by AV, 4-Oct-2021.)
|- .x. = ( .s ` W )   &    |- .+ = ( +g ` W )   &    |- V = ( Base ` W )   &    |- S = (Scalar ` W )   &    |- K = ( Base ` S )   =>    |- ( W e. CMod <-> ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ A. x e. V ( ( 1 .x. x ) = x /\ A. y e. K ( ( y .x. x ) e. V /\ A. z e. V ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ A. z e. K ( ( ( z + y ) .x. x ) = ( ( z .x. x ) .+ ( y .x. x ) ) /\ ( ( z x. y ) .x. x ) = ( z .x. ( y .x. x ) ) ) ) ) ) )
Theorem	isclmi0 22898*	Properties that determine a subcomplex module. (Contributed by NM, 5-Nov-2006.) (Revised by AV, 4-Oct-2021.)
|- .x. = ( .s ` W )   &    |- .+ = ( +g ` W )   &    |- V = ( Base ` W )   &    |- S = (Scalar ` W )   &    |- K = ( Base ` S )   &    |- S = (ℂfld ↾s K )   &    |- W e. Grp   &    |- K e. (SubRing ` ℂfld )   &    |- ( x e. V -> ( 1 .x. x ) = x )   &    |- ( ( y e. K /\ x e. V ) -> ( y .x. x ) e. V )   &    |- ( ( y e. K /\ x e. V /\ z e. V ) -> ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) )   &    |- ( ( y e. K /\ z e. K /\ x e. V ) -> ( ( z + y ) .x. x ) = ( ( z .x. x ) .+ ( y .x. x ) ) )   &    |- ( ( y e. K /\ z e. K /\ x e. V ) -> ( ( z x. y ) .x. x ) = ( z .x. ( y .x. x ) ) )   =>    |- W e. CMod
Theorem	clmvneg1 22899	Minus 1 times a vector is the negative of the vector. Equation 2 of [Kreyszig] p. 51. (lmodvneg1 18906 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
|- V = ( Base ` W )   &    |- N = ( invg ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   =>    |- ( ( W e. CMod /\ X e. V ) -> ( -u 1 .x. X ) = ( N ` X ) )
Theorem	clmvsneg 22900	Multiplication of a vector by a negated scalar. (lmodvsneg 18907 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
|- B = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- N = ( invg ` W )   &    |- K = ( Base ` F )   &    |- ( ph -> W e. CMod )   &    |- ( ph -> X e. B )   &    |- ( ph -> R e. K )   =>    |- ( ph -> ( N ` ( R .x. X ) ) = ( -u R .x. X ) )