P. 206 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20501-20600   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cfield 20501	Class of fields.
class Field
Definition	df-drng 20502	Define class of all division rings. A division ring is a ring in which the set of units is exactly the nonzero elements of the ring. (Contributed by NM, 18-Oct-2012.)
⊢ DivRing = {𝑟 ∈ Ring ∣ (Unit‘𝑟) = ((Base‘𝑟) ∖ {(0g‘𝑟)})}
Definition	df-field 20503	A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.)
⊢ Field = (DivRing ∩ CRing)
Theorem	isdrng 20504	The predicate "is a division ring". (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 })))
Theorem	drngunit 20505	Elementhood in the set of units when 𝑅 is a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing → (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 )))
Theorem	drngui 20506	The set of units of a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑅 ∈ DivRing    ⇒   ⊢ (𝐵 ∖ { 0 }) = (Unit‘𝑅)
Theorem	drngring 20507	A division ring is a ring. (Contributed by NM, 8-Sep-2011.)
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring)
Theorem	drngringd 20508	A division ring is a ring. (Contributed by SN, 16-May-2024.)
⊢ (𝜑 → 𝑅 ∈ DivRing)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Ring)
Theorem	drnggrpd 20509	A division ring is a group (deduction form). (Contributed by SN, 16-May-2024.)
⊢ (𝜑 → 𝑅 ∈ DivRing)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Grp)
Theorem	drnggrp 20510	A division ring is a group (closed form). (Contributed by NM, 8-Sep-2011.)
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Grp)
Theorem	isfld 20511	A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.)
⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
Theorem	flddrngd 20512	A field is a division ring. (Contributed by SN, 17-Jan-2025.)
⊢ (𝜑 → 𝑅 ∈ Field)    ⇒   ⊢ (𝜑 → 𝑅 ∈ DivRing)
Theorem	fldcrngd 20513	A field is a commutative ring. (Contributed by SN, 23-Nov-2024.)
⊢ (𝜑 → 𝑅 ∈ Field)    ⇒   ⊢ (𝜑 → 𝑅 ∈ CRing)
Theorem	isdrng2 20514	A division ring can equivalently be defined as a ring such that the nonzero elements form a group under multiplication (from which it follows that this is the same group as the group of units). (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 }))    ⇒   ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝐺 ∈ Grp))
Theorem	drngprop 20515	If two structures have the same ring components (properties), one is a division ring iff the other one is. (Contributed by Mario Carneiro, 11-Oct-2013.) (Revised by Mario Carneiro, 28-Dec-2014.)
⊢ (Base‘𝐾) = (Base‘𝐿)    &   ⊢ (+g‘𝐾) = (+g‘𝐿)    &   ⊢ (.r‘𝐾) = (.r‘𝐿)    ⇒   ⊢ (𝐾 ∈ DivRing ↔ 𝐿 ∈ DivRing)
Theorem	drngmgp 20516	A division ring contains a multiplicative group. (Contributed by NM, 8-Sep-2011.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 }))    ⇒   ⊢ (𝑅 ∈ DivRing → 𝐺 ∈ Grp)
Theorem	drngmcl 20517	The product of two nonzero elements of a division ring is nonzero. (Contributed by NM, 7-Sep-2011.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ (𝐵 ∖ { 0 }) ∧ 𝑌 ∈ (𝐵 ∖ { 0 })) → (𝑋 · 𝑌) ∈ (𝐵 ∖ { 0 }))
Theorem	drngid 20518	A division ring's unity is the identity element of its multiplicative group. (Contributed by NM, 7-Sep-2011.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 }))    ⇒   ⊢ (𝑅 ∈ DivRing → 1 = (0g‘𝐺))
Theorem	drngunz 20519	A division ring's unity is different from its zero. (Contributed by NM, 8-Sep-2011.)
⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing → 1 ≠ 0 )
Theorem	drngnzr 20520	All division rings are nonzero. (Contributed by Stefan O'Rear, 24-Feb-2015.)
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing)
Theorem	drngid2 20521	Properties showing that an element 𝐼 is the identity element of a division ring. (Contributed by Mario Carneiro, 11-Oct-2013.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing → ((𝐼 ∈ 𝐵 ∧ 𝐼 ≠ 0 ∧ (𝐼 · 𝐼) = 𝐼) ↔ 1 = 𝐼))
Theorem	drnginvrcl 20522	Closure of the multiplicative inverse in a division ring. (reccl 11883 analog). (Contributed by NM, 19-Apr-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐼‘𝑋) ∈ 𝐵)
Theorem	drnginvrn0 20523	The multiplicative inverse in a division ring is nonzero. (recne0 11889 analog). (Contributed by NM, 19-Apr-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐼‘𝑋) ≠ 0 )
Theorem	drnginvrcld 20524	Closure of the multiplicative inverse in a division ring. (reccld 11987 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ∈ 𝐵)
Theorem	drnginvrl 20525	Property of the multiplicative inverse in a division ring. (recid2 11891 analog). (Contributed by NM, 19-Apr-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ((𝐼‘𝑋) · 𝑋) = 1 )
Theorem	drnginvrr 20526	Property of the multiplicative inverse in a division ring. (recid 11890 analog). (Contributed by NM, 19-Apr-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝑋 · (𝐼‘𝑋)) = 1 )
Theorem	drnginvrld 20527	Property of the multiplicative inverse in a division ring. (recid2d 11990 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → ((𝐼‘𝑋) · 𝑋) = 1 )
Theorem	drnginvrrd 20528	Property of the multiplicative inverse in a division ring. (recidd 11989 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝑋 · (𝐼‘𝑋)) = 1 )
Theorem	drngmul0or 20529	A product is zero iff one of its factors is zero. (Contributed by NM, 8-Oct-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 · 𝑌) = 0 ↔ (𝑋 = 0 ∨ 𝑌 = 0 )))
Theorem	drngmulne0 20530	A product is nonzero iff both its factors are nonzero. (Contributed by NM, 18-Oct-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 · 𝑌) ≠ 0 ↔ (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 )))
Theorem	drngmuleq0 20531	An element is zero iff its product with a nonzero element is zero. (Contributed by NM, 8-Oct-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ≠ 0 )    ⇒   ⊢ (𝜑 → ((𝑋 · 𝑌) = 0 ↔ 𝑋 = 0 ))
Theorem	opprdrng 20532	The opposite of a division ring is also a division ring. (Contributed by NM, 18-Oct-2014.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing ↔ 𝑂 ∈ DivRing)
Theorem	isdrngd 20533*	Properties that characterize a division ring among rings: it should be nonzero, have no nonzero zero-divisors, and every nonzero element 𝑥 should have a left-inverse 𝐼(𝑥). See isdrngrd 20534 for the characterization using right-inverses. (Contributed by NM, 2-Aug-2013.) Remove hypothesis. (Revised by SN, 19-Feb-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → 0 = (0g‘𝑅))    &   ⊢ (𝜑 → 1 = (1r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ≠ 0 )    &   ⊢ (𝜑 → 1 ≠ 0 )    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → (𝐼 · 𝑥) = 1 )    ⇒   ⊢ (𝜑 → 𝑅 ∈ DivRing)
Theorem	isdrngrd 20534*	Properties that characterize a division ring among rings: it should be nonzero, have no nonzero zero-divisors, and every nonzero element 𝑥 should have a right-inverse 𝐼(𝑥). See isdrngd 20533 for the characterization using left-inverses. (Contributed by NM, 10-Aug-2013.) Remove hypothesis. (Revised by SN, 19-Feb-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → 0 = (0g‘𝑅))    &   ⊢ (𝜑 → 1 = (1r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ≠ 0 )    &   ⊢ (𝜑 → 1 ≠ 0 )    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → (𝑥 · 𝐼) = 1 )    ⇒   ⊢ (𝜑 → 𝑅 ∈ DivRing)
Theorem	isdrngdOLD 20535*	Obsolete version of isdrngd 20533 as of 19-Feb-2025. (Contributed by NM, 2-Aug-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → 0 = (0g‘𝑅))    &   ⊢ (𝜑 → 1 = (1r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ≠ 0 )    &   ⊢ (𝜑 → 1 ≠ 0 )    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ≠ 0 )    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → (𝐼 · 𝑥) = 1 )    ⇒   ⊢ (𝜑 → 𝑅 ∈ DivRing)
Theorem	isdrngrdOLD 20536*	Obsolete version of isdrngrd 20534 as of 19-Feb-2025. (Contributed by NM, 10-Aug-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → 0 = (0g‘𝑅))    &   ⊢ (𝜑 → 1 = (1r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ≠ 0 )    &   ⊢ (𝜑 → 1 ≠ 0 )    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ≠ 0 )    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → (𝑥 · 𝐼) = 1 )    ⇒   ⊢ (𝜑 → 𝑅 ∈ DivRing)
Theorem	drngpropd 20537*	If two structures have the same group components (properties), one is a division ring iff the other one is. (Contributed by Mario Carneiro, 27-Jun-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ DivRing ↔ 𝐿 ∈ DivRing))
Theorem	fldpropd 20538*	If two structures have the same group components (properties), one is a field iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ Field ↔ 𝐿 ∈ Field))
Theorem	rng1nnzr 20539	The (smallest) structure representing a zero ring is not a nonzero ring. (Contributed by AV, 29-Apr-2019.)
⊢ 𝑀 = {⟨(Base‘ndx), {𝑍}⟩, ⟨(+g‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩, ⟨(.r‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩}    ⇒   ⊢ (𝑍 ∈ 𝑉 → 𝑀 ∉ NzRing)
Theorem	ring1zr 20540	The only (unital) ring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). Note: The assumption 𝑅 ∈ Ring could be weakened if a definition of a non-unital ring ("Rng") was available (it would be sufficient that the multiplication is closed). (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) (Proof shortened by AV, 7-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ∗ = (.r‘𝑅)    ⇒   ⊢ (((𝑅 ∈ Ring ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) ∧ 𝑍 ∈ 𝐵) → (𝐵 = {𝑍} ↔ ( + = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩} ∧ ∗ = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩})))
Theorem	rngen1zr 20541	The only (unital) ring with one element is the zero ring (at least if its operations are internal binary operations). Note: The assumption 𝑅 ∈ Ring could be weakened if a definition of a non-unital ring ("Rng") was available (it would be sufficient that the multiplication is closed). (Contributed by FL, 14-Feb-2010.) (Revised by AV, 25-Jan-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ∗ = (.r‘𝑅)    ⇒   ⊢ (((𝑅 ∈ Ring ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) ∧ 𝑍 ∈ 𝐵) → (𝐵 ≈ 1o ↔ ( + = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩} ∧ ∗ = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩})))
Theorem	ringen1zr 20542	The only unital ring with one element is the zero ring (at least if its operations are internal binary operations). Note: The assumption 𝑅 ∈ Ring could be weakened if a definition of a non-unital ring ("Rng") was available (it would be sufficient that the multiplication is closed). (Contributed by FL, 15-Feb-2010.) (Revised by AV, 25-Jan-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ∗ = (.r‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) → (𝐵 ≈ 1o ↔ ( + = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩} ∧ ∗ = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩})))
Theorem	rng1nfld 20543	The zero ring is not a field. (Contributed by AV, 29-Apr-2019.)
⊢ 𝑀 = {⟨(Base‘ndx), {𝑍}⟩, ⟨(+g‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩, ⟨(.r‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩}    ⇒   ⊢ (𝑍 ∈ 𝑉 → 𝑀 ∉ Field)
Theorem	issubdrg 20544*	Characterize the subfields of a division ring. (Contributed by Mario Carneiro, 3-Dec-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → (𝑆 ∈ DivRing ↔ ∀𝑥 ∈ (𝐴 ∖ { 0 })(𝐼‘𝑥) ∈ 𝐴))
10.4.2  Sub-division rings
Syntax	csdrg 20545	Syntax for subfields (sub-division-rings).
class SubDRing
Definition	df-sdrg 20546*	Define the function associating with a ring the set of its sub-division-rings. A sub-division-ring of a ring is a subset of its base set which is a division ring when equipped with the induced structure (sum, multiplication, zero, and unity). If a ring is commutative (resp., a field), then its sub-division-rings are commutative (resp., are fields) (fldsdrgfld 20557), so we do not make a specific definition for subfields. (Contributed by Stefan O'Rear, 3-Oct-2015.) TODO: extend this definition to a function with domain V or at least Ring and not only DivRing.
⊢ SubDRing = (𝑤 ∈ DivRing ↦ {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ DivRing})
Theorem	issdrg 20547	Property of a division subring. (Contributed by Stefan O'Rear, 3-Oct-2015.)
⊢ (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ 𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing))
Theorem	sdrgrcl 20548	Reverse closure for a sub-division-ring predicate. (Contributed by SN, 19-Feb-2025.)
⊢ (𝐴 ∈ (SubDRing‘𝑅) → 𝑅 ∈ DivRing)
Theorem	sdrgdrng 20549	A sub-division-ring is a division ring. (Contributed by SN, 19-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubDRing‘𝑅) → 𝑆 ∈ DivRing)
Theorem	sdrgsubrg 20550	A sub-division-ring is a subring. (Contributed by SN, 19-Feb-2025.)
⊢ (𝐴 ∈ (SubDRing‘𝑅) → 𝐴 ∈ (SubRing‘𝑅))
Theorem	sdrgid 20551	Every division ring is a division subring of itself. (Contributed by Thierry Arnoux, 21-Aug-2023.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing → 𝐵 ∈ (SubDRing‘𝑅))
Theorem	sdrgss 20552	A division subring is a subset of the base set. (Contributed by Thierry Arnoux, 21-Aug-2023.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑆 ∈ (SubDRing‘𝑅) → 𝑆 ⊆ 𝐵)
Theorem	sdrgbas 20553	Base set of a sub-division-ring structure. (Contributed by SN, 19-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubDRing‘𝑅) → 𝐴 = (Base‘𝑆))
Theorem	issdrg2 20554*	Property of a division subring (closure version). (Contributed by Mario Carneiro, 3-Oct-2015.)
⊢ 𝐼 = (invr‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ 𝑆 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑆 ∖ { 0 })(𝐼‘𝑥) ∈ 𝑆))
Theorem	sdrgunit 20555	A unit of a sub-division-ring is a nonzero element of the subring. (Contributed by SN, 19-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑆)    ⇒   ⊢ (𝐴 ∈ (SubDRing‘𝑅) → (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 )))
Theorem	imadrhmcl 20556	The image of a (nontrivial) division ring homomorphism is a division ring. (Contributed by SN, 17-Feb-2025.)
⊢ 𝑅 = (𝑁 ↾s (𝐹 “ 𝑆))    &   ⊢ 0 = (0g‘𝑁)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑀 RingHom 𝑁))    &   ⊢ (𝜑 → 𝑆 ∈ (SubDRing‘𝑀))    &   ⊢ (𝜑 → ran 𝐹 ≠ { 0 })    ⇒   ⊢ (𝜑 → 𝑅 ∈ DivRing)
Theorem	fldsdrgfld 20557	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 20558*	Construction of a closure rule from a one-parameter partial operation. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎} ∈ (ACS‘𝑋))
Theorem	subrgacs 20559	Closure property of subrings. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (SubRing‘𝑅) ∈ (ACS‘𝐵))
Theorem	sdrgacs 20560	Closure property of division subrings. (Contributed by Mario Carneiro, 3-Oct-2015.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing → (SubDRing‘𝑅) ∈ (ACS‘𝐵))
Theorem	cntzsdrg 20561	Centralizers in division rings/fields are subfields. (Contributed by Mario Carneiro, 3-Oct-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubDRing‘𝑅))
Theorem	subdrgint 20562*	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 20563	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 20564	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 20565	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 20566	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 20567	The set of absolute values on a ring.
class AbsVal
Definition	df-abv 20568*	Define the set of absolute values on a ring. An absolute value is a generalization of the usual absolute value function df-abs 15187 to arbitrary rings. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ AbsVal = (𝑟 ∈ Ring ↦ {𝑓 ∈ ((0[,)+∞) ↑m (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)(((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))})
Theorem	abvfval 20569*	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 20570*	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 20571*	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 20572	Reverse closure for the absolute value set. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐴 → 𝑅 ∈ Ring)
Theorem	abvfge0 20573	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 20574	An absolute value is a function from the ring to the real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐴 → 𝐹:𝐵⟶ℝ)
Theorem	abvcl 20575	An absolute value is a function from the ring to the real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ ℝ)
Theorem	abvge0 20576	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 20577	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 20578	The absolute value of a nonzero number is nonzero. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐹‘𝑋) ≠ 0)
Theorem	abvgt0 20579	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 20580	An absolute value distributes under multiplication. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 · 𝑌)) = ((𝐹‘𝑋) · (𝐹‘𝑌)))
Theorem	abvtri 20581	An absolute value satisfies the triangle inequality. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑌)))
Theorem	abv0 20582	The absolute value of zero is zero. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐴 → (𝐹‘ 0 ) = 0)
Theorem	abv1z 20583	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 20584	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 20585	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 20586	An absolute value satisfies the triangle inequality. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ − = (-g‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 − 𝑌)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑌)))
Theorem	abvrec 20587	The absolute value distributes under reciprocal. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ (((𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 )) → (𝐹‘(𝐼‘𝑋)) = (1 / (𝐹‘𝑋)))
Theorem	abvdiv 20588	The absolute value distributes under division. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ (((𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 )) → (𝐹‘(𝑋 / 𝑌)) = ((𝐹‘𝑋) / (𝐹‘𝑌)))
Theorem	abvdom 20589	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 20590	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 20591*	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	abvtriv 20592*	The trivial absolute value. (This theorem is true as long as 𝑅 is a domain, but it is not true for rings with zero divisors, which violate the multiplication axiom; abvdom 20589 is the converse of this remark.) (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 20593*	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‘𝐿))
10.4.4  Star rings
Syntax	cstf 20594	Extend class notation with the functionalization of the *-ring involution.
class *rf
Syntax	csr 20595	Extend class notation with class of all *-rings.
class *-Ring
Definition	df-staf 20596*	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 20597*	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 20598*	The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ ∙ = (*rf‘𝑅)    ⇒   ⊢ ∙ = (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥))
Theorem	stafval 20599	The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ ∙ = (*rf‘𝑅)    ⇒   ⊢ (𝐴 ∈ 𝐵 → ( ∙ ‘𝐴) = ( ∗ ‘𝐴))
Theorem	staffn 20600	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 𝐵 → ∙ = ∗ )