P. 191 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19001-19100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lspsneli 19001	A scalar product with a vector belongs to the span of its singleton. (spansnmul 28423 analog.) (Contributed by NM, 2-Jul-2014.)
|- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> A e. K )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( A .x. X ) e. ( N ` { X } ) )
Theorem	lspsn 19002*	Span of the singleton of a vector. (Contributed by NM, 14-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) = { v | E. k e. K v = ( k .x. X ) } )
Theorem	lspsnel 19003*	Member of span of the singleton of a vector. (elspansn 28425 analog.) (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( U e. ( N ` { X } ) <-> E. k e. K U = ( k .x. X ) ) )
Theorem	lspsnvsi 19004	Span of a scalar product of a singleton. (Contributed by NM, 23-Apr-2014.) (Proof shortened by Mario Carneiro, 4-Sep-2014.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ R e. K /\ X e. V ) -> ( N ` { ( R .x. X ) } ) C_ ( N ` { X } ) )
Theorem	lspsnss2 19005*	Comparable spans of singletons must have proportional vectors. See lspsneq 19122 for equal span version. (Contributed by NM, 7-Jun-2015.)
|- V = ( Base ` W )   &    |- S = (Scalar ` W )   &    |- K = ( Base ` S )   &    |- .x. = ( .s ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( ( N ` { X } ) C_ ( N ` { Y } ) <-> E. k e. K X = ( k .x. Y ) ) )
Theorem	lspsnneg 19006	Negation does not change the span of a singleton. (Contributed by NM, 24-Apr-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- M = ( invg ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( N ` { ( M ` X ) } ) = ( N ` { X } ) )
Theorem	lspsnsub 19007	Swapping subtraction order does not change the span of a singleton. (Contributed by NM, 4-Apr-2015.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( N ` { ( X .- Y ) } ) = ( N ` { ( Y .- X ) } ) )
Theorem	lspsn0 19008	Span of the singleton of the zero vector. (spansn0 28400 analog.) (Contributed by NM, 15-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
|- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   =>    |- ( W e. LMod -> ( N ` { .0. } ) = { .0. } )
Theorem	lsp0 19009	Span of the empty set. (Contributed by Mario Carneiro, 5-Sep-2014.)
|- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   =>    |- ( W e. LMod -> ( N ` (/) ) = { .0. } )
Theorem	lspuni0 19010	Union of the span of the empty set. (Contributed by NM, 14-Mar-2015.)
|- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   =>    |- ( W e. LMod -> U. ( N ` (/) ) = .0. )
Theorem	lspun0 19011	The span of a union with the zero subspace. (Contributed by NM, 22-May-2015.)
|- V = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X C_ V )   =>    |- ( ph -> ( N ` ( X u. { .0. } ) ) = ( N ` X ) )
Theorem	lspsneq0 19012	Span of the singleton is the zero subspace iff the vector is zero. (Contributed by NM, 27-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( ( N ` { X } ) = { .0. } <-> X = .0. ) )
Theorem	lspsneq0b 19013	Equal singleton spans imply both arguments are zero or both are nonzero. (Contributed by NM, 21-Mar-2015.)
|- V = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> ( N ` { X } ) = ( N ` { Y } ) )   =>    |- ( ph -> ( X = .0. <-> Y = .0. ) )
Theorem	lmodindp1 19014	Two independent (non-colinear) vectors have nonzero sum. (Contributed by NM, 22-Apr-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   =>    |- ( ph -> ( X .+ Y ) =/= .0. )
Theorem	lsslsp 19015	Spans in submodules correspond to spans in the containing module. (Contributed by Stefan O'Rear, 12-Dec-2014.) TODO: Shouldn't we swap M ` G and N ` G since we are computing a property of N ` G? (Like we say sin 0 = 0 and not 0 = sin 0.) - NM 15-Mar-2015.
|- X = ( W ↾s U )   &    |- M = ( LSpan ` W )   &    |- N = ( LSpan ` X )   &    |- L = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ U e. L /\ G C_ U ) -> ( M ` G ) = ( N ` G ) )
Theorem	lss0v 19016	The zero vector in a submodule equals the zero vector in the including module. (Contributed by NM, 15-Mar-2015.)
|- X = ( W ↾s U )   &    |- .0. = ( 0g ` W )   &    |- Z = ( 0g ` X )   &    |- L = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ U e. L ) -> Z = .0. )
Theorem	lsspropd 19017*	If two structures have the same components (properties), they have the same subspace structure. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 14-Jun-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> B C_ W )   &    |- ( ( ph /\ ( x e. W /\ y e. W ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) e. W )   &    |- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )   &    |- ( ph -> P = ( Base ` (Scalar ` K ) ) )   &    |- ( ph -> P = ( Base ` (Scalar ` L ) ) )   =>    |- ( ph -> ( LSubSp ` K ) = ( LSubSp ` L ) )
Theorem	lsppropd 19018*	If two structures have the same components (properties), they have the same span function. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 14-Jun-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> B C_ W )   &    |- ( ( ph /\ ( x e. W /\ y e. W ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) e. W )   &    |- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )   &    |- ( ph -> P = ( Base ` (Scalar ` K ) ) )   &    |- ( ph -> P = ( Base ` (Scalar ` L ) ) )   &    |- ( ph -> K e. _V )   &    |- ( ph -> L e. _V )   =>    |- ( ph -> ( LSpan ` K ) = ( LSpan ` L ) )
10.6.3  Homomorphisms and isomorphisms of left modules
Syntax	clmhm 19019	Extend class notation with the generator of left module hom-sets.
class LMHom
Syntax	clmim 19020	The class of left module isomorphism sets.
class LMIso
Syntax	clmic 19021	The class of the left module isomorphism relation.
class ~=ph𝑚
Definition	df-lmhm 19022*	A homomorphism of left modules is a group homomorphism which additionally preserves the scalar product. This requires both structures to be left modules over the same ring. (Contributed by Stefan O'Rear, 31-Dec-2014.)
|- LMHom = ( s e. LMod , t e. LMod |-> { f e. ( s GrpHom t ) | [. (Scalar ` s ) / w ]. ( (Scalar ` t ) = w /\ A. x e. ( Base ` w ) A. y e. ( Base ` s ) ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) ) ) } )
Definition	df-lmim 19023*	An isomorphism of modules is a homomorphism which is also a bijection, i.e. it preserves equality as well as the group and scalar operations. (Contributed by Stefan O'Rear, 21-Jan-2015.)
|- LMIso = ( s e. LMod , t e. LMod |-> { g e. ( s LMHom t ) | g : ( Base ` s ) -1-1-onto-> ( Base ` t ) } )
Definition	df-lmic 19024	Two modules are said to be isomorphic iff they are connected by at least one isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- ~=ph𝑚 = ( `' LMIso " ( _V \ 1o ) )
Theorem	reldmlmhm 19025	Lemma for module homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014.)
|- Rel dom LMHom
Theorem	lmimfn 19026	Lemma for module isomorphisms. (Contributed by Stefan O'Rear, 23-Aug-2015.)
|- LMIso Fn ( LMod X. LMod )
Theorem	islmhm 19027*	Property of being a homomorphism of left modules. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Proof shortened by Mario Carneiro, 30-Apr-2015.)
|- K = (Scalar ` S )   &    |- L = (Scalar ` T )   &    |- B = ( Base ` K )   &    |- E = ( Base ` S )   &    |- .x. = ( .s ` S )   &    |- .X. = ( .s ` T )   =>    |- ( F e. ( S LMHom T ) <-> ( ( S e. LMod /\ T e. LMod ) /\ ( F e. ( S GrpHom T ) /\ L = K /\ A. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) )
Theorem	islmhm3 19028*	Property of a module homomorphism, similar to ismhm 17337. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- K = (Scalar ` S )   &    |- L = (Scalar ` T )   &    |- B = ( Base ` K )   &    |- E = ( Base ` S )   &    |- .x. = ( .s ` S )   &    |- .X. = ( .s ` T )   =>    |- ( ( S e. LMod /\ T e. LMod ) -> ( F e. ( S LMHom T ) <-> ( F e. ( S GrpHom T ) /\ L = K /\ A. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) )
Theorem	lmhmlem 19029	Non-quantified consequences of a left module homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- K = (Scalar ` S )   &    |- L = (Scalar ` T )   =>    |- ( F e. ( S LMHom T ) -> ( ( S e. LMod /\ T e. LMod ) /\ ( F e. ( S GrpHom T ) /\ L = K ) ) )
Theorem	lmhmsca 19030	A homomorphism of left modules constrains both modules to the same ring of scalars. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- K = (Scalar ` S )   &    |- L = (Scalar ` T )   =>    |- ( F e. ( S LMHom T ) -> L = K )
Theorem	lmghm 19031	A homomorphism of left modules is a homomorphism of groups. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- ( F e. ( S LMHom T ) -> F e. ( S GrpHom T ) )
Theorem	lmhmlmod2 19032	A homomorphism of left modules has a left module as codomain. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- ( F e. ( S LMHom T ) -> T e. LMod )
Theorem	lmhmlmod1 19033	A homomorphism of left modules has a left module as domain. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- ( F e. ( S LMHom T ) -> S e. LMod )
Theorem	lmhmf 19034	A homomorphism of left modules is a function. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- B = ( Base ` S )   &    |- C = ( Base ` T )   =>    |- ( F e. ( S LMHom T ) -> F : B --> C )
Theorem	lmhmlin 19035	A homomorphism of left modules is K-linear. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- K = (Scalar ` S )   &    |- B = ( Base ` K )   &    |- E = ( Base ` S )   &    |- .x. = ( .s ` S )   &    |- .X. = ( .s ` T )   =>    |- ( ( F e. ( S LMHom T ) /\ X e. B /\ Y e. E ) -> ( F ` ( X .x. Y ) ) = ( X .X. ( F ` Y ) ) )
Theorem	lmodvsinv 19036	Multiplication of a vector by a negated scalar. (Contributed by Stefan O'Rear, 28-Feb-2015.)
|- B = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- N = ( invg ` W )   &    |- M = ( invg ` F )   &    |- K = ( Base ` F )   =>    |- ( ( W e. LMod /\ R e. K /\ X e. B ) -> ( ( M ` R ) .x. X ) = ( N ` ( R .x. X ) ) )
Theorem	lmodvsinv2 19037	Multiplying a negated vector by a scalar. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- B = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- N = ( invg ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. LMod /\ R e. K /\ X e. B ) -> ( R .x. ( N ` X ) ) = ( N ` ( R .x. X ) ) )
Theorem	islmhm2 19038*	A one-equation proof of linearity of a left module homomorphism, similar to df-lss 18933. (Contributed by Mario Carneiro, 7-Oct-2015.)
|- B = ( Base ` S )   &    |- C = ( Base ` T )   &    |- K = (Scalar ` S )   &    |- L = (Scalar ` T )   &    |- E = ( Base ` K )   &    |- .+ = ( +g ` S )   &    |- .+^ = ( +g ` T )   &    |- .x. = ( .s ` S )   &    |- .X. = ( .s ` T )   =>    |- ( ( S e. LMod /\ T e. LMod ) -> ( F e. ( S LMHom T ) <-> ( F : B --> C /\ L = K /\ A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) ) ) )
Theorem	islmhmd 19039*	Deduction for a module homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015.)
|- X = ( Base ` S )   &    |- .x. = ( .s ` S )   &    |- .X. = ( .s ` T )   &    |- K = (Scalar ` S )   &    |- J = (Scalar ` T )   &    |- N = ( Base ` K )   &    |- ( ph -> S e. LMod )   &    |- ( ph -> T e. LMod )   &    |- ( ph -> J = K )   &    |- ( ph -> F e. ( S GrpHom T ) )   &    |- ( ( ph /\ ( x e. N /\ y e. X ) ) -> ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) )   =>    |- ( ph -> F e. ( S LMHom T ) )
Theorem	0lmhm 19040	The constant zero linear function between two modules. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- .0. = ( 0g ` N )   &    |- B = ( Base ` M )   &    |- S = (Scalar ` M )   &    |- T = (Scalar ` N )   =>    |- ( ( M e. LMod /\ N e. LMod /\ S = T ) -> ( B X. { .0. } ) e. ( M LMHom N ) )
Theorem	idlmhm 19041	The identity function on a module is linear. (Contributed by Stefan O'Rear, 4-Sep-2015.)
|- B = ( Base ` M )   =>    |- ( M e. LMod -> ( _I |` B ) e. ( M LMHom M ) )
Theorem	invlmhm 19042	The negative function on a module is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- I = ( invg ` M )   =>    |- ( M e. LMod -> I e. ( M LMHom M ) )
Theorem	lmhmco 19043	The composition of two module-linear functions is module-linear. (Contributed by Stefan O'Rear, 4-Sep-2015.)
|- ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) -> ( F o. G ) e. ( M LMHom O ) )
Theorem	lmhmplusg 19044	The pointwise sum of two linear functions is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- .+ = ( +g ` N )   =>    |- ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) -> ( F oF .+ G ) e. ( M LMHom N ) )
Theorem	lmhmvsca 19045	The pointwise scalar product of a linear function and a constant is linear, over a commutative ring. (Contributed by Mario Carneiro, 22-Sep-2015.)
|- V = ( Base ` M )   &    |- .x. = ( .s ` N )   &    |- J = (Scalar ` N )   &    |- K = ( Base ` J )   =>    |- ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) -> ( ( V X. { A } ) oF .x. F ) e. ( M LMHom N ) )
Theorem	lmhmf1o 19046	A bijective module homomorphism is also converse homomorphic. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- X = ( Base ` S )   &    |- Y = ( Base ` T )   =>    |- ( F e. ( S LMHom T ) -> ( F : X -1-1-onto-> Y <-> `' F e. ( T LMHom S ) ) )
Theorem	lmhmima 19047	The image of a subspace under a homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- X = ( LSubSp ` S )   &    |- Y = ( LSubSp ` T )   =>    |- ( ( F e. ( S LMHom T ) /\ U e. X ) -> ( F " U ) e. Y )
Theorem	lmhmpreima 19048	The inverse image of a subspace under a homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- X = ( LSubSp ` S )   &    |- Y = ( LSubSp ` T )   =>    |- ( ( F e. ( S LMHom T ) /\ U e. Y ) -> ( `' F " U ) e. X )
Theorem	lmhmlsp 19049	Homomorphisms preserve spans. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- V = ( Base ` S )   &    |- K = ( LSpan ` S )   &    |- L = ( LSpan ` T )   =>    |- ( ( F e. ( S LMHom T ) /\ U C_ V ) -> ( F " ( K ` U ) ) = ( L ` ( F " U ) ) )
Theorem	lmhmrnlss 19050	The range of a homomorphism is a submodule. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- ( F e. ( S LMHom T ) -> ran F e. ( LSubSp ` T ) )
Theorem	lmhmkerlss 19051	The kernel of a homomorphism is a submodule. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- K = ( `' F " { .0. } )   &    |- .0. = ( 0g ` T )   &    |- U = ( LSubSp ` S )   =>    |- ( F e. ( S LMHom T ) -> K e. U )
Theorem	reslmhm 19052	Restriction of a homomorphism to a subspace. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- U = ( LSubSp ` S )   &    |- R = ( S ↾s X )   =>    |- ( ( F e. ( S LMHom T ) /\ X e. U ) -> ( F |` X ) e. ( R LMHom T ) )
Theorem	reslmhm2 19053	Expansion of the codomain of a homomorphism. (Contributed by Stefan O'Rear, 3-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.)
|- U = ( T ↾s X )   &    |- L = ( LSubSp ` T )   =>    |- ( ( F e. ( S LMHom U ) /\ T e. LMod /\ X e. L ) -> F e. ( S LMHom T ) )
Theorem	reslmhm2b 19054	Expansion of the codomain of a homomorphism. (Contributed by Stefan O'Rear, 3-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.)
|- U = ( T ↾s X )   &    |- L = ( LSubSp ` T )   =>    |- ( ( T e. LMod /\ X e. L /\ ran F C_ X ) -> ( F e. ( S LMHom T ) <-> F e. ( S LMHom U ) ) )
Theorem	lmhmeql 19055	The equalizer of two module homomorphisms is a subspace. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- U = ( LSubSp ` S )   =>    |- ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) -> dom ( F i^i G ) e. U )
Theorem	lspextmo 19056*	A linear function is completely determined (or overdetermined) by its values on a spanning subset. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by NM, 17-Jun-2017.)
|- B = ( Base ` S )   &    |- K = ( LSpan ` S )   =>    |- ( ( X C_ B /\ ( K ` X ) = B ) -> E* g e. ( S LMHom T ) ( g |` X ) = F )
Theorem	pwsdiaglmhm 19057*	Diagonal homomorphism into a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` R )   &    |- F = ( x e. B |-> ( I X. { x } ) )   =>    |- ( ( R e. LMod /\ I e. W ) -> F e. ( R LMHom Y ) )
Theorem	pwssplit0 19058*	Splitting for structure powers, part 0: restriction is a function. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- Y = ( W ^s U )   &    |- Z = ( W ^s V )   &    |- B = ( Base ` Y )   &    |- C = ( Base ` Z )   &    |- F = ( x e. B |-> ( x |` V ) )   =>    |- ( ( W e. T /\ U e. X /\ V C_ U ) -> F : B --> C )
Theorem	pwssplit1 19059*	Splitting for structure powers, part 1: restriction is an onto function. The only actual monoid law we need here is that the base set is nonempty. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- Y = ( W ^s U )   &    |- Z = ( W ^s V )   &    |- B = ( Base ` Y )   &    |- C = ( Base ` Z )   &    |- F = ( x e. B |-> ( x |` V ) )   =>    |- ( ( W e. Mnd /\ U e. X /\ V C_ U ) -> F : B -onto-> C )
Theorem	pwssplit2 19060*	Splitting for structure powers, part 2: restriction is a group homomorphism. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- Y = ( W ^s U )   &    |- Z = ( W ^s V )   &    |- B = ( Base ` Y )   &    |- C = ( Base ` Z )   &    |- F = ( x e. B |-> ( x |` V ) )   =>    |- ( ( W e. Grp /\ U e. X /\ V C_ U ) -> F e. ( Y GrpHom Z ) )
Theorem	pwssplit3 19061*	Splitting for structure powers, part 3: restriction is a module homomorphism. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- Y = ( W ^s U )   &    |- Z = ( W ^s V )   &    |- B = ( Base ` Y )   &    |- C = ( Base ` Z )   &    |- F = ( x e. B |-> ( x |` V ) )   =>    |- ( ( W e. LMod /\ U e. X /\ V C_ U ) -> F e. ( Y LMHom Z ) )
Theorem	islmim 19062	An isomorphism of left modules is a bijective homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.)
|- B = ( Base ` R )   &    |- C = ( Base ` S )   =>    |- ( F e. ( R LMIso S ) <-> ( F e. ( R LMHom S ) /\ F : B -1-1-onto-> C ) )
Theorem	lmimf1o 19063	An isomorphism of left modules is a bijection. (Contributed by Stefan O'Rear, 21-Jan-2015.)
|- B = ( Base ` R )   &    |- C = ( Base ` S )   =>    |- ( F e. ( R LMIso S ) -> F : B -1-1-onto-> C )
Theorem	lmimlmhm 19064	An isomorphism of modules is a homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.)
|- ( F e. ( R LMIso S ) -> F e. ( R LMHom S ) )
Theorem	lmimgim 19065	An isomorphism of modules is an isomorphism of groups. (Contributed by Stefan O'Rear, 21-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- ( F e. ( R LMIso S ) -> F e. ( R GrpIso S ) )
Theorem	islmim2 19066	An isomorphism of left modules is a homomorphism whose converse is a homomorphism. (Contributed by Mario Carneiro, 6-May-2015.)
|- ( F e. ( R LMIso S ) <-> ( F e. ( R LMHom S ) /\ `' F e. ( S LMHom R ) ) )
Theorem	lmimcnv 19067	The converse of a bijective module homomorphism is a bijective module homomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- ( F e. ( S LMIso T ) -> `' F e. ( T LMIso S ) )
Theorem	brlmic 19068	The relation "is isomorphic to" for modules. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- ( R ~=ph𝑚 S <-> ( R LMIso S ) =/= (/) )
Theorem	brlmici 19069	Prove isomorphic by an explicit isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- ( F e. ( R LMIso S ) -> R ~=ph𝑚 S )
Theorem	lmiclcl 19070	Isomorphism implies the left side is a module. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- ( R ~=ph𝑚 S -> R e. LMod )
Theorem	lmicrcl 19071	Isomorphism implies the right side is a module. (Contributed by Mario Carneiro, 6-May-2015.)
|- ( R ~=ph𝑚 S -> S e. LMod )
Theorem	lmicsym 19072	Module isomorphism is symmetric. (Contributed by Stefan O'Rear, 26-Feb-2015.)
|- ( R ~=ph𝑚 S -> S ~=ph𝑚 R )
Theorem	lmhmpropd 19073*	Module homomorphism depends only on the module attributes of structures. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- ( ph -> B = ( Base ` J ) )   &    |- ( ph -> C = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> C = ( Base ` M ) )   &    |- ( ph -> F = (Scalar ` J ) )   &    |- ( ph -> G = (Scalar ` K ) )   &    |- ( ph -> F = (Scalar ` L ) )   &    |- ( ph -> G = (Scalar ` M ) )   &    |- P = ( Base ` F )   &    |- Q = ( Base ` G )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` J ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` M ) y ) )   &    |- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` J ) y ) = ( x ( .s ` L ) y ) )   &    |- ( ( ph /\ ( x e. Q /\ y e. C ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` M ) y ) )   =>    |- ( ph -> ( J LMHom K ) = ( L LMHom M ) )
10.6.4  Subspace sum; bases for a left module
Syntax	clbs 19074	Extend class notation with the set of bases for a vector space.
class LBasis
Definition	df-lbs 19075*	Define the set of bases to a left module or left vector space. (Contributed by Mario Carneiro, 24-Jun-2014.)
|- LBasis = ( w e. _V |-> { b e. ~P ( Base ` w ) | [. ( LSpan ` w ) / n ]. [. (Scalar ` w ) / s ]. ( ( n ` b ) = ( Base ` w ) /\ A. x e. b A. y e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) ) ) } )
Theorem	islbs 19076*	The predicate " B is a basis for the left module or vector space W". A subset of the base set is a basis if zero is not in the set, it spans the set, and no nonzero multiple of an element of the basis is in the span of the rest of the family. (Contributed by Mario Carneiro, 24-Jun-2014.) (Revised by Mario Carneiro, 14-Jan-2015.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   &    |- J = (LBasis ` W )   &    |- N = ( LSpan ` W )   &    |- .0. = ( 0g ` F )   =>    |- ( W e. X -> ( B e. J <-> ( B C_ V /\ ( N ` B ) = V /\ A. x e. B A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( B \ { x } ) ) ) ) )
Theorem	lbsss 19077	A basis is a set of vectors. (Contributed by Mario Carneiro, 24-Jun-2014.)
|- V = ( Base ` W )   &    |- J = (LBasis ` W )   =>    |- ( B e. J -> B C_ V )
Theorem	lbsel 19078	An element of a basis is a vector. (Contributed by Mario Carneiro, 24-Jun-2014.)
|- V = ( Base ` W )   &    |- J = (LBasis ` W )   =>    |- ( ( B e. J /\ E e. B ) -> E e. V )
Theorem	lbssp 19079	The span of a basis is the whole space. (Contributed by Mario Carneiro, 24-Jun-2014.)
|- V = ( Base ` W )   &    |- J = (LBasis ` W )   &    |- N = ( LSpan ` W )   =>    |- ( B e. J -> ( N ` B ) = V )
Theorem	lbsind 19080	A basis is linearly independent; that is, every element has a span which trivially intersects the span of the remainder of the basis. (Contributed by Mario Carneiro, 12-Jan-2015.)
|- V = ( Base ` W )   &    |- J = (LBasis ` W )   &    |- N = ( LSpan ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   &    |- .0. = ( 0g ` F )   =>    |- ( ( ( B e. J /\ E e. B ) /\ ( A e. K /\ A =/= .0. ) ) -> -. ( A .x. E ) e. ( N ` ( B \ { E } ) ) )
Theorem	lbsind2 19081	A basis is linearly independent; that is, every element is not in the span of the remainder of the basis. (Contributed by Mario Carneiro, 25-Jun-2014.) (Revised by Mario Carneiro, 12-Jan-2015.)
|- J = (LBasis ` W )   &    |- N = ( LSpan ` W )   &    |- F = (Scalar ` W )   &    |- .1. = ( 1r ` F )   &    |- .0. = ( 0g ` F )   =>    |- ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ E e. B ) -> -. E e. ( N ` ( B \ { E } ) ) )
Theorem	lbspss 19082	No proper subset of a basis spans the space. (Contributed by Mario Carneiro, 25-Jun-2014.)
|- J = (LBasis ` W )   &    |- N = ( LSpan ` W )   &    |- F = (Scalar ` W )   &    |- .1. = ( 1r ` F )   &    |- .0. = ( 0g ` F )   &    |- V = ( Base ` W )   =>    |- ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) -> ( N ` C ) =/= V )
Theorem	lsmcl 19083	The sum of two subspaces is a subspace. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   =>    |- ( ( W e. LMod /\ T e. S /\ U e. S ) -> ( T .(+) U ) e. S )
Theorem	lsmspsn 19084*	Member of subspace sum of spans of singletons. (Contributed by NM, 8-Apr-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .x. = ( .s ` W )   &    |- .(+) = ( LSSum ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( U e. ( ( N ` { X } ) .(+) ( N ` { Y } ) ) <-> E. j e. K E. k e. K U = ( ( j .x. X ) .+ ( k .x. Y ) ) ) )
Theorem	lsmelval2 19085*	Subspace sum membership in terms of a sum of 1-dim subspaces (atoms), which can be useful for treating subspaces as projective lattice elements. (Contributed by NM, 9-Aug-2014.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> T e. S )   &    |- ( ph -> U e. S )   =>    |- ( ph -> ( X e. ( T .(+) U ) <-> ( X e. V /\ E. y e. T E. z e. U ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) ) )
Theorem	lsmsp 19086	Subspace sum in terms of span. (Contributed by NM, 6-Feb-2014.) (Proof shortened by Mario Carneiro, 21-Jun-2014.)
|- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   =>    |- ( ( W e. LMod /\ T e. S /\ U e. S ) -> ( T .(+) U ) = ( N ` ( T u. U ) ) )
Theorem	lsmsp2 19087	Subspace sum of spans of subsets is the span of their union. (spanuni 28403 analog.) (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   =>    |- ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> ( ( N ` T ) .(+) ( N ` U ) ) = ( N ` ( T u. U ) ) )
Theorem	lsmssspx 19088	Subspace sum (in its extended domain) is a subset of the span of the union of its arguments. (Contributed by NM, 6-Aug-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- ( ph -> T C_ V )   &    |- ( ph -> U C_ V )   &    |- ( ph -> W e. LMod )   =>    |- ( ph -> ( T .(+) U ) C_ ( N ` ( T u. U ) ) )
Theorem	lsmpr 19089	The span of a pair of vectors equals the sum of the spans of their singletons. (Contributed by NM, 13-Jan-2015.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( N ` { X , Y } ) = ( ( N ` { X } ) .(+) ( N ` { Y } ) ) )
Theorem	lsppreli 19090	A vector expressed as a sum belongs to the span of its components. (Contributed by NM, 9-Apr-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> A e. K )   &    |- ( ph -> B e. K )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( ( A .x. X ) .+ ( B .x. Y ) ) e. ( N ` { X , Y } ) )
Theorem	lsmelpr 19091	Two ways to say that a vector belongs to the span of a pair of vectors. (Contributed by NM, 14-Jan-2015.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> Z e. V )   =>    |- ( ph -> ( X e. ( N ` { Y , Z } ) <-> ( N ` { X } ) C_ ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) ) )
Theorem	lsppr0 19092	The span of a vector paired with zero equals the span of the singleton of the vector. (Contributed by NM, 29-Aug-2014.)
|- V = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( N ` { X , .0. } ) = ( N ` { X } ) )
Theorem	lsppr 19093*	Span of a pair of vectors. (Contributed by NM, 22-Aug-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .x. = ( .s ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( N ` { X , Y } ) = { v | E. k e. K E. l e. K v = ( ( k .x. X ) .+ ( l .x. Y ) ) } )
Theorem	lspprel 19094*	Member of the span of a pair of vectors. (Contributed by NM, 10-Apr-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .x. = ( .s ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( Z e. ( N ` { X , Y } ) <-> E. k e. K E. l e. K Z = ( ( k .x. X ) .+ ( l .x. Y ) ) ) )
Theorem	lspprabs 19095	Absorption of vector sum into span of pair. (Contributed by NM, 27-Apr-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( N ` { X , ( X .+ Y ) } ) = ( N ` { X , Y } ) )
Theorem	lspvadd 19096	The span of a vector sum is included in the span of its arguments. (Contributed by NM, 22-Feb-2014.) (Proof shortened by Mario Carneiro, 21-Jun-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( N ` { ( X .+ Y ) } ) C_ ( N ` { X , Y } ) )
Theorem	lspsntri 19097	Triangle-type inequality for span of a singleton. (Contributed by NM, 24-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   =>    |- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( N ` { ( X .+ Y ) } ) C_ ( ( N ` { X } ) .(+) ( N ` { Y } ) ) )
Theorem	lspsntrim 19098	Triangle-type inequality for span of a singleton of vector difference. (Contributed by NM, 25-Apr-2014.) (Revised by Mario Carneiro, 21-Jun-2014.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- .(+) = ( LSSum ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( N ` { ( X .- Y ) } ) C_ ( ( N ` { X } ) .(+) ( N ` { Y } ) ) )
Theorem	lbspropd 19099*	If two structures have the same components (properties), they have the same set of bases. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 14-Jun-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> B C_ W )   &    |- ( ( ph /\ ( x e. W /\ y e. W ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) e. W )   &    |- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )   &    |- F = (Scalar ` K )   &    |- G = (Scalar ` L )   &    |- ( ph -> P = ( Base ` F ) )   &    |- ( ph -> P = ( Base ` G ) )   &    |- ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( x ( +g ` F ) y ) = ( x ( +g ` G ) y ) )   &    |- ( ph -> K e. _V )   &    |- ( ph -> L e. _V )   =>    |- ( ph -> (LBasis ` K ) = (LBasis ` L ) )
Theorem	pj1lmhm 19100	The left projection function is a linear operator. (Contributed by Mario Carneiro, 15-Oct-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
|- L = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- .0. = ( 0g ` W )   &    |- P = ( proj1 ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> T e. L )   &    |- ( ph -> U e. L )   &    |- ( ph -> ( T i^i U ) = { .0. } )   =>    |- ( ph -> ( T P U ) e. ( ( W ↾s ( T .(+) U ) ) LMHom W ) )