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

Metamath Proof Explorer

Definition df-prmidl

Description: Define the class of prime ideals of a ring R . A proper ideal I of R is prime if whenever A B C_ I for ideals A and B , either A C_ I or B C_ I . The more familiar definition using elements rather than ideals is equivalent provided R is commutative; see prmidl2 and isprmidlc . (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Thierry Arnoux, 14-Jan-2024)

Ref Expression
Assertion df-prmidl ⊢ PrmIdeal = r ∈ Ring ⟼ i ∈ LIdeal ⁡ r | i ≠ Base r ∧ ∀ a ∈ LIdeal ⁡ r ∀ b ∈ LIdeal ⁡ r ∀ x ∈ a ∀ y ∈ b x ⋅ r y ∈ i → a ⊆ i ∨ b ⊆ i

Detailed syntax breakdown

Step Hyp Ref Expression
0 cprmidl class PrmIdeal
1 vr setvar r
2 crg class Ring
3 vi setvar i
4 clidl class LIdeal
5 1 cv setvar r
6 5 4 cfv class LIdeal ⁡ r
7 3 cv setvar i
8 cbs class Base
9 5 8 cfv class Base r
10 7 9 wne wff i ≠ Base r
11 va setvar a
12 vb setvar b
13 vx setvar x
14 11 cv setvar a
15 vy setvar y
16 12 cv setvar b
17 13 cv setvar x
18 cmulr class ⋅ 𝑟
19 5 18 cfv class ⋅ r
20 15 cv setvar y
21 17 20 19 co class x ⋅ r y
22 21 7 wcel wff x ⋅ r y ∈ i
23 22 15 16 wral wff ∀ y ∈ b x ⋅ r y ∈ i
24 23 13 14 wral wff ∀ x ∈ a ∀ y ∈ b x ⋅ r y ∈ i
25 14 7 wss wff a ⊆ i
26 16 7 wss wff b ⊆ i
27 25 26 wo wff a ⊆ i ∨ b ⊆ i
28 24 27 wi wff ∀ x ∈ a ∀ y ∈ b x ⋅ r y ∈ i → a ⊆ i ∨ b ⊆ i
29 28 12 6 wral wff ∀ b ∈ LIdeal ⁡ r ∀ x ∈ a ∀ y ∈ b x ⋅ r y ∈ i → a ⊆ i ∨ b ⊆ i
30 29 11 6 wral wff ∀ a ∈ LIdeal ⁡ r ∀ b ∈ LIdeal ⁡ r ∀ x ∈ a ∀ y ∈ b x ⋅ r y ∈ i → a ⊆ i ∨ b ⊆ i
31 10 30 wa wff i ≠ Base r ∧ ∀ a ∈ LIdeal ⁡ r ∀ b ∈ LIdeal ⁡ r ∀ x ∈ a ∀ y ∈ b x ⋅ r y ∈ i → a ⊆ i ∨ b ⊆ i
32 31 3 6 crab class i ∈ LIdeal ⁡ r | i ≠ Base r ∧ ∀ a ∈ LIdeal ⁡ r ∀ b ∈ LIdeal ⁡ r ∀ x ∈ a ∀ y ∈ b x ⋅ r y ∈ i → a ⊆ i ∨ b ⊆ i
33 1 2 32 cmpt class r ∈ Ring ⟼ i ∈ LIdeal ⁡ r | i ≠ Base r ∧ ∀ a ∈ LIdeal ⁡ r ∀ b ∈ LIdeal ⁡ r ∀ x ∈ a ∀ y ∈ b x ⋅ r y ∈ i → a ⊆ i ∨ b ⊆ i
34 0 33 wceq wff PrmIdeal = r ∈ Ring ⟼ i ∈ LIdeal ⁡ r | i ≠ Base r ∧ ∀ a ∈ LIdeal ⁡ r ∀ b ∈ LIdeal ⁡ r ∀ x ∈ a ∀ y ∈ b x ⋅ r y ∈ i → a ⊆ i ∨ b ⊆ i