P. 515 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 51401-51412   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	veronesevrowd 51401*	The Veronese map at a point, expressed explicitly as a piecewise maps-to function on the six coordinates. (Contributed by Jiamin Zhao, 17-Aug-2026.)
⊢ (𝜑 → 𝑃 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → (veronese‘𝑃) = (𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))))))
Theorem	veronesematbasd 51402*	The matrix whose 𝑖-th row is the Veronese image of 𝐴‘𝑖 belongs to the base set of (1...6) Mat ℝfld. (Contributed by Jiamin Zhao, 19-Aug-2026.)
⊢ 𝑉 = (𝑖 ∈ (1...6), 𝑗 ∈ (1...6) ↦ ((veronese‘(𝐴‘𝑖))‘𝑗))    &   ⊢ (𝜑 → 𝐴:(1...6)⟶(ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → 𝑉 ∈ (Base‘((1...6) Mat ℝfld)))
Theorem	veronesematrowd 51403*	Currying the Veronese matrix gives the indexed family of Veronese images of the points 𝐴‘𝑖. (Contributed by Jiamin Zhao, 19-Aug-2026.)
⊢ 𝑉 = (𝑖 ∈ (1...6), 𝑗 ∈ (1...6) ↦ ((veronese‘(𝐴‘𝑖))‘𝑗))    &   ⊢ (𝜑 → 𝐴:(1...6)⟶(ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → curry 𝑉 = (𝑖 ∈ (1...6) ↦ (veronese‘(𝐴‘𝑖))))
Theorem	veronesematrowexpd 51404*	Currying the Veronese matrix gives the indexed family of Veronese images, with each image expressed explicitly by coordinates. (Contributed by Jiamin Zhao, 19-Aug-2026.)
⊢ 𝑉 = (𝑖 ∈ (1...6), 𝑗 ∈ (1...6) ↦ ((veronese‘(𝐴‘𝑖))‘𝑗))    &   ⊢ (𝜑 → 𝐴:(1...6)⟶(ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → curry 𝑉 = (𝑖 ∈ (1...6) ↦ (𝑘 ∈ (1...6) ↦ if(𝑘 = 1, (((𝐴‘𝑖)‘1)↑2), if(𝑘 = 2, (((𝐴‘𝑖)‘2)↑2), if(𝑘 = 3, (((𝐴‘𝑖)‘3)↑2), if(𝑘 = 4, (((𝐴‘𝑖)‘1) · ((𝐴‘𝑖)‘2)), if(𝑘 = 5, (((𝐴‘𝑖)‘2) · ((𝐴‘𝑖)‘3)), (((𝐴‘𝑖)‘3) · ((𝐴‘𝑖)‘1))))))))))
Theorem	veroquadgsumlem 51405*	Lemma for veroquadmodzerod 51406. Express the common homogeneous quadratic equation in ℝfld Σg form using the Veronese matrix 𝑉. (Contributed by Jiamin Zhao, 19-Aug-2026.)
⊢ 𝑉 = (𝑖 ∈ (1...6), 𝑗 ∈ (1...6) ↦ ((veronese‘(𝐴‘𝑖))‘𝑗))    &   ⊢ (𝜑 → 𝐴:(1...6)⟶(ℝ ↑m (1...3)))    &   ⊢ (𝜑 → 𝐾:(1...6)⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (1...6)) → (((((𝐾‘1) · (((𝐴‘𝑖)‘1)↑2)) + ((𝐾‘2) · (((𝐴‘𝑖)‘2)↑2))) + ((𝐾‘3) · (((𝐴‘𝑖)‘3)↑2))) + ((((𝐾‘4) · (((𝐴‘𝑖)‘1) · ((𝐴‘𝑖)‘2))) + ((𝐾‘5) · (((𝐴‘𝑖)‘2) · ((𝐴‘𝑖)‘3)))) + ((𝐾‘6) · (((𝐴‘𝑖)‘3) · ((𝐴‘𝑖)‘1))))) = 0)    ⇒   ⊢ ((𝜑 ∧ 𝑖 ∈ (1...6)) → (ℝfld Σg (𝑗 ∈ (1...6) ↦ ((𝐾‘𝑗) · ((curry 𝑉‘𝑖)‘𝑗)))) = 0)
Theorem	veroquadmodzerod 51406*	The columns of the Veronese matrix, weighted by the coefficients 𝐾, sum to the zero vector of ℝfld freeLMod (1...6). (Contributed by Jiamin Zhao, 19-Aug-2026.)
⊢ 𝑉 = (𝑖 ∈ (1...6), 𝑗 ∈ (1...6) ↦ ((veronese‘(𝐴‘𝑖))‘𝑗))    &   ⊢ (𝜑 → 𝐴:(1...6)⟶(ℝ ↑m (1...3)))    &   ⊢ (𝜑 → 𝐾:(1...6)⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (1...6)) → (((((𝐾‘1) · (((𝐴‘𝑖)‘1)↑2)) + ((𝐾‘2) · (((𝐴‘𝑖)‘2)↑2))) + ((𝐾‘3) · (((𝐴‘𝑖)‘3)↑2))) + ((((𝐾‘4) · (((𝐴‘𝑖)‘1) · ((𝐴‘𝑖)‘2))) + ((𝐾‘5) · (((𝐴‘𝑖)‘2) · ((𝐴‘𝑖)‘3)))) + ((𝐾‘6) · (((𝐴‘𝑖)‘3) · ((𝐴‘𝑖)‘1))))) = 0)    ⇒   ⊢ (𝜑 → ((ℝfld freeLMod (1...6)) Σg (𝐾 ∘f ( ·𝑠 ‘(ℝfld freeLMod (1...6)))curry tpos 𝑉)) = (0g‘(ℝfld freeLMod (1...6))))
Theorem	veroquadnolindfd 51407*	A nonzero homogeneous quadratic equation satisfied by all six points gives a linear dependence among the columns of the Veronese matrix. (Contributed by Jiamin Zhao, 27-Aug-2026.)
⊢ 𝑉 = (𝑖 ∈ (1...6), 𝑗 ∈ (1...6) ↦ ((veronese‘(𝐴‘𝑖))‘𝑗))    &   ⊢ (𝜑 → 𝐴:(1...6)⟶(ℝ ↑m (1...3)))    &   ⊢ (𝜑 → 𝐾:(1...6)⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (1...6)) → (((((𝐾‘1) · (((𝐴‘𝑖)‘1)↑2)) + ((𝐾‘2) · (((𝐴‘𝑖)‘2)↑2))) + ((𝐾‘3) · (((𝐴‘𝑖)‘3)↑2))) + ((((𝐾‘4) · (((𝐴‘𝑖)‘1) · ((𝐴‘𝑖)‘2))) + ((𝐾‘5) · (((𝐴‘𝑖)‘2) · ((𝐴‘𝑖)‘3)))) + ((𝐾‘6) · (((𝐴‘𝑖)‘3) · ((𝐴‘𝑖)‘1))))) = 0)    &   ⊢ (𝜑 → 𝐾 ≠ ((1...6) × {0}))    ⇒   ⊢ (𝜑 → ¬ curry tpos 𝑉 LIndF (ℝfld freeLMod (1...6)))
Theorem	veroquaddetzerod 51408*	The Veronese matrix of six points satisfying a common nonzero homogeneous quadratic equation has determinant zero. (Contributed by Jiamin Zhao, 27-Aug-2026.)
⊢ 𝑉 = (𝑖 ∈ (1...6), 𝑗 ∈ (1...6) ↦ ((veronese‘(𝐴‘𝑖))‘𝑗))    &   ⊢ (𝜑 → 𝐴:(1...6)⟶(ℝ ↑m (1...3)))    &   ⊢ (𝜑 → 𝐾:(1...6)⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (1...6)) → (((((𝐾‘1) · (((𝐴‘𝑖)‘1)↑2)) + ((𝐾‘2) · (((𝐴‘𝑖)‘2)↑2))) + ((𝐾‘3) · (((𝐴‘𝑖)‘3)↑2))) + ((((𝐾‘4) · (((𝐴‘𝑖)‘1) · ((𝐴‘𝑖)‘2))) + ((𝐾‘5) · (((𝐴‘𝑖)‘2) · ((𝐴‘𝑖)‘3)))) + ((𝐾‘6) · (((𝐴‘𝑖)‘3) · ((𝐴‘𝑖)‘1))))) = 0)    &   ⊢ (𝜑 → 𝐾 ≠ ((1...6) × {0}))    ⇒   ⊢ (𝜑 → (((1...6) maDet ℝfld)‘𝑉) = 0)
21.58  Mathbox for Kunhao Zheng
21.58.1  Weighted AM-GM inequality
Theorem	amgmwlem 51409	Weighted version of amgmlem 27363. (Contributed by Kunhao Zheng, 19-Jun-2021.)
⊢ 𝑀 = (mulGrp‘ℂfld)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ+)    &   ⊢ (𝜑 → 𝑊:𝐴⟶ℝ+)    &   ⊢ (𝜑 → (ℂfld Σg 𝑊) = 1)    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝐹 ∘f ↑𝑐𝑊)) ≤ (ℂfld Σg (𝐹 ∘f · 𝑊)))
Theorem	amgmlemALT 51410	Alternate proof of amgmlem 27363 using amgmwlem 51409. (Contributed by Kunhao Zheng, 20-Jun-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑀 = (mulGrp‘ℂfld)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ+)    ⇒   ⊢ (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 / (♯‘𝐴))) ≤ ((ℂfld Σg 𝐹) / (♯‘𝐴)))
Theorem	amgmw2d 51411	Weighted arithmetic-geometric mean inequality for 𝑛 = 2 (compare amgm2d 45453). (Contributed by Kunhao Zheng, 20-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑃 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑄 ∈ ℝ+)    &   ⊢ (𝜑 → (𝑃 + 𝑄) = 1)    ⇒   ⊢ (𝜑 → ((𝐴↑𝑐𝑃) · (𝐵↑𝑐𝑄)) ≤ ((𝐴 · 𝑃) + (𝐵 · 𝑄)))
Theorem	young2d 51412	Young's inequality for 𝑛 = 2, a direct application of amgmw2d 51411. (Contributed by Kunhao Zheng, 6-Jul-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑃 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑄 ∈ ℝ+)    &   ⊢ (𝜑 → ((1 / 𝑃) + (1 / 𝑄)) = 1)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ≤ (((𝐴↑𝑐𝑃) / 𝑃) + ((𝐵↑𝑐𝑄) / 𝑄)))

< Previous  Wrap >