This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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