diff --git a/set.mm b/set.mm index 85af0fec1a..ffa9094781 100644 --- a/set.mm +++ b/set.mm @@ -537807,111 +537807,80 @@ Real and complex numbers (cont.) $} $( Ordered triple membership in a triple cross product. (Contributed by - Scott Fenton, 21-Aug-2024.) $) - ot2elxp $p |- ( <. <. A , B >. , C >. e. ( ( D X. E ) X. F ) <-> + Scott Fenton, 31-Jan-2025.) $) + otelxp $p |- ( <. A , B , C >. e. ( ( D X. E ) X. F ) <-> ( A e. D /\ B e. E /\ C e. F ) ) $= - ( cop cxp wcel wa w3a opelxp anbi1i df-3an 3bitr4i ) ABGZDEHZIZCFIZJADIZBEI - ZJZSJPCGQFHITUASKRUBSABDELMPCQFLTUASNO $. - - ${ - ot21st.1 $e |- A e. _V $. - ot21st.2 $e |- B e. _V $. - ot21st.3 $e |- C e. _V $. - $( Extract the first member of an ordered triple. Deduction version. - (Contributed by Scott Fenton, 21-Aug-2024.) $) - ot21std $p |- ( X = <. <. A , B >. , C >. -> ( 1st ` ( 1st ` X ) ) = A ) $= - ( cop wceq c1st cfv opex op1std fveq2d op1st eqtrdi ) DABHZCHIZDJKZJKQJKA - RSQJQCDABLGMNABEFOP $. - - $( Extract the second member of an ordered triple. Deduction version. - (Contributed by Scott Fenton, 21-Aug-2024.) $) - ot22ndd $p |- ( X = <. <. A , B >. , C >. -> ( 2nd ` ( 1st ` X ) ) = B ) $= - ( cop wceq c1st cfv c2nd opex op1std fveq2d op2nd eqtrdi ) DABHZCHIZDJKZL - KRLKBSTRLRCDABMGNOABEFPQ $. - $} + ( cop cxp wcel wa cotp w3a opelxp anbi1i bitri df-ot eleq1i df-3an 3bitr4i + ) ABGZCGZDEHZFHZIZADIZBEIZJZCFIZJZABCKZUCIUEUFUHLUDTUBIZUHJUITCUBFMUKUGUHAB + DEMNOUJUAUCABCPQUEUFUHRS $. ${ otthne.1 $e |- A e. _V $. otthne.2 $e |- B e. _V $. otthne.3 $e |- C e. _V $. $( Contrapositive of the ordered triple theorem. (Contributed by Scott - Fenton, 21-Aug-2024.) $) - otthne $p |- ( <. <. A , B >. , C >. =/= <. <. D , E >. , F >. <-> + Fenton, 31-Jan-2025.) $) + otthne $p |- ( <. A , B , C >. =/= <. D , E , F >. <-> ( A =/= D \/ B =/= E \/ C =/= F ) ) $= - ( cop wne wo w3o opthne orbi1i opex df-3or 3bitr4i ) ABJZDEJZKZCFKZLADKZB - EKZLZUBLSCJTFJKUCUDUBMUAUEUBABDEGHNOSCTFABPINUCUDUBQR $. + ( cotp wceq wn w3o wne w3a otth notbii 3ianor bitri df-ne 3orbi123i + 3bitr4i ) ABCJZDEFJZKZLZADKZLZBEKZLZCFKZLZMZUCUDNADNZBENZCFNZMUFUGUIUKOZL + UMUEUQABDECFGHIPQUGUIUKRSUCUDTUNUHUOUJUPULADTBETCFTUAUB $. $} ${ - $d A x y z p $. $d B x y z p $. $d C x y z p $. $d D x y z p $. - $( Membership in a triple cross product. (Contributed by Scott Fenton, - 21-Aug-2024.) $) - elxpxp $p |- ( A e. ( ( B X. C ) X. D ) <-> - E. x e. B E. y e. C E. z e. D A = <. <. x , y >. , z >. ) $= - ( vp cxp wcel cv cop wceq wrex elxp2 opeq1 eqeq2d rexbidv rexxp bitri ) D - EFIZGIJDHKZCKZLZMZCGNZHUANDAKBKLZUCLZMZCGNZBFNAENHCDUAGOUFUJHABEFUBUGMZUE - UICGUKUDUHDUBUGUCPQRST $. + $d A x y z $. $d B x y z $. $d C x y z $. $d D x y z $. + $( Version of ~ elrel for triple cross products. (Contributed by Scott + Fenton, 1-Feb-2025.) $) + el2xpss $p |- ( ( R C_ ( ( B X. C ) X. D ) /\ A e. R ) -> + E. x E. y E. z A = <. x , y , z >. ) $= + ( cxp wss wcel wa cv cotp wceq wex wrex rexex reximi syl ssel2 el2xptp + sylbi ) HEFIGIZJDHKLDUDKZDAMBMCMNOZCPZBPZAPZHUDDUAUEUFCGQZBFQZAEQZUIABCDE + FGUBULUHAEQUIUKUHAEUKUGBFQUHUJUGBFUFCGRSUGBFRTSUHAERTUCT $. $} ${ - $d A x y z $. $d B x y z $. $d C x y z $. $d D x y z $. - $( Version of ~ elrel for triple cross products. (Contributed by Scott - Fenton, 21-Aug-2024.) $) - elxpxpss $p |- ( ( R C_ ( ( B X. C ) X. D ) /\ A e. R ) -> - E. x E. y E. z A = <. <. x , y >. , z >. ) $= - ( cxp wss wcel wa cv cop wceq wex wrex rexex reximi syl ssel2 elxpxp - sylbi ) HEFIGIZJDHKLDUDKZDAMBMNCMNOZCPZBPZAPZHUDDUAUEUFCGQZBFQZAEQZUIABCD - EFGUBULUHAEQUIUKUHAEUKUGBFQUHUJUGBFUFCGRSUGBFRTSUHAERTUCT $. - $} - - ${ - $d A w $. $d A x $. $d A y $. $d A z $. $d B w $. $d B x $. $d B y $. - $d B z $. $d C w $. $d C x $. $d C y $. $d C z $. $d w x $. $d w y $. - $d w z $. $d x y $. $d x z $. $d y z $. - ral3xpf.1 $e |- F/ y ph $. - ral3xpf.2 $e |- F/ z ph $. - ral3xpf.3 $e |- F/ w ph $. - ral3xpf.4 $e |- F/ x ps $. - ral3xpf.5 $e |- ( x = <. <. y , z >. , w >. -> ( ph <-> ps ) ) $. + $d A w x y z $. $d B w x y z $. $d C w x y z $. + ralxp3f.1 $e |- F/ y ph $. + ralxp3f.2 $e |- F/ z ph $. + ralxp3f.3 $e |- F/ w ph $. + ralxp3f.4 $e |- F/ x ps $. + ralxp3f.5 $e |- ( x = <. y , z , w >. -> ( ph <-> ps ) ) $. $( Restricted for all over a triple cross product. (Contributed by Scott Fenton, 22-Aug-2024.) $) ralxp3f $p |- ( A. x e. ( ( A X. B ) X. C ) ph <-> A. y e. A A. z e. B A. w e. C ps ) $= - ( wral cv wi wal wrex ralbii cxp wcel cop wceq df-ral r19.23 bitri elxpxp - imbi1i 3bitr4ri albii ralcom4 opex ceqsal bitr3i 3bitri ) ACGHUAIUAZOCPZU - QUBZAQZCRURDPEPUCZFPZUCZUDZAQZFIOZEHOZDGOZCRZBFIOZEHOZDGOZACUQUEUTVHCVDFI - SZEHSZAQZDGOVNDGSZAQVHUTVNADGJUFVGVODGVGVMAQZEHOVOVFVQEHVDAFILUFTVMAEHKUF - UGTUSVPADEFURGHIUHUIUJUKVIVGCRZDGOVLVGDCGULVRVKDGVRVFCRZEHOVKVFECHULVSVJE - HVSVECRZFIOVJVEFCIULVTBFIABCVCMVAVBUMNUNTUOTUOTUOUP $. + ( wral cv wi wal wrex ralbii wcel cotp df-ral el2xptp imbi1i r19.23 bitri + cxp wceq bitr2i albii ralcom4 otex ceqsal bitr3i 3bitri ) ACGHUHIUHZOCPZU + QUAZAQZCRURDPZEPZFPZUBZUIZAQZFIOZEHOZDGOZCRZBFIOZEHOZDGOZACUQUCUTVICUTVEF + ISZEHSZDGSZAQZVIUSVPADEFURGHIUDUEVIVOAQZDGOVQVHVRDGVHVNAQZEHOVRVGVSEHVEAF + ILUFTVNAEHKUFUGTVOADGJUFUJUGUKVJVHCRZDGOVMVHDCGULVTVLDGVTVGCRZEHOVLVGECHU + LWAVKEHWAVFCRZFIOVKVFFCIULWBBFIABCVDMVAVBVCUMNUNTUOTUOTUOUP $. $} ${ - $d A p $. $d A x $. $d A y $. $d A z $. $d B p $. $d B x $. $d B y $. - $d B z $. $d C p $. $d C x $. $d C y $. $d C z $. $d p ps $. - $d p x $. $d p y $. $d p z $. $d ph x $. $d ph y $. $d ph z $. - $d x y $. $d x z $. $d y z $. - ralxp3.1 $e |- ( p = <. <. x , y >. , z >. -> ( ph <-> ps ) ) $. - $( Restricted for-all over a triple cross product. (Contributed by Scott - Fenton, 21-Aug-2024.) $) - ralxp3 $p |- ( A. p e. ( ( A X. B ) X. C ) ph <-> - A. x e. A A. y e. B A. z e. C ps ) $= - ( nfv ralxp3f ) ABICDEFGHACKADKAEKBIKJL $. + $d A w x y z $. $d B w x y z $. $d C w x y z $. $d ph w y z $. + $d ps x $. + ralxp3.1 $e |- ( x = <. y , z , w >. -> ( ph <-> ps ) ) $. + $( Restricted for all over a triple cross product. (Contributed by Scott + Fenton, 2-Feb-2025.) $) + ralxp3 $p |- ( A. x e. ( ( A X. B ) X. C ) ph <-> + A. y e. A A. z e. B A. w e. C ps ) $= + ( nfv ralxp3f ) ABCDEFGHIADKAEKAFKBCKJL $. $} $( Equality theorem for substitution of a class for an ordered triple. (Contributed by Scott Fenton, 22-Aug-2024.) $) - sbcoteq1a $p |- ( A = <. <. x , y >. , z >. -> + sbcoteq1a $p |- ( A = <. x , y , z >. -> ( [. ( 1st ` ( 1st ` A ) ) / x ]. [. ( 2nd ` ( 1st ` A ) ) / y ]. [. ( 2nd ` A ) / z ]. ph <-> ph ) ) $= - ( cv cop wceq c2nd cfv wsbc c1st opex vex op2ndd eqcomd sbceq1a syl ot22ndd - wb ot21std 3bitrrd ) EBFZCFZGZDFZGHZAADEIJZKZUICELJZIJZKZULBUJLJZKZUGUFUHHA - UITUGUHUFUEUFEUCUDMDNZOPADUHQRUGUDUKHUIULTUGUKUDUCUDUFEBNZCNZUOSPUICUKQRUGU - CUMHULUNTUGUMUCUCUDUFEUPUQUOUAPULBUMQRUB $. + ( cv wceq c2nd cfv wsbc c1st cvv eqtr2di sbceq1a syl 2fveq3 wcel vex mp3an + wb cotp fveq2 ot3rdg elv ot2ndg ot1stg 3bitrrd ) EBFZCFZDFZUAZGZAADEHIZJZUN + CEKIZHIZJZUQBUOKIZJZULUJUMGAUNTULUMUKHIZUJEUKHUBUTUJGDUHUIUJLUCUDMADUMNOULU + IUPGUNUQTULUPUKKIZHIZUIEUKHKPUHLQZUILQZUJLQZVBUIGBRZCRZDRZUHUIUJLLLUESMUNCU + PNOULUHURGUQUSTULURVAKIZUHEUKKKPVCVDVEVIUHGVFVGVHUHUIUJLLLUFSMUQBURNOUG $. ${ - $d A w $. $d A x $. $d A y $. $d A z $. $d B w $. $d B x $. $d B y $. - $d B z $. $d C w $. $d C x $. $d C y $. $d C z $. $d ph x $. - $d w x $. $d w y $. $d w z $. $d x y $. $d x z $. $d y z $. + $d A w x y z $. $d B w x y z $. $d C w x y z $. $d ph x $. $( Restricted for-all over a triple cross product with explicit substitution. (Contributed by Scott Fenton, 22-Aug-2024.) $) ralxp3es $p |- ( A. x e. ( ( A X. B ) X. C ) @@ -539868,8 +539837,8 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $= $d u w $. $d u x $. $d u y $. $d u z $. $d w x $. $d w y $. $d w z $. frpoins3xp3g.1 $e |- ( ( x e. A /\ y e. B /\ z e. C ) -> ( A. w A. t A. u - ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , - <. <. x , y >. , z >. ) -> th ) -> ph ) ) $. + ( <. w , t , u >. e. Pred ( R , ( ( A X. B ) X. C ) , + <. x , y , z >. ) -> th ) -> ph ) ) $. frpoins3xp3g.2 $e |- ( x = w -> ( ph <-> ps ) ) $. frpoins3xp3g.3 $e |- ( y = t -> ( ps <-> ch ) ) $. frpoins3xp3g.4 $e |- ( z = u -> ( ch <-> th ) ) $. @@ -539883,34 +539852,34 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $= /\ R Se ( ( A X. B ) X. C ) ) /\ ( X e. A /\ Y e. B /\ Z e. C ) ) -> ze ) $= ( vp vq cxp wfr wpo wse w3a wral wcel cv c2nd cfv wsbc c1st cpred sbcbidv - weq cbvsbcvw sbcbii bitri ralbii cop wceq wrex wi elxpxp nfv nfsbc1v nfim - nfcv nfsbcw wa wal impexp cin elin wss predss sseqin2 eleq2i bitr3i albii - mpbi imbi1i r3al sbcoteq1a imbi12d ralxp3f ot2elxp 2albii 3bitr4ri df-ral - eleq1 biimtrid predeq3 raleqdv syl5ibrcom 3expia rexlimd ex rexlimi sylbi - 2fveq3 fveq2 sbceq1d sbceqbid frpoins2g ralxp3es sylib rspc3v mpan9 ) NOU - JPUJZQUKXSQULXSQUMUNZAJPUOIOUOHNUOZRNUPSOUPTPUPUNGXTAJUHUQZURUSZUTZIYBVAU - SZURUSZUTZHYEVAUSZUTZUHXSUOYAYIAJUIUQZURUSZUTZIYJVAUSZURUSZUTZHYMVAUSZUTZ - UHUIXSQYQUIXSQYBVBZUODLYKUTZMYNUTZKYPUTZUIYRUOZYBXSUPZYIYQUUAUIYRYQBJYKUT - ZIYNUTZKYPUTUUAYOUUEHKYPHKVDZYLUUDIYNUUFABJYKUBVCVCVEUUEYTKYPUUECJYKUTZMY - NUTYTUUDUUGIMYNIMVDBCJYKUCVCVEUUGYSMYNCDJLYKUDVEVFVGVFVGVHUUCYBHUQZIUQZVI - JUQZVIZVJZJPVKZIOVKZHNVKUUBYIVLZHIJYBNOPVMUUNUUOHNUUBYIHUUBHVNYGHYHVOVPUU - HNUPZUUMUUOIOUUPIVNUUBYIIUUBIVNYGIHYHIYHVQYDIYFVOVRVPUUPUUIOUPZUUMUUOVLUU - PUUQVSZUULUUOJPUURJVNUUBYIJUUBJVNYGJHYHJYHVQYDJIYFJYFVQAJYCVOVRVRVPUUPUUQ - UUJPUPZUULUUOVLUUPUUQUUSUNZUUOUULUUAUIXSQUUKVBZUOZAVLUVBKUQZMUQZVILUQZVIZ - UVAUPZDVLZLVTZMVTKVTZUUTAYJXSUPZYJUVAUPZUUAVLZVLZUIVTZUVMUIVTUVJUVBUVNUVM - UIUVNUVKUVLVSZUUAVLUVMUVKUVLUUAWAUVPUVLUUAUVPYJXSUVAWBZUPUVLYJXSUVAWCUVQU - VAYJUVAXSWDUVQUVAVJXSQUUKWEUVAXSWFWJZWGWHWKWHWIUVJUVMUIXSUOZUVOUVHLPUOMOU - OKNUOUVCNUPUVDOUPUVEPUPUNZUVHVLZLVTZMVTKVTUVSUVJUVHKMLNOPWLUVMUVHUIKMLNOP - UVLUUAKUVLKVNYTKYPVOVPUVLUUAMUVLMVNYTMKYPMYPVQYSMYNVOVRVPUVLUUALUVLLVNYTL - KYPLYPVQYSLMYNLYNVQDLYKVOVRVRVPUVHUIVNYJUVFVJUVLUVGUUADYJUVFUVAWTDKMLYJWM - WNWOUVIUWBKMUVHUWALUVHUVFXSUPZUVHVLZUWAUVHUWCUVGVSZDVLUWDUWEUVGDUWEUVFUVQ - UPUVGUVFXSUVAWCUVQUVAUVFUVRWGWHWKUWCUVGDWAWHUWCUVTUVHUVCUVDUVENOPWPWKVGWI - WQWRUVMUIXSWSVGUUAUIUVAWSWRUAXAUULUUBUVBYIAUULUUAUIYRUVAXSQYBUUKXBXCAHIJY - BWMWNXDXEXFXGXFXHXIXAUHUIVDZYGYOHYHYPYBYJVAVAXJUWFYDYLIYFYNYBYJURVAXJUWFA - JYCYKYBYJURXKXLXMXMXNAUHHIJNOPXOXPAGEFHIJRSTNOPUEUFUGXQXR $. + weq cbvsbcvw sbcbii bitri ralbii cotp wceq wrex el2xptp nfsbc1v nfim nfcv + wi nfv nfsbcw wal cin wss predss sseqin2 mpbi eleq2i bicomi imbi1i impexp + wa elin albii r3al sbcoteq1a imbi12d ralxp3f otelxp anbi1i 3bitr3i 3albii + eleq1 3bitr4ri df-ral biimtrid predeq3 raleqdv syl5ibrcom rexlimd rexlimi + 3expia sylbi 2fveq3 fveq2 sbceq1d sbceqbid frpoins2g ralxp3es sylib mpan9 + ex rspc3v ) NOUJPUJZQUKYAQULYAQUMUNZAJPUOIOUOHNUOZRNUPSOUPTPUPUNGYBAJUHUQ + ZURUSZUTZIYDVAUSZURUSZUTZHYGVAUSZUTZUHYAUOYCYKAJUIUQZURUSZUTZIYLVAUSZURUS + ZUTZHYOVAUSZUTZUHUIYAQYSUIYAQYDVBZUODLYMUTZMYPUTZKYRUTZUIYTUOZYDYAUPZYKYS + UUCUIYTYSBJYMUTZIYPUTZKYRUTUUCYQUUGHKYRHKVDZYNUUFIYPUUHABJYMUBVCVCVEUUGUU + BKYRUUGCJYMUTZMYPUTUUBUUFUUIIMYPIMVDBCJYMUCVCVEUUIUUAMYPCDJLYMUDVEVFVGVFV + GVHUUEYDHUQZIUQZJUQZVIZVJZJPVKZIOVKZHNVKUUDYKVPZHIJYDNOPVLUUPUUQHNUUDYKHU + UDHVQYIHYJVMVNUUJNUPZUUOUUQIOUURIVQUUDYKIUUDIVQYIIHYJIYJVOYFIYHVMVRVNUURU + UKOUPZUUOUUQVPUURUUSWIZUUNUUQJPUUTJVQUUDYKJUUDJVQYIJHYJJYJVOYFJIYHJYHVOAJ + YEVMVRVRVNUURUUSUULPUPZUUNUUQVPUURUUSUVAUNZUUQUUNUUCUIYAQUUMVBZUOZAVPUVDK + UQZMUQZLUQZVIZUVCUPZDVPZLVSMVSKVSZUVBAYLYAUPZYLUVCUPZUUCVPZVPZUIVSZUVNUIV + SZUVKUVDUVQUVPUVNUVOUIUVNUVLUVMWIZUUCVPUVOUVMUVRUUCUVMYLYAUVCVTZUPZUVRUVT + UVMUVSUVCYLUVCYAWAUVSUVCVJYAQUUMWBUVCYAWCWDZWEWFYLYAUVCWJVGWGUVLUVMUUCWHV + GWKWFUVKUVNUIYAUOZUVPUVJLPUOMOUOKNUOUVENUPUVFOUPUVGPUPUNZUVJVPZLVSMVSKVSU + WBUVKUVJKMLNOPWLUVNUVJUIKMLNOPUVMUUCKUVMKVQUUBKYRVMVNUVMUUCMUVMMVQUUBMKYR + MYRVOUUAMYPVMVRVNUVMUUCLUVMLVQUUBLKYRLYRVOUUALMYPLYPVODLYMVMVRVRVNUVJUIVQ + YLUVHVJUVMUVIUUCDYLUVHUVCWTDKMLYLWMWNWOUVJUWDKMLUVJUWCUVIWIZDVPUWDUVIUWED + UVHUVSUPUVHYAUPZUVIWIUVIUWEUVHYAUVCWJUVSUVCUVHUWAWEUWFUWCUVIUVEUVFUVGNOPW + PWQWRWGUWCUVIDWHVGWSXAUVNUIYAXBVGUUCUIUVCXBXAUAXCUUNUUDUVDYKAUUNUUCUIYTUV + CYAQYDUUMXDXEAHIJYDWMWNXFXIXGXSXGXHXJXCUHUIVDZYIYQHYJYRYDYLVAVAXKUWGYFYNI + YHYPYDYLURVAXKUWGAJYEYMYDYLURXLXMXNXNXOAUHHIJNOPXPXQAGEFHIJRSTNOPUEUFUGXT + XR $. $} - $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Ordering Cross Products, Part 2 @@ -540230,128 +540199,107 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $= $d d x $. $d d y $. $d e x $. $d e y $. $d f x $. $d f y $. $d R x $. $d R y $. $d S x $. $d S y $. $d T x $. $d T y $. $d x y $. + $( Lemma for triple ordering. Calculate the value of the relationship. (Contributed by Scott Fenton, 21-Aug-2024.) $) - xpord3lem $p |- ( <. <. a , b >. , c >. U <. <. d , e >. , f >. <-> + xpord3lem $p |- ( <. a , b , c >. U <. d , e , f >. <-> ( ( a e. A /\ b e. B /\ c e. C ) /\ ( d e. A /\ e e. B /\ f e. C ) /\ ( ( ( a R d \/ a = d ) /\ ( b S e \/ b = e ) /\ ( c T f \/ c = f ) ) /\ ( a =/= d \/ b =/= e \/ c =/= f ) ) ) ) $= - ( wbr wcel wo w3a cv cop cxp weq wne wa w3o c1st cfv wceq c2nd opex vex - ot21std breq1d eqeq1d orbi12d ot22ndd op2ndd 3anbi123d anbi12d 3anbi13d - eleq1 neeq1 breq2d eqeq2d 3anbi23d brab ot2elxp otthne anbi2i 3anbi123i - neeq2 bitri ) LUAZMUAZUBZNUAZUBZOUAZJUAZUBZKUAZUBZIQVSCDUCEUCZRZWDWERZV - OVTFQZLOUDZSZVPWAGQZMJUDZSZVRWCHQZNKUDZSZTZVSWDUEZUFZTZVOCRVPDRVRERTZVT - CRWADRWCERTZWQVOVTUEVPWAUEVRWCUEUGZUFZTAUAZWERZBUAZWERZXEUHUIZUHUIZXGUH - UIZUHUIZFQZXJXLUJZSZXIUKUIZXKUKUIZGQZXPXQUJZSZXEUKUIZXGUKUIZHQZYAYBUJZS - ZTZXEXGUEZUFZTWFXHVOXLFQZVOXLUJZSZVPXQGQZVPXQUJZSZVRYBHQZVRYBUJZSZTZVSX - GUEZUFZTWTABVSWDIVQVRULWBWCULXEVSUJZXFWFYHYTXHXEVSWEVCUUAYFYRYGYSUUAXOY - KXTYNYEYQUUAXMYIXNYJUUAXJVOXLFVOVPVRXELUMZMUMZNUMZUNZUOUUAXJVOXLUUEUPUQ - UUAXRYLXSYMUUAXPVPXQGVOVPVRXEUUBUUCUUDURZUOUUAXPVPXQUUFUPUQUUAYCYOYDYPU - UAYAVRYBHVQVRXEVOVPULUUDUSZUOUUAYAVRYBUUGUPUQUTXEVSXGVDVAVBXGWDUJZXHWGY - TWSWFXGWDWEVCUUHYRWQYSWRUUHYKWJYNWMYQWPUUHYIWHYJWIUUHXLVTVOFVTWAWCXGOUM - ZJUMZKUMZUNZVEUUHXLVTVOUULVFUQUUHYLWKYMWLUUHXQWAVPGVTWAWCXGUUIUUJUUKURZ - VEUUHXQWAVPUUMVFUQUUHYOWNYPWOUUHYBWCVRHWBWCXGVTWAULUUKUSZVEUUHYBWCVRUUN - VFUQUTXGWDVSVMVAVGPVHWFXAWGXBWSXDVOVPVRCDEVIVTWAWCCDEVIWRXCWQVOVPVRVTWA - WCUUBUUCUUDVJVKVLVN $. - $} - - ${ - $d A a $. $d a b $. $d A b $. $d a c $. $d A c $. $d a d $. - $d A d $. $d a e $. $d A e $. $d a f $. $d A f $. $d a g $. - $d A g $. $d a h $. $d A h $. $d a i $. $d A i $. $d a j $. - $d A j $. $d a k $. $d A k $. $d a l $. $d A l $. $d a ph $. - $d A x $. $d A y $. $d B a $. $d B b $. $d b c $. $d B c $. - $d b d $. $d B d $. $d b e $. $d B e $. $d b f $. $d B f $. - $d b g $. $d B g $. $d b h $. $d B h $. $d b i $. $d B i $. - $d b j $. $d B j $. $d b k $. $d B k $. $d b l $. $d B l $. - $d b ph $. $d B x $. $d B y $. $d C a $. $d C b $. $d C c $. - $d c d $. $d C d $. $d c e $. $d C e $. $d c f $. $d C f $. - $d c g $. $d C g $. $d c h $. $d C h $. $d c i $. $d C i $. - $d c j $. $d C j $. $d c k $. $d C k $. $d c l $. $d C l $. - $d c ph $. $d C x $. $d C y $. $d d e $. $d d f $. $d d g $. - $d d h $. $d d i $. $d d j $. $d d k $. $d d l $. $d d ph $. - $d d x $. $d d y $. $d e f $. $d e g $. $d e h $. $d e i $. - $d e j $. $d e k $. $d e l $. $d e ph $. $d e x $. $d e y $. - $d f g $. $d f h $. $d f i $. $d f j $. $d f k $. $d f l $. - $d f ph $. $d f x $. $d f y $. $d g h $. $d g i $. $d g j $. - $d g k $. $d g l $. $d g ph $. $d g x $. $d g y $. $d h i $. - $d h j $. $d h k $. $d h l $. $d h ph $. $d h x $. $d h y $. - $d i j $. $d i k $. $d i l $. $d i ph $. $d i x $. $d i y $. - $d j k $. $d j l $. $d j ph $. $d j x $. $d j y $. $d k l $. - $d k ph $. $d k x $. $d k y $. $d l ph $. $d l x $. $d l y $. - $d R x $. $d R y $. $d S x $. $d S y $. $d T x $. $d T y $. - $d U a $. $d U b $. $d U c $. $d U d $. $d U e $. $d U f $. - $d U g $. $d U h $. $d U i $. $d U j $. $d U k $. $d U l $. - $d x y $. + ( wcel c1st cfv cvv cv cotp wbr cxp weq wo w3a wne wceq c2nd otex eleq1 + wa w3o 2fveq3 vex ot1stg mp3an eqtrdi breq1d eqeq1d ot2ndg fveq2 ot3rdg + orbi12d elv 3anbi123d neeq1 anbi12d 3anbi13d breq2d neeq2 3anbi23d brab + eqeq2d otelxp otthne anbi2i 3anbi123i bitri ) LUAZMUAZNUAZUBZOUAZJUAZKU + AZUBZIUCWDCDUDEUDZQZWHWIQZWAWEFUCZLOUEZUFZWBWFGUCZMJUEZUFZWCWGHUCZNKUEZ + UFZUGZWDWHUHZUMZUGZWACQWBDQWCEQUGZWECQWFDQWGEQUGZXAWAWEUHWBWFUHWCWGUHUN + ZUMZUGAUAZWIQZBUAZWIQZXIRSZRSZXKRSZRSZFUCZXNXPUIZUFZXMUJSZXOUJSZGUCZXTY + AUIZUFZXIUJSZXKUJSZHUCZYEYFUIZUFZUGZXIXKUHZUMZUGWJXLWAXPFUCZWAXPUIZUFZW + BYAGUCZWBYAUIZUFZWCYFHUCZWCYFUIZUFZUGZWDXKUHZUMZUGXDABWDWHIWAWBWCUKWEWF + WGUKXIWDUIZXJWJYLUUDXLXIWDWIULUUEYJUUBYKUUCUUEXSYOYDYRYIUUAUUEXQYMXRYNU + UEXNWAXPFUUEXNWDRSZRSZWAXIWDRRUOWATQZWBTQZWCTQZUUGWAUILUPZMUPZNUPZWAWBW + CTTTUQURUSZUTUUEXNWAXPUUNVAVEUUEYBYPYCYQUUEXTWBYAGUUEXTUUFUJSZWBXIWDUJR + UOUUHUUIUUJUUOWBUIUUKUULUUMWAWBWCTTTVBURUSZUTUUEXTWBYAUUPVAVEUUEYGYSYHY + TUUEYEWCYFHUUEYEWDUJSZWCXIWDUJVCUUQWCUINWAWBWCTVDVFUSZUTUUEYEWCYFUURVAV + EVGXIWDXKVHVIVJXKWHUIZXLWKUUDXCWJXKWHWIULUUSUUBXAUUCXBUUSYOWNYRWQUUAWTU + USYMWLYNWMUUSXPWEWAFUUSXPWHRSZRSZWEXKWHRRUOWETQZWFTQZWGTQZUVAWEUIOUPZJU + PZKUPZWEWFWGTTTUQURUSZVKUUSXPWEWAUVHVOVEUUSYPWOYQWPUUSYAWFWBGUUSYAUUTUJ + SZWFXKWHUJRUOUVBUVCUVDUVIWFUIUVEUVFUVGWEWFWGTTTVBURUSZVKUUSYAWFWBUVJVOV + EUUSYSWRYTWSUUSYFWGWCHUUSYFWHUJSZWGXKWHUJVCUVKWGUIKWEWFWGTVDVFUSZVKUUSY + FWGWCUVLVOVEVGXKWHWDVLVIVMPVNWJXEWKXFXCXHWAWBWCCDEVPWEWFWGCDEVPXBXGXAWA + WBWCWEWFWGUUKUULUUMVQVRVSVT $. + $} + + ${ + $d A a b c d e f g h i p q r x y $. $d B a b c d e f g h i p q r x y $. + $d C a b c d e f g h i p q r x y $. $d R a b c d e f g h i p q r x y $. + $d S a b c d e f g h i p q r x y $. $d T a b c d e f g h i p q r x y $. + $d U a b c d e f g h i p q r $. $d ph a b c d e f g h i p q r $. poxp3.1 $e |- ( ph -> R Po A ) $. poxp3.2 $e |- ( ph -> S Po B ) $. poxp3.3 $e |- ( ph -> T Po C ) $. $( Triple cross product partial ordering. (Contributed by Scott Fenton, 21-Aug-2024.) $) poxp3 $p |- ( ph -> U Po ( ( A X. B ) X. C ) ) $= - ( vd ve wbr wrex wa wo va vb vc vf vg vh vi vj vk vl cxp cv wcel wn cop - elxpxp wi w3a weq wne w3o neirr 3pm3.2ni intnan simp3 mto breq12 anidms - wceq wb xpord3lem bitrdi mtbiri rexlimivw a1i rexlimivv sylbi 3anbi123i - adantl 3reeanv rexbii 2rexbii bitr4i simprl1 simprr2 wpo adantr simpl11 - bitri simpr11 simpr21 potr syl13anc orc syl6 expd breq1 syl6bir simp3l1 - ad2antrl mpjaod breq2 equequ2 orbi12d syl5ibcom simpl12 simpr12 simpr22 - ad2antll simp3l2 simpl13 simpr13 simpr23 simp3l3 3jca simpr3r 3orbi123i - df-ne 3ianor sylib con2bii equequ1 equcom ordir sylanbrc po2nr syl12anc - imp orcnd orbi2i 3anim123d biimtrrid mt3d jca 3adant3 3adant1 rexlimdvw - ex a1d rexlimdvv anbi12d 3adant2 imbi12d syl5ibrcom biimtrid ispod ) AU - AUBUCDEUKFUKZJUAULZUUGUMZUUHUUHJQZUNZAUUIUUHOULZPULZUOUDULZUOZVIZUDFRZP - ERZODRZUUKOPUDUUHDEFUPZUUQUUKOPDEUUQUUKUQUULDUMZUUMEUMZSUUPUUKUDFUUPUUJ - UVAUVBUUNFUMZURZUVDUULUULGQOOUSTUUMUUMHQPPUSTUUNUUNIQUDUDUSTURZUULUULUT - ZUUMUUMUTZUUNUUNUTZVAZSZURZUVKUVJUVIUVEUVFUVGUVHUULVBUUMVBUUNVBVCVDUVDU - VDUVJVEVFUUPUUJUUOUUOJQZUVKUUPUUJUVLVJUUHUUOUUHUUOJVGVHBCDEFGHIJPUDOPUD - OKVKVLVMVNVOVPVQVSAUUIUBULZUUGUMZUCULZUUGUMZURZUUHUVMJQZUVMUVOJQZSZUUHU - VOJQZUQZUVQUUPUVMUEULZUFULZUOUGULZUOZVIZUVOUHULZUIULZUOUJULZUOZVIZURZUJ - FRZUGFRUDFRZUIERZUFERPERZUHDRZUEDRODRZAUWBUVQUUSUWGUGFRZUFERZUEDRZUWLUJ - FRZUIERZUHDRZURZUWSUUIUUSUVNUXBUVPUXEUUTUEUFUGUVMDEFUPUHUIUJUVODEFUPVRU - WSUURUXAUXDURZUHDRZUEDRODRUXFUWRUXHOUEDDUWQUXGUHDUWQUUQUWTUXCURZUIERZUF - ERPERUXGUWPUXJPUFEEUWOUXIUIEUUPUWGUWLUDUGUJFFFVTWAWBUUQUWTUXCPUFUIEEEVT - WIWAWBUURUXAUXDOUEUHDDDVTWIWCAUWRUWBOUEDDAUWRUWBUQUVAUWCDUMZSAUWQUWBUHD - AUWPUWBPUFEEAUWPUWBUQUVBUWDEUMZSAUWOUWBUIEAUWNUWBUDUGFFAUWNUWBUQUVCUWEF - UMZSAUWMUWBUJFAUWBUWMUVDUXKUXLUXMURZUULUWCGQZOUEUSZTZUUMUWDHQZPUFUSZTZU - UNUWEIQZUDUGUSZTZURUULUWCUTUUMUWDUTUUNUWEUTVAZSZURZUXNUWHDUMZUWIEUMZUWJ - FUMZURZUWCUWHGQZUEUHUSZTZUWDUWIHQZUFUIUSZTZUWEUWJIQZUGUJUSZTZURZUWCUWHU - TZUWDUWIUTZUWEUWJUTZVAZSZURZSZUVDUYJUULUWHGQZOUHUSZTZUUMUWIHQZPUIUSZTZU - UNUWJIQZUDUJUSZTZURZUULUWHUTZUUMUWIUTZUUNUWJUTZVAZSZURZUQAVUGVVCAVUGSZU - VDUYJVVBUVDUXNUYEVUFAWDUXNUYJVUEUYFAWEVVDVUQVVAVVDVUJVUMVUPVVDUYKVUJUYL - VVDUXOUYKVUJUQZUXPVVDUXOUYKVUJVVDUXOUYKSZVUHVUJVVDDGWFZUVAUXKUYGVVFVUHU - QAVVGVUGLWGZVUGUVAAUVAUVBUVCUXNUYEVUFWHVSVUGUXKAUXKUXLUXMUYJVUEUYFWJVSZ - VUGUYGAUYGUYHUYIUXNVUEUYFWKVSZDUULUWCUWHGWLWMVUHVUIWNZWOWPUXPVVEUQVVDUX - PUYKVUHVUJUULUWCUWHGWQVVKWRVOUYFUXQAVUFUXQUXTUYCUYDUVDUXNWSWTZXAVVDUXQU - YLVUJVVLUYLUXOVUHUXPVUIUWCUWHUULGXBUEUHOXCXDXEVUFUYMAUYFUYMUYPUYSVUDUXN - UYJWSXIZXAVVDUYNVUMUYOVVDUXRUYNVUMUQZUXSVVDUXRUYNVUMVVDUXRUYNSZVUKVUMVV - DEHWFZUVBUXLUYHVVOVUKUQAVVPVUGMWGZVUGUVBAUVAUVBUVCUXNUYEVUFXFVSVUGUXLAU - XKUXLUXMUYJVUEUYFXGVSZVUGUYHAUYGUYHUYIUXNVUEUYFXHVSZEUUMUWDUWIHWLWMVUKV - ULWNZWOWPUXSVVNUQVVDUXSUYNVUKVUMUUMUWDUWIHWQVVTWRVOUYFUXTAVUFUXQUXTUYCU - YDUVDUXNXJWTZXAVVDUXTUYOVUMVWAUYOUXRVUKUXSVULUWDUWIUUMHXBUFUIPXCXDXEVUF - UYPAUYFUYMUYPUYSVUDUXNUYJXJXIZXAVVDUYQVUPUYRVVDUYAUYQVUPUQZUYBVVDUYAUYQ - VUPVVDUYAUYQSZVUNVUPVVDFIWFZUVCUXMUYIVWDVUNUQAVWEVUGNWGZVUGUVCAUVAUVBUV - CUXNUYEVUFXKVSVUGUXMAUXKUXLUXMUYJVUEUYFXLVSZVUGUYIAUYGUYHUYIUXNVUEUYFXM - VSZFUUNUWEUWJIWLWMVUNVUOWNZWOWPUYBVWCUQVVDUYBUYQVUNVUPUUNUWEUWJIWQVWIWR - VOUYFUYCAVUFUXQUXTUYCUYDUVDUXNXNWTZXAVVDUYCUYRVUPVWJUYRUYAVUNUYBVUOUWEU - WJUUNIXBUGUJUDXCXDXEVUFUYSAUYFUYMUYPUYSVUDUXNUYJXNXIZXAXOVVDVVAUYLUYOUY - RURZVVDVUDVWLUNZVUGVUDAUYTVUDUXNUYJUYFXPVSVUDUYLUNZUYOUNZUYRUNZVAVWMVUA - VWNVUBVWOVUCVWPUWCUWHXRUWDUWIXRUWEUWJXRXQUYLUYOUYRXSWCXTVVAUNVUIVULVUOU - RZVVDVWLVVAVWQVVAVUIUNZVULUNZVUOUNZVAVWQUNVURVWRVUSVWSVUTVWTUULUWHXRUUM - UWIXRUUNUWJXRXQVUIVULVUOXSWCYAVVDVUIUYLVULUYOVUOUYRVVDVUIUYLVVDVUISZUWH - UWCGQZUYKSZUYLVXAVXBUYLTZUYMVXCUYLTVVDVUIVXDVVDUXQVUIVXDVVLVUIUXOVXBUXP - UYLUULUWHUWCGWQVUIUXPUHUEUSUYLOUHUEYBUHUEYCVLXDXEYHVVDUYMVUIVVMWGVXBUYK - UYLYDYEVVDVXCUNZVUIVVDVVGUYGUXKVXEVVHVVJVVIDUWHUWCGYFYGWGYIYRVVDVULUYOV - VDVULSZUWIUWDHQZUYNSZUYOVXFVXGUYOTZUYPVXHUYOTVVDVULVXIVVDUXTVULVXIVWAVU - LUXRVXGUXSUYOUUMUWIUWDHWQVULUXSUIUFUSUYOPUIUFYBUIUFYCVLXDXEYHVVDUYPVULV - WBWGVXGUYNUYOYDYEVVDVXHUNZVULVVDVVPUYHUXLVXJVVQVVSVVREUWIUWDHYFYGWGYIYR - VVDVUOUYRVVDVUOSZUWJUWEIQZUYQSZUYRVXKVXLUYRTZUYSVXMUYRTVXKVXLUJUGUSZTZV - XNVVDVUOVXPVVDUYCVUOVXPVWJVUOUYAVXLUYBVXOUUNUWJUWEIWQUDUJUGYBXDXEYHVXOU - YRVXLUJUGYCYJXTVVDUYSVUOVWKWGVXLUYQUYRYDYEVVDVXMUNZVUOVVDVWEUYIUXMVXQVW - FVWHVWGFUWJUWEIYFYGWGYIYRYKYLYMYNXOYRUWMUVTVUGUWAVVCUWMUVRUYFUVSVUFUWMU - VRUUOUWFJQZUYFUUPUWGUVRVXRVJUWLUUHUUOUVMUWFJVGYOBCDEFGHIJUFUGOPUDUEKVKV - LUWMUVSUWFUWKJQZVUFUWGUWLUVSVXSVJUUPUVMUWFUVOUWKJVGYPBCDEFGHIJUIUJUEUFU - GUHKVKVLUUAUWMUWAUUOUWKJQZVVCUUPUWLUWAVXTVJUWGUUHUUOUVOUWKJVGUUBBCDEFGH - IJUIUJOPUDUHKVKVLUUCUUDYQYSYTYQYSYTYQYSYTUUEYHUUF $. + ( va vb wbr wrex w3a wa vp vq vr vc vd ve vf vg vh vi cv wcel cotp wceq + cxp wn el2xptp weq wo wne w3o neirr 3pm3.2ni intnan simp3 mto wb breq12 + anidms xpord3lem bitrdi mtbiri rexlimivw sylbi adantl wi 3reeanv rexbii + 2rexbii 3anbi123i 3bitr4ri simpr1l simpr2r simp1l1 simp2l1 simp2r1 3jca + bitri wpo potr syl2an expd biimprd a1i simpll1 3ad2ant3 mpjaod orc syl6 + breq1 equequ2 orbi12d syl5ibcom simprl1 simp1l2 simp2l2 simp2r2 simpll2 + breq2 simprl2 simp1l3 simp2l3 simp2r3 simpll3 simprl3 adantr equcom imp + simp3rr equequ1 ordir sylanbrc po2nr syl12anc necon3d 3orim123d mpd jca + orcnd ex 3adant3 3adant1 anbi12d an6 3adant2 imbi12d rexlimdvw biimtrid + syl5ibrcom ispod ) AUAUBUCDEUOFUOZJUAUKZUUAULZUUBUUBJQZUPZAUUCUUBOUKZPU + KZUDUKZUMZUNZUDFRZPERZODRZUUEOPUDUUBDEFUQZUULUUEODUUKUUEPEUUJUUEUDFUUJU + UDUUFDULZUUGEULZUUHFULZSZUURUUFUUFGQOOURUSUUGUUGHQPPURUSUUHUUHIQUDUDURU + SSZUUFUUFUTZUUGUUGUTZUUHUUHUTZVAZTZSZUVEUVDUVCUUSUUTUVAUVBUUFVBUUGVBUUH + VBVCVDUURUURUVDVEVFUUJUUDUUIUUIJQZUVEUUJUUDUVFVGUUBUUIUUBUUIJVHVIBCDEFG + HIJPUDOPUDOKVJVKVLVMVMVMVNVOAUUCUBUKZUUAULZUCUKZUUAULZSZUUBUVGJQZUVGUVI + JQZTZUUBUVIJQZVPZUVKUUJUVGUEUKZUFUKZUGUKZUMZUNZUVIUHUKZUIUKZUJUKZUMZUNZ + SZUJFRZUGFRZUDFRZUIERZUFERZPERZUHDRZUEDRZODRZAUVPUULUWAUGFRZUFERZUWFUJF + RZUIERZSZUHDRZUEDRODRUUMUWRUEDRZUWTUHDRZSUWPUVKUULUWRUWTOUEUHDDDVQUWNUX + BOUEDDUWMUXAUHDUWMUUKUWQUWSSZUIERZUFERPERUXAUWKUXFPUFEEUWJUXEUIEUUJUWAU + WFUDUGUJFFFVQVRVSUUKUWQUWSPUFUIEEEVQWHVRVSUUCUUMUVHUXCUVJUXDUUNUEUFUGUV + GDEFUQUHUIUJUVIDEFUQVTWAAUWOUVPODAUWNUVPUEDAUWMUVPUHDAUWLUVPPEAUWKUVPUF + EAUWJUVPUIEAUWIUVPUDFAUWHUVPUGFAUWGUVPUJFAUVPUWGUURUVQDULZUVREULZUVSFUL + ZSZTZUXJUWBDULZUWCEULZUWDFULZSZTZUUFUVQGQZOUEURZUSZUUGUVRHQZPUFURZUSZUU + HUVSIQZUDUGURZUSZSUUFUVQUTUUGUVRUTUUHUVSUTVAZTZUVQUWBGQZUEUHURZUSZUVRUW + CHQZUFUIURZUSZUVSUWDIQZUGUJURZUSZSZUVQUWBUTZUVRUWCUTZUVSUWDUTZVAZTZTZSZ + UURUXOUUFUWBGQZOUHURZUSZUUGUWCHQZPUIURZUSZUUHUWDIQZUDUJURZUSZSZUUFUWBUT + ZUUGUWCUTZUUHUWDUTZVAZTZSZVPAVUDVUTAVUDTZUURUXOVUSUURUXJUXPVUCAWBUXJUXO + UXKVUCAWCVVAVUNVURVVAVUGVUJVUMVVAUYHVUGUYIVVAUYHVUEVUGVVAUXQUYHVUEVPZUX + RVVAUXQUYHVUEADGWIZUUOUXGUXLSUXQUYHTVUEVPVUDLVUDUUOUXGUXLUUOUUPUUQUXJUX + PVUCWDUXGUXHUXIUXOUXKVUCWEZUXLUXMUXNUXJUXKVUCWFZWGDUUFUVQUWBGWJWKWLUXRV + VBVPVVAUXRVUEUYHUUFUVQUWBGWTWMWNVUDUXSAVUCUXKUXSUXPUXSUYBUYEUYFVUBWOWPV + OZWQVUEVUFWRWSVVAUXSUYIVUGVVFUYIUXQVUEUXRVUFUVQUWBUUFGXIUEUHOXAXBXCVUDU + YJAVUCUXKUYJUXPUYJUYMUYPVUAUYGXDWPVOZWQVVAUYKVUJUYLVVAUYKVUHVUJVVAUXTUY + KVUHVPZUYAVVAUXTUYKVUHAEHWIZUUPUXHUXMSUXTUYKTVUHVPVUDMVUDUUPUXHUXMUUOUU + PUUQUXJUXPVUCXEUXGUXHUXIUXOUXKVUCXFZUXLUXMUXNUXJUXKVUCXGZWGEUUGUVRUWCHW + JWKWLUYAVVHVPVVAUYAVUHUYKUUGUVRUWCHWTWMWNVUDUYBAVUCUXKUYBUXPUXSUYBUYEUY + FVUBXHWPVOZWQVUHVUIWRWSVVAUYBUYLVUJVVLUYLUXTVUHUYAVUIUVRUWCUUGHXIUFUIPX + AXBXCVUDUYMAVUCUXKUYMUXPUYJUYMUYPVUAUYGXJWPVOZWQVVAUYNVUMUYOVVAUYNVUKVU + MVVAUYCUYNVUKVPZUYDVVAUYCUYNVUKAFIWIZUUQUXIUXNSUYCUYNTVUKVPVUDNVUDUUQUX + IUXNUUOUUPUUQUXJUXPVUCXKUXGUXHUXIUXOUXKVUCXLZUXLUXMUXNUXJUXKVUCXMZWGFUU + HUVSUWDIWJWKWLUYDVVNVPVVAUYDVUKUYNUUHUVSUWDIWTWMWNVUDUYEAVUCUXKUYEUXPUX + SUYBUYEUYFVUBXNWPVOZWQVUKVULWRWSVVAUYEUYOVUMVVRUYOUYCVUKUYDVULUVSUWDUUH + IXIUGUJUDXAXBXCVUDUYPAVUCUXKUYPUXPUYJUYMUYPVUAUYGXOWPVOZWQWGVVAVUAVURVU + DVUAAUYQVUAUYGUXKUXPXSVOVVAUYRVUOUYSVUPUYTVUQVVAUUFUWBUVQUWBVVAVUFUYIVV + AVUFTZUYHUWBUVQGQZTZUYIVVTUYJVWAUYIUSZVWBUYIUSVVAUYJVUFVVGXPVVAVUFVWCVV + AUXSVUFVWCVVFVUFUXQVWAUXRUYIUUFUWBUVQGWTVUFUXRUHUEURUYIOUHUEXTUHUEXQVKX + BXCXRUYHVWAUYIYAYBVVAVWBUPZVUFVVAVVCUXGUXLVWDAVVCVUDLXPVUDUXGAVVDVOVUDU + XLAVVEVODUVQUWBGYCYDXPYIYJYEVVAUUGUWCUVRUWCVVAVUIUYLVVAVUITZUYKUWCUVRHQ + ZTZUYLVWEUYMVWFUYLUSZVWGUYLUSVVAUYMVUIVVMXPVVAVUIVWHVVAUYBVUIVWHVVLVUIU + XTVWFUYAUYLUUGUWCUVRHWTVUIUYAUIUFURUYLPUIUFXTUIUFXQVKXBXCXRUYKVWFUYLYAY + BVVAVWGUPZVUIVVAVVIUXHUXMVWIAVVIVUDMXPVUDUXHAVVJVOVUDUXMAVVKVOEUVRUWCHY + CYDXPYIYJYEVVAUUHUWDUVSUWDVVAVULUYOVVAVULTZUYNUWDUVSIQZTZUYOVWJUYPVWKUY + OUSZVWLUYOUSVVAUYPVULVVSXPVVAVULVWMVVAUYEVULVWMVVRVULUYCVWKUYDUYOUUHUWD + UVSIWTVULUYDUJUGURUYOUDUJUGXTUJUGXQVKXBXCXRUYNVWKUYOYAYBVVAVWLUPZVULVVA + VVOUXIUXNVWNAVVOVUDNXPVUDUXIAVVPVOVUDUXNAVVQVOFUVSUWDIYCYDXPYIYJYEYFYGY + HWGYJUWGUVNVUDUVOVUTUWGUVNUURUXJUYGSZUXJUXOVUBSZTVUDUWGUVLVWOUVMVWPUWGU + VLUUIUVTJQZVWOUUJUWAUVLVWQVGUWFUUBUUIUVGUVTJVHYKBCDEFGHIJUFUGOPUDUEKVJV + KUWGUVMUVTUWEJQZVWPUWAUWFUVMVWRVGUUJUVGUVTUVIUWEJVHYLBCDEFGHIJUIUJUEUFU + GUHKVJVKYMUURUXJUYGUXJUXOVUBYNVKUWGUVOUUIUWEJQZVUTUUJUWFUVOVWSVGUWAUUBU + UIUVIUWEJVHYOBCDEFGHIJUIUJOPUDUHKVJVKYPYSYQYQYQYQYQYQYQYQYQYRXRYT $. $} ${ @@ -540386,67 +540334,64 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $= $( Give foundedness over a triple cross product. (Contributed by Scott Fenton, 21-Aug-2024.) $) frxp3 $p |- ( ph -> U Fr ( ( A X. B ) X. C ) ) $= - ( vg c0 wa wn wi wcel vs vq vp vd va ve vb vf vc vh vi cxp wss wne wral - cv wbr wrex wal wfr cdm dmss ad2antrl dmxpss sstrdi simprr wrel wceq wb - syl simprl relxp relss mpisyl reldm0 necon3bid mpbid df-fr sylib adantr - vex dmex sseq1 neeq1 anbi12d raleq rexeqbi1dv imbi12d spcv csn cima crn - mp2and imassrn rnss rnxpss sstrid imadisj disjsn bitri necon2abii imaex - cin ad2antrr cop elimasn ad3antrrr opex wel wex w3a weq wo adantl breq1 - notbid simplrr sylibr rspcdva simpr ioran sylanbrc intn3an3d pm2.61dane - neneqd opeq1d eleq1d anbi2d orbi1d neirr orel1 olc impbii bitrdi mpbiri - intnanrd ax-mp impcom opeldm rexlimddv simplrl elxpxpss sylan w3o df-ne - con2bii biimpi intnand simplr opeq2 intn3an2d opeq1 3orass bitrid eleq1 - intn3an1d xpord3lem com12 exlimdv exlimdvv mpd ralrimiva ralbidv rspcev - breq2 syl2anc ex alrimiv ) AUAUPZDEULZFULZUMZUVIPUNZQZUBUPZUCUPZJUQZRZU - BUVIUOZUCUVIURZSZUAUSUVKJUTAUWAUAAUVNUVTAUVNQZUDUPZUEUPZGUQZRZUDUVIVAZV - AZUOZUVTUEUWHUWBUWHDUMZUWHPUNZUWIUEUWHURZUWBUWHUVJVAZDUWBUWGUVJUMZUWHUW - MUMUWBUWGUVKVAZUVJUVLUWGUWOUMAUVMUVIUVKVBVCUVJFVDVEZUWGUVJVBVJDEVDVEUWB - UWGPUNZUWKUWBUVMUWQAUVLUVMVFUWBUVIPUWGPUWBUVIVGZUVIPVHUWGPVHZVIUWBUVLUV - KVGUWRAUVLUVMVKUVJFVLUVIUVKVMVNUVIVOVJVPVQUWBUWGPUWHPUWBUWGVGZUWSUWHPVH - VIUWBUWNUVJVGUWTUWPDEVLUWGUVJVMVNUWGVOVJVPVQUWBOUPZDUMZUXAPUNZQZUWFUDUX - AUOZUEUXAURZSZOUSZUWJUWKQZUWLSZAUXHUVNADGUTUXHLOUEUDDGVRVSVTUXGUXJOUWHU - WGUVIUAWAZWBZWBUXAUWHVHZUXDUXIUXFUWLUXMUXBUWJUXCUWKUXAUWHDWCUXAUWHPWDWE - UXEUWIUEUXAUWHUWFUDUXAUWHWFWGWHWIVJWMUWBUWDUWHTZUWIQZQZUFUPZUGUPZHUQZRZ - UFUWGUWDWJZWKZUOZUVTUGUYBUXPUYBEUMZUYBPUNZUYCUGUYBURZUXPUYBUWGWLZEUWGUY - AWNUWBUYGEUMUXOUWBUYGUVJWLZEUWBUWNUYGUYHUMUWPUWGUVJWOVJDEWPVEVTWQUXPUXN - UYEUWBUXNUWIVKUXNUYBPUYBPVHUWHUYAXCPVHUXNRUWGUYAWRUWHUWDWSWTXAVSAUYDUYE - QZUYFSZUVNUXOAUXAEUMZUXCQZUXTUFUXAUOZUGUXAURZSZOUSZUYJAEHUTUYPMOUGUFEHV - RVSUYOUYJOUYBUWGUYAUXLXBUXAUYBVHZUYLUYIUYNUYFUYQUYKUYDUXCUYEUXAUYBEWCUX - AUYBPWDWEUYMUYCUGUXAUYBUXTUFUXAUYBWFWGWHWIVJXDWMUXPUXRUYBTZUYCQZQZUHUPZ - UIUPZIUQZRZUHUVIUWDUXRXEZWJZWKZUOZUVTUIVUGUYTVUGFUMZVUGPUNZVUHUIVUGURZU - WBVUIUXOUYSUWBVUGUVIWLZFUVIVUFWNUWBVULUVKWLZFUVLVULVUMUMAUVMUVIUVKWOVCU - VJFWPVEWQXDUYTVUEUWGTZVUJUYTUYRVUNUXPUYRUYCVKUWGUWDUXRUEWAZUGWAXFVSVUNV - UGPVUGPVHUWGVUFXCPVHVUNRUVIVUFWRUWGVUEWSWTXAVSAVUIVUJQZVUKSZUVNUXOUYSAU - XAFUMZUXCQZVUDUHUXAUOZUIUXAURZSZOUSZVUQAFIUTVVCNOUIUHFIVRVSVVBVUQOVUGUV - IVUFUXKXBUXAVUGVHZVUSVUPVVAVUKVVDVURVUIUXCVUJUXAVUGFWCUXAVUGPWDWEVUTVUH - UIUXAVUGVUDUHUXAVUGWFWGWHWIVJXGWMUYTVUBVUGTZVUHQZQZVUEVUBXEZUVITZUVOVVH - JUQZRZUBUVIUOZUVTVVGVVEVVIUYTVVEVUHVKUVIVUEVUBUWDUXRXHZUIWAXFVSVVGVVKUB - UVIVVGUBUAXIZQZUVOUXAUJUPZXEZUKUPZXEZVHZUKXJZUJXJOXJZVVKVVGUVLVVNVWBUXP - UVLUYSVVFAUVLUVMUXOUUAXDOUJUKUVODEFUVIUUBUUCVVOVWAVVKOUJVVOVVTVVKUKVVTV - VOVVKVVTVVOVVKSVVGVVSUVITZQZUXADTVVPETVVRFTXKZUWDDTUXRETVUBFTXKZUXAUWDG - UQZOUEXLZXMZVVPUXRHUQZUJUGXLZXMZVVRVUBIUQZUKUIXLZXMZXKZUXAUWDUNZVVPUXRU - NZVVRVUBUNZUUDZQZXKZRZSVWDVXAVWEVWFVWDVXARZUXAUWDVWHVWDVXDVWHVWDVXDSVVG - UWDVVPXEZVVRXEZUVITZQZVWPVWRVWSXMZQZRZSZVXHVXKVVPUXRVWKVXHVXKVWKVXLVVGV - UEVVRXEZUVITZQZVWPVWSQZRZSVXOVXQVVRVUBVXOVWNQVWSVWPVWNVWSRZVXOVWNVXRVWS - VWNVVRVUBUUEUUFUUGXNUUHVXOVWSQZVWPVWSVXSVWOVWIVWLVXSVWMRZVWNRVWORVXSVUD - VXTUHVUGVVRUHUKXLVUCVWMVUAVVRVUBIXOXPVXOVUHVWSUYTVVEVUHVXNXQVTVXSVXNVVR - VUGTVVGVXNVWSUUIUVIVUEVVRVVMUKWAZXFXRXSVXSVVRVUBVXOVWSXTYEVWMVWNYAYBYCY - PYDVWKVXHVXOVXKVXQVWKVXGVXNVVGVWKVXFVXMUVIVWKVXEVUEVVRVVPUXRUWDUUJYFYGY - HVWKVXJVXPVWKVXIVWSVWPVWKVXIUXRUXRUNZVWSXMZVWSVWKVWRVYBVWSVVPUXRUXRWDYI - VYCVWSVYBRVYCVWSSUXRYJVYBVWSYKYQVWSVYBYLYMYNYHXPWHYOYRVXHVWRQZVWPVXIVYD - VWLVWIVWOVYDVWJRZVWKRVWLRVYDUXTVYEUFUYBVVPUFUJXLUXSVWJUXQVVPUXRHXOXPVVG - UYCVXGVWRUXPUYRUYCVVFXQXDVYDVXEUWGTZVVPUYBTVXHVYFVWRVXGVYFVVGVXEVVRUVIU - WDVVPXHVYAYSXNVTUWGUWDVVPVUOUJWAZXFXRXSVYDVVPUXRVXHVWRXTYEVWJVWKYAYBUUK - YPYDVWHVWDVXHVXDVXKVWHVWCVXGVVGVWHVVSVXFUVIVWHVVQVXEVVRUXAUWDVVPUULYFYG - YHVWHVXAVXJVWHVWTVXIVWPVWHVWTUWDUWDUNZVXIXMZVXIVWTVWQVXIXMVWHVYIVWQVWRV - WSUUMVWHVWQVYHVXIUXAUWDUWDWDYIUUNVYIVXIVYHRVYIVXISUWDYJVYHVXIYKYQVXIVYH - YLYMYNYHXPWHYOYRVWDVWQQZVWPVWTVYJVWIVWLVWOVYJVWGRZVWHRVWIRVYJUWFVYKUDUW - HUXAUDOXLUWEVWGUWCUXAUWDGXOXPUYTUWIVVFVWCVWQUWBUXNUWIUYSXQXGVWDUXAUWHTZ - VWQVWDVVQUWGTZVYLVWCVYMVVGVVQVVRUVIUXAVVPXHVYAYSXNUXAVVPUWGOWAVYGYSVJVT - XSVYJUXAUWDVWDVWQXTYEVWGVWHYAYBUUPYPYDYCVVTVVOVWDVVKVXCVVTVVNVWCVVGUVOV - VSUVIUUOYHVVTVVJVXBVVTVVJVVSVVHJUQVXBUVOVVSVVHJXOBCDEFGHIJUGUIOUJUKUEKU - UQYNXPWHYOUURUUSUUTUVAUVBUVSVVLUCVVHUVIUVPVVHVHZUVRVVKUBUVIVYNUVQVVJUVP - VVHUVOJUVEXPUVCUVDUVFYTYTYTUVGUVHUAUCUBUVKJVRXR $. + ( cv wss c0 wa wn wcel vs vq vp vd va ve vb vf vc vg vh vi cxp wne wral + wbr wrex wi wal wfr cdm cvv vex dmex adantr dmss ad2antrl dmxpss sstrdi + a1i syl wceq wrel relxp relss mpi adantl reldm0 mp2 mpisyl fri syl22anc + wb csn cima imaex ad2antrr crn imassrn rnxpss sstrid cin imadisj disjsn + rnss bitri necon2abii biimpi cop ad3antrrr simprl sylib cotp df-ot opex + elimasn wex w3a weq wo w3o breq1 notbid simplrr simplr eqeltrrid sylibr + simpr neneqd ioran sylanbrc intn3an3d intnanrd pm2.61dane eleq1d anbi2d + rspcdva neeq1 neirr orel1 ax-mp olc impbii bitrdi imbi12d mpbiri impcom + opeldm biidd rexlimddv necon3bid biimpa anasss eqeltrid simplrl el2xpss + bitrd wel sylan df-ne con2bii intnand orbi1d intn3an2d 3orbi123d 3orass + oteq2 oteq1 3syl intn3an1d eleq1 xpord3lem com12 exlimdvv mpd ralrimiva + exlimdv breq2 ralbidv rspcev syl2anc ex alrimiv df-fr ) AUAOZDEUMZFUMZP + ZUVOQUNZRZUBOZUCOZJUPZSZUBUVOUOZUCUVOUQZURZUAUSUVQJUTAUWGUAAUVTUWFAUVTR + ZUDOZUEOZGUPZSZUDUVOVAZVAZUOZUWFUEUWNUWHUWNVBTZDGUTZUWNDPUWNQUNZUWOUEUW + NUQUWPUWHUWMUVOUAVCZVDZVDVJAUWQUVTLVEUWHUWNUVPVAZDUWHUWMUVPPZUWNUXAPUWH + UWMUVQVAZUVPUVRUWMUXCPZAUVSUVOUVQVFZVGUVPFVHZVIZUWMUVPVFVKDEVHVIAUVRUVS + UWRAUVRRZUVSUWRUXHUVOQUWNQUXHUVOQVLZUWMQVLZUWNQVLZUXHUVOVMZUXIUXJWCUVRU + XLAUVRUVQVMUXLUVPFVNUVOUVQVOVPVQUVOVRVKUXHUWMVMZUXJUXKWCUVRUXMAUVRUXDUX + CVMZUXMUXEUXCUVPPUVPVMUXNUXFDEVNUXCUVPVOVSUWMUXCVOVTVQUWMVRVKUUGUUAUUBU + UCUEUDDUWNVBGWAWBUWHUWJUWNTZUWORZRZUFOZUGOZHUPZSZUFUWMUWJWDZWEZUOZUWFUG + UYCUXQUYCVBTZEHUTZUYCEPZUYCQUNZUYDUGUYCUQUYEUXQUWMUYBUWTWFVJAUYFUVTUXPM + WGUWHUYGUXPUWHUYCUWMWHZEUWMUYBWIUWHUYIUVPWHZEUWHUXBUYIUYJPUXGUWMUVPWOVK + DEWJVIWKVEUXOUYHUWHUWOUXOUYHUXOUYCQUYCQVLUWNUYBWLQVLUXOSUWMUYBWMUWNUWJW + NWPWQWRVGUGUFEUYCVBHWAWBUXQUXSUYCTZUYDRZRZUHOZUIOZIUPZSZUHUVOUWJUXSWSZW + DZWEZUOZUWFUIUYTUYMUYTVBTZFIUTZUYTFPZUYTQUNZVUAUIUYTUQVUBUYMUVOUYSUWSWF + VJAVUCUVTUXPUYLNWTUWHVUDUXPUYLUWHUYTUVOWHZFUVOUYSWIUWHVUFUVQWHZFUVRVUFV + UGPAUVSUVOUVQWOVGUVPFWJVIWKWGUYMUYRUWMTZVUEUYMUYKVUHUXQUYKUYDXAUWMUWJUX + SUEVCZUGVCXFXBVUHUYTQUYTQVLUWMUYSWLQVLVUHSUVOUYSWMUWMUYRWNWPWQXBUIUHFUY + TVBIWAWBUYMUYOUYTTZVUARZRZUWJUXSUYOXCZUVOTUWAVUMJUPZSZUBUVOUOZUWFVULVUM + UYRUYOWSZUVOUWJUXSUYOXDVULVUJVUQUVOTUYMVUJVUAXAUVOUYRUYOUWJUXSXEZUIVCXF + XBUUDVULVUOUBUVOVULUBUAUUHZRZUWAUJOZUKOZULOZXCZVLZULXGZUKXGUJXGZVUOVULU + VRVUSVVGUXQUVRUYLVUKAUVRUVSUXPUUEWGUJUKULUWADEFUVOUUFUUIVUTVVFVUOUJUKVU + TVVEVUOULVVEVUTVUOVVEVUTVUOURVULVVDUVOTZRZVVADTVVBETVVCFTXHZUWJDTUXSETU + YOFTXHZVVAUWJGUPZUJUEXIZXJZVVBUXSHUPZUKUGXIZXJZVVCUYOIUPZULUIXIZXJZXHZV + VAUWJUNZVVBUXSUNZVVCUYOUNZXKZRZXHZSZURVVIVWFVVJVVKVVIVWFSZVVAUWJVVMVVIV + WIVVMVVIVWIURVULUWJVVBVVCXCZUVOTZRZVWAVWCVWDXJZRZSZURZVWLVWOVVBUXSVVPVW + LVWOVVPVWPVULUWJUXSVVCXCZUVOTZRZVWAVWDRZSZURVWSVXAVVCUYOVVSVXAVWSVVSVWD + VWAVVSVWDSVWDVVSVVCUYOUUJUUKWRUULVQVWSVWDRZVWAVWDVXBVVTVVNVVQVXBVVRSZVV + SSVVTSVXBUYQVXCUHUYTVVCUHULXIUYPVVRUYNVVCUYOIXLXMVWSVUAVWDUYMVUJVUAVWRX + NVEVXBUYRVVCWSZUVOTVVCUYTTVXBVXDVWQUVOUWJUXSVVCXDVULVWRVWDXOXPUVOUYRVVC + VURULVCZXFXQYGVXBVVCUYOVWSVWDXRXSVVRVVSXTYAYBYCYDVVPVWLVWSVWOVXAVVPVWKV + WRVULVVPVWJVWQUVOVVBUXSUWJVVCUUQYEYFVVPVWNVWTVVPVWMVWDVWAVVPVWMUXSUXSUN + ZVWDXJZVWDVVPVWCVXFVWDVVBUXSUXSYHUUMVXGVWDVXFSVXGVWDURUXSYIVXFVWDYJYKVW + DVXFYLYMYNYFXMYOYPYQVWLVWCRZVWAVWMVXHVVQVVNVVTVXHVVOSZVVPSVVQSVXHUYAVXI + UFUYCVVBUFUKXIUXTVVOUXRVVBUXSHXLXMVULUYDVWKVWCUXQUYKUYDVUKXNWGVXHUWJVVB + WSZUWMTZVVBUYCTVXHVXJVVCWSZUVOTVXKVXHVXLVWJUVOUWJVVBVVCXDVULVWKVWCXOXPV + XJVVCUVOUWJVVBXEVXEYRVKUWMUWJVVBVUIUKVCZXFXQYGVXHVVBUXSVWLVWCXRXSVVOVVP + XTYAUUNYCYDVVMVVIVWLVWIVWOVVMVVHVWKVULVVMVVDVWJUVOVVAUWJVVBVVCUURYEYFVV + MVWFVWNVVMVWEVWMVWAVVMVWEUWJUWJUNZVWCVWDXKZVWMVVMVWBVXNVWCVWCVWDVWDVVAU + WJUWJYHVVMVWCYSVVMVWDYSUUOVXOVXNVWMXJZVWMVXNVWCVWDUUPVXPVWMVXNSVXPVWMUR + UWJYIVXNVWMYJYKVWMVXNYLYMWPYNYFXMYOYPYQVVIVWBRZVWAVWEVXQVVNVVQVVTVXQVVL + SZVVMSVVNSVXQUWLVXRUDUWNVVAUDUJXIUWKVVLUWIVVAUWJGXLXMUYMUWOVUKVVHVWBUWH + UXOUWOUYLXNWTVXQVVAVVBWSZVVCWSZUVOTVXSUWMTVVAUWNTVXQVXTVVDUVOVVAVVBVVCX + DVULVVHVWBXOXPVXSVVCUVOVVAVVBXEVXEYRVVAVVBUWMUJVCVXMYRUUSYGVXQVVAUWJVVI + VWBXRXSVVLVVMXTYAUUTYCYDYBVVEVUTVVIVUOVWHVVEVUSVVHVULUWAVVDUVOUVAYFVVEV + UNVWGVVEVUNVVDVUMJUPVWGUWAVVDVUMJXLBCDEFGHIJUGUIUJUKULUEKUVBYNXMYOYPUVC + UVGUVDUVEUVFUWEVUPUCVUMUVOUWBVUMVLZUWDVUOUBUVOVYAUWCVUNUWBVUMUWAJUVHXMU + VIUVJUVKYTYTYTUVLUVMUAUCUBUVQJUVNXQ $. $} ${ @@ -540468,54 +540413,51 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $= $d U d $. $d U e $. $d U f $. $d U q $. $d X a $. $d X b $. $d X c $. $d x y $. $d Y b $. $d Y c $. $d Z c $. $( Calculate the predecsessor class for the triple order. (Contributed - by Scott Fenton, 21-Aug-2024.) $) + by Scott Fenton, 31-Jan-2025.) $) xpord3pred $p |- ( ( X e. A /\ Y e. B /\ Z e. C ) -> - Pred ( U , ( ( A X. B ) X. C ) , <. <. X , Y >. , Z >. ) = + Pred ( U , ( ( A X. B ) X. C ) , <. X , Y , Z >. ) = ( ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , Y ) u. { Y } ) ) X. ( Pred ( T , C , Z ) u. { Z } ) ) \ - { <. <. X , Y >. , Z >. } ) ) $= - ( cxp cop cpred csn wceq wcel wa va vb vc vq vd ve vf cv cun cdif opeq1 - opeq1d predeq3 syl sneq uneq12d xpeq1d sneqd difeq12d eqeq12d opeq2 w3a - xpeq2d cin wbr wrex wb elxpxp wi df-3an weq wo wne wn eldif opelxp elun - w3o cvv vex elpred velsn orbi12i bitri anbi12i df-ne otthne bitr3i opex - elv elsn simpr1 biantrurd orbi1d simpr2 simpr3 3anbi123d bitrdi bitr4id - xchnxbir anbi1d pm3.22 bitr2d bitrid breq1 xpord3lem bibi12d syl5ibrcom - eleq1 sylan2br anassrs rexlimdva rexlimdvva biimtrid pm5.32d ax-mp elin - 3bitr4g eqrdv wss predss snssi unssd 3ad2ant1 3ad2ant2 syl2anc 3ad2ant3 - a1i xpss12 ssdifssd sseqin2 sylib eqtrd vtocl3ga ) CDNZENZIUAUHZUBUHZOZ - UCUHZOZPZCFYQPZYQQZUIZDGYRPZYRQZUIZNZEHYTPZYTQZUIZNZUUAQZUJZRYPIJYROZYT - OZPZCFJPZJQZUIZUUHNZUULNZUUQQZUJZRYPIJKOZYTOZPZUVADGKPZKQZUIZNZUULNZUVG - QZUJZRYPIUVFLOZPZUVLEHLPZLQZUIZNZUVPQZUJZRUAUBUCJKLCDEYQJRZUUBUURUUOUVE - UWDUUAUUQRUUBUURRUWDYSUUPYTYQJYRUKULZYPIUUAUUQUMUNUWDUUMUVCUUNUVDUWDUUI - UVBUULUWDUUEUVAUUHUWDUUCUUSUUDUUTCFYQJUMYQJUOUPUQUQUWDUUAUUQUWEURUSUTYR - KRZUURUVHUVEUVOUWFUUQUVGRUURUVHRUWFUUPUVFYTYRKJVAULZYPIUUQUVGUMUNUWFUVC - UVMUVDUVNUWFUVBUVLUULUWFUUHUVKUVAUWFUUFUVIUUGUVJDGYRKUMYRKUOUPVCUQUWFUU - QUVGUWGURUSUTYTLRZUVHUVQUVOUWCUWHUVGUVPRUVHUVQRYTLUVFVAZYPIUVGUVPUMUNUW - HUVMUWAUVNUWBUWHUULUVTUVLUWHUUJUVRUUKUVSEHYTLUMYTLUOUPVCUWHUVGUVPUWIURU - SUTYQCSZYRDSZYTESZVBZUUBYPUUOVDZUUOUWMUDUUBUWNUWMUDUHZYPSZUWOUUAIVEZTZU - WPUWOUUOSZTUWOUUBSZUWOUWNSUWMUWPUWQUWSUWPUWOUEUHZUFUHZOZUGUHZOZRZUGEVFZ - UFDVFUECVFUWMUWQUWSVGZUEUFUGUWOCDEVHUWMUXGUXHUEUFCDUWMUXACSZUXBDSZTZTUX - FUXHUGEUWMUXKUXDESZUXFUXHVIZUXKUXLTUWMUXIUXJUXLVBZUXMUXIUXJUXLVJUWMUXNT - ZUXHUXFUXNUWMUXAYQFVEZUEUAVKZVLZUXBYRGVEZUFUBVKZVLZUXDYTHVEZUGUCVKZVLZV - BZUXAYQVMUXBYRVMUXDYTVMVRZTZVBZUXEUUOSZVGUYHUXNUWMTZUYGTZUXOUYIUXNUWMUY - GVJUXOUYIUYGUYKUXOUYIUXIUXPTZUXQVLZUXJUXSTZUXTVLZTZUXLUYBTZUYCVLZTZUYFT - ZUYGUYIUXEUUMSZUXEUUNSZVNZTUYTUXEUUMUUNVOVUAUYSVUCUYFVUAUXCUUISZUXDUULS - ZTUYSUXCUXDUUIUULVPVUDUYPVUEUYRVUDUXAUUESZUXBUUHSZTUYPUXAUXBUUEUUHVPVUF - UYMVUGUYOVUFUXAUUCSZUXAUUDSZVLUYMUXAUUCUUDVQVUHUYLVUIUXQVUHUYLVGUACVSFY - QUXAUEVTZWAWJUEYQWBWCWDVUGUXBUUFSZUXBUUGSZVLUYOUXBUUFUUGVQVUKUYNVULUXTV - UKUYNVGUBDVSGYRUXBUFVTZWAWJUFYRWBWCWDWEWDVUEUXDUUJSZUXDUUKSZVLUYRUXDUUJ - UUKVQVUNUYQVUOUYCVUNUYQVGUCEVSHYTUXDUGVTZWAWJUGYTWBWCWDWEWDUXEUUARZUYFV - UBVUQVNUXEUUAVMUYFUXEUUAWFUXAUXBUXDYQYRYTVUJVUMVUPWGWHUXEUUAUXCUXDWIWKW - TWEWDUXOUYEUYSUYFUXOUYEUYMUYOUYRVBUYSUXOUXRUYMUYAUYOUYDUYRUXOUXPUYLUXQU - XOUXIUXPUWMUXIUXJUXLWLWMWNUXOUXSUYNUXTUXOUXJUXSUWMUXIUXJUXLWOWMWNUXOUYB - UYQUYCUXOUXLUYBUWMUXIUXJUXLWPWMWNWQUYMUYOUYRVJWRXAWSUXOUYJUYGUWMUXNXBWM - XCXDUXFUWQUYHUWSUYIUXFUWQUXEUUAIVEUYHUWOUXEUUAIXEABCDEFGHIUBUCUEUFUGUAM - XFWRUWOUXEUUOXIXGXHXJXKXLXMXNXOUUAVSSUWTUWRVGYSYTWIYPVSIUUAUWOUDVTWAXPU - WOYPUUOXQXRXSUWMUUOYPXTUWNUUORUWMUUMYPUUNUWMUUIYOXTZUULEXTZUUMYPXTUWMUU - ECXTZUUHDXTZVURUWJUWKVUTUWLUWJUUCUUDCUUCCXTUWJCFYQYAYHYQCYBYCYDUWKUWJVV - AUWLUWKUUFUUGDUUFDXTUWKDGYRYAYHYRDYBYCYEUUECUUHDYIYFUWLUWJVUSUWKUWLUUJU - UKEUUJEXTUWLEHYTYAYHYTEYBYCYGUUIYOUULEYIYFYJUUOYPYKYLYMYN $. + { <. X , Y , Z >. } ) ) $= + ( cxp cpred csn wceq wcel wa wo va vb vc vq vd ve vf cv cotp cdif oteq1 + cun predeq3 syl sneq uneq12d xpeq1d sneqd difeq12d eqeq12d oteq2 xpeq2d + oteq3 w3a cin wbr wrex el2xptp weq wne w3o df-3an simplrl simplrr simpr + wb simpll jca biantrurd orbi1d 3anbi123d anbi1d bitr3d bitrid xpord3lem + 3jca breq1 bitrdi eleq1 eldifsn otelxp cvv vex elpred elv velsn orbi12i + bitri 3anbi123i otthne anbi12i syl5ibrcom rexlimdva rexlimdvva biimtrid + elun bibi12d pm5.32d otex ax-mp elin 3bitr4g eqrdv wss predss a1i snssi + unssd 3ad2ant1 3ad2ant2 xpss12 syl2anc 3ad2ant3 ssdifssd sylib vtocl3ga + sseqin2 eqtrd ) CDNZENZIUAUHZUBUHZUCUHZUIZOZCFYKOZYKPZULZDGYLOZYLPZULZN + ZEHYMOZYMPZULZNZYNPZUJZQYJIJYLYMUIZOZCFJOZJPZULZUUANZUUENZUUIPZUJZQYJIJ + KYMUIZOZUUMDGKOZKPZULZNZUUENZUURPZUJZQYJIJKLUIZOZUVCEHLOZLPZULZNZUVGPZU + JZQUAUBUCJKLCDEYKJQZYOUUJUUHUUQUVOYNUUIQYOUUJQYKJYLYMUKZYJIYNUUIUMUNUVO + UUFUUOUUGUUPUVOUUBUUNUUEUVOYRUUMUUAUVOYPUUKYQUULCFYKJUMYKJUOUPUQUQUVOYN + UUIUVPURUSUTYLKQZUUJUUSUUQUVFUVQUUIUURQUUJUUSQYLKJYMVAZYJIUUIUURUMUNUVQ + UUOUVDUUPUVEUVQUUNUVCUUEUVQUUAUVBUUMUVQYSUUTYTUVADGYLKUMYLKUOUPVBUQUVQU + UIUURUVRURUSUTYMLQZUUSUVHUVFUVNUVSUURUVGQUUSUVHQYMLJKVCZYJIUURUVGUMUNUV + SUVDUVLUVEUVMUVSUUEUVKUVCUVSUUCUVIUUDUVJEHYMLUMYMLUOUPVBUVSUURUVGUVTURU + SUTYKCRZYLDRZYMERZVDZYOYJUUHVEZUUHUWDUDYOUWEUWDUDUHZYJRZUWFYNIVFZSZUWGU + WFUUHRZSUWFYORZUWFUWERUWDUWGUWHUWJUWGUWFUEUHZUFUHZUGUHZUIZQZUGEVGZUFDVG + UECVGUWDUWHUWJVPZUEUFUGUWFCDEVHUWDUWQUWRUEUFCDUWDUWLCRZUWMDRZSZSZUWPUWR + UGEUXBUWNERZSZUWRUWPUWSUWTUXCVDZUWDUWLYKFVFZUEUAVIZTZUWMYLGVFZUFUBVIZTZ + UWNYMHVFZUGUCVIZTZVDZUWLYKVJUWMYLVJUWNYMVJVKZSZVDZUWSUXFSZUXGTZUWTUXISZ + UXJTZUXCUXLSZUXMTZVDZUXPSZVPUXRUXEUWDSZUXQSZUXDUYFUXEUWDUXQVLUXDUXQUYHU + YFUXDUYGUXQUXDUXEUWDUXDUWSUWTUXCUWDUWSUWTUXCVMZUWDUWSUWTUXCVNZUXBUXCVOZ + WFUWDUXAUXCVQVRVSUXDUXOUYEUXPUXDUXHUXTUXKUYBUXNUYDUXDUXFUXSUXGUXDUWSUXF + UYIVSVTUXDUXIUYAUXJUXDUWTUXIUYJVSVTUXDUXLUYCUXMUXDUXCUXLUYKVSVTWAWBWCWD + UWPUWHUXRUWJUYFUWPUWHUWOYNIVFUXRUWFUWOYNIWGABCDEFGHIUBUCUEUFUGUAMWEWHUW + PUWJUWOUUHRZUYFUWFUWOUUHWIUYLUWOUUFRZUWOYNVJZSUYFUWOUUFYNWJUYMUYEUYNUXP + UYMUWLYRRZUWMUUARZUWNUUERZVDUYEUWLUWMUWNYRUUAUUEWKUYOUXTUYPUYBUYQUYDUYO + UWLYPRZUWLYQRZTUXTUWLYPYQXFUYRUXSUYSUXGUYRUXSVPUACWLFYKUWLUEWMZWNWOUEYK + WPWQWRUYPUWMYSRZUWMYTRZTUYBUWMYSYTXFVUAUYAVUBUXJVUAUYAVPUBDWLGYLUWMUFWM + ZWNWOUFYLWPWQWRUYQUWNUUCRZUWNUUDRZTUYDUWNUUCUUDXFVUDUYCVUEUXMVUDUYCVPUC + EWLHYMUWNUGWMZWNWOUGYMWPWQWRWSWRUWLUWMUWNYKYLYMUYTVUCVUFWTXAWRWHXGXBXCX + DXEXHYNWLRUWKUWIVPYKYLYMXIYJWLIYNUWFUDWMWNXJUWFYJUUHXKXLXMUWDUUHYJXNUWE + UUHQUWDUUFYJUUGUWDUUBYIXNZUUEEXNZUUFYJXNUWDYRCXNZUUADXNZVUGUWAUWBVUIUWC + UWAYPYQCYPCXNUWACFYKXOXPYKCXQXRXSUWBUWAVUJUWCUWBYSYTDYSDXNUWBDGYLXOXPYL + DXQXRXTYRCUUADYAYBUWCUWAVUHUWBUWCUUCUUDEUUCEXNUWCEHYMXOXPYMEXQXRYCUUBYI + UUEEYAYBYDUUHYJYGYEYHYF $. $} ${ @@ -540532,35 +540474,141 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $= $( Show that the triple order is set-like. (Contributed by Scott Fenton, 21-Aug-2024.) $) sexp3 $p |- ( ph -> U Se ( ( A X. B ) X. C ) ) $= - ( va vb vc cpred cvv wcel vp cxp cv wral wse cop wceq wrex elxpxp wa wi - w3a df-3an csn cdif xpord3pred adantl simpr1 adantr setlikespec syl2anc - cun vsnex a1i unexd simpr2 simpr3 difexd eqeltrd predeq3 eleq1d biimprd - xpexd com12 syl sylan2br anassrs rexlimdva rexlimdvva biimtrid ralrimiv - dfse3 sylibr ) ADEUBFUBZJUAUCZRZSTZUAWDUDWDJUEAWGUAWDWEWDTWEOUCZPUCZUFQ - UCZUFZUGZQFUHZPEUHODUHAWGOPQWEDEFUIAWMWGOPDEAWHDTZWIETZUJZUJWLWGQFAWPWJ - FTZWLWGUKZWPWQUJAWNWOWQULZWRWNWOWQUMAWSUJZWDJWKRZSTZWRWTXADGWHRZWHUNZVB - ZEHWIRZWIUNZVBZUBZFIWJRZWJUNZVBZUBZWKUNZUOZSWSXAXOUGABCDEFGHIJWHWIWJKUP - UQWTXMXNSWTXIXLSSWTXEXHSSWTXCXDSSWTWNDGUEZXCSTAWNWOWQURAXPWSLUSDGWHUTVA - XDSTWTOVCVDVEWTXFXGSSWTWOEHUEZXFSTAWNWOWQVFAXQWSMUSEHWIUTVAXGSTWTPVCVDV - EVMWTXJXKSSWTWQFIUEZXJSTAWNWOWQVGAXRWSNUSFIWJUTVAXKSTWTQVCVDVEVMVHVIWLX - BWGWLWGXBWLWFXASWDJWEWKVJVKVLVNVOVPVQVRVSVTWAUAWDJWBWC $. - $} - - ${ - $d A a $. $d a b $. $d A b $. $d a c $. $d A c $. $d a d $. - $d A d $. $d a e $. $d A e $. $d a f $. $d A f $. $d a ps $. - $d a rh $. $d a th $. $d A x $. $d A y $. $d B a $. $d B b $. - $d b c $. $d B c $. $d b ch $. $d b d $. $d B d $. $d b e $. - $d B e $. $d b f $. $d B f $. $d b mu $. $d b th $. $d B x $. - $d B y $. $d C a $. $d C b $. $d C c $. $d c d $. $d C d $. - $d c e $. $d C e $. $d c f $. $d C f $. $d c la $. $d c th $. - $d C x $. $d C y $. $d ch f $. $d d e $. $d d f $. $d d ph $. - $d d ta $. $d e et $. $d e f $. $d e ps $. $d e ze $. $d f si $. - $d R d $. $d R e $. $d R f $. $d R x $. $d R y $. $d S d $. - $d S e $. $d S f $. $d S x $. $d S y $. $d T d $. $d T e $. - $d T f $. $d T x $. $d T y $. $d U a $. $d U b $. $d U c $. - $d U d $. $d U e $. $d U f $. $d X a $. $d X b $. $d X c $. - $d x y $. $d Y b $. $d Y c $. $d Z c $. + ( va vb vc cpred cvv wcel vp cxp cv wral wse cotp wceq wrex el2xptp w3a + df-3an csn cun cdif xpord3pred adantl simpr1 adantr setlikespec syl2anc + wa wi vsnex a1i unexd simpr2 xpexd simpr3 difexd eqeltrd predeq3 eleq1d + syl5ibrcom sylan2br rexlimdva rexlimdvva biimtrid ralrimiv dfse3 sylibr + anassrs ) ADEUBFUBZJUAUCZRZSTZUAWBUDWBJUEAWEUAWBWCWBTWCOUCZPUCZQUCZUFZU + GZQFUHZPEUHODUHAWEOPQWCDEFUIAWKWEOPDEAWFDTZWGETZVAZVAWJWEQFAWNWHFTZWJWE + VBZWNWOVAAWLWMWOUJZWPWLWMWOUKAWQVAZWEWJWBJWIRZSTWRWSDGWFRZWFULZUMZEHWGR + ZWGULZUMZUBZFIWHRZWHULZUMZUBZWIULZUNZSWQWSXLUGABCDEFGHIJWFWGWHKUOUPWRXJ + XKSWRXFXISSWRXBXESSWRWTXASSWRWLDGUEZWTSTAWLWMWOUQAXMWQLURDGWFUSUTXASTWR + OVCVDVEWRXCXDSSWRWMEHUEZXCSTAWLWMWOVFAXNWQMUREHWGUSUTXDSTWRPVCVDVEVGWRX + GXHSSWRWOFIUEZXGSTAWLWMWOVHAXOWQNURFIWHUSUTXHSTWRQVCVDVEVGVIVJWJWDWSSWB + JWCWIVKVLVMVNWAVOVPVQVRUAWBJVSVT $. + $} + + ${ + $d A a b c d e f $. $d A x y $. $d B a b c d e f $. $d B x y $. + $d C a b c d e f $. $d C x y $. $d R d e f $. $d R x y $. + $d S d e f $. $d S x y $. $d T d e f $. $d T x y $. + $d U a b c d e f $. $d X a b c $. $d Y b c $. $d Z c $. + $d ka a b c d e f $. $d ps a $. $d rh a $. $d th a $. $d ch b f $. + $d mu b $. $d th b $. $d la c $. $d th c $. $d ph d $. $d ta d $. + $d et e $. $d ps e $. $d ze e $. $d ka f $. $d si f $. + xpord3indd.x $e |- ( ka -> X e. A ) $. + xpord3indd.y $e |- ( ka -> Y e. B ) $. + xpord3indd.z $e |- ( ka -> Z e. C ) $. + xpord3indd.1 $e |- ( ka -> R Fr A ) $. + xpord3indd.2 $e |- ( ka -> R Po A ) $. + xpord3indd.3 $e |- ( ka -> R Se A ) $. + xpord3indd.4 $e |- ( ka -> S Fr B ) $. + xpord3indd.5 $e |- ( ka -> S Po B ) $. + xpord3indd.6 $e |- ( ka -> S Se B ) $. + xpord3indd.7 $e |- ( ka -> T Fr C ) $. + xpord3indd.8 $e |- ( ka -> T Po C ) $. + xpord3indd.9 $e |- ( ka -> T Se C ) $. + xpord3indd.10 $e |- ( a = d -> ( ph <-> ps ) ) $. + xpord3indd.11 $e |- ( b = e -> ( ps <-> ch ) ) $. + xpord3indd.12 $e |- ( c = f -> ( ch <-> th ) ) $. + xpord3indd.13 $e |- ( a = d -> ( ta <-> th ) ) $. + xpord3indd.14 $e |- ( b = e -> ( et <-> ta ) ) $. + xpord3indd.15 $e |- ( b = e -> ( ze <-> th ) ) $. + xpord3indd.16 $e |- ( c = f -> ( si <-> ta ) ) $. + xpord3indd.17 $e |- ( a = X -> ( ph <-> rh ) ) $. + xpord3indd.18 $e |- ( b = Y -> ( rh <-> mu ) ) $. + xpord3indd.19 $e |- ( c = Z -> ( mu <-> la ) ) $. + xpord3indd.i $e |- ( ( ka /\ ( a e. A /\ b e. B /\ c e. C ) ) -> + ( ( ( A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) + A. f e. Pred ( T , C , c ) th /\ + A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) ch /\ + A. d e. Pred ( R , A , a ) A. f e. Pred ( T , C , c ) ze ) + /\ + ( A. d e. Pred ( R , A , a ) ps /\ + A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ta /\ + A. e e. Pred ( S , B , b ) si ) /\ + A. f e. Pred ( T , C , c ) et ) + -> ph ) ) $. + $( Induction over the triple cross product ordering. Note that the + substitutions cover all possible cases of membership in the + predecessor class. (Contributed by Scott Fenton, 2-Feb-2025.) $) + xpord3indd $p |- ( ka -> la ) $= + ( cxp wfr wpo wse wcel wi frxp3 poxp3 sexp3 cv cotp cpred bi2.04 3albii + wal w3a 19.21v 2albii albii bitri wa wne w3o csn cun wral adantl bitrdi + vex wss ssun1 ssralv ax-mp ralimi syl wn weq predpoirr eleq1 syl5ibrcom + wceq notbid necon2ad imp 3mix3d pm2.27 ralimdva ralimdv mpd ssun2 biidd + adantr neeq1 3orbi123d equcoms bicomd imbi12d ralsn sylib 3mix2d ralbii + wb ralbidv 3jca 2ralbidv imbi2d xpord3pred eleq2d imbi1d eldifsn otelxp + cdif otthne anbi12i imbi1i impexp albidv 2albidv bicomi 2ralbii equcomi + r3al 3mix1d bicom1 3syl ex syld sylbid expcom a2d biimtrid frpoins3xp3g + syl33anc pm2.43i ) LKLOPVOQVOZUAVPUVIUAVQUVIUAVRUDOVSUEPVSUFQVSLKVTZLMN + OPQRSTUAUKUOURVAWALMNOPQRSTUAUKUPUSVBWBLMNOPQRSTUAUKUQUTVCWCULUMUNLAVTZ + LBVTLCVTLDVTZLIVTLJVTUVJUGUHUIUJUCUBOPQUAUDUEUFUJWDZUBWDZUCWDZWEZUVIUAU + GWDZUHWDZUIWDZWEZWFZVSZUVLVTZUCWIUBWIUJWIZLUWBDVTZUCWIZUBWIZUJWIZVTZUVQ + OVSUVRPVSUVSQVSWJZUVKUWDLUWEVTZUCWIZUBWIUJWIZUWIUWCUWKUJUBUCUWBLDWGWHUW + MLUWFVTZUBWIZUJWIZUWIUWLUWNUJUBLUWEUCWKWLUWPLUWGVTZUJWIUWIUWOUWQUJLUWFU + BWKWMLUWGUJWKWNWNWNUWJLUWHALUWJUWHAVTLUWJWOZUWHUVMUVQWPZUVNUVRWPZUVOUVS + WPZWQZDVTZUCQTUVSWFZUVSWRZWSZWTZUBPSUVRWFZUVRWRZWSZWTZUJORUVQWFZUVQWRZW + SZWTZAUWRUWHUVMUXNVSUVNUXJVSUVOUXFVSWJZUXCVTZUCWIZUBWIUJWIZUXOUWRUWFUXR + UJUBUWRUWEUXQUCUWRUWEUXPUXBWOZDVTZUXQUWRUWEUVPUXNUXJVOUXFVOZUVTWRUUFZVS + ZDVTUYAUWRUWBUYDDUWRUWAUYCUVPUWJUWAUYCXOLMNOPQRSTUAUVQUVRUVSUKUUAXAUUBU + UCUYDUXTDUYDUVPUYBVSZUVPUVTWPZWOUXTUVPUYBUVTUUDUYEUXPUYFUXBUVMUVNUVOUXN + UXJUXFUUEUVMUVNUVOUVQUVRUVSUJXCUBXCUCXCUUGUUHWNUUIXBUXPUXBDUUJXBUUKUULU + XOUXSUXCUJUBUCUXNUXJUXFUUPUUMXBUWRUXODUCUXDWTZUBUXHWTZUJUXLWTZCUBUXHWTZ + UJUXLWTZGUCUXDWTZUJUXLWTZWJZBUJUXLWTZEUCUXDWTZUBUXHWTZHUBUXHWTZWJZFUCUX + DWTZWJZALUXOVUAVTUWJLUXOVUALUXOWOZUYNUYSUYTVUBUYIUYKUYMVUBUXCUCUXDWTZUB + UXHWTZUJUXLWTZUYIUXOVUELUXOVUDUJUXNWTZVUEUXKVUDUJUXNUXKVUCUBUXJWTZVUDUX + GVUCUBUXJUXDUXFXDUXGVUCVTUXDUXEXEUXCUCUXDUXFXFXGXHZUXHUXJXDZVUGVUDVTUXH + UXIXEZVUCUBUXHUXJXFXGXIXHZUXLUXNXDZVUFVUEVTUXLUXMXEZVUDUJUXLUXNXFXGXIXA + LVUEUYIVTUXOLVUDUYHUJUXLLVUCUYGUBUXHLUXCDUCUXDLUVOUXDVSZWOZUXBUXCDVTVUO + UXAUWSUWTLVUNUXALVUNUVOUVSLVUNXJUCUIXKZUVSUXDVSZXJZLQTVQVURVBQTUVSXLXIV + UPVUNVUQUVOUVSUXDXMXPXNXQXRZXSUXBDXTXIYAYBYBYFYCVUBUWSUWTUVSUVSWPZWQZCV + TZUBUXHWTZUJUXLWTZUYKUXOVVDLUXOUXCUCUXEWTZUBUXHWTZUJUXLWTZVVDUXOVVFUJUX + NWTZVVGUXKVVFUJUXNUXKVVEUBUXJWTZVVFUXGVVEUBUXJUXEUXFXDUXGVVEVTUXEUXDYDU + XCUCUXEUXFXFXGXHZVUIVVIVVFVTVUJVVEUBUXHUXJXFXGXIXHZVULVVHVVGVTVUMVVFUJU + XLUXNXFXGXIVVEVVBUJUBUXLUXHUXCVVBUCUVSUIXCZVUPUXBVVADCVUPUWSUWSUWTUWTUX + AVUTVUPUWSYEVUPUWTYEZUVOUVSUVSYGZYHVUPCDCDYPUIUCVFYIYJYKYLZUUNYMXALVVDU + YKVTUXOLVVCUYJUJUXLLVVBCUBUXHLUVNUXHVSZWOZVVAVVBCVTVVQUWTUWSVUTLVVPUWTL + VVPUVNUVRLVVPXJUBUHXKZUVRUXHVSZXJZLPSVQVVTUSPSUVRXLXIVVRVVPVVSUVNUVRUXH + XMXPXNXQXRZYNVVACXTXIYAYBYFYCVUBUWSUVRUVRWPZUXAWQZGVTZUCUXDWTZUJUXLWTZU + YMUXOVWFLUXOVUCUBUXIWTZUJUXLWTZVWFUXOVWGUJUXNWTZVWHUXKVWGUJUXNUXKVUGVWG + VUHUXIUXJXDZVUGVWGVTUXIUXHYDZVUCUBUXIUXJXFXGXIXHZVULVWIVWHVTVUMVWGUJUXL + UXNXFXGXIVWGVWEUJUXLVUCVWEUBUVRUHXCZVVRUXCVWDUCUXDVVRUXBVWCDGVVRUWSUWSU + WTVWBUXAUXAVVRUWSYEZUVNUVRUVRYGZVVRUXAYEZYHVVRGDGDYPUHUBVIYIYJYKYQYLYOY + MXALVWFUYMVTUXOLVWEUYLUJUXLLVWDGUCUXDVUOVWCVWDGVTVUOUXAUWSVWBVUSXSVWCGX + TXIYAYBYFYCYRVUBUYOUYQUYRVUBUWSVWBVUTWQZBVTZUJUXLWTZUYOUXOVWSLUXOVVEUBU + XIWTZUJUXLWTZVWSUXOVWTUJUXNWTZVXAUXKVWTUJUXNUXKVVIVWTVVJVWJVVIVWTVTVWKV + VEUBUXIUXJXFXGXIXHVULVXBVXAVTVUMVWTUJUXLUXNXFXGXIVWTVWRUJUXLVWTVVBUBUXI + WTVWRVVEVVBUBUXIVVOYOVVBVWRUBUVRVWMVVRVVAVWQCBVVRUWSUWSUWTVWBVUTVUTVWNV + WOVVRVUTYEYHVVRBCBCYPUHUBVEYIYJYKYLWNYOYMXALVWSUYOVTUXOLVWRBUJUXLLUVMUX + LVSZWOZVWQVWRBVTVXDUWSVWBVUTLVXCUWSLVXCUVMUVQLVXCXJUJUGXKZUVQUXLVSZXJZL + ORVQVXGUPORUVQXLXIVXEVXCVXFUVMUVQUXLXMXPXNXQXRUUQVWQBXTXIYAYFYCVUBUVQUV + QWPZUWTUXAWQZEVTZUCUXDWTZUBUXHWTZUYQUXOVXLLUXOVUDUJUXMWTZVXLUXOVUFVXMVU + KUXMUXNXDZVUFVXMVTUXMUXLYDZVUDUJUXMUXNXFXGXIVUDVXLUJUVQUGXCZVXEUXCVXJUB + UCUXHUXDVXEUXBVXIDEVXEUWSVXHUWTUWTUXAUXAUVMUVQUVQYGVXEUWTYEVXEUXAYEYHVX + EEDEDYPUGUJVGYIYJYKZYSYLYMXALVXLUYQVTUXOLVXKUYPUBUXHLVXJEUCUXDVUOVXIVXJ + EVTVUOUXAVXHUWTVUSXSVXIEXTXIYAYBYFYCVUBVXHUWTVUTWQZHVTZUBUXHWTZUYRUXOVX + TLUXOVVFUJUXMWTZVXTUXOVVHVYAVVKVXNVVHVYAVTVXOVVFUJUXMUXNXFXGXIVYAVXJUCU + XEWTZUBUXHWTZVXTVVFVYCUJUVQVXPVXEUXCVXJUBUCUXHUXEVXQYSYLVYBVXSUBUXHVXJV + XSUCUVSVVLVUPVXIVXREHVUPVXHVXHUWTUWTUXAVUTVUPVXHYEVVMVVNYHEHYPUIUCUIUCX + KZHEVJYJYIYKYLYOWNYMXALVXTUYRVTUXOLVXSHUBUXHVVQVXRVXSHVTVVQUWTVXHVUTVWA + YNVXRHXTXIYAYFYCYRVUBVXHVWBUXAWQZFVTZUCUXDWTZUYTUXOVYGLUXOVWGUJUXMWTZVY + GUXOVWIVYHVWLVXNVWIVYHVTVXOVWGUJUXMUXNXFXGXIVYHVXKUBUXIWTZVYGVWGVYIUJUV + QVXPVXEUXCVXJUBUCUXIUXDVXQYSYLVXKVYGUBUVRVWMVVRVXJVYFUCUXDVVRVXIVYEEFVV + RVXHVXHUWTVWBUXAUXAVVRVXHYEVWOVWPYHVVRUHUBXKZFEYPEFYPUBUHUUOVHFEUURUUSY + KYQYLWNYMXALVYGUYTVTUXOLVYFFUCUXDVUOVYEVYFFVTVUOUXAVXHVWBVUSXSVYEFXTXIY + AYFYCYRUUTYFVNUVAUVBUVCUVDUVEUGUJXKABLVDYTVYJBCLVEYTVYDCDLVFYTUVQUDXOAI + LVKYTUVRUEXOIJLVLYTUVSUFXOJKLVMYTUVFUVGUVH $. + $} + + ${ + $d A a b c d e f $. $d A x y $. $d B a b c d e f $. $d B x y $. + $d C a b c d e f $. $d C x y $. $d R d e f $. $d R x y $. + $d S d e f $. $d S x y $. $d T d e f $. $d T x y $. + $d U a b c d e f $. $d X a b c d e f $. $d Y a b c d e f $. + $d Z a b c d e f $. $d a ps $. $d a rh $. $d a th $. $d b ch $. + $d b mu $. $d b th $. $d c la $. $d c th $. $d ch f $. $d d ph $. + $d d ta $. $d e et $. $d e ps $. $d e ze $. $d f si $. xpord3ind.1 $e |- R Fr A $. xpord3ind.2 $e |- R Po A $. xpord3ind.3 $e |- R Se A $. @@ -540595,61 +540643,12 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $= substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 4-Sep-2024.) $) xpord3ind $p |- ( ( X e. A /\ Y e. B /\ Z e. C ) -> la ) $= - ( cxp wfr wpo wse w3a wcel wtru a1i frxp3 mptru poxp3 sexp3 3pm3.2i cop - cv cpred wal wne w3o csn cun wral cdif xpord3pred eleq2d imbi1d eldifsn - wi ot2elxp vex otthne anbi12i bitri imbi1i impexp bitr2i bitr4di albidv - wa 2albidv wss ssun1 ssralv ax-mp ralimi syl wn predpoirr eleq1w mtbiri - weq necon2ai 3mix3d pm2.27 ralimia ssun2 biidd 3orbi123d bicomd equcoms - neeq1 wb imbi12d ralsn sylib 3mix2d ralbidv ralbii 3jca 2ralbidv equcom - r3al 2ralimi 3syl 2ralbii bicom 3imtr3i 3mix1d syl5 sylbid frpoins3xp3g - mpan ) NOVKPVKZTVLZUUMTVMZUUMTVNZVOUCNVPUDOVPUEPVPVOKUUNUUOUUPUUNVQLMNO - PQRSTUJNQVLVQUKVRORVLVQUNVRPSVLVQUQVRVSVTUUOVQLMNOPQRSTUJNQVMZVQULVRORV - MZVQUOVRPSVMZVQURVRWAVTUUPVQLMNOPQRSTUJNQVNVQUMVRORVNVQUPVRPSVNVQUSVRWB - VTWCABCDIJKUFUGUHUIUBUANOPTUCUDUEUFWEZNVPUGWEZOVPUHWEZPVPVOZUIWEZUAWEZW - DUBWEZWDZUUMTUUTUVAWDUVBWDZWFZVPZDWRZUBWGZUAWGUIWGZUVDUUTWHZUVEUVAWHZUV - FUVBWHZWIZDWRZUBPSUVBWFZUVBWJZWKZWLZUAORUVAWFZUVAWJZWKZWLZUINQUUTWFZUUT - WJZWKZWLZAUVCUVMUVDUWIVPUVEUWEVPUVFUWAVPVOZUVRWRZUBWGZUAWGUIWGUWJUVCUVL - UWMUIUAUVCUVKUWLUBUVCUVKUVGUWIUWEVKUWAVKZUVHWJWMZVPZDWRZUWLUVCUVJUWPDUV - CUVIUWOUVGLMNOPQRSTUUTUVAUVBUJWNWOWPUWQUWKUVQXIZDWRUWLUWPUWRDUWPUVGUWNV - PZUVGUVHWHZXIUWRUVGUWNUVHWQUWSUWKUWTUVQUVDUVEUVFUWIUWEUWAWSUVDUVEUVFUUT - UVAUVBUIWTUAWTUBWTXAXBXCXDUWKUVQDXEXFXGXHXJUVRUIUAUBUWIUWEUWAUUBXGUWJDU - BUVSWLZUAUWCWLUIUWGWLZCUAUWCWLZUIUWGWLZGUBUVSWLZUIUWGWLZVOZBUIUWGWLZEUB - UVSWLZUAUWCWLZHUAUWCWLZVOZFUBUVSWLZVOUVCAUWJUXGUXLUXMUWJUXBUXDUXFUWJUWF - UIUWGWLZUVRUBUVSWLZUAUWCWLZUIUWGWLUXBUWGUWIXKUWJUXNWRUWGUWHXLUWFUIUWGUW - IXMXNZUWFUXPUIUWGUWFUWBUAUWCWLZUXPUWCUWEXKUWFUXRWRUWCUWDXLUWBUAUWCUWEXM - XNZUWBUXOUAUWCUVSUWAXKUWBUXOWRUVSUVTXLUVRUBUVSUWAXMXNZXOXPZXOUXOUXAUIUA - UWGUWCUVRDUBUVSUVFUVSVPZUVQUVRDWRUYBUVPUVNUVOUYBUVFUVBUBUHYAZUYBUVBUVSV - PZUUSUYDXQURPSUVBXRXNUBUHUVSXSXTYBZYCUVQDYDXPYEUUCUUDUWJUVNUVOUVBUVBWHZ - WIZCWRZUAUWCWLZUIUWGWLZUXDUWJUVRUBUVTWLZUAUWCWLZUIUWGWLZUYJUWJUXNUYMUXQ - UWFUYLUIUWGUWFUXRUYLUXSUWBUYKUAUWCUVTUWAXKUWBUYKWRUVTUVSYFUVRUBUVTUWAXM - XNZXOXPZXOXPUYKUYHUIUAUWGUWCUVRUYHUBUVBUHWTZUYCUVQUYGDCUYCUVNUVNUVOUVOU - VPUYFUYCUVNYGUYCUVOYGZUVFUVBUVBYKZYHDCYLUHUBUHUBYAZCDVBYIYJYMYNZUUEYOUY - IUXCUIUWGUYHCUAUWCUVEUWCVPZUYGUYHCWRVUAUVOUVNUYFVUAUVEUVAUAUGYAZVUAUVAU - WCVPZUURVUCXQUOORUVAXRXNUAUGUWCXSXTYBZYPUYGCYDXPYEXOXPUWJUVNUVAUVAWHZUV - PWIZGWRZUBUVSWLZUIUWGWLZUXFUWJUXOUAUWDWLZUIUWGWLZVUIUWJUXNVUKUXQUWFVUJU - IUWGUWFUWBUAUWDWLZVUJUWDUWEXKUWFVULWRUWDUWCYFUWBUAUWDUWEXMXNZUWBUXOUAUW - DUXTXOXPZXOXPVUJVUHUIUWGUXOVUHUAUVAUGWTZVUBUVRVUGUBUVSVUBUVQVUFDGVUBUVN - UVNUVOVUEUVPUVPVUBUVNYGZUVEUVAUVAYKZVUBUVPYGZYHUGUAYAZGDYLVUBDGYLVEUGUA - UUAGDUUFUUGYMYQYNYRYOVUHUXEUIUWGVUGGUBUVSUYBVUFVUGGWRUYBUVPUVNVUEUYEYCV - UFGYDXPYEXOXPYSUWJUXHUXJUXKUWJUVNVUEUYFWIZBWRZUIUWGWLZUXHUWJUYKUAUWDWLZ - UIUWGWLZVVBUWJUXNVVDUXQUWFVVCUIUWGUWFVULVVCVUMUWBUYKUAUWDUYNXOXPXOXPVVC - VVAUIUWGVVCUYHUAUWDWLVVAUYKUYHUAUWDUYTYRUYHVVAUAUVAVUOVUBUYGVUTCBVUBUVN - UVNUVOVUEUYFUYFVUPVUQVUBUYFYGYHCBYLUGUAVUSBCVAYIYJYMYNXCYRYOVVABUIUWGUV - DUWGVPZVUTVVABWRVVEUVNVUEUYFVVEUVDUUTUIUFYAZVVEUUTUWGVPZUUQVVGXQULNQUUT - XRXNUIUFUWGXSXTYBUUHVUTBYDXPYEXPUWJUUTUUTWHZUVOUVPWIZEWRZUBUVSWLZUAUWCW - LZUXJUWJUXPUIUWHWLZVVLUWJUWFUIUWHWLZVVMUWHUWIXKUWJVVNWRUWHUWGYFUWFUIUWH - UWIXMXNZUWFUXPUIUWHUYAXOXPUXPVVLUIUUTUFWTZVVFUVRVVJUAUBUWCUVSVVFUVQVVID - EVVFUVNVVHUVOUVOUVPUVPUVDUUTUUTYKVVFUVOYGVVFUVPYGYHVVFEDEDYLUFUIVCYJYIY - MZYTYNYOVVKUXIUAUWCVVJEUBUVSUYBVVIVVJEWRUYBUVPVVHUVOUYEYCVVIEYDXPYEXOXP - UWJVVHUVOUYFWIZHWRZUAUWCWLZUXKUWJUYLUIUWHWLZVVTUWJVVNVWAVVOUWFUYLUIUWHU - YOXOXPVWAVVJUBUVTWLZUAUWCWLZVVTUYLVWCUIUUTVVPVVFUVRVVJUAUBUWCUVTVVQYTYN - VWBVVSUAUWCVVJVVSUBUVBUYPUYCVVIVVREHUYCVVHVVHUVOUVOUVPUYFUYCVVHYGUYQUYR - YHEHYLUHUBUYSHEVFYIYJYMYNYRXCYOVVSHUAUWCVUAVVRVVSHWRVUAUVOVVHUYFVUDYPVV - RHYDXPYEXPYSUWJVVHVUEUVPWIZFWRZUBUVSWLZUXMUWJVUJUIUWHWLZVWFUWJVVNVWGVVO - UWFVUJUIUWHVUNXOXPVWGVVKUAUWDWLZVWFVUJVWHUIUUTVVPVVFUVRVVJUAUBUWDUVSVVQ - YTYNVVKVWFUAUVAVUOVUBVVJVWEUBUVSVUBVVIVWDEFVUBVVHVVHUVOVUEUVPUVPVUBVVHY - GVUQVURYHVUBFEFEYLUGUAVDYJYIYMYQYNXCYOVWEFUBUVSUYBVWDVWEFWRUYBUVPVVHVUE - UYEYCVWDFYDXPYEXPYSVJUUIUUJUTVAVBVGVHVIUUKUUL $. + ( wcel w3a simp1 simp2 simp3 wfr a1i wpo wse cv cpred adantl xpord3indd + wral wi ) ABCDEFGHIJKUCNVKZUDOVKZUEPVKZVLZLMNOPQRSTUAUBUCUDUEUFUGUHUIUJ + WFWGWHVMWFWGWHVNWFWGWHVONQVPWIUKVQNQVRWIULVQNQVSWIUMVQORVPWIUNVQORVRWIU + OVQORVSWIUPVQPSVPWIUQVQPSVRWIURVQPSVSWIUSVQUTVAVBVCVDVEVFVGVHVIUFVTZNVK + UGVTZOVKUHVTZPVKVLDUBPSWLWAZWDUAORWKWAZWDUINQWJWAZWDCUAWNWDUIWOWDGUBWMW + DUIWOWDVLBUIWOWDEUBWMWDUAWNWDHUAWNWDVLFUBWMWDVLAWEWIVJWBWC $. $} $} @@ -540961,14 +540960,10 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $= $} ${ - $d a b $. $d a c $. $d a d $. $d a e $. $d a f $. $d a ps $. - $d a rh $. $d a th $. $d a x $. $d a y $. $d b c $. $d b ch $. - $d b d $. $d b e $. $d b f $. $d b mu $. $d b th $. $d b x $. - $d b y $. $d c d $. $d c e $. $d c f $. $d c la $. $d c th $. - $d c x $. $d c y $. $d ch f $. $d d e $. $d d f $. $d d ph $. - $d d ta $. $d d x $. $d d y $. $d e et $. $d e f $. $d e ps $. - $d e x $. $d e y $. $d e ze $. $d f si $. $d f x $. $d f y $. - $d X a $. $d X b $. $d X c $. $d x y $. $d Y b $. $d Y c $. $d Z c $. + $d X a b c d e f $. $d Y a b c d e f $. $d Z a b c d e f $. $d ps a $. + $d rh a $. $d th a b c $. $d ch b f $. $d mu b $. $d la c $. + $d ph d $. $d ta d $. $d et e $. $d ps e $. $d ze e $. $d si f $. + $d a b c d e f x y $. on3ind.1 $e |- ( a = d -> ( ph <-> ps ) ) $. on3ind.2 $e |- ( b = e -> ( ps <-> ch ) ) $. on3ind.3 $e |- ( c = f -> ( ch <-> th ) ) $. @@ -541842,17 +541837,10 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $= $} ${ - $d a b $. $d a c $. $d a d $. $d a e $. $d a f $. $d a ps $. - $d a rh $. $d a th $. $d a w $. $d a x $. $d a y $. $d a z $. - $d b c $. $d b ch $. $d b d $. $d b e $. $d b f $. $d b mu $. - $d b th $. $d b w $. $d b x $. $d b y $. $d b z $. $d c d $. - $d c e $. $d c f $. $d c la $. $d c th $. $d c w $. $d c x $. - $d c y $. $d c z $. $d ch f $. $d d e $. $d d f $. $d d ph $. - $d d ta $. $d d w $. $d d x $. $d d y $. $d d z $. $d e et $. - $d e f $. $d e ps $. $d e w $. $d e x $. $d e y $. $d e z $. - $d e ze $. $d f si $. $d f w $. $d f x $. $d f y $. $d f z $. - $d w x $. $d w y $. $d w z $. $d X a $. $d X b $. $d X c $. $d x y $. - $d x z $. $d Y b $. $d Y c $. $d y z $. $d Z c $. + $d X a b c d e f $. $d Y a b c d e f $. $d Z a b c d e f $. $d ps a $. + $d rh a $. $d th a b c $. $d ch b f $. $d mu b $. $d la c $. + $d ph d $. $d ta d $. $d et e $. $d ps e $. $d ze e $. $d si f $. + $d a b c d e f w x y z $. no3inds.1 $e |- ( a = d -> ( ph <-> ps ) ) $. no3inds.2 $e |- ( b = e -> ( ps <-> ch ) ) $. no3inds.3 $e |- ( c = f -> ( ch <-> th ) ) $. @@ -542540,7 +542528,8 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $= ${ $d A x y z a b c d p q xL yL zL xR yR zR xO yO zO $. - $d B y z a c xL yL zL xR yR zR xO yO zO $. $d C z $. + $d B x y z a c xL yL zL xR yR zR xO yO zO $. + $d C x y z a c xL yL zL xR yR zR xO yO zO $. $( Addition to both sides of surreal less-than or equal. Theorem 5 of [Conway] p. 18. (Contributed by Scott Fenton, 21-Jan-2025.) $) sleadd1 $p |- ( ( A e. No /\ B e. No /\ C e. No ) -> @@ -542866,8 +542855,9 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $= $} ${ - $d A x y z a b c d e f g xO yO zO xL yL zL xR yR zR $. $d B y z $. - $d C z $. + $d A x y z a b c d e f g xO yO zO xL yL zL xR yR zR $. + $d B x y z a b c d e f g xO yO zO xL yL zL xR yR zR $. + $d C x y z a b c d e f g xO yO zO xL yL zL xR yR zR $. $( Surreal addition is associative. Part of theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 22-Jan-2025.) $) addsass $p |- ( ( A e. No /\ B e. No /\ C e. No ) ->