![]() |
Metamath
Proof Explorer Theorem List (p. 196 of 454) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | drngui 19501 | The set of units of a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑅 ∈ DivRing ⇒ ⊢ (𝐵 ∖ { 0 }) = (Unit‘𝑅) | ||
Theorem | drngring 19502 | A division ring is a ring. (Contributed by NM, 8-Sep-2011.) |
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) | ||
Theorem | drnggrp 19503 | A division ring is a group. (Contributed by NM, 8-Sep-2011.) |
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Grp) | ||
Theorem | isfld 19504 | A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.) |
⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing)) | ||
Theorem | isdrng2 19505 | 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 19506 | 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 19507 | A division ring contains a multiplicative group. (Contributed by NM, 8-Sep-2011.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) ⇒ ⊢ (𝑅 ∈ DivRing → 𝐺 ∈ Grp) | ||
Theorem | drngmcl 19508 | 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 19509 | A division ring's unit 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 19510 | A division ring's unit is different from its zero. (Contributed by NM, 8-Sep-2011.) |
⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing → 1 ≠ 0 ) | ||
Theorem | drngid2 19511 | 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 19512 | Closure of the multiplicative inverse in a division ring. (reccl 11294 analog.) (Contributed by NM, 19-Apr-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐼‘𝑋) ∈ 𝐵) | ||
Theorem | drnginvrn0 19513 | The multiplicative inverse in a division ring is nonzero. (recne0 11300 analog.) (Contributed by NM, 19-Apr-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐼‘𝑋) ≠ 0 ) | ||
Theorem | drnginvrl 19514 | Property of the multiplicative inverse in a division ring. (recid2 11302 analog.) (Contributed by NM, 19-Apr-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ((𝐼‘𝑋) · 𝑋) = 1 ) | ||
Theorem | drnginvrr 19515 | Property of the multiplicative inverse in a division ring. (recid 11301 analog.) (Contributed by NM, 19-Apr-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝑋 · (𝐼‘𝑋)) = 1 ) | ||
Theorem | drngmul0or 19516 | 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 19517 | 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 19518 | 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 19519 | The opposite of a division ring is also a division ring. (Contributed by NM, 18-Oct-2014.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing ↔ 𝑂 ∈ DivRing) | ||
Theorem | isdrngd 19520* | 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 isdrngd 19520 for the characterization using right-inverses. (Contributed by NM, 2-Aug-2013.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → · = (.r‘𝑅)) & ⊢ (𝜑 → 0 = (0g‘𝑅)) & ⊢ (𝜑 → 1 = (1r‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ≠ 0 ) & ⊢ (𝜑 → 1 ≠ 0 ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ≠ 0 ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → (𝐼 · 𝑥) = 1 ) ⇒ ⊢ (𝜑 → 𝑅 ∈ DivRing) | ||
Theorem | isdrngrd 19521* | 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 19520 for the characterization using left-inverses. (Contributed by NM, 10-Aug-2013.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → · = (.r‘𝑅)) & ⊢ (𝜑 → 0 = (0g‘𝑅)) & ⊢ (𝜑 → 1 = (1r‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ≠ 0 ) & ⊢ (𝜑 → 1 ≠ 0 ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ≠ 0 ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → (𝑥 · 𝐼) = 1 ) ⇒ ⊢ (𝜑 → 𝑅 ∈ DivRing) | ||
Theorem | drngpropd 19522* | 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 19523* | 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)) | ||
Syntax | csubrg 19524 | Extend class notation with all subrings of a ring. |
class SubRing | ||
Syntax | crgspn 19525 | Extend class notation with span of a set of elements over a ring. |
class RingSpan | ||
Definition | df-subrg 19526* |
Define a subring of a ring as a set of elements that is a ring in its
own right and contains the multiplicative identity.
The additional constraint is necessary because the multiplicative identity of a ring, unlike the additive identity of a ring/group or the multiplicative identity of a field, cannot be identified by a local property. Thus, it is possible for a subset of a ring to be a ring while not containing the true identity if it contains a false identity. For instance, the subset (ℤ × {0}) of (ℤ × ℤ) (where multiplication is componentwise) contains the false identity 〈1, 0〉 which preserves every element of the subset and thus appears to be the identity of the subset, but is not the identity of the larger ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ SubRing = (𝑤 ∈ Ring ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ ((𝑤 ↾s 𝑠) ∈ Ring ∧ (1r‘𝑤) ∈ 𝑠)}) | ||
Definition | df-rgspn 19527* | The ring-span of a set of elements in a ring is the smallest subring which contains all of them. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
⊢ RingSpan = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡})) | ||
Theorem | issubrg 19528 | The subring predicate. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Proof shortened by AV, 12-Oct-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴))) | ||
Theorem | subrgss 19529 | A subring is a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ 𝐵) | ||
Theorem | subrgid 19530 | Every ring is a subring of itself. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐵 ∈ (SubRing‘𝑅)) | ||
Theorem | subrgring 19531 | A subring is a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring) | ||
Theorem | subrgcrng 19532 | A subring of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → 𝑆 ∈ CRing) | ||
Theorem | subrgrcl 19533 | Reverse closure for a subring predicate. (Contributed by Mario Carneiro, 3-Dec-2014.) |
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) | ||
Theorem | subrgsubg 19534 | A subring is a subgroup. (Contributed by Mario Carneiro, 3-Dec-2014.) |
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅)) | ||
Theorem | subrg0 19535 | A subring always has the same additive identity. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 0 = (0g‘𝑆)) | ||
Theorem | subrg1cl 19536 | A subring contains the multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 1 ∈ 𝐴) | ||
Theorem | subrgbas 19537 | Base set of a subring structure. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 = (Base‘𝑆)) | ||
Theorem | subrg1 19538 | A subring always has the same multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 1 = (1r‘𝑆)) | ||
Theorem | subrgacl 19539 | A subring is closed under addition. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 + 𝑌) ∈ 𝐴) | ||
Theorem | subrgmcl 19540 | A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 · 𝑌) ∈ 𝐴) | ||
Theorem | subrgsubm 19541 | A subring is a submonoid of the multiplicative monoid. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubMnd‘𝑀)) | ||
Theorem | subrgdvds 19542 | If an element divides another in a subring, then it also divides the other in the parent ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ ∥ = (∥r‘𝑅) & ⊢ 𝐸 = (∥r‘𝑆) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐸 ⊆ ∥ ) | ||
Theorem | subrguss 19543 | A unit of a subring is a unit of the parent ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑉 = (Unit‘𝑆) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑉 ⊆ 𝑈) | ||
Theorem | subrginv 19544 | A subring always has the same inversion function, for elements that are invertible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ 𝑈 = (Unit‘𝑆) & ⊢ 𝐽 = (invr‘𝑆) ⇒ ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) = (𝐽‘𝑋)) | ||
Theorem | subrgdv 19545 | A subring always has the same division function, for elements that are invertible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ / = (/r‘𝑅) & ⊢ 𝑈 = (Unit‘𝑆) & ⊢ 𝐸 = (/r‘𝑆) ⇒ ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) = (𝑋𝐸𝑌)) | ||
Theorem | subrgunit 19546 | An element of a ring is a unit of a subring iff it is a unit of the parent ring and both it and its inverse are in the subring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑉 = (Unit‘𝑆) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ (𝐼‘𝑋) ∈ 𝐴))) | ||
Theorem | subrgugrp 19547 | The units of a subring form a subgroup of the unit group of the original ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑉 = (Unit‘𝑆) & ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑉 ∈ (SubGrp‘𝐺)) | ||
Theorem | issubrg2 19548* | Characterize the subrings of a ring by closure properties. (Contributed by Mario Carneiro, 3-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐴 ∈ (SubRing‘𝑅) ↔ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴))) | ||
Theorem | opprsubrg 19549 | Being a subring is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (SubRing‘𝑅) = (SubRing‘𝑂) | ||
Theorem | subrgint 19550 | The intersection of a nonempty collection of subrings is a subring. (Contributed by Stefan O'Rear, 30-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.) |
⊢ ((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ (SubRing‘𝑅)) | ||
Theorem | subrgin 19551 | The intersection of two subrings is a subring. (Contributed by Stefan O'Rear, 30-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.) |
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ∈ (SubRing‘𝑅)) → (𝐴 ∩ 𝐵) ∈ (SubRing‘𝑅)) | ||
Theorem | subrgmre 19552 | The subrings of a ring are a Moore system. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (SubRing‘𝑅) ∈ (Moore‘𝐵)) | ||
Theorem | issubdrg 19553* | Characterize the subfields of a division ring. (Contributed by Mario Carneiro, 3-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → (𝑆 ∈ DivRing ↔ ∀𝑥 ∈ (𝐴 ∖ { 0 })(𝐼‘𝑥) ∈ 𝐴)) | ||
Theorem | subsubrg 19554 | A subring of a subring is a subring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝐵 ∈ (SubRing‘𝑆) ↔ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴))) | ||
Theorem | subsubrg2 19555 | The set of subrings of a subring are the smaller subrings. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → (SubRing‘𝑆) = ((SubRing‘𝑅) ∩ 𝒫 𝐴)) | ||
Theorem | issubrg3 19556 | A subring is an additive subgroup which is also a multiplicative submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝑆 ∈ (SubRing‘𝑅) ↔ (𝑆 ∈ (SubGrp‘𝑅) ∧ 𝑆 ∈ (SubMnd‘𝑀)))) | ||
Theorem | resrhm 19557 | Restriction of a ring homomorphism to a subring is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ 𝑈 = (𝑆 ↾s 𝑋) ⇒ ⊢ ((𝐹 ∈ (𝑆 RingHom 𝑇) ∧ 𝑋 ∈ (SubRing‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 RingHom 𝑇)) | ||
Theorem | rhmeql 19558 | The equalizer of two ring homomorphisms is a subring. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ ((𝐹 ∈ (𝑆 RingHom 𝑇) ∧ 𝐺 ∈ (𝑆 RingHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ (SubRing‘𝑆)) | ||
Theorem | rhmima 19559 | The homomorphic image of a subring is a subring. (Contributed by Stefan O'Rear, 10-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ ((𝐹 ∈ (𝑀 RingHom 𝑁) ∧ 𝑋 ∈ (SubRing‘𝑀)) → (𝐹 “ 𝑋) ∈ (SubRing‘𝑁)) | ||
Theorem | rnrhmsubrg 19560 | The range of a ring homomorphism is a subring. (Contributed by SN, 18-Nov-2023.) |
⊢ (𝐹 ∈ (𝑀 RingHom 𝑁) → ran 𝐹 ∈ (SubRing‘𝑁)) | ||
Theorem | cntzsubr 19561 | Centralizers in a ring are subrings. (Contributed by Stefan O'Rear, 6-Sep-2015.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubRing‘𝑅)) | ||
Theorem | pwsdiagrhm 19562* | Diagonal homomorphism into a structure power (Rings). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 RingHom 𝑌)) | ||
Theorem | subrgpropd 19563* | If two structures have the same group components (properties), they have the same set of subrings. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (SubRing‘𝐾) = (SubRing‘𝐿)) | ||
Theorem | rhmpropd 19564* | Ring homomorphism depends only on the ring attributes of structures. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐽)) & ⊢ (𝜑 → 𝐶 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → 𝐶 = (Base‘𝑀)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐽)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝑀)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐽)𝑦) = (𝑥(.r‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝑀)𝑦)) ⇒ ⊢ (𝜑 → (𝐽 RingHom 𝐾) = (𝐿 RingHom 𝑀)) | ||
Syntax | csdrg 19565 | Syntax for subfields (sub-division-rings). |
class SubDRing | ||
Definition | df-sdrg 19566* | A sub-division-ring is a subset of a division ring's set which is a division ring under the induced operation. If the overring is commutative this is a field; no special consideration is made of the fields in the center of a skew field. (Contributed by Stefan O'Rear, 3-Oct-2015.) |
⊢ SubDRing = (𝑤 ∈ DivRing ↦ {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ DivRing}) | ||
Theorem | issdrg 19567 | Property of a division subring. (Contributed by Stefan O'Rear, 3-Oct-2015.) |
⊢ (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ 𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing)) | ||
Theorem | sdrgid 19568 | Every division ring is a division subring of itself. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing → 𝐵 ∈ (SubDRing‘𝑅)) | ||
Theorem | sdrgss 19569 | A division subring is a subset of the base set. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑆 ∈ (SubDRing‘𝑅) → 𝑆 ⊆ 𝐵) | ||
Theorem | issdrg2 19570* | Property of a division subring (closure version). (Contributed by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝐼 = (invr‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ 𝑆 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑆 ∖ { 0 })(𝐼‘𝑥) ∈ 𝑆)) | ||
Theorem | acsfn1p 19571* | Construction of a closure rule from a one-parameter partial operation. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎} ∈ (ACS‘𝑋)) | ||
Theorem | subrgacs 19572 | Closure property of subrings. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (SubRing‘𝑅) ∈ (ACS‘𝐵)) | ||
Theorem | sdrgacs 19573 | Closure property of division subrings. (Contributed by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing → (SubDRing‘𝑅) ∈ (ACS‘𝐵)) | ||
Theorem | cntzsdrg 19574 | Centralizers in division rings/fields are subfields. (Contributed by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubDRing‘𝑅)) | ||
Theorem | subdrgint 19575* | 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 19576 | 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 19577 | 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 19578 | The prime field contains the neutral element of the division ring. (Contributed by Thierry Arnoux, 22-Aug-2023.) |
⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing → 0 ∈ ∩ (SubDRing‘𝑅)) | ||
Theorem | primefld1cl 19579 | The prime field contains the multiplicative neutral element of the division ring. (Contributed by Thierry Arnoux, 22-Aug-2023.) |
⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing → 1 ∈ ∩ (SubDRing‘𝑅)) | ||
Syntax | cabv 19580 | The set of absolute values on a ring. |
class AbsVal | ||
Definition | df-abv 19581* | Define the set of absolute values on a ring. An absolute value is a generalization of the usual absolute value function df-abs 14587 to arbitrary rings. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ AbsVal = (𝑟 ∈ Ring ↦ {𝑓 ∈ ((0[,)+∞) ↑m (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)(((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))}) | ||
Theorem | abvfval 19582* | 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 19583* | 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 19584* | 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 19585 | Reverse closure for the absolute value set. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐴 → 𝑅 ∈ Ring) | ||
Theorem | abvfge0 19586 | 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 19587 | An absolute value is a function from the ring to the real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐴 → 𝐹:𝐵⟶ℝ) | ||
Theorem | abvcl 19588 | An absolute value is a function from the ring to the real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ ℝ) | ||
Theorem | abvge0 19589 | 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 19590 | 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 19591 | The absolute value of a nonzero number is nonzero. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐹‘𝑋) ≠ 0) | ||
Theorem | abvgt0 19592 | 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 19593 | An absolute value distributes under multiplication. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 · 𝑌)) = ((𝐹‘𝑋) · (𝐹‘𝑌))) | ||
Theorem | abvtri 19594 | An absolute value satisfies the triangle inequality. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑌))) | ||
Theorem | abv0 19595 | The absolute value of zero is zero. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐴 → (𝐹‘ 0 ) = 0) | ||
Theorem | abv1z 19596 | 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 19597 | 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 19598 | 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 19599 | An absolute value satisfies the triangle inequality. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ − = (-g‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 − 𝑌)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑌))) | ||
Theorem | abvrec 19600 | The absolute value distributes under reciprocal. (Contributed by Mario Carneiro, 10-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ (((𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 )) → (𝐹‘(𝐼‘𝑋)) = (1 / (𝐹‘𝑋))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |