prmidl

Description: The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Thierry Arnoux, 12-Jan-2024)

	Ref	Expression
Hypotheses	prmidlval.1	$⊢ B = {Base}_{R}$
	prmidlval.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	prmidl	Could not format assertion : No typesetting found for \|- ( ( ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) ) /\ A. x e. I A. y e. J ( x .x. y ) e. P ) -> ( I C_ P \/ J C_ P ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		prmidlval.1	$⊢ B = {Base}_{R}$
2		prmidlval.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		raleq	$⊢ b = J \to (\forall y \in b x \underset{˙}{\cdot} y \in P \leftrightarrow \forall y \in J x \underset{˙}{\cdot} y \in P)$
4	3	ralbidv	$⊢ b = J \to (\forall x \in I \forall y \in b x \underset{˙}{\cdot} y \in P \leftrightarrow \forall x \in I \forall y \in J x \underset{˙}{\cdot} y \in P)$
5		sseq1	$⊢ b = J \to (b \subseteq P \leftrightarrow J \subseteq P)$
6	5	orbi2d	$⊢ b = J \to ((I \subseteq P \lor b \subseteq P) \leftrightarrow (I \subseteq P \lor J \subseteq P))$
7	4 6	imbi12d	$⊢ b = J \to ((\forall x \in I \forall y \in b x \underset{˙}{\cdot} y \in P \to (I \subseteq P \lor b \subseteq P)) \leftrightarrow (\forall x \in I \forall y \in J x \underset{˙}{\cdot} y \in P \to (I \subseteq P \lor J \subseteq P)))$
8		raleq	$⊢ a = I \to (\forall x \in a \forall y \in b x \underset{˙}{\cdot} y \in P \leftrightarrow \forall x \in I \forall y \in b x \underset{˙}{\cdot} y \in P)$
9		sseq1	$⊢ a = I \to (a \subseteq P \leftrightarrow I \subseteq P)$
10	9	orbi1d	$⊢ a = I \to ((a \subseteq P \lor b \subseteq P) \leftrightarrow (I \subseteq P \lor b \subseteq P))$
11	8 10	imbi12d	$⊢ a = I \to ((\forall x \in a \forall y \in b x \underset{˙}{\cdot} y \in P \to (a \subseteq P \lor b \subseteq P)) \leftrightarrow (\forall x \in I \forall y \in b x \underset{˙}{\cdot} y \in P \to (I \subseteq P \lor b \subseteq P)))$
12	11	ralbidv	$⊢ a = I \to (\forall b \in LIdeal (R) (\forall x \in a \forall y \in b x \underset{˙}{\cdot} y \in P \to (a \subseteq P \lor b \subseteq P)) \leftrightarrow \forall b \in LIdeal (R) (\forall x \in I \forall y \in b x \underset{˙}{\cdot} y \in P \to (I \subseteq P \lor b \subseteq P)))$
13	1 2	isprmidl	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 \|-
14	13	biimpa	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 \|-
15	14	simp3d	Could not format ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) -> 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 ) ) -> 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	15	adantr	Could not format ( ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) ) -> 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 ) ) /\ ( I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) ) -> 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 \|-
17		simprl	Could not format ( ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) ) -> I e. ( LIdeal ` R ) ) : No typesetting found for \|- ( ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) ) -> I e. ( LIdeal ` R ) ) with typecode \|-
18	12 16 17	rspcdva	Could not format ( ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) ) -> A. b e. ( LIdeal ` R ) ( A. x e. I A. y e. b ( x .x. y ) e. P -> ( I C_ P \/ b C_ P ) ) ) : No typesetting found for \|- ( ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) ) -> A. b e. ( LIdeal ` R ) ( A. x e. I A. y e. b ( x .x. y ) e. P -> ( I C_ P \/ b C_ P ) ) ) with typecode \|-
19		simprr	Could not format ( ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) ) -> J e. ( LIdeal ` R ) ) : No typesetting found for \|- ( ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) ) -> J e. ( LIdeal ` R ) ) with typecode \|-
20	7 18 19	rspcdva	Could not format ( ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) ) -> ( A. x e. I A. y e. J ( x .x. y ) e. P -> ( I C_ P \/ J C_ P ) ) ) : No typesetting found for \|- ( ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) ) -> ( A. x e. I A. y e. J ( x .x. y ) e. P -> ( I C_ P \/ J C_ P ) ) ) with typecode \|-
21	20	imp	Could not format ( ( ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) ) /\ A. x e. I A. y e. J ( x .x. y ) e. P ) -> ( I C_ P \/ J C_ P ) ) : No typesetting found for \|- ( ( ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) ) /\ A. x e. I A. y e. J ( x .x. y ) e. P ) -> ( I C_ P \/ J C_ P ) ) with typecode \|-

Metamath Proof Explorer

Theorem prmidl

Proof