P. 510 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 50901-50990   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cbvals 50901*	Rule used to change bound variables, using implicit substitution. (Contributed by David A. Wheeler, 12-Jul-2026.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (∀∃𝑥(𝜑 → 𝜓) ↔ ∀∃𝑦(𝜒 → 𝜃))
Theorem	als-no-surprise 50902	Demonstrate that there is never a "surprise" when using the allsome quantifier, that is, it is never possible for the consequent to be both always true and always false. This uses the definition of df-als 50884; the proof itself builds on alimp-no-surprise 50877. For a contrast, see alimp-surprise 50876. (Contributed by David A. Wheeler, 27-Oct-2018.)
⊢ ¬ (∀∃𝑥(𝜑 → 𝜓) ∧ ∀∃𝑥(𝜑 → ¬ 𝜓))
Theorem	rals-no-surprise 50903	Demonstrate that there is never a "surprise" when using the allsome quantifier restricted to a class, that is, it is never possible for the consequent to be both always true and always false of the members of 𝐴 that satisfy the antecedent. This is the restricted counterpart of als-no-surprise 50902, and follows from it by dfrals2 50886. Note that this needs no assumption that 𝐴 is nonempty, because allsome requires a member of 𝐴 satisfying 𝜑, and that member would have to satisfy both 𝜓 and ¬ 𝜓. The ordinary restricted "for all" requires no such member and can be vacuously true, as shown in empty-surprise2 50879; that is the point of allsome. (Contributed by David A. Wheeler, 12-Jul-2026.)
⊢ ¬ (∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ∧ ∀∃𝑥 ∈ 𝐴(𝜑 → ¬ 𝜓))
Theorem	ralrals 50904	If the universal part of a restricted "all some" statement holds, then the statement reduces to the existence of a member of 𝐴 satisfying its antecedent. This is the restricted counterpart of ralals 50910. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∃𝑥 ∈ 𝐴 𝜑))
Theorem	rexrals 50905	If a member of 𝐴 satisfying the antecedent exists, then a restricted "all some" statement reduces to its universal part. This is the restricted counterpart of rexals 50911. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 → (∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)))
Theorem	alsanmo 50906	An "all some" statement conjoined with the claim that at most one 𝑥 satisfies its antecedent is equivalent to the universal part conjoined with the claim that exactly one 𝑥 satisfies the antecedent. The "all some" quantifier supplies the existence of such an 𝑥 and ∃*𝑥𝜑 supplies the at-most-one part, so together they yield ∃!𝑥𝜑. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
⊢ ((∀∃𝑥(𝜑 → 𝜓) ∧ ∃*𝑥𝜑) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∃!𝑥𝜑))
Theorem	ralsanmo 50907	An "all some" statement restricted to a class, conjoined with the claim that at most one 𝑥 in 𝐴 satisfies its antecedent, is equivalent to the universal part conjoined with the claim that exactly one 𝑥 in 𝐴 satisfies the antecedent. This is the restricted counterpart of alsanmo 50906. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
⊢ ((∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃!𝑥 ∈ 𝐴 𝜑))
Theorem	alsralrex 50908*	The general "all some" quantifier with class membership as its antecedent holds if and only if 𝜑 holds for every 𝑥 in 𝐴 and some 𝑥 in 𝐴 satisfies 𝜑. (Contributed by Peter Mazsa, 27-Nov-2018.) (Revised by David A. Wheeler, 15-Jul-2026.)
⊢ (∀∃𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜑))
Theorem	alsraln0 50909*	The general "all some" quantifier with class membership as its antecedent holds if and only if 𝜑 holds for every 𝑥 in 𝐴 and 𝐴 is not empty. (Contributed by Peter Mazsa, 28-Nov-2018.) (Revised by David A. Wheeler, 15-Jul-2026.)
⊢ (∀∃𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ 𝐴 ≠ ∅))
Theorem	ralals 50910*	If 𝜑 holds for every 𝑥 in 𝐴, then the general "all some" quantifier with class membership as its antecedent reduces to the assertion that some 𝑥 in 𝐴 satisfies 𝜑. See ralrals 50904 for the restricted counterpart. (Contributed by Peter Mazsa, 19-Dec-2018.) (Revised by David A. Wheeler, 15-Jul-2026.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀∃𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑))
Theorem	rexals 50911*	If some 𝑥 in 𝐴 satisfies 𝜑, then the general "all some" quantifier with class membership as its antecedent reduces to the assertion that 𝜑 holds for every 𝑥 in 𝐴. See rexrals 50905 for the restricted counterpart. (Contributed by Peter Mazsa, 19-Dec-2018.) (Revised by David A. Wheeler, 15-Jul-2026.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 → (∀∃𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥 ∈ 𝐴 𝜑))
Theorem	n0als 50912*	If 𝐴 is not empty, then the general "all some" quantifier with class membership as its antecedent reduces to the assertion that 𝜑 holds for every 𝑥 in 𝐴. (Contributed by Peter Mazsa, 19-Dec-2018.) (Revised by David A. Wheeler, 15-Jul-2026.)
⊢ (𝐴 ≠ ∅ → (∀∃𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥 ∈ 𝐴 𝜑))
Theorem	2alsraln0 50913*	Nested general "all some" quantifiers with class membership as their antecedents: 𝜑 holds for every 𝑥 in 𝐴 and every 𝑦 in 𝐵, and both 𝐴 and 𝐵 are not empty. (Contributed by Peter Mazsa, 28-May-2019.) (Revised by David A. Wheeler, 15-Jul-2026.)
⊢ (∀∃𝑥(𝑥 ∈ 𝐴 → ∀∃𝑦(𝑦 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ (𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅)))
Theorem	2alsraln0id 50914*	Nested general "all some" quantifiers with class membership as their antecedents, for the same class 𝐴: 𝜑 holds for every 𝑥 and every 𝑦 in 𝐴, and 𝐴 is not empty. (Contributed by Peter Mazsa, 28-May-2019.) (Revised by David A. Wheeler, 15-Jul-2026.)
⊢ (∀∃𝑥(𝑥 ∈ 𝐴 → ∀∃𝑦(𝑦 ∈ 𝐴 → 𝜑)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 ∧ 𝐴 ≠ ∅))
21.53.13  Allsome one quantifier These are definitions and proofs involving the "allsome one" quantifier, which extends the "allsome" quantifier of the previous section in the same way that ∃! (df-eu 2594) extends ∃. Some systems extend "there exists" by appending a character to it. If a system provides such an extension, it should provide it for allsome as well: append the same character, let it modify allsome's existence conjunct, and change nothing else. Appending "!" gives "allsome one", so ∀∃!𝑥(𝜑 → 𝜓) means that 𝜓 is true whenever 𝜑 is true and that exactly one 𝑥 satisfies 𝜑. This is what the English word "the" usually does. "The king is hungry" claims that a king exists, that there is only one, and that he is hungry, and the form ∀∃!𝑥(𝜑 → 𝜓) claims exactly that kind of statement (specifically when 𝜑 means 𝑥 is a king and 𝜓 means 𝑥 is hungry). English says all of that in a single phrase, and the first two have a dedicated word ("the") for the construct. Many other languages have their own dedicated way of saying this. Languages reserve that kind of compression for what their speakers need constantly, which is a good reason for a formal notation to be able to say it just as directly, rather than spelling it out afresh as a conjunction of two quantified formulas every time it comes up. Russell analyzed such definite descriptions with this apparatus in "On Denoting", where his example of a phrase that appears to refer to someone but in fact denotes no one at all is "the present King of France", item (1) of [Russell1905] p. 479, France being a republic that has no king. Write "the king is hungry" as ∀𝑥(𝜑 → 𝜓) instead and only the last of those three claims survives. The existence claim is silently gone, since that formula is vacuously true when there is no king, and the uniqueness claim is silently gone as well, since that formula holds just the same when there are five kings. Russell reached the opposite verdict for the same example, remarking that every proposition of the form "the present King of France ..." is false, [Russell1905] p. 482. The reason to care is the reason that motivates allsome, only more so; see alimp-surprise 50876 and empty-surprise 50878. Note that this is not merely a way of writing ∃!𝑥(𝜑 ∧ 𝜓). Reading 𝜑 as "is a king" and 𝜓 as "is hungry", ∃!𝑥(𝜑 ∧ 𝜓) says that there is exactly one hungry king, whereas ∀∃!𝑥(𝜑 → 𝜓) says that there is exactly one king and that he is hungry. The first is true in a region with five kings exactly one of whom is hungry; the second is false there. Uniqueness attaches to the antecedent, not to the conjunction. See dfalseu2 50932 for the exact relationship between the two and alseueu 50933 for the one direction that does hold. Naming: "alseu" is allsome ("als", as in df-als 50884) extended with "exactly one" ("eu", as in df-eu 2594). The form restricted to a class is prefixed with "r", following df-rals 50885 and df-reu 3366, giving df-ralseu 50918. Soundness: df-alseu 50917 and df-ralseu 50918 are eliminable and conservative directly, so neither needs a justification theorem. Definitions are required to be eliminable and conservative; see the section comment for df-bi 210. Each is a biconditional whose left side is a new syntax construct (walseu 50915 or wralseu 50916) applied to distinct metavariables, and whose right side uses only constructs introduced earlier (∀, ∃!, ∧, →, and the restricted quantifiers df-ral 3077 and df-reu 3366), so any occurrence of the new construct can be replaced by the right side, which is eliminability. Conservativity follows, since a proof of a statement not mentioning ∀∃! can have every use of the definition replaced in this way. Every variable occurring on the right side already occurs on the left side, so no dummy variable is introduced, and introducing a dummy variable whose choice must be shown not to matter is the only circumstance here that would call for a justification theorem. For more, see "The Allsome Quantifier" by David A. Wheeler at https://dwheeler.com/essays/allsome.html 3366
Syntax	walseu 50915	Extend wff definition to include "all some one" applied to a top-level implication, which means 𝜓 is true whenever 𝜑 is true, and exactly one 𝑥 satisfies 𝜑. (Contributed by David A. Wheeler, 21-Jul-2026.)
wff ∀∃!𝑥(𝜑 → 𝜓)
Syntax	wralseu 50916	Extend wff definition to include "all some one" applied to a class, which means 𝜓 is true whenever 𝜑 is true for 𝑥 in 𝐴, and exactly one 𝑥 in 𝐴 satisfies 𝜑. (Contributed by David A. Wheeler, 21-Jul-2026.)
wff ∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓)
Definition	df-alseu 50917	Define "all some one" applied to a top-level implication, which means 𝜓 is true whenever 𝜑 is true and exactly one 𝑥 satisfies 𝜑. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (∀∃!𝑥(𝜑 → 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∃!𝑥𝜑))
Definition	df-ralseu 50918	Define "all some one" applied to a class, which means 𝜓 is true whenever 𝜑 is true for 𝑥 in 𝐴, and exactly one 𝑥 in 𝐴 satisfies 𝜑. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃!𝑥 ∈ 𝐴 𝜑))
Theorem	dfralseu2 50919	The bounded "all some one" form is the general form with the class membership folded into the antecedent. This is the "all some one" counterpart of dfrals2 50886. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∀∃!𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓))
Theorem	alseuals 50920	"All some one" implies "all some": requiring exactly one witness is stronger than requiring at least one. Any consequence of an allsome statement is therefore a consequence of the corresponding "all some one" statement, which is how alseu-no-surprise 50934 is proved. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (∀∃!𝑥(𝜑 → 𝜓) → ∀∃𝑥(𝜑 → 𝜓))
Theorem	ralseurals 50921	"All some one" restricted to a class implies "all some" restricted to that class. Restricted counterpart of alseuals 50920. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓) → ∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓))
Theorem	alseud 50922	Introduction rule: "all some one" holds if the "for all" part holds and the antecedent has exactly one witness. This is the converse of alseu1d 50924 and alseu2d 50925 taken together. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (𝜑 → ∀𝑥(𝜓 → 𝜒))    &   ⊢ (𝜑 → ∃!𝑥𝜓)    ⇒   ⊢ (𝜑 → ∀∃!𝑥(𝜓 → 𝜒))
Theorem	ralseud 50923	Introduction rule for "all some one" restricted to a class. This is the converse of ralseu1d 50926 and ralseu2d 50927 taken together. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))    &   ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → ∀∃!𝑥 ∈ 𝐴(𝜓 → 𝜒))
Theorem	alseu1d 50924	Deduction rule: Given "all some one" applied to a top-level inference, you can extract the "for all" part. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (𝜑 → ∀∃!𝑥(𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ∀𝑥(𝜓 → 𝜒))
Theorem	alseu2d 50925	Deduction rule: Given "all some one" applied to a top-level inference, you can extract the "exactly one" part. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (𝜑 → ∀∃!𝑥(𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ∃!𝑥𝜓)
Theorem	ralseu1d 50926	Deduction rule: Given "all some one" applied to a class, you can extract the "for all" part. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (𝜑 → ∀∃!𝑥 ∈ 𝐴(𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))
Theorem	ralseu2d 50927	Deduction rule: Given "all some one" applied to a class, you can extract the "exactly one" part. Note that the witness must satisfy the antecedent 𝜓, not merely be a member of 𝐴. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (𝜑 → ∀∃!𝑥 ∈ 𝐴(𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 𝜓)
Theorem	alseubii 50928	Congruence: equivalents may be substituted inside an "all some one". This is the "all some one" counterpart of alsbii 50896. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (𝜑 ↔ 𝜒)    &   ⊢ (𝜓 ↔ 𝜃)    ⇒   ⊢ (∀∃!𝑥(𝜑 → 𝜓) ↔ ∀∃!𝑥(𝜒 → 𝜃))
Theorem	ralseubii 50929	Congruence for "all some one" restricted to a class. This is the "all some one" counterpart of ralsbii 50897. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (𝜑 ↔ 𝜒)    &   ⊢ (𝜓 ↔ 𝜃)    ⇒   ⊢ (∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∀∃!𝑥 ∈ 𝐴(𝜒 → 𝜃))
Theorem	nfalseu 50930*	Bound-variable hypothesis builder for "all some one". This is the "all some one" counterpart of nfals 50899. Unlike nfals 50899 it requires 𝑥 and 𝑦 to be disjoint, because the corresponding builder for ∃! is nfeuw 2618, which requires it; the version without that requirement, nfeu 2619, depends on ax-13 2401 and its use is discouraged. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ Ⅎ𝑥∀∃!𝑦(𝜑 → 𝜓)
Theorem	nfralseu 50931*	Bound-variable hypothesis builder for "all some one" restricted to a class. This is the "all some one" counterpart of nfrals 50900. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ Ⅎ𝑥∀∃!𝑦 ∈ 𝐴(𝜑 → 𝜓)
Theorem	dfalseu2 50932	An "all some one" statement is equivalent to its universal part conjoined with the claim that exactly one 𝑥 satisfies both 𝜑 and 𝜓. In other words, given ∀𝑥(𝜑 → 𝜓), requiring exactly one 𝑥 to satisfy 𝜑, which is what df-alseu 50917 requires, and requiring exactly one 𝑥 to satisfy (𝜑 ∧ 𝜓) come to the same thing. Read 𝜑 as "is a king" and 𝜓 as "is hungry": if every king is hungry, then "there is exactly one king" and "there is exactly one hungry king" say the same thing, so either of them, together with "every king is hungry", gives "the king is hungry". The universal conjunct is what makes that work, and it cannot be dropped. ∃!𝑥(𝜑 ∧ 𝜓) on its own is strictly weaker than ∀∃!𝑥(𝜑 → 𝜓), since it is satisfied when many things are 𝜑 and just one of those is 𝜓, as in a region with five kings exactly one of whom is hungry; see alseueu 50933 for the one direction that does hold without it. Uniqueness attaches to the antecedent, not to the conjunction. Russell's analysis of a definite description is built the same way: its uniqueness clause constrains the description predicate alone, while the predication is a separate conjunct. See his worked example of "the father of Charles II was executed", [Russell1905] p. 482. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (∀∃!𝑥(𝜑 → 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∃!𝑥(𝜑 ∧ 𝜓)))
Theorem	alseueu 50933	"The 𝜑 is 𝜓 " implies that exactly one thing is both 𝜑 and 𝜓. This is the half of dfalseu2 50932 that drops the universal conjunct; it does not reverse, so ∃!𝑥(𝜑 ∧ 𝜓) cannot be used in place of an "all some one" statement. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ (∀∃!𝑥(𝜑 → 𝜓) → ∃!𝑥(𝜑 ∧ 𝜓))
Theorem	alseu-no-surprise 50934	Demonstrate that there is never a "surprise" when using the "all some one" quantifier, that is, it is never possible for the consequent to be both always true and always false. This follows from als-no-surprise 50902 by alseuals 50920. For a contrast, see alimp-surprise 50876. (Contributed by David A. Wheeler, 21-Jul-2026.)
⊢ ¬ (∀∃!𝑥(𝜑 → 𝜓) ∧ ∀∃!𝑥(𝜑 → ¬ 𝜓))
21.53.14  Miscellaneous Miscellaneous proofs.
Theorem	5m4e1 50935	Prove that 5 - 4 = 1. (Contributed by David A. Wheeler, 31-Jan-2017.)
⊢ (5 − 4) = 1
Theorem	2p2ne5 50936	Prove that 2 + 2 ≠ 5. In George Orwell's "1984", Part One, Chapter Seven, the protagonist Winston notes that, "In the end the Party would announce that two and two made five, and you would have to believe it." http://www.sparknotes.com/lit/1984/section4.rhtml. More generally, the phrase 2 + 2 = 5 has come to represent an obviously false dogma one may be required to believe. See the Wikipedia article for more about this: https://en.wikipedia.org/wiki/2_%2B_2_%3D_5. Unsurprisingly, we can easily prove that this claim is false. (Contributed by David A. Wheeler, 31-Jan-2017.)
⊢ (2 + 2) ≠ 5
Theorem	resolution 50937	Resolution rule. This is the primary inference rule in some automated theorem provers such as prover9. The resolution rule can be traced back to Davis and Putnam (1960). (Contributed by David A. Wheeler, 9-Feb-2017.)
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) → (𝜓 ∨ 𝜒))
Theorem	testable 50938	In classical logic all wffs are testable, that is, it is always true that (¬ 𝜑 ∨ ¬ ¬ 𝜑). This is not necessarily true in intuitionistic logic. In intuitionistic logic, if this statement is true for some 𝜑, then 𝜑 is testable. The proof is trivial because it's simply a special case of the law of the excluded middle, which is true in classical logic but not necessarily true in intuitionisic logic. (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ (¬ 𝜑 ∨ ¬ ¬ 𝜑)
21.53.15  Theorems about algebraic numbers
Theorem	aacllem 50939*	Lemma for other theorems about 𝔸. (Contributed by Brendan Leahy, 3-Jan-2020.) (Revised by Alexander van der Vekens and David A. Wheeler, 25-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴↑𝑘) = Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋))    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝔸)
21.54  Mathbox for Mingli Yuan
Theorem	wrdf1d 50940	A one-to-one word maps its domain into its alphabet. (Contributed by Mingli Yuan, 11-Aug-2026.)
⊢ (𝜑 → 𝑊 ∈ Word 𝐷)    &   ⊢ (𝜑 → Fun ◡𝑊)    ⇒   ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷)
21.55  Mathbox for Jiamin Zhao
21.55.1  Cross product and scalar triple product in RR^3
Theorem	1ne3 50941	1 is not equal to 3. (Contributed by Jiamin Zhao, 1-Aug-2026.)
⊢ 1 ≠ 3
Theorem	2ne3 50942	2 is not equal to 3. (Contributed by Jiamin Zhao, 1-Aug-2026.)
⊢ 2 ≠ 3
Theorem	1elfz13 50943	Membership of 1 in the integer interval ( 1 ... 3 ). (Suggested by avekens.) (Contributed by Jiamin Zhao, 1-Aug-2026.) (Proof shortened by Jiamin Zhao, 13-Aug-2026.)
⊢ 1 ∈ (1...3)
Theorem	2elfz13 50944	Membership of 2 in the integer interval ( 1 ... 3 ). (Suggested by tirix.) (Contributed by Jiamin Zhao, 1-Aug-2026.) (Proof shortened by Jiamin Zhao, 13-Aug-2026.)
⊢ 2 ∈ (1...3)
Theorem	3elfz13 50945	Membership of 3 in the integer interval ( 1 ... 3 ). (Contributed by Jiamin Zhao, 1-Aug-2026.)
⊢ 3 ∈ (1...3)
Theorem	rr3fvcl 50946	The components of a 3-dimensional real coordinate vector are real numbers. (Contributed by Jiamin Zhao, 31-Jul-2026.)
⊢ (𝐴 ∈ (ℝ ↑m (1...3)) → ((𝐴‘1) ∈ ℝ ∧ (𝐴‘2) ∈ ℝ ∧ (𝐴‘3) ∈ ℝ))
Theorem	rr3fv1cld 50947	First component of a 3-dimensional real coordinate vector is real. (Contributed by Jiamin Zhao, 10-Aug-2026.)
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → (𝐴‘1) ∈ ℝ)
Theorem	rr3fv2cld 50948	Second component of a 3-dimensional real coordinate vector is real. (Contributed by Jiamin Zhao, 10-Aug-2026.)
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → (𝐴‘2) ∈ ℝ)
Theorem	rr3fv3cld 50949	Third component of a 3-dimensional real coordinate vector is real. (Contributed by Jiamin Zhao, 10-Aug-2026.)
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → (𝐴‘3) ∈ ℝ)
Syntax	ccrossp 50950	Extend class notation to include the cross product operation. (Contributed by Jiamin Zhao, 31-Jul-2026.)
class ⊠
Definition	df-crossp 50951*	Define the cross product of two 3-dimensional real coordinate vectors. Vectors are represented as functions on (1...3). (Contributed by Jiamin Zhao, 31-Jul-2026.)
⊢ ⊠ = (𝑢 ∈ (ℝ ↑m (1...3)), 𝑣 ∈ (ℝ ↑m (1...3)) ↦ (𝑘 ∈ (1...3) ↦ if(𝑘 = 1, (((𝑢‘2) · (𝑣‘3)) − ((𝑢‘3) · (𝑣‘2))), if(𝑘 = 2, (((𝑢‘3) · (𝑣‘1)) − ((𝑢‘1) · (𝑣‘3))), (((𝑢‘1) · (𝑣‘2)) − ((𝑢‘2) · (𝑣‘1)))))))
Syntax	ctripp 50952	Extend class notation to include the scalar triple product of 3-dimensional real coordinate vectors. (Contributed by Jiamin Zhao, 31-Jul-2026.)
class tripp
Definition	df-tripp 50953*	Define the scalar triple product of three 3-dimensional real coordinate vectors as the dot product of the first vector 𝑥 with the cross product of the other two (𝑦 and 𝑧). Apply as (𝑦(tripp‘𝑥)𝑧). Vectors are represented as functions on (1...3). (Contributed by Jiamin Zhao, 31-Jul-2026.)
⊢ tripp = (𝑥 ∈ (ℝ ↑m (1...3)) ↦ (𝑦 ∈ (ℝ ↑m (1...3)), 𝑧 ∈ (ℝ ↑m (1...3)) ↦ (ℝfld Σg (𝑘 ∈ (1...3) ↦ ((𝑥‘𝑘) · ((𝑦⊠𝑧)‘𝑘))))))
Theorem	crosspval 50954*	Value of the cross product of two 3-dimensional real coordinate vectors as a function on (1...3). (Contributed by Jiamin Zhao, 31-Jul-2026.)
⊢ ((𝐴 ∈ (ℝ ↑m (1...3)) ∧ 𝐵 ∈ (ℝ ↑m (1...3))) → (𝐴⊠𝐵) = (𝑘 ∈ (1...3) ↦ if(𝑘 = 1, (((𝐴‘2) · (𝐵‘3)) − ((𝐴‘3) · (𝐵‘2))), if(𝑘 = 2, (((𝐴‘3) · (𝐵‘1)) − ((𝐴‘1) · (𝐵‘3))), (((𝐴‘1) · (𝐵‘2)) − ((𝐴‘2) · (𝐵‘1)))))))
Theorem	crosspcle1d 50955	Closure of the first component of the cross product's coordinate formula. (Contributed by Jiamin Zhao, 11-Aug-2026.)
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m (1...3)))    &   ⊢ (𝜑 → 𝐵 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → (((𝐴‘2) · (𝐵‘3)) − ((𝐴‘3) · (𝐵‘2))) ∈ ℝ)
Theorem	crosspcle2d 50956	Closure of the second component of the cross product's coordinate formula. (Contributed by Jiamin Zhao, 11-Aug-2026.)
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m (1...3)))    &   ⊢ (𝜑 → 𝐵 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → (((𝐴‘3) · (𝐵‘1)) − ((𝐴‘1) · (𝐵‘3))) ∈ ℝ)
Theorem	crosspcle3d 50957	Closure of the third component of the cross product's coordinate formula. (Contributed by Jiamin Zhao, 11-Aug-2026.)
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m (1...3)))    &   ⊢ (𝜑 → 𝐵 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → (((𝐴‘1) · (𝐵‘2)) − ((𝐴‘2) · (𝐵‘1))) ∈ ℝ)
Theorem	crosspclem 50958	Lemma for crosspcld 50959. Closure of the three-way coordinate case split used in the cross product's mapping rule. (Contributed by Jiamin Zhao, 11-Aug-2026.)
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m (1...3)))    &   ⊢ (𝜑 → 𝐵 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → if(𝑘 = 1, (((𝐴‘2) · (𝐵‘3)) − ((𝐴‘3) · (𝐵‘2))), if(𝑘 = 2, (((𝐴‘3) · (𝐵‘1)) − ((𝐴‘1) · (𝐵‘3))), (((𝐴‘1) · (𝐵‘2)) − ((𝐴‘2) · (𝐵‘1))))) ∈ ℝ)
Theorem	crosspcld 50959	Closure of the cross product: the cross product of two 3-dimensional real coordinate vectors is again such a vector. (Contributed by Jiamin Zhao, 12-Aug-2026.)
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m (1...3)))    &   ⊢ (𝜑 → 𝐵 ∈ (ℝ ↑m (1...3)))    ⇒   ⊢ (𝜑 → (𝐴⊠𝐵) ∈ (ℝ ↑m (1...3)))
Theorem	crosspv1d 50960	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 50961	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 50962	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 50963*	Lemma for crosspdotd 50965. 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 50964*	Lemma for crosspdotd 50965. 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 50965	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 50966*	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 50967*	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 50951 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 50968	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 50969*	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 50970	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 50971*	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 50972	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 50973	Lemma for veronesevrowd 50979. 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 50974	Lemma for veronesevrowd 50979. 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 50975	Lemma for veronesevrowd 50979. 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 50976	Lemma for veronesevrowd 50979. 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 50977	Lemma for veronesevrowd 50979. 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 50978	Lemma for veronesevrowd 50979. 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 50979*	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 50980*	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 50981*	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 50982*	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 50983*	Lemma for veroquadmodzerod 50984. 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 50984*	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 50985*	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 50986*	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 50987	Weighted version of amgmlem 27317. (Contributed by Kunhao Zheng, 19-Jun-2021.)
⊢ 𝑀 = (mulGrp‘ℂfld)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ+)    &   ⊢ (𝜑 → 𝑊:𝐴⟶ℝ+)    &   ⊢ (𝜑 → (ℂfld Σg 𝑊) = 1)    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝐹 ∘f ↑𝑐𝑊)) ≤ (ℂfld Σg (𝐹 ∘f · 𝑊)))
Theorem	amgmlemALT 50988	Alternate proof of amgmlem 27317 using amgmwlem 50987. (Contributed by Kunhao Zheng, 20-Jun-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑀 = (mulGrp‘ℂfld)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ+)    ⇒   ⊢ (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 / (♯‘𝐴))) ≤ ((ℂfld Σg 𝐹) / (♯‘𝐴)))
Theorem	amgmw2d 50989	Weighted arithmetic-geometric mean inequality for 𝑛 = 2 (compare amgm2d 45198). (Contributed by Kunhao Zheng, 20-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑃 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑄 ∈ ℝ+)    &   ⊢ (𝜑 → (𝑃 + 𝑄) = 1)    ⇒   ⊢ (𝜑 → ((𝐴↑𝑐𝑃) · (𝐵↑𝑐𝑄)) ≤ ((𝐴 · 𝑃) + (𝐵 · 𝑄)))
Theorem	young2d 50990	Young's inequality for 𝑛 = 2, a direct application of amgmw2d 50989. (Contributed by Kunhao Zheng, 6-Jul-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑃 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑄 ∈ ℝ+)    &   ⊢ (𝜑 → ((1 / 𝑃) + (1 / 𝑄)) = 1)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ≤ (((𝐴↑𝑐𝑃) / 𝑃) + ((𝐵↑𝑐𝑄) / 𝑄)))

< Previous  Wrap >