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	Could not format assertion : No typesetting found for |- PrmIdeal = ( r e. Ring |-> { i e. ( LIdeal ` r ) | ( i =/= ( Base ` r ) /\ A. a e. ( LIdeal ` r ) A. b e. ( LIdeal ` r ) ( A. x e. a A. y e. b ( x ( .r ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprmidl	Could not format PrmIdeal : No typesetting found for class PrmIdeal with typecode class
1		vr	$$setvarr$$
2		crg	$$class\mathrm{Ring}$$
3		vi	$$setvari$$
4		clidl	$$class\mathrm{LIdeal}$$
5	1	cv	$$setvarr$$
6	5 4	cfv	$$class\mathrm{LIdeal}\left(r\right)$$
7	3	cv	$$setvari$$
8		cbs	$$class\mathrm{Base}$$
9	5 8	cfv	$$class{\mathrm{Base}}_r$$
10	7 9	wne	$$wffi\ne {\mathrm{Base}}_r$$
11		va	$$setvara$$
12		vb	$$setvarb$$
13		vx	$$setvarx$$
14	11	cv	$$setvara$$
15		vy	$$setvary$$
16	12	cv	$$setvarb$$
17	13	cv	$$setvarx$$
18		cmulr	$$class{\cdot }_{𝑟}$$
19	5 18	cfv	$$class{\cdot }_r$$
20	15	cv	$$setvary$$
21	17 20 19	co	$$class\left(x{\cdot }_{r}y\right)$$
22	21 7	wcel	$$wffx{\cdot }_{r}y\in i$$
23	22 15 16	wral	$$wff\forall y\in bx{\cdot }_{r}y\in i$$
24	23 13 14	wral	$$wff\forall x\in a\forall y\in bx{\cdot }_{r}y\in i$$
25	14 7	wss	$$wffa\subseteq i$$
26	16 7	wss	$$wffb\subseteq i$$
27	25 26	wo	$$wff\left(a\subseteq i\vee b\subseteq i\right)$$
28	24 27	wi	$$wff\left(\forall x\in a\forall y\in bx{\cdot }_{r}y\in i\to \left(a\subseteq i\vee b\subseteq i\right)\right)$$
29	28 12 6	wral	$$wff\forall b\in \mathrm{LIdeal}\left(r\right)\left(\forall x\in a\forall y\in bx{\cdot }_{r}y\in i\to \left(a\subseteq i\vee b\subseteq i\right)\right)$$
30	29 11 6	wral	$$wff\forall a\in \mathrm{LIdeal}\left(r\right)\forall b\in \mathrm{LIdeal}\left(r\right)\left(\forall x\in a\forall y\in bx{\cdot }_{r}y\in i\to \left(a\subseteq i\vee b\subseteq i\right)\right)$$
31	10 30	wa	$$wff\left(i\ne {\mathrm{Base}}_r\wedge \forall a\in \mathrm{LIdeal}\left(r\right)\forall b\in \mathrm{LIdeal}\left(r\right)\left(\forall x\in a\forall y\in bx{\cdot }_{r}y\in i\to \left(a\subseteq i\vee b\subseteq i\right)\right)\right)$$
32	31 3 6	crab	$$class\left\{i\in \mathrm{LIdeal}\left(r\right)|\left(i\ne {\mathrm{Base}}_r\wedge \forall a\in \mathrm{LIdeal}\left(r\right)\forall b\in \mathrm{LIdeal}\left(r\right)\left(\forall x\in a\forall y\in bx{\cdot }_{r}y\in i\to \left(a\subseteq i\vee b\subseteq i\right)\right)\right)\right\}$$
33	1 2 32	cmpt	$$class\left(r\in \mathrm{Ring}⟼\left\{i\in \mathrm{LIdeal}\left(r\right)|\left(i\ne {\mathrm{Base}}_r\wedge \forall a\in \mathrm{LIdeal}\left(r\right)\forall b\in \mathrm{LIdeal}\left(r\right)\left(\forall x\in a\forall y\in bx{\cdot }_{r}y\in i\to \left(a\subseteq i\vee b\subseteq i\right)\right)\right)\right\}\right)$$
34	0 33	wceq	Could not format PrmIdeal = ( r e. Ring |-> { i e. ( LIdeal ` r ) | ( i =/= ( Base ` r ) /\ A. a e. ( LIdeal ` r ) A. b e. ( LIdeal ` r ) ( A. x e. a A. y e. b ( x ( .r ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } ) : No typesetting found for wff PrmIdeal = ( r e. Ring |-> { i e. ( LIdeal ` r ) | ( i =/= ( Base ` r ) /\ A. a e. ( LIdeal ` r ) A. b e. ( LIdeal ` r ) ( A. x e. a A. y e. b ( x ( .r ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } ) with typecode wff