P. 149 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14801-14900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lssmex 14801	If a linear subspace is inhabited, the class it is built from is a set. (Contributed by Jim Kingdon, 28-Apr-2025.)
|- S = ( LSubSp ` W )   =>    |- ( U e. S -> W e. _V )
Theorem	lsssetm 14802*	The set of all (not necessarily closed) linear subspaces of a left module or left vector space. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 15-Jul-2014.)
|- F = (Scalar ` W )   &    |- B = ( Base ` F )   &    |- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( W e. X -> S = { s e. ~P V | ( E. j j e. s /\ A. x e. B A. a e. s A. b e. s ( ( x .x. a ) .+ b ) e. s ) } )
Theorem	islssm 14803*	The predicate "is a subspace" (of a left module or left vector space). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.)
|- F = (Scalar ` W )   &    |- B = ( Base ` F )   &    |- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( U e. S <-> ( U C_ V /\ E. j j e. U /\ A. x e. B A. a e. U A. b e. U ( ( x .x. a ) .+ b ) e. U ) )
Theorem	islssmg 14804*	The predicate "is a subspace" (of a left module or left vector space). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.) Use islssm 14803 instead. (New usage is discouraged.)
|- F = (Scalar ` W )   &    |- B = ( Base ` F )   &    |- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( W e. X -> ( U e. S <-> ( U C_ V /\ E. j j e. U /\ A. x e. B A. a e. U A. b e. U ( ( x .x. a ) .+ b ) e. U ) ) )
Theorem	islssmd 14805*	Properties that determine a subspace of a left module or left vector space. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.)
|- ( ph -> F = (Scalar ` W ) )   &    |- ( ph -> B = ( Base ` F ) )   &    |- ( ph -> V = ( Base ` W ) )   &    |- ( ph -> .+ = ( +g ` W ) )   &    |- ( ph -> .x. = ( .s ` W ) )   &    |- ( ph -> S = ( LSubSp ` W ) )   &    |- ( ph -> U C_ V )   &    |- ( ph -> E. j j e. U )   &    |- ( ( ph /\ ( x e. B /\ a e. U /\ b e. U ) ) -> ( ( x .x. a ) .+ b ) e. U )   &    |- ( ph -> W e. X )   =>    |- ( ph -> U e. S )
Theorem	lssssg 14806	A subspace is a set of vectors. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( ( W e. X /\ U e. S ) -> U C_ V )
Theorem	lsselg 14807	A subspace member is a vector. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 8-Jan-2015.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( ( W e. C /\ U e. S /\ X e. U ) -> X e. V )
Theorem	lss1 14808	The set of vectors in a left module is a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( W e. LMod -> V e. S )
Theorem	lssuni 14809	The union of all subspaces is the vector space. (Contributed by NM, 13-Mar-2015.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- ( ph -> W e. LMod )   =>    |- ( ph -> U. S = V )
Theorem	lssclg 14810	Closure property of a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.)
|- F = (Scalar ` W )   &    |- B = ( Base ` F )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( ( W e. C /\ U e. S /\ ( Z e. B /\ X e. U /\ Y e. U ) ) -> ( ( Z .x. X ) .+ Y ) e. U )
Theorem	lssvacl 14811	Closure of vector addition in a subspace. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- .+ = ( +g ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> ( X .+ Y ) e. U )
Theorem	lssvsubcl 14812	Closure of vector subtraction in a subspace. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- .- = ( -g ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> ( X .- Y ) e. U )
Theorem	lssvancl1 14813	Non-closure: if one vector belongs to a subspace but another does not, their sum does not belong. Useful for obtaining a new vector not in a subspace. (Contributed by NM, 14-May-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- S = ( LSubSp ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. S )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. V )   &    |- ( ph -> -. Y e. U )   =>    |- ( ph -> -. ( X .+ Y ) e. U )
Theorem	lssvancl2 14814	Non-closure: if one vector belongs to a subspace but another does not, their sum does not belong. Useful for obtaining a new vector not in a subspace. (Contributed by NM, 20-May-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- S = ( LSubSp ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. S )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. V )   &    |- ( ph -> -. Y e. U )   =>    |- ( ph -> -. ( Y .+ X ) e. U )
Theorem	lss0cl 14815	The zero vector belongs to every subspace. (Contributed by NM, 12-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
|- .0. = ( 0g ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ U e. S ) -> .0. e. U )
Theorem	lsssn0 14816	The singleton of the zero vector is a subspace. (Contributed by NM, 13-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- .0. = ( 0g ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( W e. LMod -> { .0. } e. S )
Theorem	lss0ss 14817	The zero subspace is included in every subspace. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- .0. = ( 0g ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ X e. S ) -> { .0. } C_ X )
Theorem	lssle0 14818	No subspace is smaller than the zero subspace. (Contributed by NM, 20-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- .0. = ( 0g ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ X e. S ) -> ( X C_ { .0. } <-> X = { .0. } ) )
Theorem	lssvneln0 14819	A vector X which doesn't belong to a subspace U is nonzero. (Contributed by NM, 14-May-2015.) (Revised by AV, 19-Jul-2022.)
|- .0. = ( 0g ` W )   &    |- S = ( LSubSp ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. S )   &    |- ( ph -> -. X e. U )   =>    |- ( ph -> X =/= .0. )
Theorem	lssneln0 14820	A vector X which doesn't belong to a subspace U is nonzero. (Contributed by NM, 14-May-2015.) (Revised by AV, 17-Jul-2022.) (Proof shortened by AV, 19-Jul-2022.)
|- .0. = ( 0g ` W )   &    |- S = ( LSubSp ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. S )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. U )   =>    |- ( ph -> X e. ( V \ { .0. } ) )
Theorem	lssvscl 14821	Closure of scalar product in a subspace. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- B = ( Base ` F )   &    |- S = ( LSubSp ` W )   =>    |- ( ( ( W e. LMod /\ U e. S ) /\ ( X e. B /\ Y e. U ) ) -> ( X .x. Y ) e. U )
Theorem	lssvnegcl 14822	Closure of negative vectors in a subspace. (Contributed by Stefan O'Rear, 11-Dec-2014.)
|- S = ( LSubSp ` W )   &    |- N = ( invg ` W )   =>    |- ( ( W e. LMod /\ U e. S /\ X e. U ) -> ( N ` X ) e. U )
Theorem	lsssubg 14823	All subspaces are subgroups. (Contributed by Stefan O'Rear, 11-Dec-2014.)
|- S = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ U e. S ) -> U e. (SubGrp ` W ) )
Theorem	lsssssubg 14824	All subspaces are subgroups. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- S = ( LSubSp ` W )   =>    |- ( W e. LMod -> S C_ (SubGrp ` W ) )
Theorem	islss3 14825	A linear subspace of a module is a subset which is a module in its own right. (Contributed by Stefan O'Rear, 6-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- X = ( W ↾s U )   &    |- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( W e. LMod -> ( U e. S <-> ( U C_ V /\ X e. LMod ) ) )
Theorem	lsslmod 14826	A submodule is a module. (Contributed by Stefan O'Rear, 12-Dec-2014.)
|- X = ( W ↾s U )   &    |- S = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ U e. S ) -> X e. LMod )
Theorem	lsslss 14827	The subspaces of a subspace are the smaller subspaces. (Contributed by Stefan O'Rear, 12-Dec-2014.)
|- X = ( W ↾s U )   &    |- S = ( LSubSp ` W )   &    |- T = ( LSubSp ` X )   =>    |- ( ( W e. LMod /\ U e. S ) -> ( V e. T <-> ( V e. S /\ V C_ U ) ) )
Theorem	islss4 14828*	A linear subspace is a subgroup which respects scalar multiplication. (Contributed by Stefan O'Rear, 11-Dec-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- F = (Scalar ` W )   &    |- B = ( Base ` F )   &    |- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( W e. LMod -> ( U e. S <-> ( U e. (SubGrp ` W ) /\ A. a e. B A. b e. U ( a .x. b ) e. U ) ) )
Theorem	lss1d 14829*	One-dimensional subspace (or zero-dimensional if X is the zero vector). (Contributed by NM, 14-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   &    |- S = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> { v | E. k e. K v = ( k .x. X ) } e. S )
Theorem	lssintclm 14830*	The intersection of an inhabited set of subspaces is a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- S = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ A C_ S /\ E. w w e. A ) -> |^| A e. S )
Theorem	lssincl 14831	The intersection of two subspaces is a subspace. (Contributed by NM, 7-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- S = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ T e. S /\ U e. S ) -> ( T i^i U ) e. S )
Syntax	clspn 14832	Extend class notation with span of a set of vectors.
class LSpan
Definition	df-lsp 14833*	Define span of a set of vectors of a left module or left vector space. (Contributed by NM, 8-Dec-2013.)
|- LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
Theorem	lspfval 14834*	The span function for a left vector space (or a left module). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   =>    |- ( W e. X -> N = ( s e. ~P V |-> |^| { t e. S | s C_ t } ) )
Theorem	lspf 14835	The span function on a left module maps subsets to subspaces. (Contributed by Stefan O'Rear, 12-Dec-2014.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   =>    |- ( W e. LMod -> N : ~P V --> S )
Theorem	lspval 14836*	The span of a set of vectors (in a left module). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ U C_ V ) -> ( N ` U ) = |^| { t e. S | U C_ t } )
Theorem	lspcl 14837	The span of a set of vectors is a subspace. (Contributed by NM, 9-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ U C_ V ) -> ( N ` U ) e. S )
Theorem	lspsncl 14838	The span of a singleton is a subspace (frequently used special case of lspcl 14837). (Contributed by NM, 17-Jul-2014.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. S )
Theorem	lspprcl 14839	The span of a pair is a subspace (frequently used special case of lspcl 14837). (Contributed by NM, 11-Apr-2015.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( N ` { X , Y } ) e. S )
Theorem	lsptpcl 14840	The span of an unordered triple is a subspace (frequently used special case of lspcl 14837). (Contributed by NM, 22-May-2015.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> Z e. V )   =>    |- ( ph -> ( N ` { X , Y , Z } ) e. S )
Theorem	lspex 14841	Existence of the span of a set of vectors. (Contributed by Jim Kingdon, 25-Apr-2025.)
|- ( W e. X -> ( LSpan ` W ) e. _V )
Theorem	lspsnsubg 14842	The span of a singleton is an additive subgroup (frequently used special case of lspcl 14837). (Contributed by Mario Carneiro, 21-Apr-2016.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. (SubGrp ` W ) )
Theorem	lspid 14843	The span of a subspace is itself. (Contributed by NM, 15-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ U e. S ) -> ( N ` U ) = U )
Theorem	lspssv 14844	A span is a set of vectors. (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ U C_ V ) -> ( N ` U ) C_ V )
Theorem	lspss 14845	Span preserves subset ordering. (Contributed by NM, 11-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ U C_ V /\ T C_ U ) -> ( N ` T ) C_ ( N ` U ) )
Theorem	lspssid 14846	A set of vectors is a subset of its span. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ U C_ V ) -> U C_ ( N ` U ) )
Theorem	lspidm 14847	The span of a set of vectors is idempotent. (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ U C_ V ) -> ( N ` ( N ` U ) ) = ( N ` U ) )
Theorem	lspun 14848	The span of union is the span of the union of spans. (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> ( N ` ( T u. U ) ) = ( N ` ( ( N ` T ) u. ( N ` U ) ) ) )
Theorem	lspssp 14849	If a set of vectors is a subset of a subspace, then the span of those vectors is also contained in the subspace. (Contributed by Mario Carneiro, 4-Sep-2014.)
|- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ U e. S /\ T C_ U ) -> ( N ` T ) C_ U )
Theorem	lspsnss 14850	The span of the singleton of a subspace member is included in the subspace. (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 4-Sep-2014.)
|- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ U e. S /\ X e. U ) -> ( N ` { X } ) C_ U )
Theorem	ellspsn3 14851	A member of the span of the singleton of a vector is a member of a subspace containing the vector. (Contributed by NM, 4-Jul-2014.)
|- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. S )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. ( N ` { X } ) )   =>    |- ( ph -> Y e. U )
Theorem	lspprss 14852	The span of a pair of vectors in a subspace belongs to the subspace. (Contributed by NM, 12-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. S )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   =>    |- ( ph -> ( N ` { X , Y } ) C_ U )
Theorem	lspsnid 14853	A vector belongs to the span of its singleton. (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> X e. ( N ` { X } ) )
Theorem	ellspsn6 14854	Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 8-Aug-2014.) (Revised by Mario Carneiro, 8-Jan-2015.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. S )   =>    |- ( ph -> ( X e. U <-> ( X e. V /\ ( N ` { X } ) C_ U ) ) )
Theorem	ellspsn5b 14855	Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 8-Aug-2014.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. S )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( X e. U <-> ( N ` { X } ) C_ U ) )
Theorem	ellspsn5 14856	Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 20-Feb-2015.)
|- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. S )   &    |- ( ph -> X e. U )   =>    |- ( ph -> ( N ` { X } ) C_ U )
Theorem	lspprid1 14857	A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> X e. ( N ` { X , Y } ) )
Theorem	lspprid2 14858	A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> Y e. ( N ` { X , Y } ) )
Theorem	lspprvacl 14859	The sum of two vectors belongs to their span. (Contributed by NM, 20-May-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( X .+ Y ) e. ( N ` { X , Y } ) )
Theorem	lssats2 14860*	A way to express atomisticity (a subspace is the union of its atoms). (Contributed by NM, 3-Feb-2015.)
|- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. S )   =>    |- ( ph -> U = U_ x e. U ( N ` { x } ) )
Theorem	lspsneli 14861	A scalar product with a vector belongs to the span of its singleton. (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 14862*	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	ellspsn 14863*	Member of span of the singleton of a vector. (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 14864	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 14865*	Comparable spans of singletons must have proportional vectors. (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 14866	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 14867	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 14868	Span of the singleton of the zero vector. (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 14869	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 14870	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 14871	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 14872	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 14873	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 14874	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 14875	Spans in submodules correspond to spans in the containing module. (Contributed by Stefan O'Rear, 12-Dec-2014.) Terms in the equation were swapped as proposed by NM on 15-Mar-2015. (Revised by AV, 18-Apr-2025.)
|- X = ( W ↾s U )   &    |- M = ( LSpan ` W )   &    |- N = ( LSpan ` X )   &    |- L = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ U e. L /\ G C_ U ) -> ( N ` G ) = ( M ` G ) )
Theorem	lss0v 14876	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	lsspropdg 14877*	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 -> K e. X )   &    |- ( ph -> L e. Y )   =>    |- ( ph -> ( LSubSp ` K ) = ( LSubSp ` L ) )
Theorem	lsppropd 14878*	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.) (Revised by AV, 24-Apr-2024.)
|- ( 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. X )   &    |- ( ph -> L e. Y )   =>    |- ( ph -> ( LSpan ` K ) = ( LSpan ` L ) )
7.6  Subring algebras and ideals
7.6.1  Subring algebras
Syntax	csra 14879	Extend class notation with the subring algebra generator.
class subringAlg
Syntax	crglmod 14880	Extend class notation with the left module induced by a ring over itself.
class ringLMod
Definition	df-sra 14881*	Any ring can be regarded as a left algebra over any of its subrings. The function subringAlg associates with any ring and any of its subrings the left algebra consisting in the ring itself regarded as a left algebra over the subring. It has an inner product which is simply the ring product. (Contributed by Mario Carneiro, 27-Nov-2014.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|- subringAlg = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> ( ( ( w sSet <. (Scalar ` ndx ) , ( w ↾s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. ) sSet <. ( .i ` ndx ) , ( .r ` w ) >. ) ) )
Definition	df-rgmod 14882	Any ring can be regarded as a left algebra over itself. The function ringLMod associates with any ring the left algebra consisting in the ring itself regarded as a left algebra over itself. It has an inner product which is simply the ring product. (Contributed by Stefan O'Rear, 6-Dec-2014.)
|- ringLMod = ( w e. _V |-> ( (subringAlg ` w ) ` ( Base ` w ) ) )
Theorem	sraval 14883	Lemma for srabaseg 14885 through sravscag 14889. (Contributed by Mario Carneiro, 27-Nov-2014.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|- ( ( W e. V /\ S C_ ( Base ` W ) ) -> ( (subringAlg ` W ) ` S ) = ( ( ( W sSet <. (Scalar ` ndx ) , ( W ↾s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) )
Theorem	sralemg 14884	Lemma for srabaseg 14885 and similar theorems. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   &    |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- (Scalar ` ndx ) =/= ( E ` ndx )   &    |- ( .s ` ndx ) =/= ( E ` ndx )   &    |- ( .i ` ndx ) =/= ( E ` ndx )   =>    |- ( ph -> ( E ` W ) = ( E ` A ) )
Theorem	srabaseg 14885	Base set of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> ( Base ` W ) = ( Base ` A ) )
Theorem	sraaddgg 14886	Additive operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> ( +g ` W ) = ( +g ` A ) )
Theorem	sramulrg 14887	Multiplicative operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> ( .r ` W ) = ( .r ` A ) )
Theorem	srascag 14888	The set of scalars of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof shortened by AV, 12-Nov-2024.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> ( W ↾s S ) = (Scalar ` A ) )
Theorem	sravscag 14889	The scalar product operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof shortened by AV, 12-Nov-2024.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> ( .r ` W ) = ( .s ` A ) )
Theorem	sraipg 14890	The inner product operation of a subring algebra. (Contributed by Thierry Arnoux, 16-Jun-2019.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> ( .r ` W ) = ( .i ` A ) )
Theorem	sratsetg 14891	Topology component of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> (TopSet ` W ) = (TopSet ` A ) )
Theorem	sraex 14892	Existence of a subring algebra. (Contributed by Jim Kingdon, 16-Apr-2025.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> A e. _V )
Theorem	sratopng 14893	Topology component of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> ( TopOpen ` W ) = ( TopOpen ` A ) )
Theorem	sradsg 14894	Distance function of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> ( dist ` W ) = ( dist ` A ) )
Theorem	sraring 14895	Condition for a subring algebra to be a ring. (Contributed by Thierry Arnoux, 24-Jul-2023.)
|- A = ( (subringAlg ` R ) ` V )   &    |- B = ( Base ` R )   =>    |- ( ( R e. Ring /\ V C_ B ) -> A e. Ring )
Theorem	sralmod 14896	The subring algebra is a left module. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- A = ( (subringAlg ` W ) ` S )   =>    |- ( S e. (SubRing ` W ) -> A e. LMod )
Theorem	sralmod0g 14897	The subring module inherits a zero from its ring. (Contributed by Stefan O'Rear, 27-Dec-2014.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> .0. = ( 0g ` W ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> .0. = ( 0g ` A ) )
Theorem	issubrgd 14898*	Prove a subring by closure (definition version). (Contributed by Stefan O'Rear, 7-Dec-2014.)
|- ( ph -> S = ( I ↾s D ) )   &    |- ( ph -> .0. = ( 0g ` I ) )   &    |- ( ph -> .+ = ( +g ` I ) )   &    |- ( ph -> D C_ ( Base ` I ) )   &    |- ( ph -> .0. e. D )   &    |- ( ( ph /\ x e. D /\ y e. D ) -> ( x .+ y ) e. D )   &    |- ( ( ph /\ x e. D ) -> ( ( invg ` I ) ` x ) e. D )   &    |- ( ph -> .1. = ( 1r ` I ) )   &    |- ( ph -> .x. = ( .r ` I ) )   &    |- ( ph -> .1. e. D )   &    |- ( ( ph /\ x e. D /\ y e. D ) -> ( x .x. y ) e. D )   &    |- ( ph -> I e. Ring )   =>    |- ( ph -> D e. (SubRing ` I ) )
Theorem	rlmfn 14899	ringLMod is a function. (Contributed by Stefan O'Rear, 6-Dec-2014.)
|- ringLMod Fn _V
Theorem	rlmvalg 14900	Value of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( W e. V -> (ringLMod ` W ) = ( (subringAlg ` W ) ` ( Base ` W ) ) )