Skip to content

Commit

Permalink
Mathbox misc (metamath#3749)
Browse files Browse the repository at this point in the history 
* Mathbox only:
* bj-sylge, bj-alrimd, bj-exlimd
* remove some proofs avoiding ax-13 after they became obsolete because of improvements in Main part (but note bj-dtru)
* bj-abbi: to be move do Main
* bj-recleq, bj-reabeq
* bj-nfald, bj-nfexd
* copsex2d, copsex2b, opelopabd, opelopabb, bj-opabssvv
* bj-opelrelex, bj-opelresdm, bj-brresdm
* comment the 'functionalized identity' section before probably removing it
* various theorems about the identity relation
* direct image: bj-imdirid
* various comment edits and proof shortenings

* remove extra files

* Mathbox: remove bj-exlime as special instance of bj-sylge; add basics of real vector spaces; misc.

* typo

* Mathbox: modify df-bj-rvec and adapt proofs.

* update discouraged
  • Loading branch information
@benjub
benjub authored Jan 9, 2024
1 parent f42e3e5 commit e1005b4
Show file tree
Hide file tree
Showing 2 changed files with 180 additions and 55 deletions.
5 changes: 4 additions & 1 deletion discouraged
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14509,6 +14509,7 @@ New usage of "df-ba" is discouraged (1 uses).
New usage of "df-bdop" is discouraged (2 uses).
New usage of "df-bj-1upl" is discouraged (6 uses).
New usage of "df-bj-2upl" is discouraged (6 uses).
New usage of "df-bj-arg" is discouraged (0 uses).
New usage of "df-bj-ccinfty" is discouraged (3 uses).
New usage of "df-bj-ccinftyN" is discouraged (1 uses).
New usage of "df-bj-fractemp" is discouraged (0 uses).
Expand Down Expand Up @@ -18069,7 +18070,7 @@ Proof modification of "bj-ceqsalt1" is discouraged (118 steps).
Proof modification of "bj-ceqsaltv" is discouraged (45 steps).
Proof modification of "bj-ceqsalv" is discouraged (10 steps).
Proof modification of "bj-cleljusti" is discouraged (20 steps).
Proof modification of "bj-cmnssmnd" is discouraged (36 steps).
Proof modification of "bj-cmnssmnd" is discouraged (30 steps).
Proof modification of "bj-cmnssmndel" is discouraged (5 steps).
Proof modification of "bj-consensusALT" is discouraged (30 steps).
Proof modification of "bj-csbprc" is discouraged (47 steps).
Expand Down Expand Up @@ -18115,6 +18116,8 @@ Proof modification of "bj-fvmptunsn2" is discouraged (54 steps).
Proof modification of "bj-fvsnun2" is discouraged (44 steps).
Proof modification of "bj-gl4" is discouraged (58 steps).
Proof modification of "bj-godellob" is discouraged (19 steps).
Proof modification of "bj-grpssmnd" is discouraged (29 steps).
Proof modification of "bj-grpssmndel" is discouraged (5 steps).
Proof modification of "bj-hbaeb" is discouraged (22 steps).
Proof modification of "bj-hbaeb2" is discouraged (73 steps).
Proof modification of "bj-hbntbi" is discouraged (31 steps).
Expand Down
230 changes: 176 additions & 54 deletions set.mm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -439245,8 +439245,8 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the
althtmldef "-cc" as "-<SUB>&#8450;&#x305;</SUB>";
latexdef "-cc" as "-_{\overline{\mathbb{C}}}";
htmldef "<rr" as "<rr";
althtmldef "<rr" as "&lt;<SUB>R</SUB>";
latexdef "<rr" as "<_R";
althtmldef "<rr" as "&lt;<SUB>&#8477;&#x305;</SUB>";
latexdef "<rr" as "<_{\overline{\mathbb{R}}}";
htmldef ".cc" as " .cc ";
althtmldef ".cc" as " &#183;<SUB>&#8450;&#x305;</SUB> ";
latexdef ".cc" as " \cdot_{\overline{\mathbb{C}}} ";
Expand Down Expand Up @@ -530504,7 +530504,7 @@ Utility lemmas or strengthenings of theorems in the main part (biconditional
bj-sylge.nf $e |- ( E. x ph -> ps ) $.
bj-sylge.maj $e |- ( ch -> ph ) $.
$( Dual statement of ~ sylg (the final "e" in the label stands for
"existential (version of ~ sylg )". General instance of ~ exlimih .
"existential (version of ~ sylg )". Variant of ~ exlimih .
(Contributed by BJ, 25-Dec-2023.) $)
bj-sylge $p |- ( E. x ch -> ps ) $=
( wex eximi syl ) CDGADGBCADFHEI $.
Expand Down Expand Up @@ -530571,16 +530571,6 @@ could be deduced from it ( ~ exim would have to be proved first, see
( wb wal wa wex exbi adantl simpl imbi12d ) ABDZLCEZFACGZBCGZABMNODLABCHILM
JK $.

${
bj-exlime.1 $e |- ( E. x ps -> ps ) $.
bj-exlime.2 $e |- ( ph -> ps ) $.
$( Variant of ~ exlimih where the nonfreeness of ` x ` in ` ps ` is
expressed using an existential quantifier, thus requiring fewer axioms.
(Contributed by BJ, 17-Mar-2020.) $)
bj-exlime $p |- ( E. x ph -> ps ) $=
( wex eximi syl ) ACFBCFBABCEGDH $.
$}

$( Distribute quantifiers over a nested implication.

This and the following theorems are the general instances of already
Expand Down Expand Up @@ -530995,7 +530985,7 @@ could be deduced from it ( ~ exim would have to be proved first, see
~ cbvalvw . TODO: move after ~ cbvalivw . (Contributed by BJ,
17-Mar-2020.) $)
bj-cbvexiw $p |- ( E. x ph -> E. y ps ) $=
( wex spimew bj-exlime ) ABDHCEABDCFGIJ $.
( wex spimew bj-sylge ) BDHZKACEABDCFGIJ $.
$}

${
Expand Down Expand Up @@ -531835,8 +531825,7 @@ two more essential steps but fewer total steps (since there are fewer
( wnnf wal wi bj-nnfa alim syl9 ) ACDAACEABFCEBCEACGABCHI $.

$( Proof of the closed form of ~ exlimi from modalK (compare ~ exlimiv ).
See also ~ bj-sylget2 and ~ bj-exlime . (Contributed by BJ,
2-Dec-2023.) $)
See also ~ bj-sylget2 . (Contributed by BJ, 2-Dec-2023.) $)
bj-nnf-exlim $p |-
( F// x ps -> ( A. x ( ph -> ps ) -> ( E. x ph -> ps ) ) ) $=
( wi wal wex wnnf exim bj-nnfe syl9r ) ABDCEACFBCFBCGBABCHBCIJ $.
Expand Down Expand Up @@ -535344,10 +535333,14 @@ Moore collections (complements)

${
$d x A $. $d x B $. $d x X $.
$( If ` A ` is a collection of subsets of ` X ` , like a topology, two
equivalent ways to say that arbitrary intersections of elements of ` A `
relative to ` X ` belong to some class ` B ` (in typical applications,
` A ` itself). (Contributed by BJ, 7-Dec-2021.) $)
$( If ` A ` is a collection of subsets of ` X ` , like a Moore collection
or a topology, two equivalent ways to say that arbitrary intersections
of elements of ` A ` relative to ` X ` belong to some class ` B ` : the
LHS singles out the empty intersection (the empty intersection relative
to ` X ` is ` X ` and the intersection of a nonempty family of subsets
of ` X ` in included in ` X ` , so there is no need to intersect it with
` X ` ). In typical applications, ` B ` is ` A ` itself. (Contributed
by BJ, 7-Dec-2021.) $)
bj-0int $p |- ( A C_ ~P X -> (
( X e. B /\ A. x e. ( ~P A \ { (/) } ) |^| x e. B ) <->
A. x e. ~P A ( X i^i |^| x ) e. B ) ) $=
Expand Down Expand Up @@ -535641,8 +535634,8 @@ is a Moore collection ( ~ bj-snmoore ), this can also be stated as
Currying
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-

Currying and uncurrying. See also df-cur and ~ df-unc . Contrary to these,
the definitions in this section are parameterized.
Currying and uncurrying. See also ~ df-cur and ~ df-unc . Contrary to
these, the definitions in this section are parameterized.

$)

Expand Down Expand Up @@ -536974,11 +536967,17 @@ extended complex numbers and the complex projective line (Riemann
carg $a class Arg $.

$( 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 arctangent. (Contributed by BJ, 22-Jun-2019.) $)
it has values in ` ( -u _pi , _pi ] ` . Another convention chooses values
in ` [ 0 , 2 _pi ) ` but the present convention simplifies formulas giving
the argument as an arctangent. (Contributed by BJ, 22-Jun-2019.) The
"else" case of the second conditional operator, corresponding to infinite
extended complex numbers other than ` minfty ` , gives a definition
depending on the specific definition chosen for these numbers
( ~ df-bj-inftyexpitau ), and therefore should not be relied upon.
(New usage is discouraged.) $)
df-bj-arg $a |- Arg = ( x e. ( CCbar \ { 0 } ) |->
if ( x e. CC , ( Im ` ( log ` x ) ) , ( 1st ` x ) ) ) $.
if ( x e. CC , ( Im ` ( log ` x ) ) ,
if ( x <rr 0 , _pi , ( ( ( 1st ` x ) / ( 2 x. _pi ) ) - _pi ) ) ) ) $.

$( Token for the multiplication of extended complex numbers. $)
$c .cc $.
Expand Down Expand Up @@ -537281,8 +537280,8 @@ singleton on a couple (with disjoint domain) at a point in the domain
$( Commutative monoids are monoids. (Contributed by BJ, 9-Jun-2019.)
(Proof modification is discouraged.) $)
bj-cmnssmnd $p |- CMnd C_ Mnd $=
( vy vz vx ccmn cv cplusg cfv co wceq cbs wral cmnd df-cmn ssrab2 eqsstri
crab ) DAEZBEZCEZFGZHRQTHIBSJGZKAUAKZCLPLCABMUBCLNO $.
( vy vz vx cv cplusg cfv co wceq cbs wral cmnd ccmn df-cmn ssrab3 ) ADZBD
ZCDZEFZGPORGHBQIFZJASJCKLCABMN $.
$}

$( Commutative monoids are monoids (elemental version). This is a more
Expand All @@ -537291,6 +537290,20 @@ singleton on a couple (with disjoint domain) at a point in the domain
bj-cmnssmndel $p |- ( A e. CMnd -> A e. Mnd ) $=
( ccmn cmnd bj-cmnssmnd sseli ) BCADE $.

${
$d x y z $.
$( Groups are monoids. (Contributed by BJ, 5-Jan-2024.)
(Proof modification is discouraged.) $)
bj-grpssmnd $p |- Grp C_ Mnd $=
( vz vy vx cv cplusg cfv c0g wceq cbs wrex wral cmnd cgrp df-grp ssrab3
co ) ADBDCDZEFPQGFHAQIFZJBRKCLMCABNO $.
$}

$( Groups are monoids (elemental version). Shorter proof of ~ grpmnd .
(Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.) $)
bj-grpssmndel $p |- ( A e. Grp -> A e. Mnd ) $=
( cgrp cmnd bj-grpssmnd sseli ) BCADE $.

$( Abelian groups are groups. (Contributed by BJ, 9-Jun-2019.)
(Proof modification is discouraged.) $)
bj-ablssgrp $p |- Abel C_ Grp $=
Expand Down Expand Up @@ -537450,49 +537463,156 @@ singleton on a couple (with disjoint domain) at a point in the domain

A few basic theorems to start affine, Euclidean, and Cartesian geometry.

The first step is to define real vector spaces, then barycentric coordinates
and convex hulls.

$)


$(
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
Convex hull in real vector spaces
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.
In this section, we introduce real vector spaces.

$)

$( Variant of ~ fvimacnv where membership of ` A ` in the domain is not
needed provided the containing class ` B ` does not contain the empty set.
Note that this antecedent would not be needed with definition ~ df-afv .
(Contributed by BJ, 7-Jan-2024.) $)
bj-fvimacnv0 $p |- ( ( Fun F /\ -. (/) e. B ) ->
( ( F ` A ) e. B <-> A e. ( `' F " B ) ) ) $=
( wfun c0 wcel wn wa cfv ccnv cima cdm wceq eleq1 biimpcd con3rr3 imp ndmfv
wi ex nsyl2 simpr fvimacnv biimpd com3l sylc com3r fvimacnvi adantr impbid
) CDZEBFZGZHACIZBFZACJBKFZUKUMUOUPSZUMUOUKUPUMUOUKUPSZUMUOHZACLFZUOURUSUNEM
ZUTUMUOVAGUOVAULVAUOULUNEBNOPQACRUAUMUOUBUKUTUOUPUKUTUQUKUTHUOUPABCUCUDTUEU
FTUGQUKUPUOSUMUKUPUOABCUHTUIUJ $.

$( Fields are division rings. (Contributed by BJ, 6-Jan-2024.) $)
bj-fielddivring $p |- Field C_ DivRing $=
( cfield cdr ccrg cin df-field inss1 eqsstri ) ABCDBEBCFG $.

$( The field of real numbers is a division ring. (Contributed by BJ,
6-Jan-2024.) $)
bj-rrdrg $p |- RRfld e. DivRing $=
( cfield cdr crefld bj-fielddivring refld sselii ) ABCDEF $.

$( Symbol for the class of real vector spaces. $)
$c RRVec $.

$( Syntax for the class of real vector spaces. $)
crrvec $a class RRVec $.

$( Definition of the class of real vector spaces. (Contributed by BJ,
9-Jun-2019.) $)
df-bj-rrvec $a |- RRVec = { x e. LVec | ( Scalar ` x ) = RRfld } $.
$( Definition of the class of real vector spaces. The previous definition,
` |- RRVec = { x e. LMod | ( Scalar `` x ) = RRfld } ` , can be recovered
using ~ bj-isrvec . The present one is preferred since it does not use
any dummy variable. (Contributed by BJ, 9-Jun-2019.) $)
df-bj-rvec $a |- RRVec = ( LMod i^i ( `' Scalar " { RRfld } ) ) $.

$( The predicate "is a real vector space". (Contributed by BJ,
6-Jan-2024.) $)
bj-isrvec $p |- ( V e. RRVec <-> ( V e. LMod /\ ( Scalar ` V ) = RRfld ) ) $=
( crrvec wcel clmod csca ccnv crefld csn cima wa wceq df-bj-rvec elin2 wfun
cfv c0 c5 cr cbs mto wn cslot bj-evalfun df-sca funeqi mpbir cc0 n0ii eqcom
wb 0re mtbir fveq2 base0 rebase 3eqtr4g elsni bj-fvimacnv0 fvex elsn bitr3i
mp2an anbi2i bitri ) ABCADCZAEFGHZIZCZJVEAEOZGKZJADVGBLMVHVJVEVHVIVFCZVJENZ
PVFCZUAVKVHUJVLQUBZNQUCEVNUDUEUFVMPGKZVOPRKZVPRPKUGRUKUHPRUIULVOPSOGSOPRPGS
UMUNUOUPTPGUQTAVFEURVBVIGAEUSUTVAVCVD $.

$( Real vector spaces are modules (elemental version). (Contributed by BJ,
6-Jan-2024.) $)
bj-rvecmod $p |- ( V e. RRVec -> V e. LMod ) $=
( crrvec wcel clmod csca cfv crefld wceq bj-isrvec simplbi ) ABCADCAEFGHAIJ
$.

$( Real vector spaces are vector spaces. (Contributed by BJ, 9-Jun-2019.) $)
bj-rrvecssvec $p |- RRVec C_ LVec $=
( vx cv csca cfv crefld wceq clvec crrvec df-bj-rrvec ssrab3 ) ABCDEFAGHAIJ
$( Real vector spaces are modules. (Contributed by BJ, 6-Jan-2024.) $)
bj-rvecssmod $p |- RRVec C_ LMod $=
( vx crrvec clmod cv bj-rvecmod ssriv ) ABCADEF $.

$( The field of scalars of a rela vector space is the field of real numbers.
(Contributed by BJ, 6-Jan-2024.) $)
bj-rvecrr $p |- ( V e. RRVec -> ( Scalar ` V ) = RRfld ) $=
( crrvec wcel clmod csca cfv crefld wceq bj-isrvec simprbi ) ABCADCAEFGHAIJ
$.

$( Real vector spaces are vector spaces (elemental version). (Contributed by
BJ, 9-Jun-2019.) $)
bj-rrvecssvecel $p |- ( A e. RRVec -> A e. LVec ) $=
( crrvec clvec bj-rrvecssvec sseli ) BCADE $.
${
bj-isrvecd.scal $e |- ( ph -> ( Scalar ` V ) = K ) $.
$( The predicate "is a real vector space"; deduction form. (Contributed by
BJ, 6-Jan-2024.) $)
bj-isrvecd $p |- ( ph -> ( V e. RRVec <-> ( V e. LMod /\ K = RRfld ) ) ) $=
( crrvec wcel clmod csca cfv crefld wceq bj-isrvec eqeq1d anbi2d syl5bb
wa ) CEFCGFZCHIZJKZPAQBJKZPCLASTQARBJDMNO $.
$}

${
bj-islvecd.scal $e |- ( ph -> K = ( Scalar ` V ) ) $.
$( The predicate "is a vector space"; deduction form. (Contributed by BJ,
6-Jan-2024.) $)
bj-islvecd $p |-
( ph -> ( V e. LVec <-> ( V e. LMod /\ K e. DivRing ) ) ) $=
( clvec wcel clmod csca cfv cdr eqid islvec eqcomd eleq1d anbi2d syl5bb
wa ) CEFCGFZCHIZJFZQARBJFZQSCSKLATUARASBJABSDMNOP $.
$}

$( (The additive groups of) real vector spaces are commutative monoids.
$( Real vector spaces are vector spaces (elemental version). (Contributed by
BJ, 6-Jan-2024.) $)
bj-rvecvec $p |- ( V e. RRVec -> V e. LVec ) $=
( crrvec wcel clvec clmod crefld cdr bj-rvecmod bj-rrdrg a1i csca bj-rvecrr
cfv eqcomd bj-islvecd mpbir2and ) ABCZADCAECFGCZAHRQIJQFAQAKMFALNOP $.

$( Real vector spaces are vector spaces. (Contributed by BJ, 6-Jan-2024.) $)
bj-rvecssvec $p |- RRVec C_ LVec $=
( vx crrvec clvec cv bj-rvecvec ssriv ) ABCADEF $.

${
bj-isclmd.scal $e |- ( ph -> F = ( Scalar ` W ) ) $.
bj-isclmd.base $e |- ( ph -> K = ( Base ` F ) ) $.
$( The predicate "is a subcomplex module"; deduction form. (Contributed by
BJ, 6-Jan-2024.) $)
bj-isclmd $p |- ( ph -> ( W e. CMod <->
( W e. LMod /\ F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) ) $=
( cclm wcel clmod csca cfv ccnfld cbs cress wceq csubrg w3a eqid eqcomd
co isclm fveq2 wa eqtr syl2im mpd oveq2d eqeq12d eleq1d 3anbi23d syl5bb
ex ) DGHDIHZDJKZLUNMKZNTZOZUOLPKZHZQAUMBLCNTZOZCURHZQUNUODUNRUORUAAUQVAUS
VBUMAUNBUPUTABUNESAUOCLNABUNOZUOCOZEACBMKZOZVCVEUOOZVDFBUNMUBVFVGVDVFVGUC
CUOCVEUOUDSULUEUFZUGUHAUOCURVHUIUJUK $.
$}

$( Real vector spaces are subcomplex modules (elemental version).
(Contributed by BJ, 6-Jan-2024.) $)
bj-rveccmod $p |- ( V e. RRVec -> V e. CMod ) $=
( crrvec wcel cclm clmod crefld ccnfld cr cress co wceq csubrg cfv df-refld
bj-rvecmod a1i cdr resubdrg simpli csca bj-rvecrr eqcomd rebase bj-isclmd
cbs mpbir3and ) ABCZADCAECFGHIJKZHGLMCZAOUHUGNPUIUGUIFQCRSPUGFHAUGATMFAUAUB
HFUEMKUGUCPUDUF $.

$( Real vector spaces are subcomplex modules. (Contributed by BJ,
6-Jan-2024.) $)
bj-rvecsscmod $p |- RRVec C_ CMod $=
( vx crrvec cclm cv bj-rveccmod ssriv ) ABCADEF $.

$( Real vector spaces are subcomplex vector spaces. (Contributed by BJ,
6-Jan-2024.) $)
bj-rvecsscvec $p |- RRVec C_ CVec $=
( crrvec cclm clvec ccvs bj-rvecsscmod bj-rvecssvec ssini df-cvs sseqtr4i
cin ) ABCJDABCEFGHI $.

$( Real vector spaces are subcomplex vector spaces (elemental version).
(Contributed by BJ, 6-Jan-2024.) $)
bj-rveccvec $p |- ( V e. RRVec -> V e. CVec ) $=
( crrvec ccvs bj-rvecsscvec sseli ) BCADE $.

$( (The additive groups of) real vector spaces are commutative groups.
(Contributed by BJ, 9-Jun-2019.) $)
bj-rrvecsscmn $p |- RRVec C_ CMnd $=
( crrvec cabl clmod clvec bj-rrvecssvec bj-vecssmod bj-modssabl bj-ablsscmn
ccmn sstri ) ABIACBADCEFJGJHJ $.
bj-rvecssabl $p |- RRVec C_ Abel $=
( crrvec clmod cabl bj-rvecssmod bj-modssabl sstri ) ABCDEF $.

$( (The additive groups of) real vector spaces are commutative monoids
$( (The additive groups of) real vector spaces are commutative groups
(elemental version). (Contributed by BJ, 9-Jun-2019.) $)
bj-rrvecsscmnel $p |- ( A e. RRVec -> A e. CMnd ) $=
( crrvec ccmn bj-rrvecsscmn sseli ) BCADE $.
bj-rvecabl $p |- ( A e. RRVec -> A e. Abel ) $=
( crrvec cabl bj-rvecssabl sseli ) BCADE $.


$(
Expand Down Expand Up @@ -537546,8 +537666,8 @@ Complex numbers (supplements)
bj-bary1.b $e |- ( ph -> B e. CC ) $.
bj-bary1.x $e |- ( ph -> X e. CC ) $.
bj-bary1.neq $e |- ( ph -> A =/= B ) $.
$( A lemma for barycentric coordinates in one dimension. (Contributed by
BJ, 6-Jun-2019.) $)
$( Lemma for ~ bj-bary1 : expression for a barycenter of two points in one
dimension (complex line). (Contributed by BJ, 6-Jun-2019.) $)
bj-bary1lem $p |- ( ph -> X = ( ( ( ( B - X ) / ( B - A ) ) x. A ) +
( ( ( X - A ) / ( B - A ) ) x. B ) ) ) $=
( cmin co cmul cdiv caddc cc0 mulcld subcld oveq1d eqtrd subdird oveq12d
Expand All @@ -537563,9 +537683,9 @@ Complex numbers (supplements)

bj-bary1.s $e |- ( ph -> S e. CC ) $.
bj-bary1.t $e |- ( ph -> T e. CC ) $.
$( Existence and uniqueness (and actual computation) of barycentric
coordinates in dimension 1 (complex line). (Contributed by BJ,
6-Jun-2019.) $)
$( Lemma for bj-bary1: computation of one of the two barycentric
coordinates of a barycenter of two points in one dimension (complex
line). (Contributed by BJ, 6-Jun-2019.) $)
bj-bary1lem1 $p |- ( ph ->
( ( X = ( ( S x. A ) + ( T x. B ) ) /\ ( S + T ) = 1 ) ->
T = ( ( X - A ) / ( B - A ) ) ) ) $=
Expand All @@ -537582,7 +537702,9 @@ Complex numbers (supplements)
XIWEEMNZWIPZWKAWFXJWIAEWELXHVGVJAXKWKAWEEWIXHLAFBIGVDACBHGABCJVKVLVMVNVOV
PVQ $.

$( Barycentric coordinates in one dimension. (Contributed by BJ,
$( Barycentric coordinates in one dimension (complex line). In the
statement, ` X ` is the barycenter of the two points ` A , B ` with
respective normalized coefficients ` S , T ` . (Contributed by BJ,
6-Jun-2019.) $)
bj-bary1 $p |- ( ph ->
( ( X = ( ( S x. A ) + ( T x. B ) ) /\ ( S + T ) = 1 ) <->
Expand Down

0 comments on commit e1005b4

Please sign in to comment.