P. 340 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33901-34000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-inftyexpiinj 33901	Injectivity of the parameterization inftyexpi. Remark: a more conceptual proof would use bj-inftyexpiinv 33900 and the fact that a function with a retraction is injective. (Contributed by BJ, 22-Jun-2019.)
|- ( ( A e. ( -u pi (,] pi ) /\ B e. ( -u pi (,] pi ) ) -> ( A = B <-> (inftyexpi ` A ) = (inftyexpi ` B ) ) )
Theorem	bj-inftyexpidisj 33902	An element of the circle at infinity is not a complex number. (Contributed by BJ, 22-Jun-2019.) This utility theorem is irrelevant and should generally not be used. (New usage is discouraged.)
|- -. (inftyexpi ` A ) e. CC
Syntax	cccinfty 33903	Syntax for the circle at infinity CCinfty.
class CCinfty
Definition	df-bj-ccinfty 33904	Definition of the circle at infinity CCinfty. (Contributed by BJ, 22-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.)
|- CCinfty = ran inftyexpi
Theorem	bj-ccinftydisj 33905	The circle at infinity is disjoint from the set of complex numbers. (Contributed by BJ, 22-Jun-2019.)
|- ( CC i^i CCinfty ) = (/)
Theorem	bj-elccinfty 33906	A lemma for infinite extended complex numbers. (Contributed by BJ, 27-Jun-2019.)
|- ( A e. ( -u pi (,] pi ) -> (inftyexpi ` A ) e. CCinfty )
Syntax	cccbar 33907	Syntax for the set of extended complex numbers CCbar.
class CCbar
Definition	df-bj-ccbar 33908	Definition of the set of extended complex numbers CCbar. (Contributed by BJ, 22-Jun-2019.)
|- CCbar = ( CC u. CCinfty )
Theorem	bj-ccssccbar 33909	Complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.)
|- CC C_ CCbar
Theorem	bj-ccinftyssccbar 33910	Infinite extended complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.)
|- CCinfty C_ CCbar
Syntax	cpinfty 33911	Syntax for pinfty.
class pinfty
Definition	df-bj-pinfty 33912	Definition of pinfty. (Contributed by BJ, 27-Jun-2019.)
|- pinfty = (inftyexpi ` 0 )
Theorem	bj-pinftyccb 33913	The class pinfty is an extended complex number. (Contributed by BJ, 27-Jun-2019.)
|- pinfty e. CCbar
Theorem	bj-pinftynrr 33914	The extended complex number pinfty is not a complex number. (Contributed by BJ, 27-Jun-2019.)
|- -. pinfty e. CC
Syntax	cminfty 33915	Syntax for minfty.
class minfty
Definition	df-bj-minfty 33916	Definition of minfty. (Contributed by BJ, 27-Jun-2019.)
|- minfty = (inftyexpi ` pi )
Theorem	bj-minftyccb 33917	The class minfty is an extended complex number. (Contributed by BJ, 27-Jun-2019.)
|- minfty e. CCbar
Theorem	bj-minftynrr 33918	The extended complex number minfty is not a complex number. (Contributed by BJ, 27-Jun-2019.)
|- -. minfty e. CC
Theorem	bj-pinftynminfty 33919	The extended complex numbers pinfty and minfty are different. (Contributed by BJ, 27-Jun-2019.)
|- pinfty =/= minfty
Syntax	crrbar 33920	Syntax for the set of extended real numbers RRbar.
class RRbar
Definition	df-bj-rrbar 33921	Definition of the set of extended real numbers RRbar. See df-xr 9633. (Contributed by BJ, 29-Jun-2019.)
|- RRbar = ( RR u. {minfty , pinfty } )
Syntax	cinfty 33922	Syntax for infty.
class infty
Definition	df-bj-infty 33923	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 33924	Syntax for CChat.
class CChat
Definition	df-bj-cchat 33925	Define the complex projective line, or Riemann sphere. (Contributed by BJ, 27-Jun-2019.)
|- CChat = ( CC u. {infty } )
Syntax	crrhat 33926	Syntax for RRhat.
class RRhat
Definition	df-bj-rrhat 33927	Define the real projective line. (Contributed by BJ, 27-Jun-2019.)
|- RRhat = ( RR u. {infty } )
Theorem	bj-rrhatsscchat 33928	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 33929	Syntax for the addition of extended complex numbers.
class +cc
Definition	df-bj-addc 33930	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 33931	Syntax for the opposite of extended complex numbers.
class -cc
Definition	df-bj-oppc 33932	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 33933	Syntax for the function prcpal.
class prcpal
Definition	df-bj-prcpal 33934	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 33935	Syntax for the argument of a nonzero extended complex number.
class Arg
Definition	df-bj-arg 33936	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 33937	Syntax for the multiplication of extended complex numbers.
class .cc
Definition	df-bj-mulc 33938	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 33939	Syntax for the inverse of nonzero extended complex numbers.
class invc
Definition	df-bj-invc 33940	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 16613 and subsequents. The first few statements of this subsection can be put very early after ccmn 16613. Proposal: in the main part, make separate subsections of commutative monoids and abelian groups. Relabel cabl 16614 to "cabl" or, preferably, other labels containing "abl" to "abel", for consistency.
Theorem	bj-cmnssmnd 33941	Commutative monoids are monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
|- CMnd C_ Mnd
Theorem	bj-cmnssmndel 33942	Commutative monoids are monoids (elemental version). This is a more direct proof of cmnmnd 16628, which relies on iscmn 16620. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
|- ( A e. CMnd -> A e. Mnd )
Theorem	bj-ablssgrp 33943	Abelian groups are groups. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
|- Abel C_ Grp
Theorem	bj-ablssgrpel 33944	Abelian groups are groups (elemental version). This is a shorter proof of ablgrp 16618. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
|- ( A e. Abel -> A e. Grp )
Theorem	bj-ablsscmn 33945	Abelian groups are commutative monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
|- Abel C_ CMnd
Theorem	bj-ablsscmnel 33946	Abelian groups are commutative monoids (elemental version). This is a shorter proof of ablcmn 16619. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
|- ( A e. Abel -> A e. CMnd )
Theorem	bj-modssabl 33947	(The additive groups of) modules are abelian groups. (The elemental version is lmodabl 17369; see also lmodgrp 17331 and lmodcmn 17370.) (Contributed by BJ, 9-Jun-2019.)
|- LMod C_ Abel
Theorem	bj-vecssmod 33948	Vector spaces are modules. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
|- LVec C_ LMod
Theorem	bj-vecssmodel 33949	Vector spaces are modules (elemental version). This is a shorter proof of lveclmod 17564. (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 14701 (although it mixes finite and infinite sums, which makes it harder to understand).
Syntax	cfinsum 33950	Syntax for the class "finite summation in monoids".
class FinSum
Definition	df-bj-finsum 33951*	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 33952*	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 33953	Syntax for the class of real vector spaces.
class RR-Vec
Definition	df-bj-rrvec 33954	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 33955	Real vector spaces are vector spaces. (Contributed by BJ, 9-Jun-2019.)
|- RR-Vec C_ LVec
Theorem	bj-rrvecssvecel 33956	Real vector spaces are vector spaces (elemental version). (Contributed by BJ, 9-Jun-2019.)
|- ( A e. RR-Vec -> A e. LVec )
Theorem	bj-rrvecsscmn 33957	(The additive groups of) real vector spaces are commutative monoids. (Contributed by BJ, 9-Jun-2019.)
|- RR-Vec C_ CMnd
Theorem	bj-rrvecsscmnel 33958	(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 33959	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 33960	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 33961	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 33962	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 33963	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 33964	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 33965	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 33966	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 33967	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 33970 (which computes them).
Theorem	bj-bary1lem 33968	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 33969	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 33970	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 33999, means that the definition or theorem is not used for the derivation of hlathil 36978. This is a temporary renaming to assist cleaning up the theorems needed by hlathil 36978.
Theorem	fsumshftd 33971*	Index shift of a finite sum with a weaker "implicit substitution" hypothesis than fsumshft 13561. The proof demonstrates how this can be derived starting from from fsumshft 13561. (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 33972*	Obsolete version of fsumshftd 33971 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 33973	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 5551. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) WARNING: THIS "AXIOM", WHICH IS THE OLD df-riota 6246, CONFLICTS WITH (THE NEW) df-riota 6246 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 33974*	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 33975*	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 33976*	Deduction version of riotasv 33979. (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 33977*	Value of description binder D for a single-valued class expression C ( y ) (as in e.g. reusv2 4653). Special case of riota2f 6268. (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 33978*	The value of description binder D for a single-valued class expression C ( y ) (as in e.g. reusv2 4653) in the form of a substitution instance. Special case of riota2f 6268. (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 33979*	Value of description binder D for a single-valued class expression C ( y ) (as in e.g. reusv2 4653). Special case of riota2f 6268. (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 33980*	A property ch holding for a representative of a single-valued class expression C ( y ) (see e.g. reusv2 4653) 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 33981	A version of elimhyp 3998 using explicit substitution. (Contributed by NM, 15-Jun-2019.)
|- [. B / x ]. ph   =>    |- [. if ( ph , x , B ) / x ]. ph
Theorem	dedths 33982	A version of weak deduction theorem dedth 3991 using explicit substitution. (Contributed by NM, 15-Jun-2019.)
|- [. if ( ph , x , B ) / x ]. ps   =>    |- ( ph -> ps )
Theorem	renegclALT 33983	Closure law for negative of reals. Demonstrates use of weak deduction theorem with explicit substitution. The proof is much longer than that of renegcl 9883. (Contributed by NM, 15-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A e. RR -> -u A e. RR )
Theorem	elimhyps2 33984	Generalization of elimhyps 33981 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 33985	Generalization of dedths 33982 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 33986	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 33987*	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 33988	Extend class notation with all 1-dim subspaces (atoms) of a left module or left vector space.
class LSAtoms
Syntax	clsh 33989	Extend class notation with all subspaces of a left module or left vector space that are hyperplanes.
class LSHyp
Definition	df-lsatoms 33990*	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 33991*	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 33992*	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 33993*	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 33994*	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 33995	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 33996	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 33997	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 33998	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 33999	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 34000	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. )