P. 148 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14701-14800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lssclg 14701	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 14702	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 14703	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 14704	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 14705	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 14706	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 14707	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 14708	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 14709	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 14710	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 14711	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 14712	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 14713	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 14714	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 14715	All subspaces are subgroups. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- S = ( LSubSp ` W )   =>    |- ( W e. LMod -> S C_ (SubGrp ` W ) )
Theorem	islss3 14716	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 14717	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 14718	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 14719*	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 14720*	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 14721*	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 14722	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 14723	Extend class notation with span of a set of vectors.
class LSpan
Definition	df-lsp 14724*	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 14725*	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 14726	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 14727*	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 14728	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 14729	The span of a singleton is a subspace (frequently used special case of lspcl 14728). (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 14730	The span of a pair is a subspace (frequently used special case of lspcl 14728). (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 14731	The span of an unordered triple is a subspace (frequently used special case of lspcl 14728). (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 14732	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 14733	The span of a singleton is an additive subgroup (frequently used special case of lspcl 14728). (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 14734	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 14735	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 14736	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 14737	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 14738	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 14739	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 14740	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 14741	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 14742	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 14743	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 14744	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 14745	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 14746	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 14747	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 14748	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 14749	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 14750	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 14751*	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 14752	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 14753*	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 14754*	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 14755	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 14756*	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 14757	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 14758	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 14759	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 14760	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 14761	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 14762	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 14763	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 14764	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 14765	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 14766	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 14767	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 14768*	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 14769*	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 14770	Extend class notation with the subring algebra generator.
class subringAlg
Syntax	crglmod 14771	Extend class notation with the left module induced by a ring over itself.
class ringLMod
Definition	df-sra 14772*	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 14773	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 14774	Lemma for srabaseg 14776 through sravscag 14780. (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 14775	Lemma for srabaseg 14776 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 14776	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 14777	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 14778	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 14779	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 14780	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 14781	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 14782	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 14783	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 14784	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 14785	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 14786	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 14787	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 14788	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 14789*	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 14790	ringLMod is a function. (Contributed by Stefan O'Rear, 6-Dec-2014.)
|- ringLMod Fn _V
Theorem	rlmvalg 14791	Value of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( W e. V -> (ringLMod ` W ) = ( (subringAlg ` W ) ` ( Base ` W ) ) )
Theorem	rlmbasg 14792	Base set of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( R e. V -> ( Base ` R ) = ( Base ` (ringLMod ` R ) ) )
Theorem	rlmplusgg 14793	Vector addition in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( R e. V -> ( +g ` R ) = ( +g ` (ringLMod ` R ) ) )
Theorem	rlm0g 14794	Zero vector in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- ( R e. V -> ( 0g ` R ) = ( 0g ` (ringLMod ` R ) ) )
Theorem	rlmsubg 14795	Subtraction in the ring module. (Contributed by Thierry Arnoux, 30-Jun-2019.)
|- ( R e. V -> ( -g ` R ) = ( -g ` (ringLMod ` R ) ) )
Theorem	rlmmulrg 14796	Ring multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( R e. V -> ( .r ` R ) = ( .r ` (ringLMod ` R ) ) )
Theorem	rlmscabas 14797	Scalars in the ring module have the same base set. (Contributed by Jim Kingdon, 29-Apr-2025.)
|- ( R e. X -> ( Base ` R ) = ( Base ` (Scalar ` (ringLMod ` R ) ) ) )
Theorem	rlmvscag 14798	Scalar multiplication in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( R e. V -> ( .r ` R ) = ( .s ` (ringLMod ` R ) ) )
Theorem	rlmtopng 14799	Topology component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( R e. V -> ( TopOpen ` R ) = ( TopOpen ` (ringLMod ` R ) ) )
Theorem	rlmdsg 14800	Metric component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( R e. V -> ( dist ` R ) = ( dist ` (ringLMod ` R ) ) )