P. 305 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 30401-30500   *Has distinct variable group(s)

Type	Label	Description
Statement
Axiom	ax-flt 30401	This factoid is e.g. useful for nrt2irr 30402. Andrew has a proof, I'll have a go at formalizing it after my coffee break. In the mean time let's add it as an axiom. (Contributed by Prof. Loof Lirpa, 1-Apr-2025.) (New usage is discouraged.)
⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ (𝑋 ∈ ℕ ∧ 𝑌 ∈ ℕ ∧ 𝑍 ∈ ℕ)) → ((𝑋↑𝑁) + (𝑌↑𝑁)) ≠ (𝑍↑𝑁))
Theorem	nrt2irr 30402	The 𝑁-th root of 2 is irrational for 𝑁 greater than 2. For 𝑁 = 2, see sqrt2irr 16217. This short and rather elegant proof has the minor disadvantage that it refers to ax-flt 30401, which is still to be formalized. For a proof not requiring ax-flt 30401, see rtprmirr 26670. (Contributed by Prof. Loof Lirpa, 1-Apr-2025.) (Proof modification is discouraged.)
⊢ (𝑁 ∈ (ℤ≥‘3) → ¬ (2↑𝑐(1 / 𝑁)) ∈ ℚ)
18.3  (Future - to be reviewed and classified)
18.3.1  Planar incidence geometry
Syntax	cplig 30403	Extend class notation with the class of all planar incidence geometries.
class Plig
Definition	df-plig 30404*	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 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 30405*	The predicate "is a planar incidence geometry" for sets. (Contributed by FL, 2-Aug-2009.)
⊢ 𝑃 = ∪ 𝐺    ⇒   ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ Plig ↔ (∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 → ∃!𝑙 ∈ 𝐺 (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙)) ∧ ∀𝑙 ∈ 𝐺 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙) ∧ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙))))
Theorem	ispligb 30406*	The predicate "is a planar incidence geometry". (Contributed by BJ, 2-Dec-2021.)
⊢ 𝑃 = ∪ 𝐺    ⇒   ⊢ (𝐺 ∈ Plig ↔ (𝐺 ∈ V ∧ (∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 → ∃!𝑙 ∈ 𝐺 (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙)) ∧ ∀𝑙 ∈ 𝐺 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙) ∧ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙))))
Theorem	tncp 30407*	In any planar incidence geometry, there exist three non-collinear points. (Contributed by FL, 3-Aug-2009.)
⊢ 𝑃 = ∪ 𝐺    ⇒   ⊢ (𝐺 ∈ Plig → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙))
Theorem	l2p 30408*	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 30409*	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 30410	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 30411	Alternate version of nsnlplig 30410 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 30412	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 30413	Alternate version of n0lplig 30412 using the predicate ∉ instead of ¬ ∈ and whose proof bypasses nsnlplig 30410. (Contributed by AV, 28-Nov-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐺 ∈ Plig → ∅ ∉ 𝐺)
Theorem	eulplig 30414*	Through two distinct points of a planar incidence geometry, there is a unique line. (Contributed by BJ, 2-Dec-2021.)
⊢ 𝑃 = ∪ 𝐺    ⇒   ⊢ ((𝐺 ∈ Plig ∧ ((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ 𝐴 ≠ 𝐵)) → ∃!𝑙 ∈ 𝐺 (𝐴 ∈ 𝑙 ∧ 𝐵 ∈ 𝑙))
Theorem	pliguhgr 30415	Any planar incidence geometry 𝐺 can be regarded as a hypergraph with its points as vertices and its lines as edges. See incistruhgr 29006 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)
18.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 30416	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 30417	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 19  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)".
19.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.
19.1.1  Definitions and basic properties for groups
Syntax	cgr 30418	Extend class notation with the class of all group operations.
class GrpOp
Syntax	cgi 30419	Extend class notation with a function mapping a group operation to the group's identity element.
class GId
Syntax	cgn 30420	Extend class notation with a function mapping a group operation to the inverse function for the group.
class inv
Syntax	cgs 30421	Extend class notation with a function mapping a group operation to the division (or subtraction) operation for the group.
class /𝑔
Definition	df-grpo 30422*	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 30423*	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 30424*	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 30425*	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 30426*	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 30427*	Properties that determine a group operation. Read 𝑁 as 𝑁(𝑥). (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.)
⊢ 𝑋 ∈ V    &   ⊢ 𝐺:(𝑋 × 𝑋)⟶𝑋    &   ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))    &   ⊢ 𝑈 ∈ 𝑋    &   ⊢ (𝑥 ∈ 𝑋 → (𝑈𝐺𝑥) = 𝑥)    &   ⊢ (𝑥 ∈ 𝑋 → 𝑁 ∈ 𝑋)    &   ⊢ (𝑥 ∈ 𝑋 → (𝑁𝐺𝑥) = 𝑈)    ⇒   ⊢ 𝐺 ∈ GrpOp
Theorem	grpofo 30428	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 30429	Closure law for a group operation. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)
Theorem	grpolidinv 30430*	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 30431	The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ GrpOp → 𝑋 ≠ ∅)
Theorem	grpoass 30432	A group operation is associative. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = (𝐴𝐺(𝐵𝐺𝐶)))
Theorem	grpoidinvlem1 30433	Lemma for grpoidinv 30437. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝐺 ∈ GrpOp ∧ (𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) ∧ ((𝑌𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝐴) = 𝐴)) → (𝑈𝐺𝐴) = 𝑈)
Theorem	grpoidinvlem2 30434	Lemma for grpoidinv 30437. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝐺 ∈ GrpOp ∧ (𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) ∧ ((𝑈𝐺𝑌) = 𝑌 ∧ (𝑌𝐺𝐴) = 𝑈)) → ((𝐴𝐺𝑌)𝐺(𝐴𝐺𝑌)) = (𝐴𝐺𝑌))
Theorem	grpoidinvlem3 30435*	Lemma for grpoidinv 30437. (Contributed by NM, 11-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)    &   ⊢ (𝜓 ↔ ∀𝑥 ∈ 𝑋 ∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈)    ⇒   ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈))
Theorem	grpoidinvlem4 30436*	Lemma for grpoidinv 30437. (Contributed by NM, 14-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)) → (𝐴𝐺𝑈) = (𝑈𝐺𝐴))
Theorem	grpoidinv 30437*	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 30438*	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 30439	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 30440	The empty set is not a group. (Contributed by NM, 25-Apr-2007.) (New usage is discouraged.)
⊢ ¬ ∅ ∈ GrpOp
Theorem	gidval 30441*	The value of the identity element of a group. (Contributed by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ 𝑉 → (GId‘𝐺) = (℩𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)))
Theorem	grpoidval 30442*	Lemma for grpoidcl 30443 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 30443	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 30444*	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 30445	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 30446	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 30447	Right cancellation law for groups. (Contributed by NM, 26-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐶) = (𝐵𝐺𝐶) ↔ 𝐴 = 𝐵))
Theorem	grpoinveu 30448*	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 30449	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 30450	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 30451*	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 30452*	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 30453	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 30454	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 30455	The left inverse of a group element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝐴)𝐺𝐴) = 𝑈)
Theorem	grporinv 30456	The right inverse of a group element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺(𝑁‘𝐴)) = 𝑈)
Theorem	grpoinvid1 30457	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 30458	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	grpolcan 30459	Left cancellation law for groups. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐶𝐺𝐴) = (𝐶𝐺𝐵) ↔ 𝐴 = 𝐵))
Theorem	grpo2inv 30460	Double inverse law for groups. Lemma 2.2.1(c) of [Herstein] p. 55. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝑁‘(𝑁‘𝐴)) = 𝐴)
Theorem	grpoinvf 30461	Mapping of the inverse function of a group. (Contributed by NM, 29-Mar-2008.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ (𝐺 ∈ GrpOp → 𝑁:𝑋–1-1-onto→𝑋)
Theorem	grpoinvop 30462	The inverse of the group operation reverses the arguments. Lemma 2.2.1(d) of [Herstein] p. 55. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐺𝐵)) = ((𝑁‘𝐵)𝐺(𝑁‘𝐴)))
Theorem	grpodivfval 30463*	Group division (or subtraction) operation. (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑁 = (inv‘𝐺)    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ (𝐺 ∈ GrpOp → 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝐺(𝑁‘𝑦))))
Theorem	grpodivval 30464	Group division (or subtraction) operation value. (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑁 = (inv‘𝐺)    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐴𝐺(𝑁‘𝐵)))
Theorem	grpodivinv 30465	Group division by an inverse. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑁 = (inv‘𝐺)    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷(𝑁‘𝐵)) = (𝐴𝐺𝐵))
Theorem	grpoinvdiv 30466	Inverse of a group division. (Contributed by NM, 24-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑁 = (inv‘𝐺)    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐷𝐵)) = (𝐵𝐷𝐴))
Theorem	grpodivf 30467	Mapping for group division. (Contributed by NM, 10-Apr-2008.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ (𝐺 ∈ GrpOp → 𝐷:(𝑋 × 𝑋)⟶𝑋)
Theorem	grpodivcl 30468	Closure of group division (or subtraction) operation. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ 𝑋)
Theorem	grpodivdiv 30469	Double group division. (Contributed by NM, 24-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷(𝐵𝐷𝐶)) = (𝐴𝐺(𝐶𝐷𝐵)))
Theorem	grpomuldivass 30470	Associative-type law for multiplication and division. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐷𝐶) = (𝐴𝐺(𝐵𝐷𝐶)))
Theorem	grpodivid 30471	Division of a group member by itself. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    &   ⊢ 𝑈 = (GId‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝐴𝐷𝐴) = 𝑈)
Theorem	grponpcan 30472	Cancellation law for group division. (npcan 11430 analog.) (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐷𝐵)𝐺𝐵) = 𝐴)
19.1.2  Abelian groups
Syntax	cablo 30473	Extend class notation with the class of all Abelian group operations.
class AbelOp
Definition	df-ablo 30474*	Define the class of all Abelian group operations. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.)
⊢ AbelOp = {𝑔 ∈ GrpOp ∣ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(𝑥𝑔𝑦) = (𝑦𝑔𝑥)}
Theorem	isablo 30475*	The predicate "is an Abelian (commutative) group operation." (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ AbelOp ↔ (𝐺 ∈ GrpOp ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐺𝑦) = (𝑦𝐺𝑥)))
Theorem	ablogrpo 30476	An Abelian group operation is a group operation. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.)
⊢ (𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp)
Theorem	ablocom 30477	An Abelian group operation is commutative. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝐺 ∈ AbelOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) = (𝐵𝐺𝐴))
Theorem	ablo32 30478	Commutative/associative law for Abelian groups. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐺𝐵))
Theorem	ablo4 30479	Commutative/associative law for Abelian groups. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺(𝐶𝐺𝐷)) = ((𝐴𝐺𝐶)𝐺(𝐵𝐺𝐷)))
Theorem	isabloi 30480*	Properties that determine an Abelian group operation. (Contributed by NM, 5-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 ∈ GrpOp    &   ⊢ dom 𝐺 = (𝑋 × 𝑋)    &   ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥))    ⇒   ⊢ 𝐺 ∈ AbelOp
Theorem	ablomuldiv 30481	Law for group multiplication and division. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐷𝐶) = ((𝐴𝐷𝐶)𝐺𝐵))
Theorem	ablodivdiv 30482	Law for double group division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷(𝐵𝐷𝐶)) = ((𝐴𝐷𝐵)𝐺𝐶))
Theorem	ablodivdiv4 30483	Law for double group division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐷𝐶) = (𝐴𝐷(𝐵𝐺𝐶)))
Theorem	ablodiv32 30484	Swap the second and third terms in a double division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐷𝐶) = ((𝐴𝐷𝐶)𝐷𝐵))
Theorem	ablonncan 30485	Cancellation law for group division. (nncan 11451 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ AbelOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷(𝐴𝐷𝐵)) = 𝐵)
Theorem	ablonnncan1 30486	Cancellation law for group division. (nnncan1 11458 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐷(𝐴𝐷𝐶)) = (𝐶𝐷𝐵))
19.2  Complex vector spaces
19.2.1  Definition and basic properties
Syntax	cvc 30487	Extend class notation with the class of all complex vector spaces.
class CVecOLD
Definition	df-vc 30488*	Define the class of all complex vector spaces. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
⊢ CVecOLD = {⟨𝑔, 𝑠⟩ ∣ (𝑔 ∈ AbelOp ∧ 𝑠:(ℂ × ran 𝑔)⟶ran 𝑔 ∧ ∀𝑥 ∈ ran 𝑔((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))))}
Theorem	vcrel 30489	The class of all complex vector spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.)
⊢ Rel CVecOLD
Theorem	vciOLD 30490*	Obsolete version of cvsi 25030. The properties of a complex vector space, which is an Abelian group (i.e. the vectors, with the operation of vector addition) accompanied by a scalar multiplication operation on the field of complex numbers. The variable 𝑊 was chosen because V is already used for the universal class. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑆 = (2nd ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑊 ∈ CVecOLD → (𝐺 ∈ AbelOp ∧ 𝑆:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ((1𝑆𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑆(𝑥𝐺𝑧)) = ((𝑦𝑆𝑥)𝐺(𝑦𝑆𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑆𝑥) = ((𝑦𝑆𝑥)𝐺(𝑧𝑆𝑥)) ∧ ((𝑦 · 𝑧)𝑆𝑥) = (𝑦𝑆(𝑧𝑆𝑥)))))))
Theorem	vcsm 30491	Functionality of th scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑆 = (2nd ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑊 ∈ CVecOLD → 𝑆:(ℂ × 𝑋)⟶𝑋)
Theorem	vccl 30492	Closure of the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑆 = (2nd ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑊 ∈ CVecOLD ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (𝐴𝑆𝐵) ∈ 𝑋)
Theorem	vcidOLD 30493	Identity element for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) Obsolete theorem, use clmvs1 24993 together with cvsclm 25026 instead. (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑆 = (2nd ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴)
Theorem	vcdi 30494	Distributive law for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑆 = (2nd ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑊 ∈ CVecOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑆(𝐵𝐺𝐶)) = ((𝐴𝑆𝐵)𝐺(𝐴𝑆𝐶)))
Theorem	vcdir 30495	Distributive law for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑆 = (2nd ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑊 ∈ CVecOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 + 𝐵)𝑆𝐶) = ((𝐴𝑆𝐶)𝐺(𝐵𝑆𝐶)))
Theorem	vcass 30496	Associative law for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑆 = (2nd ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑊 ∈ CVecOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 · 𝐵)𝑆𝐶) = (𝐴𝑆(𝐵𝑆𝐶)))
Theorem	vc2OLD 30497	A vector plus itself is two times the vector. (Contributed by NM, 1-Feb-2007.) Obsolete theorem, use clmvs2 24994 together with cvsclm 25026 instead. (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑆 = (2nd ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝐴) = (2𝑆𝐴))
Theorem	vcablo 30498	Vector addition is an Abelian group operation. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    ⇒   ⊢ (𝑊 ∈ CVecOLD → 𝐺 ∈ AbelOp)
Theorem	vcgrp 30499	Vector addition is a group operation. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    ⇒   ⊢ (𝑊 ∈ CVecOLD → 𝐺 ∈ GrpOp)
Theorem	vclcan 30500	Left cancellation law for vector addition. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑊 ∈ CVecOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐶𝐺𝐴) = (𝐶𝐺𝐵) ↔ 𝐴 = 𝐵))