# 固定基底下的平面向量：逐分量運算、相等判定與減法方向 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-vector/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-vector-01 · production-20261019-adopted-96 ## 目標與範圍 在固定標準基底下，設 u=(3,−1)、v=(−2,4)、w=(1,3)、k=−2。逐分量計算 u+v、u−v、v−u、ku、0u、2u+v；求滿足 u+x=v 的向量 x；核對 k(u+v)=ku+kv；並判定 u=w 與 u=(−1,3) 是否成立。 在 MKO 的範圍內工作：固定標準基底、實數分量與純量，題目用整數的精確數值。示範逐分量運算與逐分量相等，並證明三個一般小引理（u−v=−(v−u)、u+x=v 的唯一解、純量對向量加法的分配律）。不由分量推論長度、角度、單位向量或基底變換；不處理一般向量空間公理或物理單位；不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - cartesian_product_def - add_inverse - distributive - neg_mul - numeric_evaluation - neg_vec_def - G1 — 基底固定為標準基底；向量是分量對 (z₁,z₂)∈ℝ²，加法、減法與純量乘法逐分量進行，兩向量相等當且僅當兩個對應分量都相等，零向量為 (0,0)。 - G2 — u=(3,−1)、v=(−2,4)、w=(1,3)、k=−2（整數分量與整數純量，MKO 假設 a1）。 - G3 — 這裡的有序對代表向量分量，不把幾何點、位置向量與任意座標系混為同一對象（MKO 假設 a2）。 - u=(u_1,u_2) — 以固定標準基底的分量表示的平面向量 - u+v,\ u-v — 逐分量的和與差 - ku — 純量 k 乘向量 u，結果仍是向量 - -z — (−1)z=(−z_1,−z_2) - (0,0) — 零向量 ## 規則與來源 - cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。 - add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。 - distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。 - neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - add_comm · prerequisite — 加法交換律：u+v=v+u。 - eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。 - add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。 - add_zero · prerequisite — 加法單位元：u+0=u。 - mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。 - mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - mko_vector_ops · cited — 在固定標準基底下，平面向量 u=(u₁,u₂)∈R²；u+v=(u₁+v₁,u₂+v₂)，k u=(k u₁,k u₂)，u−v=(u₁−v₁,u₂−v₂)。向量相等當且僅當兩個對應分量相等；零向量為 (0,0)。 · mko-vector - neg_vec_def · prerequisite — 向量的負：−z 表示 (−1)z=(−z₁,−z₂)。 - L_sub_reverse · lemma — 對所有 u、v∈ℝ²：u−v=−(v−u)。 - L_solve_vec · lemma — 對所有 u、v、x∈ℝ²：u+x=v ⇔ x=v−u。 - L_scalar_distrib · lemma — 對所有實數 k 與 u、v∈ℝ²：k(u+v)=ku+kv。 ## 逐步主鏈 S01 · definition操作前 u=(3,-1),\ v=(-2,4),\ w=(1,3),\ k=-2 操作後 u+v=(u_1+v_1,u_2+v_2),\ ku=(ku_1,ku_2),\ u-v=(u_1-v_1,u_2-v_2) 條件：無 規則：mko_vector_ops · 依賴：G1, G2, G3, mko_vector_ops 葉節點依據：mko_vector_ops 基底固定為標準基底，向量就是分量對 (z₁,z₂)∈ℝ²。依 MKO，加法、純量乘法、減法都逐分量進行；兩向量相等當且僅當兩個對應分量都相等；零向量為 (0,0)。這裡的有序對代表向量分量，不當作幾何點。 S02 · equivalent操作前 u+v 操作後 (3+(-2),\,-1+4)=(1,3) 條件：無 規則：mko_vector_ops · 依賴：S01, G2 葉節點依據：mko_vector_ops + numeric_evaluation 逐分量相加：第一分量 3+(−2)=1，第二分量 −1+4=3，所以 u+v=(1,3)。不能把分量混在一起，例如只算全部分量的總和 3+(−1)+(−2)+4=4，那不是向量。 S03 · equivalent操作前 u-v 操作後 (3-(-2),\,-1-4)=(5,-5) 條件：無 規則：mko_vector_ops · 依賴：S01, G2 葉節點依據：mko_vector_ops + numeric_evaluation 逐分量相減，順序是 u 的分量減 v 的分量：3−(−2)=5，−1−4=−5，所以 u−v=(5,−5)。 S04 · equivalent操作前 v-u 操作後 (-2-3,\,4-(-1))=(-5,5) 條件：無 規則：mko_vector_ops · 依賴：S01, G2 葉節點依據：mko_vector_ops + numeric_evaluation 交換順序：v 的分量減 u 的分量，−2−3=−5，4−(−1)=5，所以 v−u=(−5,5)。 S05 · theorem_application操作前 u-v=(5,-5),\ v-u=(-5,5) 操作後 u-v=-(v-u) 條件：無 規則：L_sub_reverse · 依賴：S03, S04, L_sub_reverse 葉節點依據：mko_vector_ops + neg_vec_def + distributive + neg_mul 依引理 L_sub_reverse，u−v=−(v−u)。核對本例：−(v−u)=(−1)(−5,5)=(5,−5)，與 S03 的 u−v 相同。交換減法順序得到相反向量，而不是同一個向量。 S06 · implies操作前 u-v=(5,-5),\ v-u=(-5,5) 操作後 u-v\neq v-u 條件：無 規則：cartesian_product_def · 依賴：S03, S04, cartesian_product_def 葉節點依據：cartesian_product_def + numeric_evaluation 向量相等需要兩個對應分量都相等。第一分量 5≠−5，已經不相等，所以 u−v≠v−u。減法的方向有意義：u−v 與 v−u 是互為相反的兩個向量，只有在 u=v 時才會相同。 S07 · equivalent操作前 u+x=v 操作後 x=v-u=(-5,5) 條件：無 規則：L_solve_vec · 依賴：S04, L_solve_vec, G2 葉節點依據：mko_vector_ops + eq_congruence + add_inverse + add_assoc + add_zero 依引理 L_solve_vec，u+x=v 當且僅當 x=v−u；由 S04，x=(−5,5)。代回核對：u+x=(3+(−5),−1+5)=(−2,4)=v。從 u 到 v 的向量是 v−u，不是 u−v。 S08 · equivalent操作前 ku,\ k=-2 操作後 (-2\cdot 3,\,-2\cdot(-1))=(-6,2) 條件：無 規則：mko_vector_ops · 依賴：S01, G2 葉節點依據：mko_vector_ops + numeric_evaluation + neg_mul 純量乘法逐分量乘 k：−2·3=−6，−2·(−1)=2，所以 ku=(−6,2)。結果仍是 ℝ² 的向量，不是一個數。負純量給出方向反轉的代數表示：ku=2·(−u)，其中 −u=(−3,1)。 S09 · equivalent操作前 0u 操作後 (0\cdot 3,\,0\cdot(-1))=(0,0) 條件：無 規則：mul_zero · 依賴：S01, G2, mul_zero 葉節點依據：mul_zero + mul_comm + mko_vector_ops 純量 0 乘每個分量都得 0（u·0=0 與乘法交換律），所以 0u=(0,0)，即零向量。MKO 第二段：純量零給出零向量。 S10 · equivalent操作前 2u+v 操作後 (6,-2)+(-2,4)=(4,2) 條件：無 規則：mko_vector_ops · 依賴：S01, G2 葉節點依據：mko_vector_ops + numeric_evaluation 先做純量乘法 2u=(6,−2)，再逐分量加 v：6+(−2)=4，−2+4=2，所以 2u+v=(4,2)。要判定 2u+v 是否等於 (4,2)，必須兩個分量都相等，這裡兩者都成立。 S11 · theorem_application操作前 k(u+v),\ ku+kv 操作後 -2(1,3)=(-2,-6)=(-6,2)+(4,-8) 條件：無 規則：L_scalar_distrib · 依賴：S02, S08, L_scalar_distrib 葉節點依據：distributive + mko_vector_ops + numeric_evaluation 依引理 L_scalar_distrib，k(u+v)=ku+kv。核對本例：k(u+v)=−2·(1,3)=(−2,−6)；kv=(−2·(−2),−2·4)=(4,−8)，ku+kv=(−6+4,2+(−8))=(−2,−6)。兩邊逐分量相同（N16、N17）。 S12 · implies操作前 u=(3,-1),\ w=(1,3),\ u_1^2+u_2^2=w_1^2+w_2^2=10 操作後 u\neq w 條件：無 規則：cartesian_product_def · 依賴：G2, cartesian_product_def 葉節點依據：cartesian_product_def + numeric_evaluation u 與 w 有相同的平方和：3²+(−1)²=10=1²+3²（N19）。但向量相等只看對應分量：第一分量 3≠1，所以 u≠w。本條目不由分量推論長度；即使某個由分量算出的數量相同，也不能據此判定相等。 S13 · implies操作前 u=(3,-1),\ (-1,3) 操作後 u\neq(-1,3) 條件：無 規則：cartesian_product_def · 依賴：G2, cartesian_product_def 葉節點依據：cartesian_product_def + numeric_evaluation (−1,3) 用了與 u 相同的兩個數，只是交換位置。分量有固定的位置：u 的第一分量 3，(−1,3) 的第一分量 −1，3≠−1，所以兩者不相等。分量和相同也不夠：u 與 (1,1) 的分量和都是 2，但 3≠1。 S14 · implies操作前 \text{S02 to S13} 操作後 u+v=(1,3),\ u-v=(5,-5),\ v-u=(-5,5),\ ku=(-6,2),\ 0u=(0,0),\ 2u+v=(4,2),\ x=(-5,5) 條件：無 規則：and_intro_elim · 依賴：S02, S03, S04, S06, S07, S08, S09, S10, S11, S12, S13 葉節點依據：and_intro_elim 彙整：u+v=(1,3)、u−v=(5,−5)、v−u=(−5,5)=−(u−v)、ku=(−6,2)、0u=(0,0)、2u+v=(4,2)；u+x=v 的唯一解是 x=v−u=(−5,5)；k(u+v)=ku+kv=(−2,−6)；u≠w，u≠(−1,3)。 ## 局部子步與引理 S05.1 · equivalent操作前 u-v,\quad -(v-u) 操作後 (u_1-v_1,\,u_2-v_2),\quad (-(v_1-u_1),\,-(v_2-u_2)) 條件：無 規則：mko_vector_ops · 依賴：mko_vector_ops, neg_vec_def 葉節點依據：mko_vector_ops + neg_vec_def 對任意 u、v∈ℝ²，把兩邊逐分量展開：u−v=(u₁−v₁,u₂−v₂)；v−u=(v₁−u₁,v₂−u₂)，再依 neg_vec_def 乘 −1 得 −(v−u)=(−(v₁−u₁),−(v₂−u₂))。 S05.2 · equivalent操作前 -(v_i-u_i) 操作後 u_i-v_i\quad(i=1,2) 條件：無 規則：distributive · 依賴：S05.1, distributive, neg_mul, add_comm 葉節點依據：distributive + neg_mul + add_comm + cartesian_product_def 對實數 a、b：−(b−a)=(−1)(b+(−a))=(−1)b+(−1)(−a)=−b+a=a+(−b)=a−b（分配律、負號與乘法、加法交換律；N7 做恆等式核對）。取 a=u_i、b=v_i，兩個分量都相等，依向量相等的定義 u−v=−(v−u)。S05.1 與 S05.2 證得引理 L_sub_reverse。 S07.1 · implies操作前 u+x=v 操作後 x=v-u 條件：無 規則：eq_congruence · 依賴：mko_vector_ops, cartesian_product_def, eq_congruence 葉節點依據：cartesian_product_def + eq_congruence + add_assoc + add_comm + add_inverse + add_zero ⇒：u+x=v 依向量相等拆成 u₁+x₁=v₁ 與 u₂+x₂=v₂。每式兩邊同加 −u_i：x_i=(u_i+x_i)+(−u_i)=v_i−u_i（結合律、交換律、反元素、加法單位元）。兩個分量都等於 v−u 的分量，所以 x=v−u。 S07.2 · implies操作前 x=v-u 操作後 u+x=v 條件：無 規則：add_inverse · 依賴：mko_vector_ops, add_inverse 葉節點依據：add_inverse + add_assoc + add_comm + add_zero + mko_vector_ops ⇐：若 x=v−u，則 u+x 的第 i 個分量是 u_i+(v_i−u_i)=u_i+(v_i+(−u_i))=v_i+(u_i+(−u_i))=v_i+0=v_i，所以 u+x=v。S07.1 與 S07.2 證得引理 L_solve_vec，同時說明這樣的 x 唯一。 S11.1 · equivalent操作前 k(u+v) 操作後 (k(u_1+v_1),k(u_2+v_2))=(ku_1+kv_1,ku_2+kv_2)=ku+kv 條件：無 規則：distributive · 依賴：mko_vector_ops, distributive 葉節點依據：mko_vector_ops + distributive + cartesian_product_def 對任意實數 k 與 u、v∈ℝ²：先逐分量展開 u+v，再乘 k 得 (k(u₁+v₁),k(u₂+v₂))；每個分量用實數分配律 k(a+b)=ka+kb，得 (ku₁+kv₁,ku₂+kv₂)，這正是 ku 與 kv 的逐分量和。這證得引理 L_scalar_distrib（N18 做恆等式核對）。 ## 逐步反向審查 - S14 · sufficient_goal_reduction · S02, S03, S04, S07, S08, S09, S10, S11, S12, S13, and_intro_elim — 目標 G：題目要求的各項計算與判定。足夠條件 H：所列各步的結論；H⇒G 只是合取，H 由 G1、G2 正向證成，沒有把 G 當作前提。 - S13 · premise_audit · cartesian_product_def — 有序對相等需要逐位置相等；一個位置不同就足以否定。 - S12 · premise_audit · cartesian_product_def, numeric_evaluation — 一個分量不同就足以推出不等（N20）；不宣稱平方和與任何幾何量的關係。 - S11.1 · inverse_equivalence · mko_vector_ops, distributive, cartesian_product_def — 每個等號都是恆等式，兩個分量都相等，所以雙向成立。 - S11 · premise_audit · L_scalar_distrib, S02, S08 — 引理在 S11.1 對所有 k、u、v 證明；本例數字只是核對，不取代證明。 - S10 · inverse_equivalence · mko_vector_ops, numeric_evaluation — 逐分量重算（N14、N15）。 - S09 · inverse_equivalence · mul_zero, mul_comm, mko_vector_ops — 逐分量相等（N12、N13），兩向成立。 - S08 · inverse_equivalence · mko_vector_ops, numeric_evaluation, neg_mul — 逐分量重算（N10、N11）；兩邊是同一個向量。 - S07.2 · premise_audit · add_inverse, add_assoc, add_comm, add_zero — 只用到實數加法的群性質，對任何 u、v 都成立。 - S07.1 · premise_audit · cartesian_product_def, eq_congruence, add_inverse — 這是引理的「⇒」方向，反向另在 S07.2 證明；兩邊同加同一個數總是可行。 - S07 · inverse_equivalence · L_solve_vec — 引理兩向在 S07.1、S07.2 證明；代回核對見 N8、N9。 - S06 · premise_audit · cartesian_product_def, S03, S04 — 一個分量不同就足以推出不等；最後一句的一般說法不在此證明，只是說明，判定只依本例的分量。 - S05.2 · inverse_equivalence · distributive, neg_mul, add_comm, cartesian_product_def — 所用的是對所有實數成立的恆等式，雙向成立；向量相等需要兩個分量都相等，這裡兩者都成立。 - S05.1 · inverse_equivalence · mko_vector_ops, neg_vec_def — 展開定義是雙向的。 - S05 · premise_audit · L_sub_reverse, S03, S04 — 引理在 S05.1、S05.2 對所有向量證明；本例的數字只是核對。 - S04 · inverse_equivalence · mko_vector_ops, numeric_evaluation — 逐分量重算（N5、N6）。 - S03 · inverse_equivalence · mko_vector_ops, numeric_evaluation — 逐分量重算（N3、N4）；兩邊是同一個分量對。 - S02 · inverse_equivalence · mko_vector_ops, numeric_evaluation — 兩邊是同一個分量對；逐分量重算（N1、N2）。 - S01 · premise_audit · G1, G2, G3, mko_vector_ops — 此步只寫出定義與資料，不推出新事實；若基底不固定，同一組分量可能代表不同向量。 ## 錯誤控制與反例 分量有位置，減法有方向MKO 指出的誤解之一是把向量座標當成可交換。(3,−1) 與 (−1,3) 不同（S13）；u−v=(5,−5) 與 v−u=(−5,5) 互為相反向量（S05、S06）。從 u 到 v 要加的是 v−u（S07），寫成 u−v 會得到相反方向。 相等要逐分量，不看長度或分量和MKO 的第二個誤解是以為向量相等只需長度相同。u 與 w 的平方和都是 10，但 3≠1，所以 u≠w（S12）；u 與 (1,1) 的分量和都是 2，也不相等（S13）。相等的唯一判準是兩個對應分量都相等。 純量乘法不是內積MKO 的第三個誤解是把純量乘法當成內積。ku=(−6,2) 是 ℝ² 的向量（S08），不是一個數；把 ku 的分量加起來得到 −4 已經離開本條目的運算。內積是另一種運算，本條目不定義也不使用它。 - u−v=v−u，因為兩者都是 u 與 v 的差 → reject — u−v=(5,−5)，v−u=(−5,5)，第一分量 5≠−5。 - u=w，因為 u₁²+u₂²=w₁²+w₂²=10 → reject — 相等需逐分量相同；第一分量 3≠1。 - (3,−1)=(−1,3)，因為兩者用了相同的兩個數 → reject — 有序對逐位置比較；3≠−1。 - ku 是一個數：(−2)·3+(−2)·(−1)=−4 → reject — ku=(−6,2) 是向量；把分量相加不是純量乘法的一部分。 ## 結論與限制 在固定標準基底下：u+v=(1,3)，u−v=(5,−5)，v−u=(−5,5)=−(u−v)，所以 u−v≠v−u；ku=(−6,2)，0u=(0,0)，2u+v=(4,2)；滿足 u+x=v 的唯一向量是 x=v−u=(−5,5)；k(u+v)=ku+kv=(−2,−6)。u≠w（雖然平方和都是 10），u≠(−1,3)（分量交換位置）。 - N7 與 N18 是各變數次數至多為一的多項式恆等式格點核對，對應 S05.2 與 S11.1 的代數論證；論證本身不依賴它們。 - 本稿不涉及長度、角度、內積或基底變換（MKO 第三段明示另有義務）。 ## 驗證及來源綁定 20 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: bc749cb55fd9feab11176f4265e52ebf388cff1d90049efe15d0c6b29999d5c1 - original source SHA-256: bc749cb55fd9feab11176f4265e52ebf388cff1d90049efe15d0c6b29999d5c1 - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-vector-01.json)