P. 142 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14101-14200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lssvancl2 14101	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 14102	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 14103	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 14104	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 14105	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 14106	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 14107	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 14108	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 14109	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 14110	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 14111	All subspaces are subgroups. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- S = ( LSubSp ` W )   =>    |- ( W e. LMod -> S C_ (SubGrp ` W ) )
Theorem	islss3 14112	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 14113	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 14114	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 14115*	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 14116*	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 14117*	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 14118	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 14119	Extend class notation with span of a set of vectors.
class LSpan
Definition	df-lsp 14120*	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 14121*	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 14122	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 14123*	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 14124	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 14125	The span of a singleton is a subspace (frequently used special case of lspcl 14124). (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 14126	The span of a pair is a subspace (frequently used special case of lspcl 14124). (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 14127	The span of an unordered triple is a subspace (frequently used special case of lspcl 14124). (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 14128	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 14129	The span of a singleton is an additive subgroup (frequently used special case of lspcl 14124). (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 14130	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 14131	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 14132	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 14133	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 14134	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 14135	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 14136	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 14137	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	lspsnel3 14138	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 14139	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 14140	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	lspsnel6 14141	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	lspsnel5 14142	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	lspsnel5a 14143	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 14144	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 14145	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 14146	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 14147*	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 14148	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 14149*	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 14150*	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 14151	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 14152*	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 14153	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 14154	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 14155	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 14156	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 14157	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 14158	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 14159	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 14160	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 14161	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 14162	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 14163	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 14164*	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 14165*	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 14166	Extend class notation with the subring algebra generator.
class subringAlg
Syntax	crglmod 14167	Extend class notation with the left module induced by a ring over itself.
class ringLMod
Definition	df-sra 14168*	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 14169	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 14170	Lemma for srabaseg 14172 through sravscag 14176. (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 14171	Lemma for srabaseg 14172 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 14172	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 14173	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 14174	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 14175	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 14176	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 14177	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 14178	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 14179	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 14180	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 14181	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 14182	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 14183	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 14184	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 14185*	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 14186	ringLMod is a function. (Contributed by Stefan O'Rear, 6-Dec-2014.)
|- ringLMod Fn _V
Theorem	rlmvalg 14187	Value of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( W e. V -> (ringLMod ` W ) = ( (subringAlg ` W ) ` ( Base ` W ) ) )
Theorem	rlmbasg 14188	Base set of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( R e. V -> ( Base ` R ) = ( Base ` (ringLMod ` R ) ) )
Theorem	rlmplusgg 14189	Vector addition in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( R e. V -> ( +g ` R ) = ( +g ` (ringLMod ` R ) ) )
Theorem	rlm0g 14190	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 14191	Subtraction in the ring module. (Contributed by Thierry Arnoux, 30-Jun-2019.)
|- ( R e. V -> ( -g ` R ) = ( -g ` (ringLMod ` R ) ) )
Theorem	rlmmulrg 14192	Ring multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( R e. V -> ( .r ` R ) = ( .r ` (ringLMod ` R ) ) )
Theorem	rlmscabas 14193	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 14194	Scalar multiplication in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( R e. V -> ( .r ` R ) = ( .s ` (ringLMod ` R ) ) )
Theorem	rlmtopng 14195	Topology component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( R e. V -> ( TopOpen ` R ) = ( TopOpen ` (ringLMod ` R ) ) )
Theorem	rlmdsg 14196	Metric component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( R e. V -> ( dist ` R ) = ( dist ` (ringLMod ` R ) ) )
Theorem	rlmlmod 14197	The ring module is a module. (Contributed by Stefan O'Rear, 6-Dec-2014.)
|- ( R e. Ring -> (ringLMod ` R ) e. LMod )
Theorem	rlmvnegg 14198	Vector negation in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014.) (Revised by Mario Carneiro, 5-Jun-2015.)
|- ( R e. V -> ( invg ` R ) = ( invg ` (ringLMod ` R ) ) )
Theorem	ixpsnbasval 14199*	The value of an infinite Cartesian product of the base of a left module over a ring with a singleton. (Contributed by AV, 3-Dec-2018.)
|- ( ( R e. V /\ X e. W ) -> X_ x e. { X } ( Base ` ( ( { X } X. { (ringLMod ` R ) } ) ` x ) ) = { f | ( f Fn { X } /\ ( f ` X ) e. ( Base ` R ) ) } )
7.6.2  Ideals and spans
Syntax	clidl 14200	Ring left-ideal function.
class LIdeal