Metamath Proof Explorer


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𝑤 ) 𝑦 ) ≠ 𝑧 } )