P. 289 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28801-28900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ex-pss 28801	Example for df-pss 3907. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ {1, 2} ⊊ {1, 2, 3}
Theorem	ex-pw 28802	Example for df-pw 4536. Example by David A. Wheeler. (Contributed by Mario Carneiro, 2-Jul-2016.)
⊢ (𝐴 = {3, 5, 7} → 𝒫 𝐴 = (({∅} ∪ {{3}, {5}, {7}}) ∪ ({{3, 5}, {3, 7}, {5, 7}} ∪ {{3, 5, 7}})))
Theorem	ex-pr 28803	Example for df-pr 4565. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ (𝐴 ∈ {1, -1} → (𝐴↑2) = 1)
Theorem	ex-br 28804	Example for df-br 5076. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝑅 = {⟨2, 6⟩, ⟨3, 9⟩} → 3𝑅9)
Theorem	ex-opab 28805*	Example for df-opab 5138. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ (𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (𝑥 + 1) = 𝑦)} → 3𝑅4)
Theorem	ex-eprel 28806	Example for df-eprel 5496. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 5 E {1, 5}
Theorem	ex-id 28807	Example for df-id 5490. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ (5 I 5 ∧ ¬ 4 I 5)
Theorem	ex-po 28808	Example for df-po 5504. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ ( < Po ℝ ∧ ¬ ≤ Po ℝ)
Theorem	ex-xp 28809	Example for df-xp 5596. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ ({1, 5} × {2, 7}) = ({⟨1, 2⟩, ⟨1, 7⟩} ∪ {⟨5, 2⟩, ⟨5, 7⟩})
Theorem	ex-cnv 28810	Example for df-cnv 5598. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ ◡{⟨2, 6⟩, ⟨3, 9⟩} = {⟨6, 2⟩, ⟨9, 3⟩}
Theorem	ex-co 28811	Example for df-co 5599. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ ((exp ∘ cos)‘0) = e
Theorem	ex-dm 28812	Example for df-dm 5600. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ (𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → dom 𝐹 = {2, 3})
Theorem	ex-rn 28813	Example for df-rn 5601. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ (𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9})
Theorem	ex-res 28814	Example for df-res 5602. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ ((𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} ∧ 𝐵 = {1, 2}) → (𝐹 ↾ 𝐵) = {⟨2, 6⟩})
Theorem	ex-ima 28815	Example for df-ima 5603. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ ((𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} ∧ 𝐵 = {1, 2}) → (𝐹 “ 𝐵) = {6})
Theorem	ex-fv 28816	Example for df-fv 6445. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ (𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → (𝐹‘3) = 9)
Theorem	ex-1st 28817	Example for df-1st 7840. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ (1st ‘⟨3, 4⟩) = 3
Theorem	ex-2nd 28818	Example for df-2nd 7841. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ (2nd ‘⟨3, 4⟩) = 4
Theorem	1kp2ke3k 28819	Example for df-dec 12447, 1000 + 2000 = 3000. This proof disproves (by counterexample) the assertion of Hao Wang, who stated, "There is a theorem in the primitive notation of set theory that corresponds to the arithmetic theorem 1000 + 2000 = 3000. The formula would be forbiddingly long... even if (one) knows the definitions and is asked to simplify the long formula according to them, chances are he will make errors and arrive at some incorrect result." (Hao Wang, "Theory and practice in mathematics" , In Thomas Tymoczko, editor, New Directions in the Philosophy of Mathematics, pp 129-152, Birkauser Boston, Inc., Boston, 1986. (QA8.6.N48). The quote itself is on page 140.) This is noted in Metamath: A Computer Language for Pure Mathematics by Norman Megill (2007) section 1.1.3. Megill then states, "A number of writers have conveyed the impression that the kind of absolute rigor provided by Metamath is an impossible dream, suggesting that a complete, formal verification of a typical theorem would take millions of steps in untold volumes of books... These writers assume, however, that in order to achieve the kind of complete formal verification they desire one must break down a proof into individual primitive steps that make direct reference to the axioms. This is not necessary. There is no reason not to make use of previously proved theorems rather than proving them over and over... A hierarchy of theorems and definitions permits an exponential growth in the formula sizes and primitive proof steps to be described with only a linear growth in the number of symbols used. Of course, this is how ordinary informal mathematics is normally done anyway, but with Metamath it can be done with absolute rigor and precision." The proof here starts with (2 + 1) = 3, commutes it, and repeatedly multiplies both sides by ten. This is certainly longer than traditional mathematical proofs, e.g., there are a number of steps explicitly shown here to show that we're allowed to do operations such as multiplication. However, while longer, the proof is clearly a manageable size - even though every step is rigorously derived all the way back to the primitive notions of set theory and logic. And while there's a risk of making errors, the many independent verifiers make it much less likely that an incorrect result will be accepted. This proof heavily relies on the decimal constructor df-dec 12447 developed by Mario Carneiro in 2015. The underlying Metamath language has an intentionally very small set of primitives; it doesn't even have a built-in construct for numbers. Instead, the digits are defined using these primitives, and the decimal constructor is used to make it easy to express larger numbers as combinations of digits. (Contributed by David A. Wheeler, 29-Jun-2016.) (Shortened by Mario Carneiro using the arithmetic algorithm in mmj2, 30-Jun-2016.)
⊢ (;;;1000 + ;;;2000) = ;;;3000
Theorem	ex-fl 28820	Example for df-fl 13521. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ ((⌊‘(3 / 2)) = 1 ∧ (⌊‘-(3 / 2)) = -2)
Theorem	ex-ceil 28821	Example for df-ceil 13522. (Contributed by AV, 4-Sep-2021.)
⊢ ((⌈‘(3 / 2)) = 2 ∧ (⌈‘-(3 / 2)) = -1)
Theorem	ex-mod 28822	Example for df-mod 13599. (Contributed by AV, 3-Sep-2021.)
⊢ ((5 mod 3) = 2 ∧ (-7 mod 2) = 1)
Theorem	ex-exp 28823	Example for df-exp 13792. (Contributed by AV, 4-Sep-2021.)
⊢ ((5↑2) = ;25 ∧ (-3↑-2) = (1 / 9))
Theorem	ex-fac 28824	Example for df-fac 13997. (Contributed by AV, 4-Sep-2021.)
⊢ (!‘5) = ;;120
Theorem	ex-bc 28825	Example for df-bc 14026. (Contributed by AV, 4-Sep-2021.)
⊢ (5C3) = ;10
Theorem	ex-hash 28826	Example for df-hash 14054. (Contributed by AV, 4-Sep-2021.)
⊢ (♯‘{0, 1, 2}) = 3
Theorem	ex-sqrt 28827	Example for df-sqrt 14955. (Contributed by AV, 4-Sep-2021.)
⊢ (√‘;25) = 5
Theorem	ex-abs 28828	Example for df-abs 14956. (Contributed by AV, 4-Sep-2021.)
⊢ (abs‘-2) = 2
Theorem	ex-dvds 28829	Example for df-dvds 15973: 3 divides into 6. (Contributed by David A. Wheeler, 19-May-2015.)
⊢ 3 ∥ 6
Theorem	ex-gcd 28830	Example for df-gcd 16211. (Contributed by AV, 5-Sep-2021.)
⊢ (-6 gcd 9) = 3
Theorem	ex-lcm 28831	Example for df-lcm 16304. (Contributed by AV, 5-Sep-2021.)
⊢ (6 lcm 9) = ;18
Theorem	ex-prmo 28832	Example for df-prmo 16742: (#p‘10) = 2 · 3 · 5 · 7. (Contributed by AV, 6-Sep-2021.)
⊢ (#p‘;10) = ;;210
17.1.5  Other examples
Theorem	aevdemo 28833*	Proof illustrating the comment of aev2 2062. (Contributed by BJ, 30-Mar-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ((∃𝑎∀𝑏 𝑐 = 𝑑 ∨ ∃𝑒 𝑓 = 𝑔) ∧ ∀ℎ(𝑖 = 𝑗 → 𝑘 = 𝑙)))
Theorem	ex-ind-dvds 28834	Example of a proof by induction (divisibility result). (Contributed by Stanislas Polu, 9-Mar-2020.) (Revised by BJ, 24-Mar-2020.)
⊢ (𝑁 ∈ ℕ0 → 3 ∥ ((4↑𝑁) + 2))
Theorem	ex-fpar 28835	Formalized example provided in the comment for fpar 7965. (Contributed by AV, 3-Jan-2024.)
⊢ 𝐻 = ((◡(1st ↾ (V × V)) ∘ (𝐹 ∘ (1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V)))))    &   ⊢ 𝐴 = (0[,)+∞)    &   ⊢ 𝐵 = ℝ    &   ⊢ 𝐹 = (√ ↾ 𝐴)    &   ⊢ 𝐺 = (sin ↾ 𝐵)    ⇒   ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋( + ∘ 𝐻)𝑌) = ((√‘𝑋) + (sin‘𝑌)))
17.2  Humor
17.2.1  April Fool's theorem
Theorem	avril1 28836	Poisson d'Avril's Theorem. This theorem is noted for its Selbstdokumentieren property, which means, literally, "self-documenting" and recalls the principle of quidquid german dictum sit, altum viditur, often used in set theory. Starting with the seemingly simple yet profound fact that any object 𝑥 equals itself (proved by Tarski in 1965; see Lemma 6 of [Tarski] p. 68), we demonstrate that the power set of the real numbers, as a relation on the value of the imaginary unit, does not conjoin with an empty relation on the product of the additive and multiplicative identity elements, leading to this startling conclusion that has left even seasoned professional mathematicians scratching their heads. (Contributed by Prof. Loof Lirpa, 1-Apr-2005.) (Proof modification is discouraged.) (New usage is discouraged.) A reply to skeptics can be found at mmnotes.txt, under the 1-Apr-2006 entry.
⊢ ¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1))
Theorem	2bornot2b 28837	The law of excluded middle. Act III, Theorem 1 of Shakespeare, Hamlet, Prince of Denmark (1602). Its author leaves its proof as an exercise for the reader - "To be, or not to be: that is the question" - starting a trend that has become standard in modern-day textbooks, serving to make the frustrated reader feel inferior, or in some cases to mask the fact that the author does not know its solution. (Contributed by Prof. Loof Lirpa, 1-Apr-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (2 · 𝐵 ∨ ¬ 2 · 𝐵)
Theorem	helloworld 28838	The classic "Hello world" benchmark has been translated into 314 computer programming languages - see http://helloworldcollection.de. However, for many years it eluded a proof that it is more than just a conjecture, even though a wily mathematician once claimed, "I have discovered a truly marvelous proof of this, which this margin is too narrow to contain." Using an IBM 709 mainframe, a team of mathematicians led by Prof. Loof Lirpa, at the New College of Tahiti, were finally able to put it to rest with a remarkably short proof only four lines long. (Contributed by Prof. Loof Lirpa, 1-Apr-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ (ℎ ∈ (𝐿𝐿0) ∧ 𝑊∅(R1𝑑))
Theorem	1p1e2apr1 28839	One plus one equals two. Using proof-shortening techniques pioneered by Mr. Mel L. O'Cat, along with the latest supercomputer technology, Prof. Loof Lirpa and colleagues were able to shorten Whitehead and Russell's 360-page proof that 1+1=2 in Principia Mathematica to this remarkable proof only two steps long, thus establishing a new world's record for this famous theorem. (Contributed by Prof. Loof Lirpa, 1-Apr-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (1 + 1) = 2
Theorem	eqid1 28840	Law of identity (reflexivity of class equality). Theorem 6.4 of [Quine] p. 41. This law is thought to have originated with Aristotle (Metaphysics, Book VII, Part 17). It is one of the three axioms of Ayn Rand's philosophy (Atlas Shrugged, Part Three, Chapter VII). While some have proposed extending Rand's axiomatization to include Compassion and Kindness, others fear that such an extension may flirt with logical inconsistency. (Contributed by Stefan Allan, 1-Apr-2009.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 = 𝐴
Theorem	1div0apr 28841	Division by zero is forbidden! If we try, we encounter the DO NOT ENTER sign, which in mathematics means it is foolhardy to venture any further, possibly putting the underlying fabric of reality at risk. Based on a dare by David A. Wheeler. (Contributed by Mario Carneiro, 1-Apr-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (1 / 0) = ∅
Theorem	topnfbey 28842	Nothing seems to be impossible to Prof. Lirpa. After years of intensive research, he managed to find a proof that when given a chance to reach infinity, one could indeed go beyond, thus giving formal soundness to Buzz Lightyear's motto "To infinity... and beyond!" (Contributed by Prof. Loof Lirpa, 1-Apr-2020.) (Revised by Thierry Arnoux, 2-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐵 ∈ (0...+∞) → +∞ < 𝐵)
Theorem	9p10ne21 28843	9 + 10 is not equal to 21. This disproves a popular meme which asserts that 9 + 10 does equal 21. See https://www.quora.com/Can-someone-try-to-prove-to-me-that-9+10-21 for attempts to prove that 9 + 10 = 21, and see https://tinyurl.com/9p10e21 for the history of the 9 + 10 = 21 meme. (Contributed by BTernaryTau, 25-Aug-2023.)
⊢ (9 + ;10) ≠ ;21
Theorem	9p10ne21fool 28844	9 + 10 equals 21. This astonishing thesis lives as a meme on the internet, and may be believed by quite some people. At least repeated requests to falsify it are a permanent part of the story. Prof. Loof Lirpa did not rest until he finally came up with a computer verifiable mathematical proof, that only a fool can think so. (Contributed by Prof. Loof Lirpa, 26-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((9 + ;10) = ;21 → 𝐹∅(0 · 1))
17.3  (Future - to be reviewed and classified)
17.3.1  Planar incidence geometry
Syntax	cplig 28845	Extend class notation with the class of all planar incidence geometries.
class Plig
Definition	df-plig 28846*	Define the class of planar incidence geometries. We use Hilbert's axioms and adapt them to planar geometry. We use ∈ for the incidence relation. We could have used a generic binary relation, but using ∈ allows us to reuse previous results. Much of what follows is directly borrowed from Aitken, Incidence-Betweenness Geometry, 2008, http://public.csusm.edu/aitken_html/m410/betweenness.08.pdf. The class Plig is the class of planar incidence geometries, where a planar incidence geometry is defined as a set of lines satisfying three axioms. In the definition below, 𝑥 denotes a planar incidence geometry, so ∪ 𝑥 denotes the union of its lines, that is, the set of points in the plane, 𝑙 denotes a line, and 𝑎, 𝑏, 𝑐 denote points. Therefore, the axioms are: 1) for all pairs of (distinct) points, there exists a unique line containing them; 2) all lines contain at least two points; 3) there exist three non-collinear points. (Contributed by FL, 2-Aug-2009.)
⊢ Plig = {𝑥 ∣ (∀𝑎 ∈ ∪ 𝑥∀𝑏 ∈ ∪ 𝑥(𝑎 ≠ 𝑏 → ∃!𝑙 ∈ 𝑥 (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙)) ∧ ∀𝑙 ∈ 𝑥 ∃𝑎 ∈ ∪ 𝑥∃𝑏 ∈ ∪ 𝑥(𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙) ∧ ∃𝑎 ∈ ∪ 𝑥∃𝑏 ∈ ∪ 𝑥∃𝑐 ∈ ∪ 𝑥∀𝑙 ∈ 𝑥 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙))}
Theorem	isplig 28847*	The predicate "is a planar incidence geometry" for sets. (Contributed by FL, 2-Aug-2009.)
⊢ 𝑃 = ∪ 𝐺    ⇒   ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ Plig ↔ (∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 → ∃!𝑙 ∈ 𝐺 (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙)) ∧ ∀𝑙 ∈ 𝐺 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙) ∧ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙))))
Theorem	ispligb 28848*	The predicate "is a planar incidence geometry". (Contributed by BJ, 2-Dec-2021.)
⊢ 𝑃 = ∪ 𝐺    ⇒   ⊢ (𝐺 ∈ Plig ↔ (𝐺 ∈ V ∧ (∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 → ∃!𝑙 ∈ 𝐺 (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙)) ∧ ∀𝑙 ∈ 𝐺 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙) ∧ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙))))
Theorem	tncp 28849*	In any planar incidence geometry, there exist three non-collinear points. (Contributed by FL, 3-Aug-2009.)
⊢ 𝑃 = ∪ 𝐺    ⇒   ⊢ (𝐺 ∈ Plig → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙))
Theorem	l2p 28850*	For any line in a planar incidence geometry, there exist two different points on the line. (Contributed by AV, 28-Nov-2021.)
⊢ 𝑃 = ∪ 𝐺    ⇒   ⊢ ((𝐺 ∈ Plig ∧ 𝐿 ∈ 𝐺) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝐿))
Theorem	lpni 28851*	For any line in a planar incidence geometry, there exists a point not on the line. (Contributed by Jeff Hankins, 15-Aug-2009.)
⊢ 𝑃 = ∪ 𝐺    ⇒   ⊢ ((𝐺 ∈ Plig ∧ 𝐿 ∈ 𝐺) → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿)
Theorem	nsnlplig 28852	There is no "one-point line" in a planar incidence geometry. (Contributed by BJ, 2-Dec-2021.) (Proof shortened by AV, 5-Dec-2021.)
⊢ (𝐺 ∈ Plig → ¬ {𝐴} ∈ 𝐺)
Theorem	nsnlpligALT 28853	Alternate version of nsnlplig 28852 using the predicate ∉ instead of ¬ ∈ and whose proof is shorter. (Contributed by AV, 5-Dec-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐺 ∈ Plig → {𝐴} ∉ 𝐺)
Theorem	n0lplig 28854	There is no "empty line" in a planar incidence geometry. (Contributed by AV, 28-Nov-2021.) (Proof shortened by BJ, 2-Dec-2021.)
⊢ (𝐺 ∈ Plig → ¬ ∅ ∈ 𝐺)
Theorem	n0lpligALT 28855	Alternate version of n0lplig 28854 using the predicate ∉ instead of ¬ ∈ and whose proof bypasses nsnlplig 28852. (Contributed by AV, 28-Nov-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐺 ∈ Plig → ∅ ∉ 𝐺)
Theorem	eulplig 28856*	Through two distinct points of a planar incidence geometry, there is a unique line. (Contributed by BJ, 2-Dec-2021.)
⊢ 𝑃 = ∪ 𝐺    ⇒   ⊢ ((𝐺 ∈ Plig ∧ ((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ 𝐴 ≠ 𝐵)) → ∃!𝑙 ∈ 𝐺 (𝐴 ∈ 𝑙 ∧ 𝐵 ∈ 𝑙))
Theorem	pliguhgr 28857	Any planar incidence geometry 𝐺 can be regarded as a hypergraph with its points as vertices and its lines as edges. See incistruhgr 27458 for a generalization of this case for arbitrary incidence structures (planar incidence geometries are such incidence structures). (Proposed by Gerard Lang, 24-Nov-2021.) (Contributed by AV, 28-Nov-2021.)
⊢ (𝐺 ∈ Plig → ⟨∪ 𝐺, ( I ↾ 𝐺)⟩ ∈ UHGraph)
17.3.2  Aliases kept to prevent broken links This section contains a few aliases that we temporarily keep to prevent broken links. If you land on any of these, please let the originating site and/or us know that the link that made you land here should be changed.
Theorem	dummylink 28858	Alias for a1ii 2 that may be referenced in some older works, and kept here to prevent broken links. If you landed here, please let the originating site and/or us know that the link that made you land here should be changed to a link to a1ii 2. (Contributed by NM, 7-Feb-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ 𝜑
Theorem	id1 28859	Alias for idALT 23 that may be referenced in some older works, and kept here to prevent broken links. If you landed here, please let the originating site and/or us know that the link that made you land here should be changed to a link to idALT 23. (Contributed by NM, 30-Sep-1992.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜑)
PART 18  COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED) The intent is for this deprecated section to be deleted once its theorems have extensible structure versions (or are not useful). You can make a list of "terminal" theorems (i.e., theorems not referenced by anything else) and for each theorem see if there exists an extensible structure version (or decide it is not useful), and if so, delete it. Then, repeat this recursively. One way to search for terminal theorems is to log the output ("MM> OPEN LOG xxx.txt") of "MM> SHOW USAGE <label-match>" in the Metamath program and search for "(None)".
18.1  Additional material on group theory (deprecated) This section contains an earlier development of groups that was defined before extensible structures were introduced. The intent is for this deprecated section to be deleted once the corresponding definitions and theorems for complex topological vector spaces, which are using them, are revised accordingly.
18.1.1  Definitions and basic properties for groups
Syntax	cgr 28860	Extend class notation with the class of all group operations.
class GrpOp
Syntax	cgi 28861	Extend class notation with a function mapping a group operation to the group's identity element.
class GId
Syntax	cgn 28862	Extend class notation with a function mapping a group operation to the inverse function for the group.
class inv
Syntax	cgs 28863	Extend class notation with a function mapping a group operation to the division (or subtraction) operation for the group.
class /𝑔
Definition	df-grpo 28864*	Define the class of all group operations. The base set for a group can be determined from its group operation. Based on the definition in Exercise 28 of [Herstein] p. 54. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.)
⊢ GrpOp = {𝑔 ∣ ∃𝑡(𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢))}
Definition	df-gid 28865*	Define a function that maps a group operation to the group's identity element. (Contributed by FL, 5-Feb-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
⊢ GId = (𝑔 ∈ V ↦ (℩𝑢 ∈ ran 𝑔∀𝑥 ∈ ran 𝑔((𝑢𝑔𝑥) = 𝑥 ∧ (𝑥𝑔𝑢) = 𝑥)))
Definition	df-ginv 28866*	Define a function that maps a group operation to the group's inverse function. (Contributed by NM, 26-Oct-2006.) (New usage is discouraged.)
⊢ inv = (𝑔 ∈ GrpOp ↦ (𝑥 ∈ ran 𝑔 ↦ (℩𝑧 ∈ ran 𝑔(𝑧𝑔𝑥) = (GId‘𝑔))))
Definition	df-gdiv 28867*	Define a function that maps a group operation to the group's division (or subtraction) operation. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)
⊢ /𝑔 = (𝑔 ∈ GrpOp ↦ (𝑥 ∈ ran 𝑔, 𝑦 ∈ ran 𝑔 ↦ (𝑥𝑔((inv‘𝑔)‘𝑦))))
Theorem	isgrpo 28868*	The predicate "is a group operation." Note that 𝑋 is the base set of the group. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ GrpOp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢))))
Theorem	isgrpoi 28869*	Properties that determine a group operation. Read 𝑁 as 𝑁(𝑥). (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.)
⊢ 𝑋 ∈ V    &   ⊢ 𝐺:(𝑋 × 𝑋)⟶𝑋    &   ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))    &   ⊢ 𝑈 ∈ 𝑋    &   ⊢ (𝑥 ∈ 𝑋 → (𝑈𝐺𝑥) = 𝑥)    &   ⊢ (𝑥 ∈ 𝑋 → 𝑁 ∈ 𝑋)    &   ⊢ (𝑥 ∈ 𝑋 → (𝑁𝐺𝑥) = 𝑈)    ⇒   ⊢ 𝐺 ∈ GrpOp
Theorem	grpofo 28870	A group operation maps onto the group's underlying set. (Contributed by NM, 30-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ GrpOp → 𝐺:(𝑋 × 𝑋)–onto→𝑋)
Theorem	grpocl 28871	Closure law for a group operation. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)
Theorem	grpolidinv 28872*	A group has a left identity element, and every member has a left inverse. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ GrpOp → ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢))
Theorem	grpon0 28873	The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ GrpOp → 𝑋 ≠ ∅)
Theorem	grpoass 28874	A group operation is associative. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = (𝐴𝐺(𝐵𝐺𝐶)))
Theorem	grpoidinvlem1 28875	Lemma for grpoidinv 28879. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝐺 ∈ GrpOp ∧ (𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) ∧ ((𝑌𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝐴) = 𝐴)) → (𝑈𝐺𝐴) = 𝑈)
Theorem	grpoidinvlem2 28876	Lemma for grpoidinv 28879. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝐺 ∈ GrpOp ∧ (𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) ∧ ((𝑈𝐺𝑌) = 𝑌 ∧ (𝑌𝐺𝐴) = 𝑈)) → ((𝐴𝐺𝑌)𝐺(𝐴𝐺𝑌)) = (𝐴𝐺𝑌))
Theorem	grpoidinvlem3 28877*	Lemma for grpoidinv 28879. (Contributed by NM, 11-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)    &   ⊢ (𝜓 ↔ ∀𝑥 ∈ 𝑋 ∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈)    ⇒   ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈))
Theorem	grpoidinvlem4 28878*	Lemma for grpoidinv 28879. (Contributed by NM, 14-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)) → (𝐴𝐺𝑈) = (𝑈𝐺𝐴))
Theorem	grpoidinv 28879*	A group has a left and right identity element, and every member has a left and right inverse. (Contributed by NM, 14-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ GrpOp → ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑥) = 𝑢 ∧ (𝑥𝐺𝑦) = 𝑢)))
Theorem	grpoideu 28880*	The left identity element of a group is unique. Lemma 2.2.1(a) of [Herstein] p. 55. (Contributed by NM, 14-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ GrpOp → ∃!𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥)
Theorem	grporndm 28881	A group's range in terms of its domain. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.)
⊢ (𝐺 ∈ GrpOp → ran 𝐺 = dom dom 𝐺)
Theorem	0ngrp 28882	The empty set is not a group. (Contributed by NM, 25-Apr-2007.) (New usage is discouraged.)
⊢ ¬ ∅ ∈ GrpOp
Theorem	gidval 28883*	The value of the identity element of a group. (Contributed by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ 𝑉 → (GId‘𝐺) = (℩𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)))
Theorem	grpoidval 28884*	Lemma for grpoidcl 28885 and others. (Contributed by NM, 5-Feb-2010.) (Proof shortened by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    ⇒   ⊢ (𝐺 ∈ GrpOp → 𝑈 = (℩𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥))
Theorem	grpoidcl 28885	The identity element of a group belongs to the group. (Contributed by NM, 24-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    ⇒   ⊢ (𝐺 ∈ GrpOp → 𝑈 ∈ 𝑋)
Theorem	grpoidinv2 28886*	A group's properties using the explicit identity element. (Contributed by NM, 5-Feb-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (((𝑈𝐺𝐴) = 𝐴 ∧ (𝐴𝐺𝑈) = 𝐴) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))
Theorem	grpolid 28887	The identity element of a group is a left identity. (Contributed by NM, 24-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝑈𝐺𝐴) = 𝐴)
Theorem	grporid 28888	The identity element of a group is a right identity. (Contributed by NM, 24-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝑈) = 𝐴)
Theorem	grporcan 28889	Right cancellation law for groups. (Contributed by NM, 26-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐶) = (𝐵𝐺𝐶) ↔ 𝐴 = 𝐵))
Theorem	grpoinveu 28890*	The left inverse element of a group is unique. Lemma 2.2.1(b) of [Herstein] p. 55. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → ∃!𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)
Theorem	grpoid 28891	Two ways of saying that an element of a group is the identity element. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝐴 = 𝑈 ↔ (𝐴𝐺𝐴) = 𝐴))
Theorem	grporn 28892	The range of a group operation. Useful for satisfying group base set hypotheses of the form 𝑋 = ran 𝐺. (Contributed by NM, 5-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 ∈ GrpOp    &   ⊢ dom 𝐺 = (𝑋 × 𝑋)    ⇒   ⊢ 𝑋 = ran 𝐺
Theorem	grpoinvfval 28893*	The inverse function of a group. (Contributed by NM, 26-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ (𝐺 ∈ GrpOp → 𝑁 = (𝑥 ∈ 𝑋 ↦ (℩𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈)))
Theorem	grpoinvval 28894*	The inverse of a group element. (Contributed by NM, 26-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (℩𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈))
Theorem	grpoinvcl 28895	A group element's inverse is a group element. (Contributed by NM, 27-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ 𝑋)
Theorem	grpoinv 28896	The properties of a group element's inverse. (Contributed by NM, 27-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (((𝑁‘𝐴)𝐺𝐴) = 𝑈 ∧ (𝐴𝐺(𝑁‘𝐴)) = 𝑈))
Theorem	grpolinv 28897	The left inverse of a group element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝐴)𝐺𝐴) = 𝑈)
Theorem	grporinv 28898	The right inverse of a group element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺(𝑁‘𝐴)) = 𝑈)
Theorem	grpoinvid1 28899	The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘𝐴) = 𝐵 ↔ (𝐴𝐺𝐵) = 𝑈))
Theorem	grpoinvid2 28900	The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘𝐴) = 𝐵 ↔ (𝐵𝐺𝐴) = 𝑈))