rsprprmprmidl

Description: In a commutative ring, ideals generated by prime elements are prime ideals. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	rsprprmprmidl.k	$⊢ K = RSpan (R)$
	rsprprmprmidl.r	$⊢ φ \to R \in CRing$
	rsprprmprmidl.p	$⊢ φ \to P \in RPrime (R)$
Assertion	rsprprmprmidl	Could not format assertion : No typesetting found for \|- ( ph -> ( K ` { P } ) e. ( PrmIdeal ` R ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		rsprprmprmidl.k	$⊢ K = RSpan (R)$
2		rsprprmprmidl.r	$⊢ φ \to R \in CRing$
3		rsprprmprmidl.p	$⊢ φ \to P \in RPrime (R)$
4	2	crngringd	$⊢ φ \to R \in Ring$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6		eqid	$⊢ RPrime (R) = RPrime (R)$
7	5 6 2 3	rprmcl	$⊢ φ \to P \in {Base}_{R}$
8	7	snssd	$⊢ φ \to \{P\} \subseteq {Base}_{R}$
9		eqid	$⊢ LIdeal (R) = LIdeal (R)$
10	1 5 9	rspcl	$⊢ (R \in Ring \land \{P\} \subseteq {Base}_{R}) \to K (\{P\}) \in LIdeal (R)$
11	4 8 10	syl2anc	$⊢ φ \to K (\{P\}) \in LIdeal (R)$
12		eqid	$⊢ 1_{R} = 1_{R}$
13	5 12	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
14	4 13	syl	$⊢ φ \to 1_{R} \in {Base}_{R}$
15		eqid	$⊢ Unit (R) = Unit (R)$
16	6 15 2 3	rprmnunit	$⊢ φ \to \neg P \in Unit (R)$
17	2	adantr	$⊢ (φ \land P ∥_{r} (R) 1_{R}) \to R \in CRing$
18		simpr	$⊢ (φ \land P ∥_{r} (R) 1_{R}) \to P ∥_{r} (R) 1_{R}$
19	15 12	1unit	$⊢ R \in Ring \to 1_{R} \in Unit (R)$
20	4 19	syl	$⊢ φ \to 1_{R} \in Unit (R)$
21	20	adantr	$⊢ (φ \land P ∥_{r} (R) 1_{R}) \to 1_{R} \in Unit (R)$
22		eqid	$⊢ ∥_{r} (R) = ∥_{r} (R)$
23	15 22	dvdsunit	$⊢ (R \in CRing \land P ∥_{r} (R) 1_{R} \land 1_{R} \in Unit (R)) \to P \in Unit (R)$
24	17 18 21 23	syl3anc	$⊢ (φ \land P ∥_{r} (R) 1_{R}) \to P \in Unit (R)$
25	16 24	mtand	$⊢ φ \to \neg P ∥_{r} (R) 1_{R}$
26	5 1 22 4 7	ellpi	$⊢ φ \to (1_{R} \in K (\{P\}) \leftrightarrow P ∥_{r} (R) 1_{R})$
27	25 26	mtbird	$⊢ φ \to \neg 1_{R} \in K (\{P\})$
28		nelne1	$⊢ (1_{R} \in {Base}_{R} \land \neg 1_{R} \in K (\{P\})) \to {Base}_{R} \neq K (\{P\})$
29	14 27 28	syl2anc	$⊢ φ \to {Base}_{R} \neq K (\{P\})$
30	29	necomd	$⊢ φ \to K (\{P\}) \neq {Base}_{R}$
31	5 1 22 4 7	ellpi	$⊢ φ \to (x \in K (\{P\}) \leftrightarrow P ∥_{r} (R) x)$
32	31	ad3antrrr	$⊢ (((φ \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land x \cdot_{R} y \in K (\{P\})) \to (x \in K (\{P\}) \leftrightarrow P ∥_{r} (R) x)$
33	32	biimpar	$⊢ ((((φ \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land x \cdot_{R} y \in K (\{P\})) \land P ∥_{r} (R) x) \to x \in K (\{P\})$
34	4	ad2antrr	$⊢ ((φ \land x \in {Base}_{R}) \land y \in {Base}_{R}) \to R \in Ring$
35	34	adantr	$⊢ (((φ \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land x \cdot_{R} y \in K (\{P\})) \to R \in Ring$
36	7	ad2antrr	$⊢ ((φ \land x \in {Base}_{R}) \land y \in {Base}_{R}) \to P \in {Base}_{R}$
37	36	adantr	$⊢ (((φ \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land x \cdot_{R} y \in K (\{P\})) \to P \in {Base}_{R}$
38	5 1 22 35 37	ellpi	$⊢ (((φ \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land x \cdot_{R} y \in K (\{P\})) \to (y \in K (\{P\}) \leftrightarrow P ∥_{r} (R) y)$
39	38	biimpar	$⊢ ((((φ \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land x \cdot_{R} y \in K (\{P\})) \land P ∥_{r} (R) y) \to y \in K (\{P\})$
40		eqid	$⊢ \cdot_{R} = \cdot_{R}$
41	2	ad3antrrr	$⊢ (((φ \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land x \cdot_{R} y \in K (\{P\})) \to R \in CRing$
42	3	ad3antrrr	$⊢ (((φ \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land x \cdot_{R} y \in K (\{P\})) \to P \in RPrime (R)$
43		simpllr	$⊢ (((φ \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land x \cdot_{R} y \in K (\{P\})) \to x \in {Base}_{R}$
44		simplr	$⊢ (((φ \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land x \cdot_{R} y \in K (\{P\})) \to y \in {Base}_{R}$
45	5 1 22 34 36	ellpi	$⊢ ((φ \land x \in {Base}_{R}) \land y \in {Base}_{R}) \to (x \cdot_{R} y \in K (\{P\}) \leftrightarrow P ∥_{r} (R) (x \cdot_{R} y))$
46	45	biimpa	$⊢ (((φ \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land x \cdot_{R} y \in K (\{P\})) \to P ∥_{r} (R) (x \cdot_{R} y)$
47	5 6 22 40 41 42 43 44 46	rprmdvds	$⊢ (((φ \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land x \cdot_{R} y \in K (\{P\})) \to (P ∥_{r} (R) x \lor P ∥_{r} (R) y)$
48	33 39 47	orim12da	$⊢ (((φ \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land x \cdot_{R} y \in K (\{P\})) \to (x \in K (\{P\}) \lor y \in K (\{P\}))$
49	48	ex	$⊢ ((φ \land x \in {Base}_{R}) \land y \in {Base}_{R}) \to (x \cdot_{R} y \in K (\{P\}) \to (x \in K (\{P\}) \lor y \in K (\{P\})))$
50	49	anasss	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to (x \cdot_{R} y \in K (\{P\}) \to (x \in K (\{P\}) \lor y \in K (\{P\})))$
51	50	ralrimivva	$⊢ φ \to \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x \cdot_{R} y \in K (\{P\}) \to (x \in K (\{P\}) \lor y \in K (\{P\})))$
52	5 40	isprmidlc	Could not format ( R e. CRing -> ( ( K ` { P } ) e. ( PrmIdeal ` R ) <-> ( ( K ` { P } ) e. ( LIdeal ` R ) /\ ( K ` { P } ) =/= ( Base ` R ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. ( K ` { P } ) -> ( x e. ( K ` { P } ) \/ y e. ( K ` { P } ) ) ) ) ) ) : No typesetting found for \|- ( R e. CRing -> ( ( K ` { P } ) e. ( PrmIdeal ` R ) <-> ( ( K ` { P } ) e. ( LIdeal ` R ) /\ ( K ` { P } ) =/= ( Base ` R ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. ( K ` { P } ) -> ( x e. ( K ` { P } ) \/ y e. ( K ` { P } ) ) ) ) ) ) with typecode \|-
53	52	biimpar	Could not format ( ( R e. CRing /\ ( ( K ` { P } ) e. ( LIdeal ` R ) /\ ( K ` { P } ) =/= ( Base ` R ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. ( K ` { P } ) -> ( x e. ( K ` { P } ) \/ y e. ( K ` { P } ) ) ) ) ) -> ( K ` { P } ) e. ( PrmIdeal ` R ) ) : No typesetting found for \|- ( ( R e. CRing /\ ( ( K ` { P } ) e. ( LIdeal ` R ) /\ ( K ` { P } ) =/= ( Base ` R ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. ( K ` { P } ) -> ( x e. ( K ` { P } ) \/ y e. ( K ` { P } ) ) ) ) ) -> ( K ` { P } ) e. ( PrmIdeal ` R ) ) with typecode \|-
54	2 11 30 51 53	syl13anc	Could not format ( ph -> ( K ` { P } ) e. ( PrmIdeal ` R ) ) : No typesetting found for \|- ( ph -> ( K ` { P } ) e. ( PrmIdeal ` R ) ) with typecode \|-

Metamath Proof Explorer

Theorem rsprprmprmidl

Proof