Definition df-irred

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cir	⊢ Irred
1		vw	⊢ 𝑤
2		cvv	⊢ V
3		cbs	⊢ Base
4	1	cv	⊢ 𝑤
5	4 3	cfv	⊢ ( Base ‘ 𝑤 )
6		cui	⊢ Unit
7	4 6	cfv	⊢ ( Unit ‘ 𝑤 )
8	5 7	cdif	⊢ ( ( Base ‘ 𝑤 ) ∖ ( Unit ‘ 𝑤 ) )
9		vb	⊢ 𝑏
10		vz	⊢ 𝑧
11	9	cv	⊢ 𝑏
12		vx	⊢ 𝑥
13		vy	⊢ 𝑦
14	12	cv	⊢ 𝑥
15		cmulr	⊢ .r
16	4 15	cfv	⊢ ( .r ‘ 𝑤 )
17	13	cv	⊢ 𝑦
18	14 17 16	co	⊢ ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 )
19	10	cv	⊢ 𝑧
20	18 19	wne	⊢ ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) ≠ 𝑧
21	20 13 11	wral	⊢ ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) ≠ 𝑧
22	21 12 11	wral	⊢ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) ≠ 𝑧
23	22 10 11	crab	⊢ { 𝑧 ∈ 𝑏 ∣ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) ≠ 𝑧 }
24	9 8 23	csb	⊢ ⦋ ( ( Base ‘ 𝑤 ) ∖ ( Unit ‘ 𝑤 ) ) / 𝑏 ⦌ { 𝑧 ∈ 𝑏 ∣ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) ≠ 𝑧 }
25	1 2 24	cmpt	⊢ ( 𝑤 ∈ V ↦ ⦋ ( ( Base ‘ 𝑤 ) ∖ ( Unit ‘ 𝑤 ) ) / 𝑏 ⦌ { 𝑧 ∈ 𝑏 ∣ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) ≠ 𝑧 } )
26	0 25	wceq	⊢ Irred = ( 𝑤 ∈ V ↦ ⦋ ( ( Base ‘ 𝑤 ) ∖ ( Unit ‘ 𝑤 ) ) / 𝑏 ⦌ { 𝑧 ∈ 𝑏 ∣ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) ≠ 𝑧 } )