P. 208 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20701-20800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fldsdrgfld 20701	A sub-division-ring of a field is itself a field, so it is a subfield. We can therefore use SubDRing to express subfields. (Contributed by Thierry Arnoux, 11-Jan-2025.)
⊢ ((𝐹 ∈ Field ∧ 𝐴 ∈ (SubDRing‘𝐹)) → (𝐹 ↾s 𝐴) ∈ Field)
Theorem	acsfn1p 20702*	Construction of a closure rule from a one-parameter partial operation. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎} ∈ (ACS‘𝑋))
Theorem	subrgacs 20703	Closure property of subrings. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (SubRing‘𝑅) ∈ (ACS‘𝐵))
Theorem	sdrgacs 20704	Closure property of division subrings. (Contributed by Mario Carneiro, 3-Oct-2015.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing → (SubDRing‘𝑅) ∈ (ACS‘𝐵))
Theorem	cntzsdrg 20705	Centralizers in division rings/fields are subfields. (Contributed by Mario Carneiro, 3-Oct-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubDRing‘𝑅))
Theorem	subdrgint 20706*	The intersection of a nonempty collection of sub division rings is a sub division ring. (Contributed by Thierry Arnoux, 21-Aug-2023.)
⊢ 𝐿 = (𝑅 ↾s ∩ 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ⊆ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑆 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑅 ↾s 𝑠) ∈ DivRing)    ⇒   ⊢ (𝜑 → 𝐿 ∈ DivRing)
Theorem	sdrgint 20707	The intersection of a nonempty collection of sub division rings is a sub division ring. (Contributed by Thierry Arnoux, 21-Aug-2023.)
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ (SubDRing‘𝑅) ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ (SubDRing‘𝑅))
Theorem	primefld 20708	The smallest sub division ring of a division ring, here named 𝑃, is a field, called the Prime Field of 𝑅. (Suggested by GL, 4-Aug-2023.) (Contributed by Thierry Arnoux, 21-Aug-2023.)
⊢ 𝑃 = (𝑅 ↾s ∩ (SubDRing‘𝑅))    ⇒   ⊢ (𝑅 ∈ DivRing → 𝑃 ∈ Field)
Theorem	primefld0cl 20709	The prime field contains the zero element of the division ring. (Contributed by Thierry Arnoux, 22-Aug-2023.)
⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing → 0 ∈ ∩ (SubDRing‘𝑅))
Theorem	primefld1cl 20710	The prime field contains the unity element of the division ring. (Contributed by Thierry Arnoux, 22-Aug-2023.)
⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing → 1 ∈ ∩ (SubDRing‘𝑅))
10.4.3  Absolute value (abstract algebra)
Syntax	cabv 20711	The set of absolute values on a ring.
class AbsVal
Definition	df-abv 20712*	Define the set of absolute values on a ring. An absolute value is a generalization of the usual absolute value function df-abs 15161 to arbitrary rings. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ AbsVal = (𝑟 ∈ Ring ↦ {𝑓 ∈ ((0[,)+∞) ↑m (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)(((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))})
Theorem	abvfval 20713*	Value of the set of absolute values. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐴 = {𝑓 ∈ ((0[,)+∞) ↑m 𝐵) ∣ ∀𝑥 ∈ 𝐵 (((𝑓‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝐵 ((𝑓‘(𝑥 · 𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥 + 𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))})
Theorem	isabv 20714*	Elementhood in the set of absolute values. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐹 ∈ 𝐴 ↔ (𝐹:𝐵⟶(0[,)+∞) ∧ ∀𝑥 ∈ 𝐵 (((𝐹‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝐵 ((𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)))))))
Theorem	isabvd 20715*	Properties that determine an absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.) (Revised by Mario Carneiro, 4-Dec-2014.)
⊢ (𝜑 → 𝐴 = (AbsVal‘𝑅))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → + = (+g‘𝑅))    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → 0 = (0g‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐹:𝐵⟶ℝ)    &   ⊢ (𝜑 → (𝐹‘ 0 ) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) → 0 < (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝐴)
Theorem	abvrcl 20716	Reverse closure for the absolute value set. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐴 → 𝑅 ∈ Ring)
Theorem	abvfge0 20717	An absolute value is a function from the ring to the nonnegative real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐴 → 𝐹:𝐵⟶(0[,)+∞))
Theorem	abvf 20718	An absolute value is a function from the ring to the real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐴 → 𝐹:𝐵⟶ℝ)
Theorem	abvcl 20719	An absolute value is a function from the ring to the real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ ℝ)
Theorem	abvge0 20720	The absolute value of a number is greater than or equal to zero. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → 0 ≤ (𝐹‘𝑋))
Theorem	abveq0 20721	The value of an absolute value is zero iff the argument is zero. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → ((𝐹‘𝑋) = 0 ↔ 𝑋 = 0 ))
Theorem	abvne0 20722	The absolute value of a nonzero number is nonzero. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐹‘𝑋) ≠ 0)
Theorem	abvgt0 20723	The absolute value of a nonzero number is strictly positive. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 0 < (𝐹‘𝑋))
Theorem	abvmul 20724	An absolute value distributes under multiplication. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 · 𝑌)) = ((𝐹‘𝑋) · (𝐹‘𝑌)))
Theorem	abvtri 20725	An absolute value satisfies the triangle inequality. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑌)))
Theorem	abv0 20726	The absolute value of zero is zero. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐴 → (𝐹‘ 0 ) = 0)
Theorem	abv1z 20727	The absolute value of one is one in a non-trivial ring. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → (𝐹‘ 1 ) = 1)
Theorem	abv1 20728	The absolute value of one is one in a division ring. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐴) → (𝐹‘ 1 ) = 1)
Theorem	abvneg 20729	The absolute value of a negative is the same as that of the positive. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑁‘𝑋)) = (𝐹‘𝑋))
Theorem	abvsubtri 20730	An absolute value satisfies the triangle inequality. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ − = (-g‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 − 𝑌)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑌)))
Theorem	abvrec 20731	The absolute value distributes under reciprocal. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ (((𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 )) → (𝐹‘(𝐼‘𝑋)) = (1 / (𝐹‘𝑋)))
Theorem	abvdiv 20732	The absolute value distributes under division. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ (((𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 )) → (𝐹‘(𝑋 / 𝑌)) = ((𝐹‘𝑋) / (𝐹‘𝑌)))
Theorem	abvdom 20733	Any ring with an absolute value is a domain, which is to say that it contains no zero divisors. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 )) → (𝑋 · 𝑌) ≠ 0 )
Theorem	abvres 20734	The restriction of an absolute value to a subring is an absolute value. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝑆 = (𝑅 ↾s 𝐶)    &   ⊢ 𝐵 = (AbsVal‘𝑆)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) → (𝐹 ↾ 𝐶) ∈ 𝐵)
Theorem	abvtrivd 20735*	The trivial absolute value. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if(𝑥 = 0 , 0, 1))    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → (𝑦 · 𝑧) ≠ 0 )    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝐴)
Theorem	abvtrivg 20736*	The trivial absolute value. This theorem is not true for rings with zero divisors, which violate the multiplication axiom; abvdom 20733 is the converse of this theorem. (Contributed by SN, 25-Jun-2025.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if(𝑥 = 0 , 0, 1))    ⇒   ⊢ (𝑅 ∈ Domn → 𝐹 ∈ 𝐴)
Theorem	abvtriv 20737*	The trivial absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if(𝑥 = 0 , 0, 1))    ⇒   ⊢ (𝑅 ∈ DivRing → 𝐹 ∈ 𝐴)
Theorem	abvpropd 20738*	If two structures have the same ring components, they have the same collection of absolute values. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (AbsVal‘𝐾) = (AbsVal‘𝐿))
Theorem	abvn0b 20739	Another characterization of domains, hinted at in abvtrivg 20736: a nonzero ring is a domain iff it has an absolute value. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ 𝐴 = (AbsVal‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ 𝐴 ≠ ∅))
10.4.4  Star rings
Syntax	cstf 20740	Extend class notation with the functionalization of the *-ring involution.
class *rf
Syntax	csr 20741	Extend class notation with class of all *-rings.
class *-Ring
Definition	df-staf 20742*	Define the functionalization of the involution in a star ring. This is not strictly necessary but by having *𝑟 as an actual function we can state the principal properties of an involution much more cleanly. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ *rf = (𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑓) ↦ ((*𝑟‘𝑓)‘𝑥)))
Definition	df-srng 20743*	Define class of all star rings. A star ring is a ring with an involution (conjugation) function. Involution (unlike say the ring zero) is not unique and therefore must be added as a new component to the ring. For example, two possible involutions for complex numbers are the identity function and complex conjugation. Definition of involution in [Holland95] p. 204. (Contributed by NM, 22-Sep-2011.) (Revised by Mario Carneiro, 6-Oct-2015.)
⊢ *-Ring = {𝑓 ∣ [(*rf‘𝑓) / 𝑖](𝑖 ∈ (𝑓 RingHom (oppr‘𝑓)) ∧ 𝑖 = ◡𝑖)}
Theorem	staffval 20744*	The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ ∙ = (*rf‘𝑅)    ⇒   ⊢ ∙ = (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥))
Theorem	stafval 20745	The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ ∙ = (*rf‘𝑅)    ⇒   ⊢ (𝐴 ∈ 𝐵 → ( ∙ ‘𝐴) = ( ∗ ‘𝐴))
Theorem	staffn 20746	The functionalization is equal to the original function, if it is a function on the right base set. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ ∙ = (*rf‘𝑅)    ⇒   ⊢ ( ∗ Fn 𝐵 → ∙ = ∗ )
Theorem	issrng 20747	The predicate "is a star ring". (Contributed by NM, 22-Sep-2011.) (Revised by Mario Carneiro, 6-Oct-2015.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ ∗ = (*rf‘𝑅)    ⇒   ⊢ (𝑅 ∈ *-Ring ↔ ( ∗ ∈ (𝑅 RingHom 𝑂) ∧ ∗ = ◡ ∗ ))
Theorem	srngrhm 20748	The involution function in a star ring is an antiautomorphism. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ ∗ = (*rf‘𝑅)    ⇒   ⊢ (𝑅 ∈ *-Ring → ∗ ∈ (𝑅 RingHom 𝑂))
Theorem	srngring 20749	A star ring is a ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (𝑅 ∈ *-Ring → 𝑅 ∈ Ring)
Theorem	srngcnv 20750	The involution function in a star ring is its own inverse function. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ∗ = (*rf‘𝑅)    ⇒   ⊢ (𝑅 ∈ *-Ring → ∗ = ◡ ∗ )
Theorem	srngf1o 20751	The involution function in a star ring is a bijection. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ∗ = (*rf‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ *-Ring → ∗ :𝐵–1-1-onto→𝐵)
Theorem	srngcl 20752	The involution function in a star ring is closed in the ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵) → ( ∗ ‘𝑋) ∈ 𝐵)
Theorem	srngnvl 20753	The involution function in a star ring is an involution. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵) → ( ∗ ‘( ∗ ‘𝑋)) = 𝑋)
Theorem	srngadd 20754	The involution function in a star ring distributes over addition. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ∗ ‘(𝑋 + 𝑌)) = (( ∗ ‘𝑋) + ( ∗ ‘𝑌)))
Theorem	srngmul 20755	The involution function in a star ring distributes over multiplication, with a change in the order of the factors. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ∗ ‘(𝑋 · 𝑌)) = (( ∗ ‘𝑌) · ( ∗ ‘𝑋)))
Theorem	srng1 20756	The conjugate of the ring identity is the identity. (This is sometimes taken as an axiom, and indeed the proof here follows because we defined *𝑟 to be a ring homomorphism, which preserves 1; nevertheless, it is redundant, as can be seen from the proof of issrngd 20758.) (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ *-Ring → ( ∗ ‘ 1 ) = 1 )
Theorem	srng0 20757	The conjugate of the ring zero is zero. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ *-Ring → ( ∗ ‘ 0 ) = 0 )
Theorem	issrngd 20758*	Properties that determine a star ring. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Mario Carneiro, 6-Oct-2015.)
⊢ (𝜑 → 𝐾 = (Base‘𝑅))    &   ⊢ (𝜑 → + = (+g‘𝑅))    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → ∗ = (*𝑟‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ( ∗ ‘𝑥) ∈ 𝐾)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → ( ∗ ‘(𝑥 + 𝑦)) = (( ∗ ‘𝑥) + ( ∗ ‘𝑦)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → ( ∗ ‘(𝑥 · 𝑦)) = (( ∗ ‘𝑦) · ( ∗ ‘𝑥)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ( ∗ ‘( ∗ ‘𝑥)) = 𝑥)    ⇒   ⊢ (𝜑 → 𝑅 ∈ *-Ring)
Theorem	idsrngd 20759*	A commutative ring is a star ring when the conjugate operation is the identity. (Contributed by Thierry Arnoux, 19-Apr-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( ∗ ‘𝑥) = 𝑥)    ⇒   ⊢ (𝜑 → 𝑅 ∈ *-Ring)
10.4.5  Totally ordered rings and fields
Syntax	corng 20760	Extend class notation with the class of all ordered rings.
class oRing
Syntax	cofld 20761	Extend class notation with the class of all ordered fields.
class oField
Definition	df-orng 20762*	Define class of all ordered rings. An ordered ring is a ring with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ oRing = {𝑟 ∈ (Ring ∩ oGrp) ∣ [(Base‘𝑟) / 𝑣][(0g‘𝑟) / 𝑧][(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))}
Definition	df-ofld 20763	Define class of all ordered fields. An ordered field is a field with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 18-Jan-2018.)
⊢ oField = (Field ∩ oRing)
Theorem	isorng 20764*	An ordered ring is a ring with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 18-Jan-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ≤ = (le‘𝑅)    ⇒   ⊢ (𝑅 ∈ oRing ↔ (𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏) → 0 ≤ (𝑎 · 𝑏))))
Theorem	orngring 20765	An ordered ring is a ring. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ (𝑅 ∈ oRing → 𝑅 ∈ Ring)
Theorem	orngogrp 20766	An ordered ring is an ordered group. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ (𝑅 ∈ oRing → 𝑅 ∈ oGrp)
Theorem	isofld 20767	An ordered field is a field with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ (𝐹 ∈ oField ↔ (𝐹 ∈ Field ∧ 𝐹 ∈ oRing))
Theorem	orngmul 20768	In an ordered ring, the ordering is compatible with the ring multiplication operation. (Contributed by Thierry Arnoux, 20-Jan-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ≤ = (le‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ oRing ∧ (𝑋 ∈ 𝐵 ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ 𝐵 ∧ 0 ≤ 𝑌)) → 0 ≤ (𝑋 · 𝑌))
Theorem	orngsqr 20769	In an ordered ring, all squares are positive. (Contributed by Thierry Arnoux, 20-Jan-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ≤ = (le‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) → 0 ≤ (𝑋 · 𝑋))
Theorem	ornglmulle 20770	In an ordered ring, multiplication with a positive does not change comparison. (Contributed by Thierry Arnoux, 10-Apr-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ oRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ ≤ = (le‘𝑅)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 0 ≤ 𝑍)    ⇒   ⊢ (𝜑 → (𝑍 · 𝑋) ≤ (𝑍 · 𝑌))
Theorem	orngrmulle 20771	In an ordered ring, multiplication with a positive does not change comparison. (Contributed by Thierry Arnoux, 10-Apr-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ oRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ ≤ = (le‘𝑅)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 0 ≤ 𝑍)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑍) ≤ (𝑌 · 𝑍))
Theorem	ornglmullt 20772	In an ordered ring, multiplication with a positive does not change strict comparison. (Contributed by Thierry Arnoux, 9-Apr-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ oRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ < = (lt‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 < 𝑌)    &   ⊢ (𝜑 → 0 < 𝑍)    ⇒   ⊢ (𝜑 → (𝑍 · 𝑋) < (𝑍 · 𝑌))
Theorem	orngrmullt 20773	In an ordered ring, multiplication with a positive does not change strict comparison. (Contributed by Thierry Arnoux, 9-Apr-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ oRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ < = (lt‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 < 𝑌)    &   ⊢ (𝜑 → 0 < 𝑍)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑍) < (𝑌 · 𝑍))
Theorem	orngmullt 20774	In an ordered ring, the strict ordering is compatible with the ring multiplication operation. (Contributed by Thierry Arnoux, 9-Sep-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ < = (lt‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ oRing)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 0 < 𝑋)    &   ⊢ (𝜑 → 0 < 𝑌)    ⇒   ⊢ (𝜑 → 0 < (𝑋 · 𝑌))
Theorem	ofldfld 20775	An ordered field is a field. (Contributed by Thierry Arnoux, 20-Jan-2018.)
⊢ (𝐹 ∈ oField → 𝐹 ∈ Field)
Theorem	ofldtos 20776	An ordered field is a totally ordered set. (Contributed by Thierry Arnoux, 20-Jan-2018.)
⊢ (𝐹 ∈ oField → 𝐹 ∈ Toset)
Theorem	orng0le1 20777	In an ordered ring, the ring unity is positive. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ 0 = (0g‘𝐹)    &   ⊢ 1 = (1r‘𝐹)    &   ⊢ ≤ = (le‘𝐹)    ⇒   ⊢ (𝐹 ∈ oRing → 0 ≤ 1 )
Theorem	ofldlt1 20778	In an ordered field, the ring unity is strictly positive. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ 0 = (0g‘𝐹)    &   ⊢ 1 = (1r‘𝐹)    &   ⊢ < = (lt‘𝐹)    ⇒   ⊢ (𝐹 ∈ oField → 0 < 1 )
Theorem	suborng 20779	Every subring of an ordered ring is also an ordered ring. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → (𝑅 ↾s 𝐴) ∈ oRing)
Theorem	subofld 20780	Every subfield of an ordered field is also an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ ((𝐹 ∈ oField ∧ (𝐹 ↾s 𝐴) ∈ Field) → (𝐹 ↾s 𝐴) ∈ oField)
10.5  Left modules
10.5.1  Definition and basic properties
Syntax	clmod 20781	Extend class notation with class of all left modules.
class LMod
Syntax	cscaf 20782	The functionalization of the scalar multiplication operation.
class ·sf
Definition	df-lmod 20783*	Define the class of all left modules, which are generalizations of left vector spaces. A left module over a ring is an (Abelian) group (vectors) together with a ring (scalars) and a left scalar product connecting them. (Contributed by NM, 4-Nov-2013.)
⊢ LMod = {𝑔 ∈ Grp ∣ [(Base‘𝑔) / 𝑣][(+g‘𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠 ‘𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)))}
Definition	df-scaf 20784*	Define the functionalization of the ·𝑠 operator. This restricts the value of ·𝑠 to the stated domain, which is necessary when working with restricted structures, whose operations may be defined on a larger set than the true base. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ ·sf = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠 ‘𝑔)𝑦)))
Theorem	islmod 20785*	The predicate "is a left module". (Contributed by NM, 4-Nov-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ ⨣ = (+g‘𝐹)    &   ⊢ × = (.r‘𝐹)    &   ⊢ 1 = (1r‘𝐹)    ⇒   ⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
Theorem	lmodlema 20786	Lemma for properties of a left module. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ ⨣ = (+g‘𝐹)    &   ⊢ × = (.r‘𝐹)    &   ⊢ 1 = (1r‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌)))
Theorem	islmodd 20787*	Properties that determine a left module. See note in isgrpd2 18853 regarding the 𝜑 on hypotheses that name structure components. (Contributed by Mario Carneiro, 22-Jun-2014.)
⊢ (𝜑 → 𝑉 = (Base‘𝑊))    &   ⊢ (𝜑 → + = (+g‘𝑊))    &   ⊢ (𝜑 → 𝐹 = (Scalar‘𝑊))    &   ⊢ (𝜑 → · = ( ·𝑠 ‘𝑊))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐹))    &   ⊢ (𝜑 → ⨣ = (+g‘𝐹))    &   ⊢ (𝜑 → × = (.r‘𝐹))    &   ⊢ (𝜑 → 1 = (1r‘𝐹))    &   ⊢ (𝜑 → 𝐹 ∈ Ring)    &   ⊢ (𝜑 → 𝑊 ∈ Grp)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑉) → (𝑥 · 𝑦) ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 1 · 𝑥) = 𝑥)    ⇒   ⊢ (𝜑 → 𝑊 ∈ LMod)
Theorem	lmodgrp 20788	A left module is a group. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 25-Jun-2014.)
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
Theorem	lmodring 20789	The scalar component of a left module is a ring. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring)
Theorem	lmodfgrp 20790	The scalar component of a left module is an additive group. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Grp)
Theorem	lmodgrpd 20791	A left module is a group. (Contributed by SN, 16-May-2024.)
⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝑊 ∈ Grp)
Theorem	lmodbn0 20792	The base set of a left module is nonempty. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → 𝐵 ≠ ∅)
Theorem	lmodacl 20793	Closure of ring addition for a left module. (Contributed by NM, 14-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ + = (+g‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 + 𝑌) ∈ 𝐾)
Theorem	lmodmcl 20794	Closure of ring multiplication for a left module. (Contributed by NM, 14-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = (.r‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 · 𝑌) ∈ 𝐾)
Theorem	lmodsn0 20795	The set of scalars in a left module is nonempty. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ (𝑊 ∈ LMod → 𝐵 ≠ ∅)
Theorem	lmodvacl 20796	Closure of vector addition for a left module. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉)
Theorem	lmodass 20797	Left module vector sum is associative. (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Theorem	lmodlcan 20798	Left cancellation law for vector sum. (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉)) → ((𝑍 + 𝑋) = (𝑍 + 𝑌) ↔ 𝑋 = 𝑌))
Theorem	lmodvscl 20799	Closure of scalar product for a left module. (hvmulcl 30975 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑅 · 𝑋) ∈ 𝑉)
Theorem	lmodvscld 20800	Closure of scalar product for a left module. (Contributed by SN, 15-Mar-2025.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑅 · 𝑋) ∈ 𝑉)