Theorem isprmidl

Description: The predicate "is a prime ideal". (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	isprmidl	Could not format assertion : No typesetting found for |- ( R e. Ring -> ( P e. ( PrmIdeal ` R ) <-> ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		prmidlval.1	$$⊢B={\mathrm{Base}}_R$$
2		prmidlval.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3	1 2	prmidlval	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 |-
4	3	eleq2d	Could not format ( R e. Ring -> ( P e. ( PrmIdeal ` R ) <-> P e. { 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 -> ( P e. ( PrmIdeal ` R ) <-> P e. { 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 |-
5		neeq1	$$⊢i=P\to \left(i\ne B\leftrightarrow P\ne B\right)$$
6		eleq2	$$⊢i=P\to \left(x\underset{\dot{}}{·}y\in i\leftrightarrow x\underset{\dot{}}{·}y\in P\right)$$
7	6	2ralbidv	$$⊢i=P\to \left(\forall x\in a\forall y\in bx\underset{\dot{}}{·}y\in i\leftrightarrow \forall x\in a\forall y\in bx\underset{\dot{}}{·}y\in P\right)$$
8		sseq2	$$⊢i=P\to \left(a\subseteq i\leftrightarrow a\subseteq P\right)$$
9		sseq2	$$⊢i=P\to \left(b\subseteq i\leftrightarrow b\subseteq P\right)$$
10	8 9	orbi12d	$$⊢i=P\to \left(\left(a\subseteq i\vee b\subseteq i\right)\leftrightarrow \left(a\subseteq P\vee b\subseteq P\right)\right)$$
11	7 10	imbi12d	$$⊢i=P\to \left(\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)\leftrightarrow \left(\forall x\in a\forall y\in bx\underset{\dot{}}{·}y\in P\to \left(a\subseteq P\vee b\subseteq P\right)\right)\right)$$
12	11	2ralbidv	$$⊢i=P\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\underset{\dot{}}{·}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 P\to \left(a\subseteq P\vee b\subseteq P\right)\right)\right)$$
13	5 12	anbi12d	$$⊢i=P\to \left(\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)\leftrightarrow \left(P\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 P\to \left(a\subseteq P\vee b\subseteq P\right)\right)\right)\right)$$
14	13	elrab	$$⊢P\in \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\}\leftrightarrow \left(P\in \mathrm{LIdeal}\left(R\right)\wedge \left(P\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 P\to \left(a\subseteq P\vee b\subseteq P\right)\right)\right)\right)$$
15	4 14	syl6bb	Could not format ( R e. Ring -> ( P e. ( PrmIdeal ` R ) <-> ( P e. ( LIdeal ` R ) /\ ( P =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) ) ) : No typesetting found for |- ( R e. Ring -> ( P e. ( PrmIdeal ` R ) <-> ( P e. ( LIdeal ` R ) /\ ( P =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) ) ) with typecode |-
16		3anass	$$⊢\left(P\in \mathrm{LIdeal}\left(R\right)\wedge P\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 P\to \left(a\subseteq P\vee b\subseteq P\right)\right)\right)\leftrightarrow \left(P\in \mathrm{LIdeal}\left(R\right)\wedge \left(P\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 P\to \left(a\subseteq P\vee b\subseteq P\right)\right)\right)\right)$$
17	15 16	syl6bbr	Could not format ( R e. Ring -> ( P e. ( PrmIdeal ` R ) <-> ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) ) : No typesetting found for |- ( R e. Ring -> ( P e. ( PrmIdeal ` R ) <-> ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) ) with typecode |-