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 = ( 𝑟 ∈ Ring ↦ { 𝑖 ∈ ( LIdeal ‘ 𝑟 ) ∣ ( 𝑖 ≠ ( Base ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑟 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprmidl	⊢ PrmIdeal
1		vr	⊢ 𝑟
2		crg	⊢ Ring
3		vi	⊢ 𝑖
4		clidl	⊢ LIdeal
5	1	cv	⊢ 𝑟
6	5 4	cfv	⊢ ( LIdeal ‘ 𝑟 )
7	3	cv	⊢ 𝑖
8		cbs	⊢ Base
9	5 8	cfv	⊢ ( Base ‘ 𝑟 )
10	7 9	wne	⊢ 𝑖 ≠ ( Base ‘ 𝑟 )
11		va	⊢ 𝑎
12		vb	⊢ 𝑏
13		vx	⊢ 𝑥
14	11	cv	⊢ 𝑎
15		vy	⊢ 𝑦
16	12	cv	⊢ 𝑏
17	13	cv	⊢ 𝑥
18		cmulr	⊢ .r
19	5 18	cfv	⊢ ( .r ‘ 𝑟 )
20	15	cv	⊢ 𝑦
21	17 20 19	co	⊢ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 )
22	21 7	wcel	⊢ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ∈ 𝑖
23	22 15 16	wral	⊢ ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ∈ 𝑖
24	23 13 14	wral	⊢ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ∈ 𝑖
25	14 7	wss	⊢ 𝑎 ⊆ 𝑖
26	16 7	wss	⊢ 𝑏 ⊆ 𝑖
27	25 26	wo	⊢ ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 )
28	24 27	wi	⊢ ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) )
29	28 12 6	wral	⊢ ∀ 𝑏 ∈ ( LIdeal ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) )
30	29 11 6	wral	⊢ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑟 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) )
31	10 30	wa	⊢ ( 𝑖 ≠ ( Base ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑟 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) )
32	31 3 6	crab	⊢ { 𝑖 ∈ ( LIdeal ‘ 𝑟 ) ∣ ( 𝑖 ≠ ( Base ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑟 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) }
33	1 2 32	cmpt	⊢ ( 𝑟 ∈ Ring ↦ { 𝑖 ∈ ( LIdeal ‘ 𝑟 ) ∣ ( 𝑖 ≠ ( Base ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑟 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) } )
34	0 33	wceq	⊢ PrmIdeal = ( 𝑟 ∈ Ring ↦ { 𝑖 ∈ ( LIdeal ‘ 𝑟 ) ∣ ( 𝑖 ≠ ( Base ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑟 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) } )