Definition df-irred 20569

Description: Define the set of irreducible elements in a ring. (Contributed by Mario Carneiro, 4-Dec-2014.)

Assertion

Ref	Expression
df-irred	⊢ Irred = (𝑤 ∈ V ↦ ⦋((Base‘𝑤) ∖ (Unit‘𝑤)) / 𝑏⦌{𝑧 ∈ 𝑏 ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑤)𝑦) ≠ 𝑧})

Distinct variable group:   𝑤,𝑏,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-irred

Step	Hyp	Ref	Expression
1		cir 20566	. 2 class Irred
2		vw	. . 3 setvar 𝑤
3		cvv 3451	. . 3 class V
4		vb	. . . 4 setvar 𝑏
5	2	cv 1569	. . . . . 6 class 𝑤
6		cbs 17367	. . . . . 6 class Base
7	5, 6	cfv 6531	. . . . 5 class (Base‘𝑤)
8		cui 20565	. . . . . 6 class Unit
9	5, 8	cfv 6531	. . . . 5 class (Unit‘𝑤)
10	7, 9	cdif 3896	. . . 4 class ((Base‘𝑤) ∖ (Unit‘𝑤))
11		vx	. . . . . . . . . 10 setvar 𝑥
12	11	cv 1569	. . . . . . . . 9 class 𝑥
13		vy	. . . . . . . . . 10 setvar 𝑦
14	13	cv 1569	. . . . . . . . 9 class 𝑦
15		cmulr 17409	. . . . . . . . . 10 class .r
16	5, 15	cfv 6531	. . . . . . . . 9 class (.r‘𝑤)
17	12, 14, 16	co 7412	. . . . . . . 8 class (𝑥(.r‘𝑤)𝑦)
18		vz	. . . . . . . . 9 setvar 𝑧
19	18	cv 1569	. . . . . . . 8 class 𝑧
20	17, 19	wne 2956	. . . . . . 7 wff (𝑥(.r‘𝑤)𝑦) ≠ 𝑧
21	4	cv 1569	. . . . . . 7 class 𝑏
22	20, 13, 21	wral 3077	. . . . . 6 wff ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑤)𝑦) ≠ 𝑧
23	22, 11, 21	wral 3077	. . . . 5 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑤)𝑦) ≠ 𝑧
24	23, 18, 21	crab 3413	. . . 4 class {𝑧 ∈ 𝑏 ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑤)𝑦) ≠ 𝑧}
25	4, 10, 24	csb 3847	. . 3 class ⦋((Base‘𝑤) ∖ (Unit‘𝑤)) / 𝑏⦌{𝑧 ∈ 𝑏 ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑤)𝑦) ≠ 𝑧}
26	2, 3, 25	cmpt 5186	. 2 class (𝑤 ∈ V ↦ ⦋((Base‘𝑤) ∖ (Unit‘𝑤)) / 𝑏⦌{𝑧 ∈ 𝑏 ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑤)𝑦) ≠ 𝑧})
27	1, 26	wceq 1570	1 wff Irred = (𝑤 ∈ V ↦ ⦋((Base‘𝑤) ∖ (Unit‘𝑤)) / 𝑏⦌{𝑧 ∈ 𝑏 ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑤)𝑦) ≠ 𝑧})

This definition is used by:  isirred  20629