P. 326 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32501-32600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-1uplex 32501	A monuple is a set if and only if its coordinates are sets. (Contributed by BJ, 6-Apr-2019.)
|- ((| A|) e. _V <-> A e. _V )
Theorem	bj-1upln0 32502	A monuple is nonempty. (Contributed by BJ, 6-Apr-2019.)
|- (| A|) =/= (/)
Syntax	bj-c2uple 32503	Syntax for Morse couple. (Contributed by BJ, 6-Oct-2018.)
class (| A, B|)
Definition	df-bj-2upl 32504	Definition of the Morse couple. See df-bj-1upl 32491. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-2upleq 32505, bj-2uplth 32514, bj-2uplex 32515, and the properties of the projections (see df-bj-pr1 32494 and df-bj-pr2 32508). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
|- (| A, B|) = ((| A|) u. ( { 1o } X. tag B ) )
Theorem	bj-2upleq 32505	Substitution property for (| - , - |). (Contributed by BJ, 6-Oct-2018.)
|- ( A = B -> ( C = D -> (| A, C|) = (| B, D|) ) )
Theorem	bj-pr21val 32506	Value of the first projection of a couple. (Contributed by BJ, 6-Oct-2018.)
|- pr1 (| A, B|) = A
Syntax	bj-cpr2 32507	Syntax for the second class tuple projection. (Contributed by BJ, 6-Oct-2018.)
class pr2 A
Definition	df-bj-pr2 32508	Definition of the second projection of a class tuple. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-pr2eq 32509, bj-pr22val 32512, bj-pr2ex 32513. (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
|- pr2 A = ( 1o Proj A )
Theorem	bj-pr2eq 32509	Substitution property for pr2. (Contributed by BJ, 6-Oct-2018.)
|- ( A = B -> pr2 A = pr2 B )
Theorem	bj-pr2un 32510	The second projection preserves unions. (Contributed by BJ, 6-Apr-2019.)
|- pr2 ( A u. B ) = (pr2 A u. pr2 B )
Theorem	bj-pr2val 32511	Value of the second projection. (Contributed by BJ, 6-Apr-2019.)
|- pr2 ( { A } X. tag B ) = if ( A = 1o , B , (/) )
Theorem	bj-pr22val 32512	Value of the second projection of a couple. (Contributed by BJ, 6-Oct-2018.)
|- pr2 (| A, B|) = B
Theorem	bj-pr2ex 32513	Sethood of the second projection. (Contributed by BJ, 6-Oct-2018.)
|- ( A e. V -> pr2 A e. _V )
Theorem	bj-2uplth 32514	The characteristic property of couples. Note that this holds without sethood hypotheses (compare opth 4566). (Contributed by BJ, 6-Oct-2018.)
|- ((| A, B|) = (| C, D|) <-> ( A = C /\ B = D ) )
Theorem	bj-2uplex 32515	A couple is a set if and only if its coordinates are sets. (Contributed by BJ, 6-Oct-2018.)
|- ((| A, B|) e. _V <-> ( A e. _V /\ B e. _V ) )
Theorem	bj-2upln0 32516	A couple is nonempty. (Contributed by BJ, 21-Apr-2019.)
|- (| A, B|) =/= (/)
Theorem	bj-2upln1upl 32517	A couple is never equal to a monuple. It is in order to have this "non-clashing" result that tagging was used. Without tagging, we would have (| A , (/)|) = (| A|). Note that in the context of Morse tuples, it is natural to define the 0-tuple as the empty set. Therefore, the present theorem together with bj-1upln0 32502 and bj-2upln0 32516 tell us that an m-tuple may equal an n-tuple only when m = n, at least for m, n <= 2, but this result would extend as soon as we define n-tuples for higher values of n. (Contributed by BJ, 21-Apr-2019.)
|- (| A, B|) =/= (| C|)
21.29.5.13  Set theory: miscellaneous
Theorem	bj-vtoclgfALT 32518	Alternate proof of vtoclgf 3028. Proof from vtoclgft 3020. (This may have been the original proof before shortening.) (Contributed by BJ, 30-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/_ x A   &    |- F/ x ps   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ph   =>    |- ( A e. V -> ps )
Theorem	bj-pwcfsdom 32519	Remove hypothesis from pwcfsdom 8747. Illustration of how to remove a "proof-facilitating hypothesis". (Can use it to shorten theorems using pwcfsdom 8747.) (Contributed by BJ, 14-Sep-2019.)
|- ( aleph ` A ) ~< ( ( aleph ` A ) ^m ( cf ` ( aleph ` A ) ) )
Theorem	bj-grur1 32520	Remove hypothesis from grur1a 8986. Illustration of how to remove a "definitional hypothesis". This makes its uses longer, but the theorem feels more self-contained. Looks preferable when the defined term appears only once in the conclusion. (Contributed by BJ, 14-Sep-2019.)
|- ( ( U e. Univ /\ U e. U. ( R1 " On ) ) -> U = ( R1 ` ( U i^i On ) ) )
21.29.6  Extended real and complex numbers, real and complex projectives lines In this section, we indroduce several supersets of the set RR of real numbers and the set CC of complex numbers. Once they are given their usual topologies, which are locally compact, both topological spaces have a one-point compactification. They are denoted by RRhat and CChat respectively, defined in df-bj-cchat 32556 and df-bj-rrhat 32558, and the point at infinity is denoted by infty, defined in df-bj-infty 32554. Both RR and CC also have "directional compactifications", denoted respectively by RRbar, defined in df-bj-rrbar 32552 (already defined as RR*, see df-xr 9422) and CCbar, defined in df-bj-ccbar 32539. Since CCbar does not seem to be standard, we describe it in some detail. It is obtained by adding to CC a "point at infinity at the end of each ray with origin at 0". Although CCbar is not an important object in itself, the motivation for introducing it is to provide a common superset to both RRbar and CC and to define algebraic operations (addition, opposite, multiplication, inverse) as widely as reasonably possible. Mathematically, CCbar is the quotient of ( ( CC X. RR>=0 ) \ { <. 0 , 0 >. } ) by the diagonal multiplicative action of RR+ (think of the closed "northern hemisphere" in R^3 identified with ( CC X. RR ), that each open ray from 0 included in the closed northern half-space intersects exactly once). Since in set.mm, we want to have a genuine inclusion CC C_ CCbar, we instead define CCbar as the (disjoint) union of CC with a circle at infinity denoted by CCinfty. To have a genuine inclusion RRbar C_ CCbar, we define pinfty and minfty as certain points in CCinfty. Thanks to this framework, we have the genuine inclusions RR C_ RRbar and RR C_ RRhat and similarly with the complex systems, and furthermore RR C_ CC and similarly for the "overlined" and "hatted" versions. Furthermore, we define the main algebraic operations on (CCbar u. CChat ), which is not very mathematical, but "overloads" the operations, so that one can use the same notation in all cases.
21.29.6.1  Diagonal in a Cartesian square Complements on the idendity relation and definition of the diagonal in the Cartesian square of a set.
Theorem	bj-elid 32521	Characterization of the elements of _I. (Contributed by BJ, 22-Jun-2019.)
|- ( A e. ( V X. V ) -> ( A e. _I <-> ( 1st ` A ) = ( 2nd ` A ) ) )
Theorem	bj-elopg 32522	Characterization of the elements of an ordered pair (closed form of elop 4558, which actually has one unnecessary hypothesis). (Contributed by BJ, 22-Jun-2019.)
|- ( ( A e. V /\ B e. W ) -> ( C e. <. A , B >. <-> ( C = { A } \/ C = { A , B } ) ) )
Syntax	cdiag2 32523	Syntax for the diagonal of the Cartesian square of a set.
class Diag
Definition	df-bj-diag 32524	Define the diagonal of the Cartesian square of a set. (Contributed by BJ, 22-Jun-2019.)
|- Diag = ( x e. _V |-> ( _I i^i ( x X. x ) ) )
Theorem	bj-diagval 32525	Value of the diagonal. (Contributed by BJ, 22-Jun-2019.)
|- ( A e. V -> (Diag ` A ) = ( _I i^i ( A X. A ) ) )
Theorem	bj-eldiag 32526	Characterization of the elements the diagonal of a Cartesian square. (Contributed by BJ, 22-Jun-2019.)
|- ( A e. V -> ( B e. (Diag ` A ) <-> ( B e. ( A X. A ) /\ ( 1st ` B ) = ( 2nd ` B ) ) ) )
Theorem	bj-flbi3 32527	The floor of a real number in [ 0 , 1 ) is 0. Remark: may shorten the proof of modid 11732 or a version of it where the antecedent is membership in an interval. (Contributed by BJ, 29-Jun-2019.)
|- ( A e. ( 0 [,) 1 ) -> ( |_ ` A ) = 0 )
Theorem	bj-pirp 32528	Duplication of pirp 35613. (Contributed by Jim Kingdon, 19-Feb-2019.)
|- pi e. RR+
21.29.6.2  Extended numbers and projective lines as sets TODO(?): replace inftyexpi with a function inftyexpi2pi defined on ( 0 [,) 1 ) since we plan to put this section as early as possible, before the definition of pi. It looks like to define the sets, the addition and the opposite, one only needs some basic results about addition, opposite and ordering, which could use df-plr 9228, df-ltr 9230, df-0r 9231, df-1r 9232, df-ltr 9230. The idea is then to define the order relation directly on RRbar, skipping RR.
Syntax	cinftyexpi 32529	Syntax for the function inftyexpi parameterizing CCinfty.
class inftyexpi
Definition	df-bj-inftyexpi 32530	Definition of the auxiliary function inftyexpi parameterizing the circle at infinity CCinfty in CCbar. We use coupling with CC to simplify the proof of bj-ccinftydisj 32536. It could seem more natural to define inftyexpi on all of RR using prcpal but we want to use only basic functions in the definition of CCbar. (Contributed by BJ, 22-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.)
|- inftyexpi = ( x e. ( -u pi (,] pi ) |-> <. x , CC >. )
Theorem	bj-inftyexpiinv 32531	Utility theorem for the inverse of inftyexpi. (Contributed by BJ, 22-Jun-2019.) This utility theorem is irrelevant and should generally not be used. (New usage is discouraged.)
|- ( A e. ( -u pi (,] pi ) -> ( 1st ` (inftyexpi ` A ) ) = A )
Theorem	bj-inftyexpiinj 32532	Injectivity of the parameterization inftyexpi. Remark: a more conceptual proof would use bj-inftyexpiinv 32531 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 32533	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 32534	Syntax for the circle at infinity CCinfty.
class CCinfty
Definition	df-bj-ccinfty 32535	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 32536	The circle at infinity is disjoint form the set of complex numbers. (Contributed by BJ, 22-Jun-2019.)
|- ( CC i^i CCinfty ) = (/)
Theorem	bj-elccinfty 32537	A lemma for infinite extended complex numbers. (Contributed by BJ, 27-Jun-2019.)
|- ( A e. ( -u pi (,] pi ) -> (inftyexpi ` A ) e. CCinfty )
Syntax	cccbar 32538	Syntax for the set of extended complex numbers CCbar.
class CCbar
Definition	df-bj-ccbar 32539	Definition of the set of extended complex numbers CCbar. (Contributed by BJ, 22-Jun-2019.)
|- CCbar = ( CC u. CCinfty )
Theorem	bj-ccssccbar 32540	Complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.)
|- CC C_ CCbar
Theorem	bj-ccinftyssccbar 32541	Infinite extended complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.)
|- CCinfty C_ CCbar
Syntax	cpinfty 32542	Syntax for pinfty.
class pinfty
Definition	df-bj-pinfty 32543	Definition of pinfty. (Contributed by BJ, 27-Jun-2019.)
|- pinfty = (inftyexpi ` 0 )
Theorem	bj-pinftyccb 32544	The class pinfty is an extended complex number. (Contributed by BJ, 27-Jun-2019.)
|- pinfty e. CCbar
Theorem	bj-pinftynrr 32545	The extended complex number pinfty is not a complex number. (Contributed by BJ, 27-Jun-2019.)
|- -. pinfty e. CC
Syntax	cminfty 32546	Syntax for minfty.
class minfty
Definition	df-bj-minfty 32547	Definition of minfty. (Contributed by BJ, 27-Jun-2019.)
|- minfty = (inftyexpi ` pi )
Theorem	bj-minftyccb 32548	The class minfty is an extended complex number. (Contributed by BJ, 27-Jun-2019.)
|- minfty e. CCbar
Theorem	bj-minftynrr 32549	The extended complex number minfty is not a complex number. (Contributed by BJ, 27-Jun-2019.)
|- -. minfty e. CC
Theorem	bj-pinftynminfty 32550	The extended complex numbers pinfty and minfty are different. (Contributed by BJ, 27-Jun-2019.)
|- pinfty =/= minfty
Syntax	crrbar 32551	Syntax for the set of extended real numbers RRbar.
class RRbar
Definition	df-bj-rrbar 32552	Definition of the set of extended real numbers RRbar. See df-xr 9422. (Contributed by BJ, 29-Jun-2019.)
|- RRbar = ( RR u. {minfty , pinfty } )
Syntax	cinfty 32553	Syntax for infty.
class infty
Definition	df-bj-infty 32554	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 32555	Syntax for CChat.
class CChat
Definition	df-bj-cchat 32556	Define the complex projective line, or Riemann sphere. (Contributed by BJ, 27-Jun-2019.)
|- CChat = ( CC u. {infty } )
Syntax	crrhat 32557	Syntax for RRhat.
class RRhat
Definition	df-bj-rrhat 32558	Define the real projective line. (Contributed by BJ, 27-Jun-2019.)
|- RRhat = ( RR u. {infty } )
Theorem	bj-rrhatsscchat 32559	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 32560	Syntax for the addition of extended complex numbers.
class +cc
Definition	df-bj-addc 32561	Define the additions of extended complex numbers (on the subset of (CCbar X. CCbar ) where it makes sense) and of the projective line. (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 32562	Syntax for the opposite of extended complex numbers.
class -cc
Definition	df-bj-oppc 32563	Define the opposite of an extended complex number or an element of the projective line (or more precisely, the operation giving the opposite, sometimes called negation). 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 32564	Syntax for the function prcpal.
class prcpal
Definition	df-bj-prcpal 32565	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 32566	Syntax for the argument of a nonzero extended complex number.
class Arg
Definition	df-bj-arg 32567	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 32568	Syntax for the multiplication of extended complex numbers.
class .cc
Definition	df-bj-mulc 32569	Define the multiplications of extended complex numbers and of the complex projective line. In our convention, a product with 0 is 0. Another convention leaves products of 0 with an infinite number undefined since the multiplication is not continuous at these points. (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 32570	Syntax for the inverse of nonzero extended complex numbers.
class invc
Definition	df-bj-invc 32571	Define inversion, which maps a nonzero extended complex number or element of the projective line to its inverse. Beware of the overloading: the equality (invc ` 0 ) = infty is to be understood in the 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 16277 and subsequents. The first few statements of this subsection can be put very early after ccmn 16277. Proposal: in the main part, make separate subsections of commutative monoids and abelian groups. Relabel cabel 16278 to "cabl" or other labels containing "abl" to "abel".
Theorem	bj-cmnssmnd 32572	Commutative monoids are monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
|- CMnd C_ Mnd
Theorem	bj-cmnssmndel 32573	Commutative monoids are monoids (elemental version). This is a more direct proof of cmnmnd 16292, which relies on iscmn 16284. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
|- ( A e. CMnd -> A e. Mnd )
Theorem	bj-ablssgrp 32574	Abelian groups are groups. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
|- Abel C_ Grp
Theorem	bj-ablssgrpel 32575	Abelian groups are groups (elemental version). This is a shorter proof of ablgrp 16282. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
|- ( A e. Abel -> A e. Grp )
Theorem	bj-ablsscmn 32576	Abelian groups are commutative monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
|- Abel C_ CMnd
Theorem	bj-ablsscmnel 32577	Abelian groups are commutative monoids (elemental version). This is a shorter proof of ablcmn 16283. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
|- ( A e. Abel -> A e. CMnd )
Theorem	bj-modssabl 32578	(The additive groups of) modules are abelian groups. (The elemental version is lmodabl 16992; see also lmodgrp 16955 and lmodcmn 16993.) (Contributed by BJ, 9-Jun-2019.)
|- LMod C_ Abel
Theorem	bj-vecssmod 32579	Vector spaces are modules. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
|- LVec C_ LMod
Theorem	bj-vecssmodel 32580	Vector spaces are modules (elemental version). This is a shorter proof of lveclmod 17187. (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 14381 (although it mixes finite and infinite sums, which makes it harder to understand).
Syntax	cfinsum 32581	Syntax for the class "finite summation in monoids".
class FinSum
Definition	df-bj-finsum 32582*	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 32583*	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 32584	Syntax for the class of real vector spaces.
class RR-Vec
Definition	df-bj-rrvec 32585	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 32586	Real vector spaces are vector spaces. (Contributed by BJ, 9-Jun-2019.)
|- RR-Vec C_ LVec
Theorem	bj-rrvecssvecel 32587	Real vector spaces are vector spaces (elemental version). (Contributed by BJ, 9-Jun-2019.)
|- ( A e. RR-Vec -> A e. LVec )
Theorem	bj-rrvecsscmn 32588	(The additive groups of) real vector spaces are commutative monoids. (Contributed by BJ, 9-Jun-2019.)
|- RR-Vec C_ CMnd
Theorem	bj-rrvecsscmnel 32589	(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 32590	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 32591	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 32592	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 32593	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 32594	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 32595	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 32596	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 32597	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 32598	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 32601 (which computes them).
Theorem	bj-bary1lem 32599	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 32600	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 ) ) ) )