P. 187 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18601-18700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mulgass2 18601	An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ × = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑁 · 𝑋) × 𝑌) = (𝑁 · (𝑋 × 𝑌)))
Theorem	ring1 18602	The (smallest) structure representing a zero ring. (Contributed by AV, 28-Apr-2019.)
⊢ 𝑀 = {⟨(Base‘ndx), {𝑍}⟩, ⟨(+g‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩, ⟨(.r‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩}    ⇒   ⊢ (𝑍 ∈ 𝑉 → 𝑀 ∈ Ring)
Theorem	ringn0 18603	Rings exist. (Contributed by AV, 29-Apr-2019.)
⊢ Ring ≠ ∅
Theorem	ringlghm 18604*	Left-multiplication in a ring by a fixed element of the ring is a group homomorphism. (It is not usually a ring homomorphism.) (Contributed by Mario Carneiro, 4-May-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥)) ∈ (𝑅 GrpHom 𝑅))
Theorem	ringrghm 18605*	Right-multiplication in a ring by a fixed element of the ring is a group homomorphism. (It is not usually a ring homomorphism.) (Contributed by Mario Carneiro, 4-May-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋)) ∈ (𝑅 GrpHom 𝑅))
Theorem	gsummulc1 18606*	A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 10-Jul-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 )    ⇒   ⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ 𝐴 ↦ (𝑋 · 𝑌))) = ((𝑅 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) · 𝑌))
Theorem	gsummulc2 18607*	A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 10-Jul-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 )    ⇒   ⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ 𝐴 ↦ (𝑌 · 𝑋))) = (𝑌 · (𝑅 Σg (𝑘 ∈ 𝐴 ↦ 𝑋))))
Theorem	gsummgp0 18608*	If one factor in a finite group sum of the multiplicative group of a commutative ring is 0, the whole "sum" (i.e. product) is 0. (Contributed by AV, 3-Jan-2019.)
⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐴 ∈ (Base‘𝑅))    &   ⊢ ((𝜑 ∧ 𝑛 = 𝑖) → 𝐴 = 𝐵)    &   ⊢ (𝜑 → ∃𝑖 ∈ 𝑁 𝐵 = 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑁 ↦ 𝐴)) = 0 )
Theorem	gsumdixp 18609*	Distribute a binary product of sums to a sum of binary products in a ring. (Contributed by Mario Carneiro, 8-Mar-2015.) (Revised by AV, 10-Jul-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑋 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝑋) finSupp 0 )    &   ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ 𝑌) finSupp 0 )    ⇒   ⊢ (𝜑 → ((𝑅 Σg (𝑥 ∈ 𝐼 ↦ 𝑋)) · (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑌))) = (𝑅 Σg (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌))))
Theorem	prdsmgp 18610	The multiplicative monoid of a product is the product of the multiplicative monoids of the factors. (Contributed by Mario Carneiro, 11-Mar-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑌)    &   ⊢ 𝑍 = (𝑆Xs(mulGrp ∘ 𝑅))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    ⇒   ⊢ (𝜑 → ((Base‘𝑀) = (Base‘𝑍) ∧ (+g‘𝑀) = (+g‘𝑍)))
Theorem	prdsmulrcl 18611	A structure product of rings has closed binary operation. (Contributed by Mario Carneiro, 11-Mar-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ · = (.r‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Ring)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 · 𝐺) ∈ 𝐵)
Theorem	prdsringd 18612	A product of rings is a ring. (Contributed by Mario Carneiro, 11-Mar-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Ring)    ⇒   ⊢ (𝜑 → 𝑌 ∈ Ring)
Theorem	prdscrngd 18613	A product of commutative rings is a commutative ring. Since the resulting ring will have zero divisors in all nontrivial cases, this cannot be strengthened much further. (Contributed by Mario Carneiro, 11-Mar-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶CRing)    ⇒   ⊢ (𝜑 → 𝑌 ∈ CRing)
Theorem	prds1 18614	Value of the ring unit in a structure family product. (Contributed by Mario Carneiro, 11-Mar-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Ring)    ⇒   ⊢ (𝜑 → (1r ∘ 𝑅) = (1r‘𝑌))
Theorem	pwsring 18615	A structure power of a ring is a ring. (Contributed by Mario Carneiro, 11-Mar-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ Ring)
Theorem	pws1 18616	Value of the ring unit in a structure power. (Contributed by Mario Carneiro, 11-Mar-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (𝐼 × { 1 }) = (1r‘𝑌))
Theorem	pwscrng 18617	A structure power of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 11-Mar-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ CRing)
Theorem	pwsmgp 18618	The multiplicative group of the power structure resembles the power of the multiplicative group. (Contributed by Mario Carneiro, 12-Mar-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑍 = (𝑀 ↑s 𝐼)    &   ⊢ 𝑁 = (mulGrp‘𝑌)    &   ⊢ 𝐵 = (Base‘𝑁)    &   ⊢ 𝐶 = (Base‘𝑍)    &   ⊢ + = (+g‘𝑁)    &   ⊢ ✚ = (+g‘𝑍)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝐵 = 𝐶 ∧ + = ✚ ))
Theorem	imasring 18619*	The image structure of a ring is a ring. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞))))    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → (𝑈 ∈ Ring ∧ (𝐹‘ 1 ) = (1r‘𝑈)))
Theorem	qusring2 18620*	The quotient structure of a ring is a ring. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 + 𝑏) ∼ (𝑝 + 𝑞)))    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → (𝑈 ∈ Ring ∧ [ 1 ] ∼ = (1r‘𝑈)))
Theorem	crngbinom 18621*	The binomial theorem for commutative rings (special case of csrgbinom 18546): (𝐴 + 𝐵)↑𝑁 is the sum from 𝑘 = 0 to 𝑁 of (𝑁C𝑘) · ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)). (Contributed by AV, 24-Aug-2019.)
⊢ 𝑆 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ ↑ = (.g‘𝐺)    ⇒   ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))
10.4.4  Opposite ring
Syntax	coppr 18622	The opposite ring operation.
class oppr
Definition	df-oppr 18623	Define an opposite ring, which is the same as the original ring but with multiplication written the other way around. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ oppr = (𝑓 ∈ V ↦ (𝑓 sSet ⟨(.r‘ndx), tpos (.r‘𝑓)⟩))
Theorem	opprval 18624	Value of the opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ 𝑂 = (𝑅 sSet ⟨(.r‘ndx), tpos · ⟩)
Theorem	opprmulfval 18625	Value of the multiplication operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ ∙ = (.r‘𝑂)    ⇒   ⊢ ∙ = tpos ·
Theorem	opprmul 18626	Value of the multiplication operation of an opposite ring. Hypotheses eliminated by a suggestion of Stefan O'Rear, 30-Aug-2015. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Aug-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ ∙ = (.r‘𝑂)    ⇒   ⊢ (𝑋 ∙ 𝑌) = (𝑌 · 𝑋)
Theorem	crngoppr 18627	In a commutative ring, the opposite ring is equivalent to the original ring (for theorems like unitpropd 18697). (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ ∙ = (.r‘𝑂)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) = (𝑋 ∙ 𝑌))
Theorem	opprlem 18628	Lemma for opprbas 18629 and oppradd 18630. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑁 < 3    ⇒   ⊢ (𝐸‘𝑅) = (𝐸‘𝑂)
Theorem	opprbas 18629	Base set of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ 𝐵 = (Base‘𝑂)
Theorem	oppradd 18630	Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ + = (+g‘𝑂)
Theorem	opprring 18631	An opposite ring is a ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Aug-2015.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑂 ∈ Ring)
Theorem	opprringb 18632	Bidirectional form of opprring 18631. (Contributed by Mario Carneiro, 6-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring ↔ 𝑂 ∈ Ring)
Theorem	oppr0 18633	Additive identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ 0 = (0g‘𝑂)
Theorem	oppr1 18634	Multiplicative identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ 1 = (1r‘𝑂)
Theorem	opprneg 18635	The negative function in an opposite ring. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    ⇒   ⊢ 𝑁 = (invg‘𝑂)
Theorem	opprsubg 18636	Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (SubGrp‘𝑅) = (SubGrp‘𝑂)
Theorem	mulgass3 18637	An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ × = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 × (𝑁 · 𝑌)) = (𝑁 · (𝑋 × 𝑌)))
10.4.5  Divisibility
Syntax	cdsr 18638	Ring divisibility relation.
class ∥r
Syntax	cui 18639	Ring unit.
class Unit
Syntax	cir 18640	Ring irreducibles.
class Irred
Definition	df-dvdsr 18641*	Define the (right) divisibility relation in a ring. Access to the left divisibility relation is available through (∥r‘(oppr‘𝑅)). (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ ∥r = (𝑤 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑤) ∧ ∃𝑧 ∈ (Base‘𝑤)(𝑧(.r‘𝑤)𝑥) = 𝑦)})
Definition	df-unit 18642	Define the set of units in a ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ Unit = (𝑤 ∈ V ↦ (◡((∥r‘𝑤) ∩ (∥r‘(oppr‘𝑤))) “ {(1r‘𝑤)}))
Definition	df-irred 18643*	Define the set of irreducible elements in a ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ Irred = (𝑤 ∈ V ↦ ⦋((Base‘𝑤) ∖ (Unit‘𝑤)) / 𝑏⦌{𝑧 ∈ 𝑏 ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑤)𝑦) ≠ 𝑧})
Theorem	reldvdsr 18644	The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ Rel ∥
Theorem	dvdsrval 18645*	Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ∥ = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)}
Theorem	dvdsr 18646*	Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑋 ∥ 𝑌 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑋) = 𝑌))
Theorem	dvdsr2 18647*	Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑋 ∈ 𝐵 → (𝑋 ∥ 𝑌 ↔ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑋) = 𝑌))
Theorem	dvdsrmul 18648	A left-multiple of 𝑋 is divisible by 𝑋. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∥ (𝑌 · 𝑋))
Theorem	dvdsrcl 18649	Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ (𝑋 ∥ 𝑌 → 𝑋 ∈ 𝐵)
Theorem	dvdsrcl2 18650	Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∥ 𝑌) → 𝑌 ∈ 𝐵)
Theorem	dvdsrid 18651	An element in a (unital) ring divides itself. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 𝑋 ∥ 𝑋)
Theorem	dvdsrtr 18652	Divisibility is transitive. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∥ 𝑍 ∧ 𝑍 ∥ 𝑋) → 𝑌 ∥ 𝑋)
Theorem	dvdsrmul1 18653	The divisibility relation is preserved under right-multiplication. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ∧ 𝑋 ∥ 𝑌) → (𝑋 · 𝑍) ∥ (𝑌 · 𝑍))
Theorem	dvdsrneg 18654	An element divides its negative. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 𝑋 ∥ (𝑁‘𝑋))
Theorem	dvdsr01 18655	In a ring, zero is divisible by all elements. ("Zero divisor" as a term has a somewhat different meaning, see df-rlreg 19283.) (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 𝑋 ∥ 0 )
Theorem	dvdsr02 18656	Only zero is divisible by zero. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ( 0 ∥ 𝑋 ↔ 𝑋 = 0 ))
Theorem	isunit 18657	Property of being a unit of a ring. A unit is an element that left- and right-divides one. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 8-Dec-2015.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ 𝑆 = (oppr‘𝑅)    &   ⊢ 𝐸 = (∥r‘𝑆)    ⇒   ⊢ (𝑋 ∈ 𝑈 ↔ (𝑋 ∥ 1 ∧ 𝑋𝐸 1 ))
Theorem	1unit 18658	The multiplicative identity is a unit. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 1 ∈ 𝑈)
Theorem	unitcl 18659	A unit is an element of the base set. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝑋 ∈ 𝑈 → 𝑋 ∈ 𝐵)
Theorem	unitss 18660	The set of units is contained in the base set. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ 𝑈 ⊆ 𝐵
Theorem	opprunit 18661	Being a unit is a symmetric property, so it transfers to the opposite ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑆 = (oppr‘𝑅)    ⇒   ⊢ 𝑈 = (Unit‘𝑆)
Theorem	crngunit 18662	Property of being a unit in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → (𝑋 ∈ 𝑈 ↔ 𝑋 ∥ 1 ))
Theorem	dvdsunit 18663	A divisor of a unit is a unit. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑌 ∥ 𝑋 ∧ 𝑋 ∈ 𝑈) → 𝑌 ∈ 𝑈)
Theorem	unitmulcl 18664	The product of units is a unit. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 · 𝑌) ∈ 𝑈)
Theorem	unitmulclb 18665	Reversal of unitmulcl 18664 in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) ∈ 𝑈 ↔ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)))
Theorem	unitgrpbas 18666	The base set of the group of units. (Contributed by Mario Carneiro, 25-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈)    ⇒   ⊢ 𝑈 = (Base‘𝐺)
Theorem	unitgrp 18667	The group of units is a group under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Grp)
Theorem	unitabl 18668	The group of units of a commutative ring is abelian. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈)    ⇒   ⊢ (𝑅 ∈ CRing → 𝐺 ∈ Abel)
Theorem	unitgrpid 18669	The identity of the multiplicative group is 1r. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 1 = (0g‘𝐺))
Theorem	unitsubm 18670	The group of units is a submonoid of the multiplicative monoid of the ring. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑈 ∈ (SubMnd‘𝑀))
Syntax	cinvr 18671	Extend class notation with multiplicative inverse.
class invr
Definition	df-invr 18672	Define multiplicative inverse. (Contributed by NM, 21-Sep-2011.)
⊢ invr = (𝑟 ∈ V ↦ (invg‘((mulGrp‘𝑟) ↾s (Unit‘𝑟))))
Theorem	invrfval 18673	Multiplicative inverse function for a division ring. (Contributed by NM, 21-Sep-2011.) (Revised by Mario Carneiro, 25-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ 𝐼 = (invg‘𝐺)
Theorem	unitinvcl 18674	The inverse of a unit exists and is a unit. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) ∈ 𝑈)
Theorem	unitinvinv 18675	The inverse of the inverse of a unit is the same element. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝐼‘(𝐼‘𝑋)) = 𝑋)
Theorem	ringinvcl 18676	The inverse of a unit is an element of the ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) ∈ 𝐵)
Theorem	unitlinv 18677	A unit times its inverse is the identity. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → ((𝐼‘𝑋) · 𝑋) = 1 )
Theorem	unitrinv 18678	A unit times its inverse is the identity. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑋 · (𝐼‘𝑋)) = 1 )
Theorem	1rinv 18679	The inverse of the identity is the identity. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 𝐼 = (invr‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐼‘ 1 ) = 1 )
Theorem	0unit 18680	The additive identity is a unit if and only if 1 = 0, i.e. we are in the zero ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → ( 0 ∈ 𝑈 ↔ 1 = 0 ))
Theorem	unitnegcl 18681	The negative of a unit is a unit. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑁‘𝑋) ∈ 𝑈)
Syntax	cdvr 18682	Extend class notation with ring division.
class /r
Definition	df-dvr 18683*	Define ring division. (Contributed by Mario Carneiro, 2-Jul-2014.)
⊢ /r = (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Unit‘𝑟) ↦ (𝑥(.r‘𝑟)((invr‘𝑟)‘𝑦))))
Theorem	dvrfval 18684*	Division operation in a ring. (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ / = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦)))
Theorem	dvrval 18685	Division operation in a ring. (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) = (𝑋 · (𝐼‘𝑌)))
Theorem	dvrcl 18686	Closure of division operation. (Contributed by Mario Carneiro, 2-Jul-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) ∈ 𝐵)
Theorem	unitdvcl 18687	The units are closed under division. (Contributed by Mario Carneiro, 2-Jul-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) ∈ 𝑈)
Theorem	dvrid 18688	A cancellation law for division. (divid 10714 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑋 / 𝑋) = 1 )
Theorem	dvr1 18689	A cancellation law for division. (div1 10716 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑋 / 1 ) = 𝑋)
Theorem	dvrass 18690	An associative law for division. (divass 10703 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈)) → ((𝑋 · 𝑌) / 𝑍) = (𝑋 · (𝑌 / 𝑍)))
Theorem	dvrcan1 18691	A cancellation law for division. (divcan1 10694 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 / 𝑌) · 𝑌) = 𝑋)
Theorem	dvrcan3 18692	A cancellation law for division. (divcan3 10711 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 18-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 · 𝑌) / 𝑌) = 𝑋)
Theorem	dvreq1 18693	A cancellation law for division. (diveq1 10718 analog.) (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 / 𝑌) = 1 ↔ 𝑋 = 𝑌))
Theorem	ringinvdv 18694	Write the inverse function in terms of division. (Contributed by Mario Carneiro, 2-Jul-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) = ( 1 / 𝑋))
Theorem	rngidpropd 18695*	The ring identity depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (1r‘𝐾) = (1r‘𝐿))
Theorem	dvdsrpropd 18696*	The divisibility relation depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (∥r‘𝐾) = (∥r‘𝐿))
Theorem	unitpropd 18697*	The set of units depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (Unit‘𝐾) = (Unit‘𝐿))
Theorem	invrpropd 18698*	The ring inverse function depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.) (Revised by Mario Carneiro, 5-Oct-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (invr‘𝐾) = (invr‘𝐿))
Theorem	isirred 18699*	An irreducible element of a ring is a non-unit that is not the product of two non-units. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ 𝑁 = (𝐵 ∖ 𝑈)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑋 ∈ 𝐼 ↔ (𝑋 ∈ 𝑁 ∧ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑋))
Theorem	isnirred 18700*	The property of being a non-irreducible (reducible) element in a ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ 𝑁 = (𝐵 ∖ 𝑈)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑋 ∈ 𝐵 → (¬ 𝑋 ∈ 𝐼 ↔ (𝑋 ∈ 𝑈 ∨ ∃𝑥 ∈ 𝑁 ∃𝑦 ∈ 𝑁 (𝑥 · 𝑦) = 𝑋)))