Theorem prmidlval

Description: The class of prime ideals of a ring R . (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Thierry Arnoux, 12-Jan-2024)

	Ref	Expression
Hypotheses	prmidlval.1	$$⊢B={\mathrm{Base}}_R$$
	prmidlval.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	prmidlval	Could not format assertion : No typesetting found for |- ( R e. Ring -> ( PrmIdeal ` R ) = { i e. ( LIdeal ` R ) | ( i =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		prmidlval.1	$$⊢B={\mathrm{Base}}_R$$
2		prmidlval.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		df-prmidl	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 |- 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 |-
4		fveq2	$$⊢r=R\to \mathrm{LIdeal}\left(r\right)=\mathrm{LIdeal}\left(R\right)$$
5		fveq2	$$⊢r=R\to {\mathrm{Base}}_r={\mathrm{Base}}_R$$
6	5 1	eqtr4di	$$⊢r=R\to {\mathrm{Base}}_r=B$$
7	6	neeq2d	$$⊢r=R\to \left(i\ne {\mathrm{Base}}_r\leftrightarrow i\ne B\right)$$
8		fveq2	$$⊢r=R\to {\cdot }_r={\cdot }_R$$
9	8 2	eqtr4di	$$⊢r=R\to {\cdot }_r=\underset{\dot{}}{·}$$
10	9	oveqd	$$⊢r=R\to x{\cdot }_{r}y=x\underset{\dot{}}{·}y$$
11	10	eleq1d	$$⊢r=R\to \left(x{\cdot }_{r}y\in i\leftrightarrow x\underset{\dot{}}{·}y\in i\right)$$
12	11	2ralbidv	$$⊢r=R\to \left(\forall x\in a\forall y\in bx{\cdot }_{r}y\in i\leftrightarrow \forall x\in a\forall y\in bx\underset{\dot{}}{·}y\in i\right)$$
13	12	imbi1d	$$⊢r=R\to \left(\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)\leftrightarrow \left(\forall x\in a\forall y\in bx\underset{\dot{}}{·}y\in i\to \left(a\subseteq i\vee b\subseteq i\right)\right)\right)$$
14	4 13	raleqbidv	$$⊢r=R\to \left(\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)\leftrightarrow \forall b\in \mathrm{LIdeal}\left(R\right)\left(\forall x\in a\forall y\in bx\underset{\dot{}}{·}y\in i\to \left(a\subseteq i\vee b\subseteq i\right)\right)\right)$$
15	4 14	raleqbidv	$$⊢r=R\to \left(\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)\leftrightarrow \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\underset{\dot{}}{·}y\in i\to \left(a\subseteq i\vee b\subseteq i\right)\right)\right)$$
16	7 15	anbi12d	$$⊢r=R\to \left(\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)\leftrightarrow \left(i\ne B\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\underset{\dot{}}{·}y\in i\to \left(a\subseteq i\vee b\subseteq i\right)\right)\right)\right)$$
17	4 16	rabeqbidv	$$⊢r=R\to \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\}=\left\{i\in \mathrm{LIdeal}\left(R\right)|\left(i\ne B\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\underset{\dot{}}{·}y\in i\to \left(a\subseteq i\vee b\subseteq i\right)\right)\right)\right\}$$
18		id	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Ring}$$
19		eqid	$$⊢\left\{i\in \mathrm{LIdeal}\left(R\right)|\left(i\ne B\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\underset{\dot{}}{·}y\in i\to \left(a\subseteq i\vee b\subseteq i\right)\right)\right)\right\}=\left\{i\in \mathrm{LIdeal}\left(R\right)|\left(i\ne B\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\underset{\dot{}}{·}y\in i\to \left(a\subseteq i\vee b\subseteq i\right)\right)\right)\right\}$$
20		fvexd	$$⊢R\in \mathrm{Ring}\to \mathrm{LIdeal}\left(R\right)\in \mathrm{V}$$
21	19 20	rabexd	$$⊢R\in \mathrm{Ring}\to \left\{i\in \mathrm{LIdeal}\left(R\right)|\left(i\ne B\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\underset{\dot{}}{·}y\in i\to \left(a\subseteq i\vee b\subseteq i\right)\right)\right)\right\}\in \mathrm{V}$$
22	3 17 18 21	fvmptd3	Could not format ( R e. Ring -> ( PrmIdeal ` R ) = { i e. ( LIdeal ` R ) | ( i =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } ) : No typesetting found for |- ( R e. Ring -> ( PrmIdeal ` R ) = { i e. ( LIdeal ` R ) | ( i =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } ) with typecode |-