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 = w ∈ V ⟼ ⦋ Base w ∖ Unit ⁡ w / b⦌ z ∈ b | ∀ x ∈ b ∀ y ∈ b x ⋅ w y ≠ z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cir class Irred
1 vw setvar w
2 cvv class V
3 cbs class Base
4 1 cv setvar w
5 4 3 cfv class Base w
6 cui class Unit
7 4 6 cfv class Unit ⁡ w
8 5 7 cdif class Base w ∖ Unit ⁡ w
9 vb setvar b
10 vz setvar z
11 9 cv setvar b
12 vx setvar x
13 vy setvar y
14 12 cv setvar x
15 cmulr class ⋅ 𝑟
16 4 15 cfv class ⋅ w
17 13 cv setvar y
18 14 17 16 co class x ⋅ w y
19 10 cv setvar z
20 18 19 wne wff x ⋅ w y ≠ z
21 20 13 11 wral wff ∀ y ∈ b x ⋅ w y ≠ z
22 21 12 11 wral wff ∀ x ∈ b ∀ y ∈ b x ⋅ w y ≠ z
23 22 10 11 crab class z ∈ b | ∀ x ∈ b ∀ y ∈ b x ⋅ w y ≠ z
24 9 8 23 csb class ⦋ Base w ∖ Unit ⁡ w / b⦌ z ∈ b | ∀ x ∈ b ∀ y ∈ b x ⋅ w y ≠ z
25 1 2 24 cmpt class w ∈ V ⟼ ⦋ Base w ∖ Unit ⁡ w / b⦌ z ∈ b | ∀ x ∈ b ∀ y ∈ b x ⋅ w y ≠ z
26 0 25 wceq wff Irred = w ∈ V ⟼ ⦋ Base w ∖ Unit ⁡ w / b⦌ z ∈ b | ∀ x ∈ b ∀ y ∈ b x ⋅ w y ≠ z