P. 509 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 50801-50831   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	crosspv1d 50801	Value of the first component of the cross product. (Contributed by Jiamin Zhao, 12-Aug-2026.)
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m (1...3)))    &   ⊢ (𝜑 → 𝐵 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → ((𝐴⊠𝐵)‘1) = (((𝐴‘2) · (𝐵‘3)) − ((𝐴‘3) · (𝐵‘2))))
Theorem	crosspv2d 50802	Value of the second component of the cross product. (Contributed by Jiamin Zhao, 12-Aug-2026.)
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m (1...3)))    &   ⊢ (𝜑 → 𝐵 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → ((𝐴⊠𝐵)‘2) = (((𝐴‘3) · (𝐵‘1)) − ((𝐴‘1) · (𝐵‘3))))
Theorem	crosspv3d 50803	Value of the third component of the cross product. (Contributed by Jiamin Zhao, 12-Aug-2026.)
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m (1...3)))    &   ⊢ (𝜑 → 𝐵 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → ((𝐴⊠𝐵)‘3) = (((𝐴‘1) · (𝐵‘2)) − ((𝐴‘2) · (𝐵‘1))))
Theorem	crosspdot0lem 50804*	Lemma for crosspdotd 50806. Unfold the curried scalar triple product application into an explicit group sum. (Contributed by Jiamin Zhao, 12-Aug-2026.)
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m (1...3)))    &   ⊢ (𝜑 → 𝐵 ∈ (ℝ ↑m (1...3)))    &   ⊢ (𝜑 → 𝐶 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → (𝐵(tripp‘𝐴)𝐶) = (ℝfld Σg (𝑘 ∈ (1...3) ↦ ((𝐴‘𝑘) · ((𝐵⊠𝐶)‘𝑘)))))
Theorem	crosspdotsumlem 50805*	Lemma for crosspdotd 50806. Expand the group sum over (1...3) into an explicit three-term sum. (Contributed by Jiamin Zhao, 12-Aug-2026.)
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m (1...3)))    &   ⊢ (𝜑 → 𝐵 ∈ (ℝ ↑m (1...3)))    &   ⊢ (𝜑 → 𝐶 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → (ℝfld Σg (𝑘 ∈ (1...3) ↦ ((𝐴‘𝑘) · ((𝐵⊠𝐶)‘𝑘)))) = (((𝐴‘1) · ((𝐵⊠𝐶)‘1)) + (((𝐴‘2) · ((𝐵⊠𝐶)‘2)) + ((𝐴‘3) · ((𝐵⊠𝐶)‘3)))))
Theorem	crosspdotd 50806	Value of the scalar triple product, expanded into the standard six-term Sarrus polynomial. (Contributed by Jiamin Zhao, 12-Aug-2026.)
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m (1...3)))    &   ⊢ (𝜑 → 𝐵 ∈ (ℝ ↑m (1...3)))    &   ⊢ (𝜑 → 𝐶 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → (𝐵(tripp‘𝐴)𝐶) = (((((𝐴‘1) · (𝐵‘2)) · (𝐶‘3)) − (((𝐴‘1) · (𝐵‘3)) · (𝐶‘2))) + (((((𝐴‘2) · (𝐵‘3)) · (𝐶‘1)) − (((𝐴‘2) · (𝐵‘1)) · (𝐶‘3))) + ((((𝐴‘3) · (𝐵‘1)) · (𝐶‘2)) − (((𝐴‘3) · (𝐵‘2)) · (𝐶‘1))))))
Theorem	crosspaltd 50807*	Antisymmetry of the cross product: swapping the two vectors negates the result. (Contributed by Jiamin Zhao, 12-Aug-2026.)
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m (1...3)))    &   ⊢ (𝜑 → 𝐵 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → (𝐴⊠𝐵) = (𝑘 ∈ (1...3) ↦ -((𝐵⊠𝐴)‘𝑘)))
Theorem	crossp3d 50808*	The vector triple product expansion (BAC-CAB rule): the cross product of 𝑋 with (𝑌⊠𝑍) equals 𝑌 scaled by the dot product of 𝑋 and 𝑍, minus 𝑍 scaled by the dot product of 𝑋 and 𝑌. The dot products are written out as explicit three-term sums of component products, matching the pointwise style of df-crossp 50792 rather than introducing a separate dot product operator. (Contributed by Jiamin Zhao, 12-Aug-2026.)
⊢ (𝜑 → 𝑋 ∈ (ℝ ↑m (1...3)))    &   ⊢ (𝜑 → 𝑌 ∈ (ℝ ↑m (1...3)))    &   ⊢ (𝜑 → 𝑍 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → (𝑋⊠(𝑌⊠𝑍)) = (𝑘 ∈ (1...3) ↦ ((((((𝑋‘1) · (𝑍‘1)) + ((𝑋‘2) · (𝑍‘2))) + ((𝑋‘3) · (𝑍‘3))) · (𝑌‘𝑘)) − (((((𝑋‘1) · (𝑌‘1)) + ((𝑋‘2) · (𝑌‘2))) + ((𝑋‘3) · (𝑌‘3))) · (𝑍‘𝑘)))))
21.55.2  Veronese map and linear dependence
Syntax	cveronese 50809	Extend class notation to include the quadratic Veronese map on real 3-vectors. (Contributed by Jiamin Zhao, 14-Aug-2026.)
class veronese
Definition	df-veronese 50810*	Define the quadratic Veronese map on real 3-vectors, with coordinates ordered as ( x^2 , y^2 , z^2 , x y , y z , z x ). (Contributed by Jiamin Zhao, 14-Aug-2026.)
⊢ veronese = (𝑞 ∈ (ℝ ↑m (1...3)) ↦ (𝑘 ∈ (1...6) ↦ (((if(𝑘 = 1, ((𝑞‘1)↑2), 0) + if(𝑘 = 2, ((𝑞‘2)↑2), 0)) + if(𝑘 = 3, ((𝑞‘3)↑2), 0)) + ((if(𝑘 = 4, ((𝑞‘1) · (𝑞‘2)), 0) + if(𝑘 = 5, ((𝑞‘2) · (𝑞‘3)), 0)) + if(𝑘 = 6, ((𝑞‘3) · (𝑞‘1)), 0)))))
Theorem	nellindf 50811	A nonzero coefficient vector whose weighted combination of 𝐹 sums to the zero vector implies that 𝐹 is not linearly independent. (Contributed by Jiamin Zhao, 27-Aug-2026.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑌 = (0g‘𝑅)    &   ⊢ 𝐿 = (Base‘(𝑅 freeLMod 𝐼))    ⇒   ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ V ∧ 𝐹:𝐼⟶𝐵) ∧ (𝐾 ∈ 𝐿 ∧ 𝐾 ≠ (𝐼 × {𝑌}) ∧ (𝑊 Σg (𝐾 ∘f · 𝐹)) = 0 )) → ¬ 𝐹 LIndF 𝑊)
Theorem	veronesevald 50812*	Value of the Veronese map at a point, expressed as a maps-to function on the six coordinates. (Contributed by Jiamin Zhao, 14-Aug-2026.)
⊢ (𝜑 → 𝑃 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → (veronese‘𝑃) = (𝑘 ∈ (1...6) ↦ (((if(𝑘 = 1, ((𝑃‘1)↑2), 0) + if(𝑘 = 2, ((𝑃‘2)↑2), 0)) + if(𝑘 = 3, ((𝑃‘3)↑2), 0)) + ((if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), 0) + if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), 0)) + if(𝑘 = 6, ((𝑃‘3) · (𝑃‘1)), 0)))))
Theorem	veronesefvcl 50813	Every coordinate of the Veronese map of a real 3-vector is real. (Contributed by Jiamin Zhao, 19-Aug-2026.)
⊢ ((𝑄 ∈ (ℝ ↑m (1...3)) ∧ 𝐾 ∈ (1...6)) → ((veronese‘𝑄)‘𝐾) ∈ ℝ)
Theorem	veronesev1lem 50814	Lemma for veronesevrowd 50820. Value of the first coordinate of the Veronese map at a point. (Contributed by Jiamin Zhao, 15-Aug-2026.)
⊢ (𝜑 → 𝑃 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → ((veronese‘𝑃)‘1) = ((𝑃‘1)↑2))
Theorem	veronesev2lem 50815	Lemma for veronesevrowd 50820. Value of the second coordinate of the Veronese map at a point. (Contributed by Jiamin Zhao, 16-Aug-2026.)
⊢ (𝜑 → 𝑃 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → ((veronese‘𝑃)‘2) = ((𝑃‘2)↑2))
Theorem	veronesev3lem 50816	Lemma for veronesevrowd 50820. Value of the third coordinate of the Veronese map at a point. (Contributed by Jiamin Zhao, 17-Aug-2026.)
⊢ (𝜑 → 𝑃 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → ((veronese‘𝑃)‘3) = ((𝑃‘3)↑2))
Theorem	veronesev4lem 50817	Lemma for veronesevrowd 50820. Value of the fourth coordinate of the Veronese map at a point. (Contributed by Jiamin Zhao, 17-Aug-2026.)
⊢ (𝜑 → 𝑃 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → ((veronese‘𝑃)‘4) = ((𝑃‘1) · (𝑃‘2)))
Theorem	veronesev5lem 50818	Lemma for veronesevrowd 50820. Value of the fifth coordinate of the Veronese map at a point. (Contributed by Jiamin Zhao, 17-Aug-2026.)
⊢ (𝜑 → 𝑃 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → ((veronese‘𝑃)‘5) = ((𝑃‘2) · (𝑃‘3)))
Theorem	veronesev6lem 50819	Lemma for veronesevrowd 50820. Value of the sixth coordinate of the Veronese map at a point. (Contributed by Jiamin Zhao, 17-Aug-2026.)
⊢ (𝜑 → 𝑃 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → ((veronese‘𝑃)‘6) = ((𝑃‘3) · (𝑃‘1)))
Theorem	veronesevrowd 50820*	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 50821*	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 50822*	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 50823*	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 50824*	Lemma for veroquadmodzerod 50825. 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 50825*	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 50826*	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 50827*	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.56  Mathbox for Kunhao Zheng
21.56.1  Weighted AM-GM inequality
Theorem	amgmwlem 50828	Weighted version of amgmlem 27234. (Contributed by Kunhao Zheng, 19-Jun-2021.)
⊢ 𝑀 = (mulGrp‘ℂfld)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ+)    &   ⊢ (𝜑 → 𝑊:𝐴⟶ℝ+)    &   ⊢ (𝜑 → (ℂfld Σg 𝑊) = 1)    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝐹 ∘f ↑𝑐𝑊)) ≤ (ℂfld Σg (𝐹 ∘f · 𝑊)))
Theorem	amgmlemALT 50829	Alternate proof of amgmlem 27234 using amgmwlem 50828. (Contributed by Kunhao Zheng, 20-Jun-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑀 = (mulGrp‘ℂfld)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ+)    ⇒   ⊢ (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 / (♯‘𝐴))) ≤ ((ℂfld Σg 𝐹) / (♯‘𝐴)))
Theorem	amgmw2d 50830	Weighted arithmetic-geometric mean inequality for 𝑛 = 2 (compare amgm2d 45046). (Contributed by Kunhao Zheng, 20-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑃 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑄 ∈ ℝ+)    &   ⊢ (𝜑 → (𝑃 + 𝑄) = 1)    ⇒   ⊢ (𝜑 → ((𝐴↑𝑐𝑃) · (𝐵↑𝑐𝑄)) ≤ ((𝐴 · 𝑃) + (𝐵 · 𝑄)))
Theorem	young2d 50831	Young's inequality for 𝑛 = 2, a direct application of amgmw2d 50830. (Contributed by Kunhao Zheng, 6-Jul-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑃 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑄 ∈ ℝ+)    &   ⊢ (𝜑 → ((1 / 𝑃) + (1 / 𝑄)) = 1)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ≤ (((𝐴↑𝑐𝑃) / 𝑃) + ((𝐵↑𝑐𝑄) / 𝑄)))

< Previous  Wrap >