P. 211 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21001-21100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	abvdiv 21001	The absolute value distributes under division. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ (((𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 )) → (𝐹‘(𝑋 / 𝑌)) = ((𝐹‘𝑋) / (𝐹‘𝑌)))
Theorem	abvdom 21002	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 21003	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 21004*	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 21005*	The trivial absolute value. This theorem is not true for rings with zero divisors, which violate the multiplication axiom; abvdom 21002 is the converse of this theorem. (Contributed by SN, 25-Jun-2025.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if(𝑥 = 0 , 0, 1))    ⇒   ⊢ (𝑅 ∈ Domn → 𝐹 ∈ 𝐴)
Theorem	abvtriv 21006*	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 21007*	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 21008	Another characterization of domains, hinted at in abvtrivg 21005: 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 21009	Extend class notation with the functionalization of the *-ring involution.
class *rf
Syntax	csr 21010	Extend class notation with class of all *-rings.
class *-Ring
Definition	df-staf 21011*	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 21012*	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 21013*	The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ ∙ = (*rf‘𝑅)    ⇒   ⊢ ∙ = (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥))
Theorem	stafval 21014	The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ ∙ = (*rf‘𝑅)    ⇒   ⊢ (𝐴 ∈ 𝐵 → ( ∙ ‘𝐴) = ( ∗ ‘𝐴))
Theorem	staffn 21015	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 21016	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 21017	The involution function in a star ring is an antiautomorphism. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ ∗ = (*rf‘𝑅)    ⇒   ⊢ (𝑅 ∈ *-Ring → ∗ ∈ (𝑅 RingHom 𝑂))
Theorem	srngring 21018	A star ring is a ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (𝑅 ∈ *-Ring → 𝑅 ∈ Ring)
Theorem	srngcnv 21019	The involution function in a star ring is its own inverse function. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ∗ = (*rf‘𝑅)    ⇒   ⊢ (𝑅 ∈ *-Ring → ∗ = ◡ ∗ )
Theorem	srngf1o 21020	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 21021	The involution function in a star ring is closed in the ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵) → ( ∗ ‘𝑋) ∈ 𝐵)
Theorem	srngnvl 21022	The involution function in a star ring is an involution. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵) → ( ∗ ‘( ∗ ‘𝑋)) = 𝑋)
Theorem	srngadd 21023	The involution function in a star ring distributes over addition. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ∗ ‘(𝑋 + 𝑌)) = (( ∗ ‘𝑋) + ( ∗ ‘𝑌)))
Theorem	srngmul 21024	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 21025	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 21027.) (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ *-Ring → ( ∗ ‘ 1 ) = 1 )
Theorem	srng0 21026	The conjugate of the ring zero is zero. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ *-Ring → ( ∗ ‘ 0 ) = 0 )
Theorem	issrngd 21027*	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 21028*	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 21029	Extend class notation with the class of all ordered rings.
class oRing
Syntax	cofld 21030	Extend class notation with the class of all ordered fields.
class oField
Definition	df-orng 21031*	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 21032	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 21033*	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 21034	An ordered ring is a ring. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ (𝑅 ∈ oRing → 𝑅 ∈ Ring)
Theorem	orngogrp 21035	An ordered ring is an ordered group. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ (𝑅 ∈ oRing → 𝑅 ∈ oGrp)
Theorem	isofld 21036	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 21037	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 21038	In an ordered ring, all squares are positive. (Contributed by Thierry Arnoux, 20-Jan-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ≤ = (le‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) → 0 ≤ (𝑋 · 𝑋))
Theorem	ornglmulle 21039	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 21040	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 21041	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 21042	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 21043	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 21044	An ordered field is a field. (Contributed by Thierry Arnoux, 20-Jan-2018.)
⊢ (𝐹 ∈ oField → 𝐹 ∈ Field)
Theorem	ofldtos 21045	An ordered field is a totally ordered set. (Contributed by Thierry Arnoux, 20-Jan-2018.)
⊢ (𝐹 ∈ oField → 𝐹 ∈ Toset)
Theorem	orng0le1 21046	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 21047	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 21048	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 21049	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 21050	Extend class notation with class of all left modules.
class LMod
Syntax	cscaf 21051	The functionalization of the scalar multiplication operation.
class ·sf
Definition	df-lmod 21052*	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 21053*	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 21054*	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 21055	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 21056*	Properties that determine a left module. See note in isgrpd2 19086 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 21057	A left module is a group. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 25-Jun-2014.)
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
Theorem	lmodring 21058	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 21059	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 21060	A left module is a group. (Contributed by SN, 16-May-2024.)
⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝑊 ∈ Grp)
Theorem	lmodbn0 21061	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 21062	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 21063	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 21064	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 21065	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 21066	Left module vector sum is associative. (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Theorem	lmodlcan 21067	Left cancellation law for vector sum. (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉)) → ((𝑍 + 𝑋) = (𝑍 + 𝑌) ↔ 𝑋 = 𝑌))
Theorem	lmodvscl 21068	Closure of scalar product for a left module. (hvmulcl 31502 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑅 · 𝑋) ∈ 𝑉)
Theorem	lmodvscld 21069	Closure of scalar product for a left module. (Contributed by SN, 15-Mar-2025.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑅 · 𝑋) ∈ 𝑉)
Theorem	scaffval 21070*	The scalar multiplication operation as a function. (Contributed by Mario Carneiro, 5-Oct-2015.) (Proof shortened by AV, 2-Mar-2024.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ ∙ = ( ·sf ‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ ∙ = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦))
Theorem	scafval 21071	The scalar multiplication operation as a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ ∙ = ( ·sf ‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ ((𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∙ 𝑌) = (𝑋 · 𝑌))
Theorem	scafeq 21072	If the scalar multiplication operation is already a function, the functionalization of it is equal to the original operation. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ ∙ = ( ·sf ‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ ( · Fn (𝐾 × 𝐵) → ∙ = · )
Theorem	scaffn 21073	The scalar multiplication operation is a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ ∙ = ( ·sf ‘𝑊)    ⇒   ⊢ ∙ Fn (𝐾 × 𝐵)
Theorem	lmodscaf 21074	The scalar multiplication operation is a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ ∙ = ( ·sf ‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → ∙ :(𝐾 × 𝐵)⟶𝐵)
Theorem	lmodvsdi 21075	Distributive law for scalar product (left-distributivity). (ax-hvdistr1 31497 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌)))
Theorem	lmodvsdir 21076	Distributive law for scalar product (right-distributivity). (ax-hvdistr1 31497 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ ⨣ = (+g‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 ⨣ 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋)))
Theorem	lmodvsass 21077	Associative law for scalar product. (ax-hvmulass 31496 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ × = (.r‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋)))
Theorem	lmod0cl 21078	The ring zero in a left module belongs to the set of scalars. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝐹)    ⇒   ⊢ (𝑊 ∈ LMod → 0 ∈ 𝐾)
Theorem	lmod1cl 21079	The ring unity in a left module belongs to the set of scalars. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 1 = (1r‘𝐹)    ⇒   ⊢ (𝑊 ∈ LMod → 1 ∈ 𝐾)
Theorem	lmodvs1 21080	Scalar product with the ring unity. (ax-hvmulid 31495 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 1 = (1r‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ( 1 · 𝑋) = 𝑋)
Theorem	lmod0vcl 21081	The zero vector is a vector. (ax-hv0cl 31492 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → 0 ∈ 𝑉)
Theorem	lmod0vlid 21082	Left identity law for the zero vector. (hvaddlid 31512 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ( 0 + 𝑋) = 𝑋)
Theorem	lmod0vrid 21083	Right identity law for the zero vector. (ax-hvaddid 31493 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑋 + 0 ) = 𝑋)
Theorem	lmod0vid 21084	Identity equivalent to the value of the zero vector. Provides a convenient way to compute the value. (Contributed by NM, 9-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑋 + 𝑋) = 𝑋 ↔ 0 = 𝑋))
Theorem	lmod0vs 21085	Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (ax-hvmul0 31499 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑂 = (0g‘𝐹)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑂 · 𝑋) = 0 )
Theorem	lmodvs0 21086	Anything times the zero vector is the zero vector. Equation 1b of [Kreyszig] p. 51. (hvmul0 31513 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾) → (𝑋 · 0 ) = 0 )
Theorem	lmodvsmmulgdi 21087	Distributive law for a group multiple of a scalar multiplication. (Contributed by AV, 2-Sep-2019.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ ↑ = (.g‘𝑊)    &   ⊢ 𝐸 = (.g‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ (𝐶 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉)) → (𝑁 ↑ (𝐶 · 𝑋)) = ((𝑁𝐸𝐶) · 𝑋))
Theorem	lmodfopnelem1 21088	Lemma 1 for lmodfopne 21090. (Contributed by AV, 2-Oct-2021.)
⊢ · = ( ·sf ‘𝑊)    &   ⊢ + = (+𝑓‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑆)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ + = · ) → 𝑉 = 𝐾)
Theorem	lmodfopnelem2 21089	Lemma 2 for lmodfopne 21090. (Contributed by AV, 2-Oct-2021.)
⊢ · = ( ·sf ‘𝑊)    &   ⊢ + = (+𝑓‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 1 = (1r‘𝑆)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ + = · ) → ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉))
Theorem	lmodfopne 21090	The (functionalized) operations of a left module (over a nonzero ring) cannot be identical. (Contributed by NM, 31-May-2008.) (Revised by AV, 2-Oct-2021.)
⊢ · = ( ·sf ‘𝑊)    &   ⊢ + = (+𝑓‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 1 = (1r‘𝑆)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 1 ≠ 0 ) → + ≠ · )
Theorem	lcomf 21091	A linear-combination sum is a function. (Contributed by Stefan O'Rear, 28-Feb-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺:𝐼⟶𝐾)    &   ⊢ (𝜑 → 𝐻:𝐼⟶𝐵)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐺 ∘f · 𝐻):𝐼⟶𝐵)
Theorem	lcomfsupp 21092	A linear-combination sum is finitely supported if the coefficients are. (Contributed by Stefan O'Rear, 28-Feb-2015.) (Revised by AV, 15-Jul-2019.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺:𝐼⟶𝐾)    &   ⊢ (𝜑 → 𝐻:𝐼⟶𝐵)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑌 = (0g‘𝐹)    &   ⊢ (𝜑 → 𝐺 finSupp 𝑌)    ⇒   ⊢ (𝜑 → (𝐺 ∘f · 𝐻) finSupp 0 )
Theorem	lmodvnegcl 21093	Closure of vector negative. (Contributed by NM, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘𝑋) ∈ 𝑉)
Theorem	lmodvnegid 21094	Addition of a vector with its negative. (Contributed by NM, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑋 + (𝑁‘𝑋)) = 0 )
Theorem	lmodvneg1 21095	Minus 1 times a vector is the negative of the vector. Equation 2 of [Kreyszig] p. 51. (Contributed by NM, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 1 = (1r‘𝐹)    &   ⊢ 𝑀 = (invg‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑀‘ 1 ) · 𝑋) = (𝑁‘𝑋))
Theorem	lmodvsneg 21096	Multiplication of a vector by a negated scalar. (Contributed by Stefan O'Rear, 28-Feb-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝑀 = (invg‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (𝑁‘(𝑅 · 𝑋)) = ((𝑀‘𝑅) · 𝑋))
Theorem	lmodvsubcl 21097	Closure of vector subtraction. (hvsubcl 31506 analog.) (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 − 𝑌) ∈ 𝑉)
Theorem	lmodcom 21098	Left module vector sum is commutative. (Contributed by Gérard Lang, 25-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	lmodabl 21099	A left module is an abelian group (of vectors, under addition). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 25-Jun-2014.)
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel)
Theorem	lmodcmn 21100	A left module is a commutative monoid under addition. (Contributed by NM, 7-Jan-2015.)
⊢ (𝑊 ∈ LMod → 𝑊 ∈ CMnd)