P. 342 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34101-34200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-minftyccb 34101	The class minfty is an extended complex number. (Contributed by BJ, 27-Jun-2019.)
|- minfty e. CCbar
Theorem	bj-minftynrr 34102	The extended complex number minfty is not a complex number. (Contributed by BJ, 27-Jun-2019.)
|- -. minfty e. CC
Theorem	bj-pinftynminfty 34103	The extended complex numbers pinfty and minfty are different. (Contributed by BJ, 27-Jun-2019.)
|- pinfty =/= minfty
Syntax	crrbar 34104	Syntax for the set of extended real numbers RRbar.
class RRbar
Definition	df-bj-rrbar 34105	Definition of the set of extended real numbers RRbar. See df-xr 9644. (Contributed by BJ, 29-Jun-2019.)
|- RRbar = ( RR u. {minfty , pinfty } )
Syntax	cinfty 34106	Syntax for infty.
class infty
Definition	df-bj-infty 34107	Definition of infty, the point at infinity of the real or complex projective line. (Contributed by BJ, 27-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.)
|- infty = ~P U. CC
Syntax	ccchat 34108	Syntax for CChat.
class CChat
Definition	df-bj-cchat 34109	Define the complex projective line, or Riemann sphere. (Contributed by BJ, 27-Jun-2019.)
|- CChat = ( CC u. {infty } )
Syntax	crrhat 34110	Syntax for RRhat.
class RRhat
Definition	df-bj-rrhat 34111	Define the real projective line. (Contributed by BJ, 27-Jun-2019.)
|- RRhat = ( RR u. {infty } )
Theorem	bj-rrhatsscchat 34112	The real projective line is included in the complex projective line. (Contributed by BJ, 27-Jun-2019.)
|- RRhat C_ CChat
21.29.6.3  Addition and opposite We define the operations on the extended real and complex numbers and on the real and complex projective lines simultaneously, thus "overloading" the operations.
Syntax	caddcc 34113	Syntax for the addition of extended complex numbers.
class +cc
Definition	df-bj-addc 34114	Define the additions on the extended complex numbers (on the subset of (CCbar X. CCbar ) where it makes sense) and on the complex projective line (Riemann sphere). (Contributed by BJ, 22-Jun-2019.)
|- +cc = ( x e. ( ( ( CC X. CCbar ) u. (CCbar X. CC ) ) u. ( (CChat X. CChat ) u. (Diag ` CCinfty ) ) ) |-> if ( ( ( 1st ` x ) = infty \/ ( 2nd ` x ) = infty ) , infty , if ( ( 1st ` x ) e. CC , if ( ( 2nd ` x ) e. CC , ( ( 1st ` x ) + ( 2nd ` x ) ) , ( 2nd ` x ) ) , ( 1st ` x ) ) ) )
Syntax	coppcc 34115	Syntax for the opposite of extended complex numbers.
class -cc
Definition	df-bj-oppc 34116	Define the negation (operation givin the opposite) the set of extended complex numbers and the complex projective line (Riemann sphere). One could use the prcpal function in the infinite case, but we want to use only basic functions at this point. (Contributed by BJ, 22-Jun-2019.)
|- -cc = ( x e. (CCbar u. CChat ) |-> if ( x = infty , infty , if ( x e. CC , -u x , (inftyexpi ` if ( 0 < ( 1st ` x ) , ( ( 1st ` x ) - pi ) , ( ( 1st ` x ) + pi ) ) ) ) ) )
21.29.6.4  Argument, multiplication and inverse Since one needs arguments in order to define multiplication in CCbar, it seems harder to put this at the very beginning of the introduction of complex numbers.
Syntax	cprcpal 34117	Syntax for the function prcpal.
class prcpal
Definition	df-bj-prcpal 34118	Define the function prcpal. (Contributed by BJ, 22-Jun-2019.)
|- prcpal = ( x e. RR |-> ( ( x mod ( 2 x. pi ) ) - if ( ( x mod ( 2 x. pi ) ) <_ pi , 0 , ( 2 x. pi ) ) ) )
Syntax	carg 34119	Syntax for the argument of a nonzero extended complex number.
class Arg
Definition	df-bj-arg 34120	Define the argument of a nonzero extended complex number. By convention, it has values in ( -u pi , pi ]. Another convention chooses [ 0 , 2 pi ) but the present one simplifies formulas giving the argument as an arc-tangent. (Contributed by BJ, 22-Jun-2019.)
|- Arg = ( x e. (CCbar \ { 0 } ) |-> if ( x e. CC , ( Im ` ( log ` x ) ) , ( 1st ` x ) ) )
Syntax	cmulc 34121	Syntax for the multiplication of extended complex numbers.
class .cc
Definition	df-bj-mulc 34122	Define the multiplication of extended complex numbers and of the complex projective line (Riemann sphere). In our convention, a product with 0 is 0, even when the other factor is infinite. An alternate convention leaves products of 0 with an infinite number undefined since the multiplication is not continuous at these points. Note that our convention entails ( 0 / 0 ) = 0. (Contributed by BJ, 22-Jun-2019.)
|- .cc = ( x e. ( (CCbar X. CCbar ) u. (CChat X. CChat ) ) |-> if ( ( ( 1st ` x ) = 0 \/ ( 2nd ` x ) = 0 ) , 0 , if ( ( ( 1st ` x ) = infty \/ ( 2nd ` x ) = infty ) , infty , if ( x e. ( CC X. CC ) , ( ( 1st ` x ) x. ( 2nd ` x ) ) , (inftyexpi ` (prcpal ` ( (Arg ` ( 1st ` x ) ) + (Arg ` ( 2nd ` x ) ) ) ) ) ) ) ) )
Syntax	cinvc 34123	Syntax for the inverse of nonzero extended complex numbers.
class invc
Definition	df-bj-invc 34124	Define inversion, which maps a nonzero extended complex number or element of the complex projective line (Riemann sphere) to its inverse. Beware of the overloading: the equality (invc ` 0 ) = infty is to be understood in the complex projective line, but 0 as an extended complex number does not have an inverse, which we can state as (invc ` 0 ) e/ CCbar. (Contributed by BJ, 22-Jun-2019.)
|- invc = ( x e. (CCbar u. CChat ) |-> if ( x = 0 , infty , if ( x e. CC , ( 1 / x ) , 0 ) ) )
21.29.7  Monoids See ccmn 16671 and subsequents. The first few statements of this subsection can be put very early after ccmn 16671. Proposal: in the main part, make separate subsections of commutative monoids and abelian groups. Relabel cabl 16672 to "cabl" or, preferably, other labels containing "abl" to "abel", for consistency.
Theorem	bj-cmnssmnd 34125	Commutative monoids are monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
|- CMnd C_ Mnd
Theorem	bj-cmnssmndel 34126	Commutative monoids are monoids (elemental version). This is a more direct proof of cmnmnd 16686, which relies on iscmn 16678. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
|- ( A e. CMnd -> A e. Mnd )
Theorem	bj-ablssgrp 34127	Abelian groups are groups. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
|- Abel C_ Grp
Theorem	bj-ablssgrpel 34128	Abelian groups are groups (elemental version). This is a shorter proof of ablgrp 16676. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
|- ( A e. Abel -> A e. Grp )
Theorem	bj-ablsscmn 34129	Abelian groups are commutative monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
|- Abel C_ CMnd
Theorem	bj-ablsscmnel 34130	Abelian groups are commutative monoids (elemental version). This is a shorter proof of ablcmn 16677. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
|- ( A e. Abel -> A e. CMnd )
Theorem	bj-modssabl 34131	(The additive groups of) modules are abelian groups. (The elemental version is lmodabl 17428; see also lmodgrp 17390 and lmodcmn 17429.) (Contributed by BJ, 9-Jun-2019.)
|- LMod C_ Abel
Theorem	bj-vecssmod 34132	Vector spaces are modules. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
|- LVec C_ LMod
Theorem	bj-vecssmodel 34133	Vector spaces are modules (elemental version). This is a shorter proof of lveclmod 17623. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
|- ( A e. LVec -> A e. LMod )
21.29.7.1  Finite sums in monoids UPDATE: a similar summation is already defined as df-gsum 14715 (although it mixes finite and infinite sums, which makes it harder to understand).
Syntax	cfinsum 34134	Syntax for the class "finite summation in monoids".
class FinSum
Definition	df-bj-finsum 34135*	Finite summation in commutative monoids. This finite summation function can be extended to pairs <. y , z >. where y is a left-unital magma and z is defined on a totally ordered set (choosing left-associative composition), or dropping unitality and requiring nonempty families, or on any monoids for families of permutable elements, etc. We use the term "summation", even though the definition stands for any unital, commutative and associative composition law. (Contributed by BJ, 9-Jun-2019.)
|- FinSum = ( x e. { <. y , z >. | ( y e. CMnd /\ E. t e. Fin z : t --> ( Base ` y ) ) } |-> ( iota s E. m e. NN0 E. f ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) ) ) )
Theorem	bj-finsumval0 34136*	Value of a finite sum. (Contributed by BJ, 9-Jun-2019.)
|- ( ph -> A e. CMnd )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> B : I --> ( Base ` A ) )   =>    |- ( ph -> ( A FinSum B ) = ( iota s E. m e. NN0 E. f ( f : ( 1 ... m ) -1-1-onto-> I /\ s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) ) )
21.29.8  Affine, Euclidean, and Cartesian geometry A few basic theorems to start affine, Euclidean, and Cartesian geometry.
21.29.8.1  Convex hull in real vector spaces A few basic definitions and theorems about convex hulls in real vector spaces. TODO: prove inclusion in the class of subcomplex vector spaces.
Syntax	crrvec 34137	Syntax for the class of real vector spaces.
class RR-Vec
Definition	df-bj-rrvec 34138	Definition of the class of real vector spaces. (Contributed by BJ, 9-Jun-2019.)
|- RR-Vec = { x e. LVec | (Scalar ` x ) = RRfld }
Theorem	bj-rrvecssvec 34139	Real vector spaces are vector spaces. (Contributed by BJ, 9-Jun-2019.)
|- RR-Vec C_ LVec
Theorem	bj-rrvecssvecel 34140	Real vector spaces are vector spaces (elemental version). (Contributed by BJ, 9-Jun-2019.)
|- ( A e. RR-Vec -> A e. LVec )
Theorem	bj-rrvecsscmn 34141	(The additive groups of) real vector spaces are commutative monoids. (Contributed by BJ, 9-Jun-2019.)
|- RR-Vec C_ CMnd
Theorem	bj-rrvecsscmnel 34142	(The additive groups of) real vector spaces are commutative monoids (elemental version). (Contributed by BJ, 9-Jun-2019.)
|- ( A e. RR-Vec -> A e. CMnd )
21.29.8.2  Complex numbers (supplements) Some lemmas to ease algebraic manipulations.
Theorem	bj-subcom 34143	A consequence of commutativity of multiplication. (Contributed by BJ, 6-Jun-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( A x. B ) - ( B x. A ) ) = 0 )
Theorem	bj-lsub 34144	Left-subtraction. (Contributed by BJ, 6-Jun-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + B ) = C <-> A = ( C - B ) ) )
Theorem	bj-rsub 34145	Right-subtraction. (Contributed by BJ, 6-Jun-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + B ) = C <-> B = ( C - A ) ) )
Theorem	bj-msub 34146	A subtraction law. (Contributed by BJ, 6-Jun-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( A = ( C - B ) <-> B = ( C - A ) ) )
Theorem	bj-ldiv 34147	Left-division. (Contributed by BJ, 6-Jun-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( ( A x. B ) = C <-> A = ( C / B ) ) )
Theorem	bj-rdiv 34148	Right-division. (Contributed by BJ, 6-Jun-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( ( A x. B ) = C <-> B = ( C / A ) ) )
Theorem	bj-mdiv 34149	A division law. (Contributed by BJ, 6-Jun-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( A = ( C / B ) <-> B = ( C / A ) ) )
Theorem	bj-lineq 34150	Solution of a (scalar) linear equation. (Contributed by BJ, 6-Jun-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> Y e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( ( ( A x. X ) + B ) = Y <-> X = ( ( Y - B ) / A ) ) )
Theorem	bj-lineqi 34151	Solution of a (scalar) linear equation. (Contributed by BJ, 6-Jun-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> Y e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> ( ( A x. X ) + B ) = Y )   =>    |- ( ph -> X = ( ( Y - B ) / A ) )
21.29.8.3  Barycentric coordinates Lemmas about barycentric coordinates. For the moment, this is limited to the one-dimensional case (complex line), where existence and uniqueness of barycentric coordinates is proved by bj-bary1 34154 (which computes them).
Theorem	bj-bary1lem 34152	A lemma for barycentric coordinates in one dimension. (Contributed by BJ, 6-Jun-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> X = ( ( ( ( B - X ) / ( B - A ) ) x. A ) + ( ( ( X - A ) / ( B - A ) ) x. B ) ) )
Theorem	bj-bary1lem1 34153	Existence and uniqueness (and actual computation) of barycentric coordinates in dimension 1 (complex line). (Contributed by BJ, 6-Jun-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> A =/= B )   &    |- ( ph -> S e. CC )   &    |- ( ph -> T e. CC )   =>    |- ( ph -> ( ( X = ( ( S x. A ) + ( T x. B ) ) /\ ( S + T ) = 1 ) -> T = ( ( X - A ) / ( B - A ) ) ) )
Theorem	bj-bary1 34154	Barycentric coordinates in one dimension. (Contributed by BJ, 6-Jun-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> A =/= B )   &    |- ( ph -> S e. CC )   &    |- ( ph -> T e. CC )   =>    |- ( ph -> ( ( X = ( ( S x. A ) + ( T x. B ) ) /\ ( S + T ) = 1 ) <-> ( S = ( ( B - X ) / ( B - A ) ) /\ T = ( ( X - A ) / ( B - A ) ) ) ) )
21.30  Mathbox for Norm Megill Note: A label suffixed with "N" (after the "Atoms..." section below), such as lshpnel2N 34183, means that the definition or theorem is not used for the derivation of hlathil 37162. This is a temporary renaming to assist cleaning up the theorems needed by hlathil 37162.
Theorem	fsumshftd 34155*	Index shift of a finite sum with a weaker "implicit substitution" hypothesis than fsumshft 13575. The proof demonstrates how this can be derived starting from from fsumshft 13575. (Contributed by NM, 1-Nov-2019.)
|- ( ph -> K e. ZZ )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )   &    |- ( ( ph /\ j = ( k - K ) ) -> A = B )   =>    |- ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( M + K ) ... ( N + K ) ) B )
Theorem	fsumshftdOLD 34156*	Obsolete version of fsumshftd 34155 as of 1-Nov-2019. (Contributed by NM, 1-Nov-2019.)
|- ( ph -> K e. ZZ )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )   &    |- ( ( ph /\ j = ( k - K ) ) -> A = B )   =>    |- ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( M + K ) ... ( N + K ) ) B )
Axiom	ax-riotaBAD 34157	Define restricted description binder. In case it doesn't exist, we return a set which is not a member of the domain of discourse A. See also comments for df-iota 5557. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) WARNING: THIS "AXIOM", WHICH IS THE OLD df-riota 6256, CONFLICTS WITH (THE NEW) df-riota 6256 AND MAKES THE SYSTEM IN set.mm INCONSISTENT. IT IS TEMPORARY AND WILL BE DELETED AFTER ALL USES ARE ELIMINATED.
|- ( iota_ x e. A ph ) = if ( E! x e. A ph , ( iota x ( x e. A /\ ph ) ) , ( Undef ` { x | x e. A } ) )
Theorem	riotaclbgBAD 34158*	Closure of restricted iota. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 24-Dec-2016.)
|- ( A e. V -> ( E! x e. A ph <-> ( iota_ x e. A ph ) e. A ) )
Theorem	riotaclbBAD 34159*	Closure of restricted iota. (Contributed by NM, 15-Sep-2011.)
|- A e. _V   =>    |- ( E! x e. A ph <-> ( iota_ x e. A ph ) e. A )
Theorem	riotasvd 34160*	Deduction version of riotasv 34163. (Contributed by NM, 4-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- ( ph -> D = ( iota_ x e. A A. y e. B ( ps -> x = C ) ) )   &    |- ( ph -> D e. A )   =>    |- ( ( ph /\ A e. V ) -> ( ( y e. B /\ ps ) -> D = C ) )
Theorem	riotasv2d 34161*	Value of description binder D for a single-valued class expression C ( y ) (as in e.g. reusv2 4659). Special case of riota2f 6278. (Contributed by NM, 2-Mar-2013.)
|- F/ y ph   &    |- ( ph -> F/_ y F )   &    |- ( ph -> F/ y ch )   &    |- ( ph -> D = ( iota_ x e. A A. y e. B ( ps -> x = C ) ) )   &    |- ( ( ph /\ y = E ) -> ( ps <-> ch ) )   &    |- ( ( ph /\ y = E ) -> C = F )   &    |- ( ph -> D e. A )   &    |- ( ph -> E e. B )   &    |- ( ph -> ch )   =>    |- ( ( ph /\ A e. V ) -> D = F )
Theorem	riotasv2s 34162*	The value of description binder D for a single-valued class expression C ( y ) (as in e.g. reusv2 4659) in the form of a substitution instance. Special case of riota2f 6278. (Contributed by NM, 3-Mar-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
|- D = ( iota_ x e. A A. y e. B ( ph -> x = C ) )   =>    |- ( ( A e. V /\ D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) -> D = [_ E / y ]_ C )
Theorem	riotasv 34163*	Value of description binder D for a single-valued class expression C ( y ) (as in e.g. reusv2 4659). Special case of riota2f 6278. (Contributed by NM, 26-Jan-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
|- A e. _V   &    |- D = ( iota_ x e. A A. y e. B ( ph -> x = C ) )   =>    |- ( ( D e. A /\ y e. B /\ ph ) -> D = C )
Theorem	riotasv3d 34164*	A property ch holding for a representative of a single-valued class expression C ( y ) (see e.g. reusv2 4659) also holds for its description binder D (in the form of property th). (Contributed by NM, 5-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/ y ph   &    |- ( ph -> F/ y th )   &    |- ( ph -> D = ( iota_ x e. A A. y e. B ( ps -> x = C ) ) )   &    |- ( ( ph /\ C = D ) -> ( ch <-> th ) )   &    |- ( ph -> ( ( y e. B /\ ps ) -> ch ) )   &    |- ( ph -> D e. A )   &    |- ( ph -> E. y e. B ps )   =>    |- ( ( ph /\ A e. V ) -> th )
21.30.1  Experiments with weak deduction theorem
Theorem	elimhyps 34165	A version of elimhyp 4004 using explicit substitution. (Contributed by NM, 15-Jun-2019.)
|- [. B / x ]. ph   =>    |- [. if ( ph , x , B ) / x ]. ph
Theorem	dedths 34166	A version of weak deduction theorem dedth 3997 using explicit substitution. (Contributed by NM, 15-Jun-2019.)
|- [. if ( ph , x , B ) / x ]. ps   =>    |- ( ph -> ps )
Theorem	renegclALT 34167	Closure law for negative of reals. Demonstrates use of weak deduction theorem with explicit substitution. The proof is much longer than that of renegcl 9894. (Contributed by NM, 15-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A e. RR -> -u A e. RR )
Theorem	elimhyps2 34168	Generalization of elimhyps 34165 that is not useful unless we can separately prove |- A e. _V. (Contributed by NM, 13-Jun-2019.)
|- [. B / x ]. ph   =>    |- [. if ( [. A / x ]. ph , A , B ) / x ]. ph
Theorem	dedths2 34169	Generalization of dedths 34166 that is not useful unless we can separately prove |- A e. _V. (Contributed by NM, 13-Jun-2019.)
|- [. if ( [. A / x ]. ph , A , B ) / x ]. ps   =>    |- ( [. A / x ]. ph -> [. A / x ]. ps )
21.30.2  Miscellanea
Theorem	cnaddcom 34170	Recover the commutative law of addition for complex numbers from the Abelian group structure. (Contributed by NM, 17-Mar-2013.) (Proof modification is discouraged.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
Theorem	toycom 34171*	Show the commutative law for an operation O on a toy structure class C of commuatitive operations on CC. This illustrates how a structure class can be partially specialized. In practice, we would ordinarily define a new constant such as "CAbel" in place of C. (Contributed by NM, 17-Mar-2013.) (Proof modification is discouraged.)
|- C = { g e. Abel | ( Base ` g ) = CC }   &    |- .+ = ( +g ` K )   =>    |- ( ( K e. C /\ A e. CC /\ B e. CC ) -> ( A .+ B ) = ( B .+ A ) )
21.30.3  Atoms, hyperplanes, and covering in a left vector space (or module)
Syntax	clsa 34172	Extend class notation with all 1-dim subspaces (atoms) of a left module or left vector space.
class LSAtoms
Syntax	clsh 34173	Extend class notation with all subspaces of a left module or left vector space that are hyperplanes.
class LSHyp
Definition	df-lsatoms 34174*	Define the set of all 1-dim subspaces (atoms) of a left module or left vector space. (Contributed by NM, 9-Apr-2014.)
|- LSAtoms = ( w e. _V |-> ran ( v e. ( ( Base ` w ) \ { ( 0g ` w ) } ) |-> ( ( LSpan ` w ) ` { v } ) ) )
Definition	df-lshyp 34175*	Define the set of all hyperplanes of a left module or left vector space. Also called co-atoms, these are subspaces that are one dimension less that the full space. (Contributed by NM, 29-Jun-2014.)
|- LSHyp = ( w e. _V |-> { s e. ( LSubSp ` w ) | ( s =/= ( Base ` w ) /\ E. v e. ( Base ` w ) ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) ) } )
Theorem	lshpset 34176*	The set of all hyperplanes of a left module or left vector space. The vector v is called a generating vector for the hyperplane. (Contributed by NM, 29-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- S = ( LSubSp ` W )   &    |- H = (LSHyp ` W )   =>    |- ( W e. X -> H = { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } )
Theorem	islshp 34177*	The predicate "is a hyperplane" (of a left module or left vector space). (Contributed by NM, 29-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- S = ( LSubSp ` W )   &    |- H = (LSHyp ` W )   =>    |- ( W e. X -> ( U e. H <-> ( U e. S /\ U =/= V /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) ) )
Theorem	islshpsm 34178*	Hyperplane properties expressed with subspace sum. (Contributed by NM, 3-Jul-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LMod )   =>    |- ( ph -> ( U e. H <-> ( U e. S /\ U =/= V /\ E. v e. V ( U .(+) ( N ` { v } ) ) = V ) ) )
Theorem	lshplss 34179	A hyperplane is a subspace. (Contributed by NM, 3-Jul-2014.)
|- S = ( LSubSp ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. H )   =>    |- ( ph -> U e. S )
Theorem	lshpne 34180	A hyperplane is not equal to the vector space. (Contributed by NM, 4-Jul-2014.)
|- V = ( Base ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. H )   =>    |- ( ph -> U =/= V )
Theorem	lshpnel 34181	A hyperplane's generating vector does not belong to the hyperplane. (Contributed by NM, 3-Jul-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. H )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { X } ) ) = V )   =>    |- ( ph -> -. X e. U )
Theorem	lshpnelb 34182	The subspace sum of a hyperplane and the span of an element equals the vector space iff the element is not in the hyperplane. (Contributed by NM, 2-Oct-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( -. X e. U <-> ( U .(+) ( N ` { X } ) ) = V ) )
Theorem	lshpnel2N 34183	Condition that determines a hyperplane. (Contributed by NM, 3-Oct-2014.) (New usage is discouraged.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. S )   &    |- ( ph -> U =/= V )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. U )   =>    |- ( ph -> ( U e. H <-> ( U .(+) ( N ` { X } ) ) = V ) )
Theorem	lshpne0 34184	The member of the span in the hyperplane definition does not belong to the hyperplane. (Contributed by NM, 14-Jul-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- .0. = ( 0g ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. H )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { X } ) ) = V )   =>    |- ( ph -> X =/= .0. )
Theorem	lshpdisj 34185	A hyperplane and the span in the hyperplane definition are disjoint. (Contributed by NM, 3-Jul-2014.)
|- V = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { X } ) ) = V )   =>    |- ( ph -> ( U i^i ( N ` { X } ) ) = { .0. } )
Theorem	lshpcmp 34186	If two hyperplanes are comparable, they are equal. (Contributed by NM, 9-Oct-2014.)
|- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> T e. H )   &    |- ( ph -> U e. H )   =>    |- ( ph -> ( T C_ U <-> T = U ) )
Theorem	lshpinN 34187	The intersection of two different hyperplanes is not a hyperplane. (Contributed by NM, 29-Oct-2014.) (New usage is discouraged.)
|- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> T e. H )   &    |- ( ph -> U e. H )   =>    |- ( ph -> ( ( T i^i U ) e. H <-> T = U ) )
Theorem	lsatset 34188*	The set of all 1-dim subspaces (atoms) of a left module or left vector space. (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   =>    |- ( W e. X -> A = ran ( v e. ( V \ { .0. } ) |-> ( N ` { v } ) ) )
Theorem	islsat 34189*	The predicate "is a 1-dim subspace (atom)" (of a left module or left vector space). (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   =>    |- ( W e. X -> ( U e. A <-> E. x e. ( V \ { .0. } ) U = ( N ` { x } ) ) )
Theorem	lsatlspsn2 34190	The span of a non-zero singleton is an atom. TODO: make this obsolete and use lsatlspsn 34191 instead? (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   =>    |- ( ( W e. LMod /\ X e. V /\ X =/= .0. ) -> ( N ` { X } ) e. A )
Theorem	lsatlspsn 34191	The span of a non-zero singleton is an atom. (Contributed by NM, 16-Jan-2015.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. ( V \ { .0. } ) )   =>    |- ( ph -> ( N ` { X } ) e. A )
Theorem	islsati 34192*	A 1-dim subspace (atom) (of a left module or left vector space) equals the span of some vector. (Contributed by NM, 1-Oct-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- A = (LSAtoms ` W )   =>    |- ( ( W e. X /\ U e. A ) -> E. v e. V U = ( N ` { v } ) )
Theorem	lsateln0 34193*	A 1-dim subspace (atom) (of a left module or left vector space) contains a nonzero vector. (Contributed by NM, 2-Jan-2015.)
|- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. A )   =>    |- ( ph -> E. v e. U v =/= .0. )
Theorem	lsatlss 34194	The set of 1-dim subspaces is a set of subspaces. (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
|- S = ( LSubSp ` W )   &    |- A = (LSAtoms ` W )   =>    |- ( W e. LMod -> A C_ S )
Theorem	lsatlssel 34195	An atom is a subspace. (Contributed by NM, 25-Aug-2014.)
|- S = ( LSubSp ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. A )   =>    |- ( ph -> U e. S )
Theorem	lsatssv 34196	An atom is a set of vectors. (Contributed by NM, 27-Feb-2015.)
|- V = ( Base ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> Q e. A )   =>    |- ( ph -> Q C_ V )
Theorem	lsatn0 34197	A 1-dim subspace (atom) of a left module or left vector space is nonzero. (atne0 27087 analog.) (Contributed by NM, 25-Aug-2014.)
|- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. A )   =>    |- ( ph -> U =/= { .0. } )
Theorem	lsatspn0 34198	The span of a vector is an atom iff the vector is nonzero. (Contributed by NM, 4-Feb-2015.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( ( N ` { X } ) e. A <-> X =/= .0. ) )
Theorem	lsator0sp 34199	The span of a vector is either an atom or the zero subspace. (Contributed by NM, 15-Mar-2015.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( ( N ` { X } ) e. A \/ ( N ` { X } ) = { .0. } ) )
Theorem	lsatssn0 34200	A subspace (or any class) including an atom is nonzero. (Contributed by NM, 3-Feb-2015.)
|- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> Q e. A )   &    |- ( ph -> Q C_ U )   =>    |- ( ph -> U =/= { .0. } )