免費論壇 繁體 | 簡體
Sclub交友聊天~加入聊天室當版主
分享
返回列表 发帖

导线段比的形式化的尝试

本帖最后由 hbghlyj 于 2020-5-13 13:44 编辑

尝试把一类线段乘积恒等式的证明过程形式化。欢迎提出更好的方法!
其通式为$A_1B_1\cdot A_2B_2\cdot\cdots\cdot A_nB_n=C_1D_1\cdot C_2D_2\cdot\cdots\cdot C_nD_n$
把它对应为线性方程组$i_{a_1,b_1}+i_{a_2,b_2}\cdot\cdots\cdot i_{a_n,b_n}=i_{c_1,d_1}+i_{c_2,d_2}+\cdots+i_{c_n,d_n}$
并约定$i_{a,b}=i_{b,a}$
一、平行线截线段成比例
我们不会用到AB+BC=AC这样的线段恒等式(因为它出现了线段的和),这意味着,“ABC,ADE共线,BC∥DE"需表示为三个等式
  1. px[a_, b_, c_, d_,
  2.   e_] = {Subscript[i, a, b] - Subscript[i, a, d] ==
  3.    Subscript[i, a, c] - Subscript[i, a, e],
  4.   Subscript[i, b, d] - Subscript[i, a, d] ==
  5.    Subscript[i, c, e] - Subscript[i, a, e],
  6.   Subscript[i, a, b] - Subscript[i, a, d] ==
  7.    Subscript[i, b, c] - Subscript[i, d, e]}
复制代码
二、点列、线束的交比
和上面类似的理由,(a,b;c,d)=(e,f;g,h)需表示为两个等式
  1. cd[a_, b_, c_, d_, e_, f_, g_,
  2.    h_] = {Subscript[i, a, b] - Subscript[i, a, d] - Subscript[i, b,
  3.      c] + Subscript[i, c, d] ==
  4.     Subscript[i, e, f] - Subscript[i, e, h] - Subscript[i, f, g] +
  5.      Subscript[i, g, h],
  6.    Subscript[i, a, c] + Subscript[i, b, d] - Subscript[i, a, d] -
  7.      Subscript[i, b, c] ==
  8.     Subscript[i, e, g] + Subscript[i, f, h] - Subscript[i, e, h] -
  9.      Subscript[i, f, g]};
复制代码
尝试五个点的交比:
  1. blb[{a_, b_}] = Subscript[i, a, b]
  2. list = blb /@ Subsets[{a, b, c, d, e, f, g, h, k, j}, {2}]
  3. blb2[{a_, b_}] = Subscript[i, b, a] -> Subscript[i, a, b]
  4. list2 = blb2 /@ Subsets[{a, b, c, d, e, f, g, h, k, j}, {2}]
  5. eq = Join[cd[a, b, c, d, f, g, h, k], cd[a, b, c, e, f, g, h, j],
  6.    cd[a, b, d, e, f, g, k, j], cd[a, c, d, e, f, h, k, j],
  7.    cd[b, c, d, e, g, h, k, j]] /. list2
  8. Reduce[eq, list]
复制代码
输出:
  1. Subscript[i, g, k] ==
  2.   Subscript[i, a, c] - Subscript[i, a, d] - Subscript[i, b, c] +
  3.    Subscript[i, b, d] - Subscript[i, f, h] + Subscript[i, f, k] +
  4.    Subscript[i, g, h] &&
  5. Subscript[i, g, j] ==
  6.   Subscript[i, a, c] - Subscript[i, a, e] - Subscript[i, b, c] +
  7.    Subscript[i, b, e] - Subscript[i, f, h] + Subscript[i, f, j] +
  8.    Subscript[i, g, h] &&
  9. Subscript[i, h, k] ==
  10.   Subscript[i, a, b] - Subscript[i, a, d] - Subscript[i, b, c] +
  11.    Subscript[i, c, d] - Subscript[i, f, g] + Subscript[i, f, k] +
  12.    Subscript[i, g, h] &&
  13. Subscript[i, h, j] ==
  14.   Subscript[i, a, b] - Subscript[i, a, e] - Subscript[i, b, c] +
  15.    Subscript[i, c, e] - Subscript[i, f, g] + Subscript[i, f, j] +
  16.    Subscript[i, g, h] &&
  17. Subscript[i, k, j] ==
  18.   Subscript[i, a, b] + Subscript[i, a, c] - Subscript[i, a, d] -
  19.    Subscript[i, a, e] - Subscript[i, b, c] + Subscript[i, d, e] -
  20.    Subscript[i, f, g] - Subscript[i, f, h] + Subscript[i, f, j] +
  21.    Subscript[i, f, k] + Subscript[i, g, h]
复制代码
所以将五个点的点列的交比等式表示为五个等式
  1. cd[a_, b_, c_, d_, e_, f_, g_, h_, k_,
  2.   j_] = {Subscript[i, g, k] ==
  3.    Subscript[i, a, c] - Subscript[i, a, d] - Subscript[i, b, c] +
  4.     Subscript[i, b, d] - Subscript[i, f, h] + Subscript[i, f, k] +
  5.     Subscript[i, g, h],
  6.   Subscript[i, g, j] ==
  7.    Subscript[i, a, c] - Subscript[i, a, e] - Subscript[i, b, c] +
  8.     Subscript[i, b, e] - Subscript[i, f, h] + Subscript[i, f, j] +
  9.     Subscript[i, g, h],
  10.   Subscript[i, h, k] ==
  11.    Subscript[i, a, b] - Subscript[i, a, d] - Subscript[i, b, c] +
  12.     Subscript[i, c, d] - Subscript[i, f, g] + Subscript[i, f, k] +
  13.     Subscript[i, g, h],
  14.   Subscript[i, h, j] ==
  15.    Subscript[i, a, b] - Subscript[i, a, e] - Subscript[i, b, c] +
  16.     Subscript[i, c, e] - Subscript[i, f, g] + Subscript[i, f, j] +
  17.     Subscript[i, g, h],
  18.   Subscript[i, k, j] ==
  19.    Subscript[i, a, b] + Subscript[i, a, c] - Subscript[i, a, d] -
  20.     Subscript[i, a, e] - Subscript[i, b, c] + Subscript[i, d, e] -
  21.     Subscript[i, f, g] - Subscript[i, f, h] + Subscript[i, f, j] +
  22.     Subscript[i, f, k] + Subscript[i, g, h]}
复制代码
这里用字母k是防止与i混淆

本帖最后由 hbghlyj 于 2020-5-15 17:30 编辑

新建位图图像.gif
2020-5-15 11:49

(纯3323)$BC\parallel MN,P=FN\cap EM,$,求证\[
\frac{\S{BCE}}{\S{BCF}}\frac{\S{BFP}-\S{BFE}}{\S{CEP}-\S{CEF}}=\frac{\S{BEP}}{\S{CFP}}\]
证明:$\frac{\S{BCE}}{\S{BCF}}\frac{\S{BFP}-\S{BFE}}{\S{CEP}-\S{CEF}}\frac{\S{CFP}}{\S{BEP}}=\frac{ET}{FT}\frac{1+\frac{\S{PEF}}{\S{BPF}}\frac{\S{BPF}}{\S{BEP}}}{1+\frac{\S{PEF}}{\S{CPE}}\frac{\S{CPE}}{\S{CFP}}}=\frac{ET}{FT}\frac{1+\frac{EN}{NB}\frac{FQ}{QE}}{1+\frac{FM}{MC}\frac{ER}{RF}}=\frac{ET}{FT}\frac{1+\frac{ES}{ST}\frac{FQ}{QE}}{1+\frac{FS}{ST}\frac{ER}{RF}}$
等价形式:
QQ图片20200513132152.jpg
2020-5-13 13:22

TOP

本帖最后由 hbghlyj 于 2020-5-14 17:18 编辑

三、面积比
△ABC和△DEF同时内接于圆O,并且同时外切于圆I,X是圆O上任意一点,XA、XD分别交直线EF、BC于P、Q。求证:直线PQ与圆I相切。
新建位图图像.gif
2020-5-14 10:12

The statement is true.

The conclusion is: PARA P Q E F.
This is equivalent to:   (-S(PFE)) = (-S(QFE))
The Machine Proof

(-S(PFE)) / (-S(QFE))

because S(QFE) = (-S(FED)S(MNC)+S(NFE)S(MDC)) / (-S(MNCD))

= (-S(PFE))(-S(MNCD)) / (S(FED)S(MNC)-S(NFE)S(MDC))

because S(PFE) = (S(FEB)S(MNA)+S(NBA)S(MFE)) / S(MNBA)

= (-S(FEB)S(MNA)-S(NBA)S(MFE))(-S(MNCD)) / (S(FED)S(MNC)-S(NFE)S(MDC))S(MNBA)

because S(MNBA) = 1/2(-S(NDAB)+S(NBA))
               S(MDC) = 1/2S(DCA)
               S(MNC) = 1/2(-S(NDC)+S(NCA))
               S(MNCD) = 1/2(-S(NDC)+S(NCDA))
               S(MFE) = 1/2(S(FED)+S(FEA))
               S(MNA) = 1/2(-S(NDA))

= (S(FEB)S(NDA)+(-S(FED)-S(FEA))S(NBA))(S(NDC)-S(NCDA))22 / (-S(DCA)S(NFE)-S(FED)S(NDC)+S(FED)S(NCA))(-S(NDAB)+S(NBA))22

Eliminating the common factors: (2)^{2}

= (S(FEB)S(NDA)+(-S(FED)-S(FEA))S(NBA))(S(NDC)-S(NCDA)) / (S(DCA)S(NFE)+S(FED)S(NDC)-S(FED)S(NCA))(S(NDAB)-S(NBA))

because S(NDAB) = 1/2(-S(DCBA)-S(DBA))
               S(NCA) = 1/2(-S(CBA))
               S(NFE) = 1/2(S(FEC)+S(FEB))
               S(NCDA) = 1/2(-S(DCBA)-S(DCA))
               S(NDC) = 1/2S(DCB)
               S(NBA) = 1/2S(CBA)
               S(NDA) = 1/2(-S(DCA)-S(DBA))

= (-S(CBA)S(FED)+(-S(DCA)-S(DBA))S(FEB)-S(CBA)S(FEA))(S(DCB)+S(DCBA)+S(DCA))22 / ((S(DCB)+S(CBA))S(FED)+S(DCA)S(FEC)+S(DCA)S(FEB))(-S(DCBA)-S(DBA)-S(CBA))22

Eliminating the common factors: (2)^{2}

= -(S(CBA)S(FED)+(S(DCA)+S(DBA))S(FEB)+S(CBA)S(FEA))(S(DCB)+S(DCBA)+S(DCA)) / -((S(DCB)+S(CBA))S(FED)+S(DCA)S(FEC)+S(DCA)S(FEB))(S(DCBA)+S(DBA)+S(CBA))

because S(FEC) = 1/2(-S(EDC))
               S(FEA) = 1/2(-S(EDA)-S(ECA))
               S(FEB) = 1/2(-S(EDB)-S(ECB))
               S(FED) = 1/2S(EDC)

= -(S(CBA)S(EDC)+(-S(DCA)-S(DBA))S(EDB)-S(CBA)S(EDA)+(-S(DCA)-S(DBA))S(ECB)-S(CBA)S(ECA))(S(DCB)+S(DCBA)+S(DCA))2 / -((S(DCB)-S(DCA)+S(CBA))S(EDC)-S(DCA)S(EDB)-S(DCA)S(ECB))(S(DCBA)+S(DBA)+S(CBA))2

Eliminating the common factors: 2

= -(S(CBA)S(EDC)+(-S(DCA)-S(DBA))S(EDB)-S(CBA)S(EDA)+(-S(DCA)-S(DBA))S(ECB)-S(CBA)S(ECA))(S(DCB)+S(DCBA)+S(DCA)) / -((S(DCB)-S(DCA)+S(CBA))S(EDC)-S(DCA)S(EDB)-S(DCA)S(ECB))(S(DCBA)+S(DBA)+S(CBA))

because S(ECA) = 1/2(-S(CBA))
               S(ECB) = 1/2S(CBA)
               S(EDA) = 1/2(-S(DBA))
               S(EDB) = 1/2S(DBA)
               S(EDC) = 1/2(S(DCB)+S(DCA))

= -(S(CBA)S(DCB)-S(DBA)S(DCA)-S(DBA)^{2}+S(CBA)^{2})(S(DCB)+S(DCBA)+S(DCA))2 / -(S(DCB)^{2}+S(CBA)S(DCB)-S(DCA)^{2}-S(DBA)S(DCA))(S(DCBA)+S(DBA)+S(CBA))2

Eliminating the common factors: 2

= -(S(CBA)S(DCB)-S(DBA)S(DCA)-S(DBA)^{2}+S(CBA)^{2})(S(DCB)+S(DCBA)+S(DCA)) / -(S(DCB)^{2}+S(CBA)S(DCB)-S(DCA)^{2}-S(DBA)S(DCA))(S(DCBA)+S(DBA)+S(CBA))

because S(DCBA) = (S(CBA)+S(DCA))
               S(DBA) = S(DBA)
               S(DCA) = S(DCA)
               S(DCB) = (S(CBA)+S(DCA)-S(DBA))

= -(2S(CBA)^{2}+(S(DCA)-S(DBA))S(CBA)-S(DBA)S(DCA)-S(DBA)^{2})(2S(CBA)+3S(DCA)-S(DBA)) / -(2S(CBA)^{2}+(3S(DCA)-3S(DBA))S(CBA)-3S(DBA)S(DCA)+S(DBA)^{2})(2S(CBA)+S(DCA)+S(DBA))

Eliminating the common factors: (2S(CBA)+S(DCA)+S(DBA))(2S(CBA)+3S(DCA)-S(DBA))(S(CBA)-S(DBA))

= 1

TOP

本帖最后由 hbghlyj 于 2020-6-7 00:25 编辑

射影几何命题是否都归结为判定一个图是自对偶的?最简单且经典的就是帕普斯和笛沙格,另一个例子是三线性极点极线也是对偶图13点13线
A对a,P对l,P下标A对l下标a,Q下标A对h下标a,R下标A对g下标a
QQ图片20200607000557.jpg
2020-6-7 00:07

回答:否。
我拿帕斯卡和布列安桑给你拼了一道。因为有“一个三角形的点在另一个三角形的边上”这种新的关系。
等面三面角.png
2020-6-7 00:00

QQ图片20200607000028.png
2020-6-7 00:03
QQ图片20200607000015.png
2020-6-7 00:04

就单说这个图
它是一个纯粹的线-点的图
最后的巧合点的生成,需要这剩下的20个点,18条线的每一个
所以那个叙述是不成立的,如果甚至数量都不一样,就更别提对偶之后能不能一样了
如果对称构造也能嵌入一个对偶图
对称地做了五个pascal和五个brianchon
有五个十个巧合点:五个brianchon,五个神奇巧合
QQ图片20200607000557.jpg
2020-6-7 00:18

所以说,轮换地造出全部命题之后图形还是会自对偶的
我突然意识到每个点的“对偶”用的不是这个点处锥线的切线...
我遍历了把初始的五个点(过五线)对偶给每一个可能的五点共线,都不能把对偶图形包含进来
QQ图片20200607000557.jpg
2020-6-7 00:19

所以虽然这个图点线数量相等,具有相同连接数的点线数量也想等,但是它不能自对偶...
你如果要加“对称地构造”这个条件的话
你得搞清楚这种对称要什么要求我上面那个图的对称群是V_4你这个是S_5
帕普斯的图,站在生成元素的角度上来说是S_3xZ_2
站在整个图的角度上来说是S_3xS_3(大概是吧)
QQ图片20200607000557.jpg
2020-6-7 00:24

如果一个构图的线数等于点数,而且每个点过的线数都一样,是否一定自对偶?书上写的是用点数,线数,每个点上线数(每个点都一样),每个线上点数(每个线都一样)就可以表示一个构图,所以我想这四个数应该已经够确定唯一性了?
回答:否。
如果每个点都过三条线,每条线过三个点那么它只能是帕普斯图吗?
回答:否。Fano平面。再举一个例子,四元集的所有三元子集也满足上面的条件,甚至能嵌入R^3里,一个四面体,元素是点,集合是面,或者反过来。更大一点的例子,任意的n,所有{i,i+1,i+2}组成的三元集,满足条件。


PS:批量上传图片失败了。我用了“Flash修复工具”也失败了。我用普通传图好像也出问题了,我每次传的一个图片,但每次都会显示传了两个重复的

TOP

返回列表 回复 发帖