smprngprmrng

Description: A simple ring (a nonzero ring whose only ideals are .0. and R ) is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011) (Revised by AV, 18-Jun-2026)

	Ref	Expression
Hypotheses	smprngprmrng.b	$⊢ B = {Base}_{R}$
	smprngprmrng.z	$⊢ \underset{˙}{0} = 0_{R}$
	smprngprmrng.u	$⊢ U = LIdeal (R)$
Assertion	smprngprmrng	Could not format assertion : No typesetting found for \|- ( ( R e. NzRing /\ U = { { .0. } , B } ) -> R e. PrmRing ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		smprngprmrng.b	$⊢ B = {Base}_{R}$
2		smprngprmrng.z	$⊢ \underset{˙}{0} = 0_{R}$
3		smprngprmrng.u	$⊢ U = LIdeal (R)$
4		nzrring	$⊢ R \in NzRing \to R \in Ring$
5	4	adantr	$⊢ (R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \to R \in Ring$
6		eqid	$⊢ LIdeal (R) = LIdeal (R)$
7	6 2	lidl0	$⊢ R \in Ring \to \{\underset{˙}{0}\} \in LIdeal (R)$
8	4 7	syl	$⊢ R \in NzRing \to \{\underset{˙}{0}\} \in LIdeal (R)$
9	8	adantr	$⊢ (R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \to \{\underset{˙}{0}\} \in LIdeal (R)$
10	2 1	drnglidl1ne0	$⊢ R \in NzRing \to B \neq \{\underset{˙}{0}\}$
11	10	necomd	$⊢ R \in NzRing \to \{\underset{˙}{0}\} \neq B$
12	11	adantr	$⊢ (R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \to \{\underset{˙}{0}\} \neq B$
13		df-pr	$⊢ \{\{\underset{˙}{0}\}, B\} = \{\{\underset{˙}{0}\}\} \cup \{B\}$
14	13	eqeq2i	$⊢ U = \{\{\underset{˙}{0}\}, B\} \leftrightarrow U = \{\{\underset{˙}{0}\}\} \cup \{B\}$
15		id	$⊢ U = \{\{\underset{˙}{0}\}\} \cup \{B\} \to U = \{\{\underset{˙}{0}\}\} \cup \{B\}$
16	3 15	eqtr3id	$⊢ U = \{\{\underset{˙}{0}\}\} \cup \{B\} \to LIdeal (R) = \{\{\underset{˙}{0}\}\} \cup \{B\}$
17	16	eleq2d	$⊢ U = \{\{\underset{˙}{0}\}\} \cup \{B\} \to (a \in LIdeal (R) \leftrightarrow a \in (\{\{\underset{˙}{0}\}\} \cup \{B\}))$
18	16	eleq2d	$⊢ U = \{\{\underset{˙}{0}\}\} \cup \{B\} \to (b \in LIdeal (R) \leftrightarrow b \in (\{\{\underset{˙}{0}\}\} \cup \{B\}))$
19	17 18	anbi12d	$⊢ U = \{\{\underset{˙}{0}\}\} \cup \{B\} \to ((a \in LIdeal (R) \land b \in LIdeal (R)) \leftrightarrow (a \in (\{\{\underset{˙}{0}\}\} \cup \{B\}) \land b \in (\{\{\underset{˙}{0}\}\} \cup \{B\})))$
20		elun	$⊢ a \in (\{\{\underset{˙}{0}\}\} \cup \{B\}) \leftrightarrow (a \in \{\{\underset{˙}{0}\}\} \lor a \in \{B\})$
21		velsn	$⊢ a \in \{\{\underset{˙}{0}\}\} \leftrightarrow a = \{\underset{˙}{0}\}$
22		velsn	$⊢ a \in \{B\} \leftrightarrow a = B$
23	21 22	orbi12i	$⊢ (a \in \{\{\underset{˙}{0}\}\} \lor a \in \{B\}) \leftrightarrow (a = \{\underset{˙}{0}\} \lor a = B)$
24	20 23	bitri	$⊢ a \in (\{\{\underset{˙}{0}\}\} \cup \{B\}) \leftrightarrow (a = \{\underset{˙}{0}\} \lor a = B)$
25		elun	$⊢ b \in (\{\{\underset{˙}{0}\}\} \cup \{B\}) \leftrightarrow (b \in \{\{\underset{˙}{0}\}\} \lor b \in \{B\})$
26		velsn	$⊢ b \in \{\{\underset{˙}{0}\}\} \leftrightarrow b = \{\underset{˙}{0}\}$
27		velsn	$⊢ b \in \{B\} \leftrightarrow b = B$
28	26 27	orbi12i	$⊢ (b \in \{\{\underset{˙}{0}\}\} \lor b \in \{B\}) \leftrightarrow (b = \{\underset{˙}{0}\} \lor b = B)$
29	25 28	bitri	$⊢ b \in (\{\{\underset{˙}{0}\}\} \cup \{B\}) \leftrightarrow (b = \{\underset{˙}{0}\} \lor b = B)$
30	24 29	anbi12i	$⊢ (a \in (\{\{\underset{˙}{0}\}\} \cup \{B\}) \land b \in (\{\{\underset{˙}{0}\}\} \cup \{B\})) \leftrightarrow ((a = \{\underset{˙}{0}\} \lor a = B) \land (b = \{\underset{˙}{0}\} \lor b = B))$
31	19 30	bitrdi	$⊢ U = \{\{\underset{˙}{0}\}\} \cup \{B\} \to ((a \in LIdeal (R) \land b \in LIdeal (R)) \leftrightarrow ((a = \{\underset{˙}{0}\} \lor a = B) \land (b = \{\underset{˙}{0}\} \lor b = B)))$
32	14 31	sylbi	$⊢ U = \{\{\underset{˙}{0}\}, B\} \to ((a \in LIdeal (R) \land b \in LIdeal (R)) \leftrightarrow ((a = \{\underset{˙}{0}\} \lor a = B) \land (b = \{\underset{˙}{0}\} \lor b = B)))$
33	32	adantl	$⊢ (R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \to ((a \in LIdeal (R) \land b \in LIdeal (R)) \leftrightarrow ((a = \{\underset{˙}{0}\} \lor a = B) \land (b = \{\underset{˙}{0}\} \lor b = B)))$
34		eqimss	$⊢ a = \{\underset{˙}{0}\} \to a \subseteq \{\underset{˙}{0}\}$
35	34	orcd	$⊢ a = \{\underset{˙}{0}\} \to (a \subseteq \{\underset{˙}{0}\} \lor b \subseteq \{\underset{˙}{0}\})$
36	35	adantr	$⊢ (a = \{\underset{˙}{0}\} \land b = \{\underset{˙}{0}\}) \to (a \subseteq \{\underset{˙}{0}\} \lor b \subseteq \{\underset{˙}{0}\})$
37	36	a1i13	$⊢ R \in NzRing \to ((a = \{\underset{˙}{0}\} \land b = \{\underset{˙}{0}\}) \to (\forall x \in a \forall y \in b x \cdot_{R} y \in \{\underset{˙}{0}\} \to (a \subseteq \{\underset{˙}{0}\} \lor b \subseteq \{\underset{˙}{0}\})))$
38		eqimss	$⊢ b = \{\underset{˙}{0}\} \to b \subseteq \{\underset{˙}{0}\}$
39	38	olcd	$⊢ b = \{\underset{˙}{0}\} \to (a \subseteq \{\underset{˙}{0}\} \lor b \subseteq \{\underset{˙}{0}\})$
40	39	adantl	$⊢ (a = B \land b = \{\underset{˙}{0}\}) \to (a \subseteq \{\underset{˙}{0}\} \lor b \subseteq \{\underset{˙}{0}\})$
41	40	a1i13	$⊢ R \in NzRing \to ((a = B \land b = \{\underset{˙}{0}\}) \to (\forall x \in a \forall y \in b x \cdot_{R} y \in \{\underset{˙}{0}\} \to (a \subseteq \{\underset{˙}{0}\} \lor b \subseteq \{\underset{˙}{0}\})))$
42	35	adantr	$⊢ (a = \{\underset{˙}{0}\} \land b = B) \to (a \subseteq \{\underset{˙}{0}\} \lor b \subseteq \{\underset{˙}{0}\})$
43	42	a1i13	$⊢ R \in NzRing \to ((a = \{\underset{˙}{0}\} \land b = B) \to (\forall x \in a \forall y \in b x \cdot_{R} y \in \{\underset{˙}{0}\} \to (a \subseteq \{\underset{˙}{0}\} \lor b \subseteq \{\underset{˙}{0}\})))$
44		eqid	$⊢ 1_{R} = 1_{R}$
45	1 44	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
46	4 45	syl	$⊢ R \in NzRing \to 1_{R} \in B$
47	44 2	nzrnz	$⊢ R \in NzRing \to 1_{R} \neq \underset{˙}{0}$
48	47	neneqd	$⊢ R \in NzRing \to \neg 1_{R} = \underset{˙}{0}$
49		ringsrg	$⊢ R \in Ring \to R \in SRing$
50	49 45	jca	$⊢ R \in Ring \to (R \in SRing \land 1_{R} \in B)$
51		eqid	$⊢ \cdot_{R} = \cdot_{R}$
52	1 51 44	srgridm	$⊢ (R \in SRing \land 1_{R} \in B) \to 1_{R} \cdot_{R} 1_{R} = 1_{R}$
53	4 50 52	3syl	$⊢ R \in NzRing \to 1_{R} \cdot_{R} 1_{R} = 1_{R}$
54	53	eqeq1d	$⊢ R \in NzRing \to (1_{R} \cdot_{R} 1_{R} = \underset{˙}{0} \leftrightarrow 1_{R} = \underset{˙}{0})$
55	48 54	mtbird	$⊢ R \in NzRing \to \neg 1_{R} \cdot_{R} 1_{R} = \underset{˙}{0}$
56		ovex	$⊢ 1_{R} \cdot_{R} 1_{R} \in V$
57	56	elsn	$⊢ 1_{R} \cdot_{R} 1_{R} \in \{\underset{˙}{0}\} \leftrightarrow 1_{R} \cdot_{R} 1_{R} = \underset{˙}{0}$
58	55 57	sylnibr	$⊢ R \in NzRing \to \neg 1_{R} \cdot_{R} 1_{R} \in \{\underset{˙}{0}\}$
59		oveq1	$⊢ x = 1_{R} \to x \cdot_{R} y = 1_{R} \cdot_{R} y$
60	59	eleq1d	$⊢ x = 1_{R} \to (x \cdot_{R} y \in \{\underset{˙}{0}\} \leftrightarrow 1_{R} \cdot_{R} y \in \{\underset{˙}{0}\})$
61	60	notbid	$⊢ x = 1_{R} \to (\neg x \cdot_{R} y \in \{\underset{˙}{0}\} \leftrightarrow \neg 1_{R} \cdot_{R} y \in \{\underset{˙}{0}\})$
62		oveq2	$⊢ y = 1_{R} \to 1_{R} \cdot_{R} y = 1_{R} \cdot_{R} 1_{R}$
63	62	eleq1d	$⊢ y = 1_{R} \to (1_{R} \cdot_{R} y \in \{\underset{˙}{0}\} \leftrightarrow 1_{R} \cdot_{R} 1_{R} \in \{\underset{˙}{0}\})$
64	63	notbid	$⊢ y = 1_{R} \to (\neg 1_{R} \cdot_{R} y \in \{\underset{˙}{0}\} \leftrightarrow \neg 1_{R} \cdot_{R} 1_{R} \in \{\underset{˙}{0}\})$
65	61 64	rspc2ev	$⊢ (1_{R} \in B \land 1_{R} \in B \land \neg 1_{R} \cdot_{R} 1_{R} \in \{\underset{˙}{0}\}) \to \exists x \in B \exists y \in B \neg x \cdot_{R} y \in \{\underset{˙}{0}\}$
66	46 46 58 65	syl3anc	$⊢ R \in NzRing \to \exists x \in B \exists y \in B \neg x \cdot_{R} y \in \{\underset{˙}{0}\}$
67		rexnal2	$⊢ \exists x \in B \exists y \in B \neg x \cdot_{R} y \in \{\underset{˙}{0}\} \leftrightarrow \neg \forall x \in B \forall y \in B x \cdot_{R} y \in \{\underset{˙}{0}\}$
68	66 67	sylib	$⊢ R \in NzRing \to \neg \forall x \in B \forall y \in B x \cdot_{R} y \in \{\underset{˙}{0}\}$
69	68	pm2.21d	$⊢ R \in NzRing \to (\forall x \in B \forall y \in B x \cdot_{R} y \in \{\underset{˙}{0}\} \to (a \subseteq \{\underset{˙}{0}\} \lor b \subseteq \{\underset{˙}{0}\}))$
70		raleq	$⊢ a = B \to (\forall x \in a \forall y \in b x \cdot_{R} y \in \{\underset{˙}{0}\} \leftrightarrow \forall x \in B \forall y \in b x \cdot_{R} y \in \{\underset{˙}{0}\})$
71		raleq	$⊢ b = B \to (\forall y \in b x \cdot_{R} y \in \{\underset{˙}{0}\} \leftrightarrow \forall y \in B x \cdot_{R} y \in \{\underset{˙}{0}\})$
72	71	ralbidv	$⊢ b = B \to (\forall x \in B \forall y \in b x \cdot_{R} y \in \{\underset{˙}{0}\} \leftrightarrow \forall x \in B \forall y \in B x \cdot_{R} y \in \{\underset{˙}{0}\})$
73	70 72	sylan9bb	$⊢ (a = B \land b = B) \to (\forall x \in a \forall y \in b x \cdot_{R} y \in \{\underset{˙}{0}\} \leftrightarrow \forall x \in B \forall y \in B x \cdot_{R} y \in \{\underset{˙}{0}\})$
74	73	imbi1d	$⊢ (a = B \land b = B) \to ((\forall x \in a \forall y \in b x \cdot_{R} y \in \{\underset{˙}{0}\} \to (a \subseteq \{\underset{˙}{0}\} \lor b \subseteq \{\underset{˙}{0}\})) \leftrightarrow (\forall x \in B \forall y \in B x \cdot_{R} y \in \{\underset{˙}{0}\} \to (a \subseteq \{\underset{˙}{0}\} \lor b \subseteq \{\underset{˙}{0}\})))$
75	69 74	syl5ibrcom	$⊢ R \in NzRing \to ((a = B \land b = B) \to (\forall x \in a \forall y \in b x \cdot_{R} y \in \{\underset{˙}{0}\} \to (a \subseteq \{\underset{˙}{0}\} \lor b \subseteq \{\underset{˙}{0}\})))$
76	37 41 43 75	ccased	$⊢ R \in NzRing \to (((a = \{\underset{˙}{0}\} \lor a = B) \land (b = \{\underset{˙}{0}\} \lor b = B)) \to (\forall x \in a \forall y \in b x \cdot_{R} y \in \{\underset{˙}{0}\} \to (a \subseteq \{\underset{˙}{0}\} \lor b \subseteq \{\underset{˙}{0}\})))$
77	76	adantr	$⊢ (R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \to (((a = \{\underset{˙}{0}\} \lor a = B) \land (b = \{\underset{˙}{0}\} \lor b = B)) \to (\forall x \in a \forall y \in b x \cdot_{R} y \in \{\underset{˙}{0}\} \to (a \subseteq \{\underset{˙}{0}\} \lor b \subseteq \{\underset{˙}{0}\})))$
78	33 77	sylbid	$⊢ (R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \to ((a \in LIdeal (R) \land b \in LIdeal (R)) \to (\forall x \in a \forall y \in b x \cdot_{R} y \in \{\underset{˙}{0}\} \to (a \subseteq \{\underset{˙}{0}\} \lor b \subseteq \{\underset{˙}{0}\})))$
79	78	ralrimivv	$⊢ (R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \to \forall a \in LIdeal (R) \forall b \in LIdeal (R) (\forall x \in a \forall y \in b x \cdot_{R} y \in \{\underset{˙}{0}\} \to (a \subseteq \{\underset{˙}{0}\} \lor b \subseteq \{\underset{˙}{0}\}))$
80	1 51	isprmidl	$⊢ R \in Ring \to (\{\underset{˙}{0}\} \in PrmIdeal (R) \leftrightarrow (\{\underset{˙}{0}\} \in LIdeal (R) \land \{\underset{˙}{0}\} \neq B \land \forall a \in LIdeal (R) \forall b \in LIdeal (R) (\forall x \in a \forall y \in b x \cdot_{R} y \in \{\underset{˙}{0}\} \to (a \subseteq \{\underset{˙}{0}\} \lor b \subseteq \{\underset{˙}{0}\}))))$
81	4 80	syl	$⊢ R \in NzRing \to (\{\underset{˙}{0}\} \in PrmIdeal (R) \leftrightarrow (\{\underset{˙}{0}\} \in LIdeal (R) \land \{\underset{˙}{0}\} \neq B \land \forall a \in LIdeal (R) \forall b \in LIdeal (R) (\forall x \in a \forall y \in b x \cdot_{R} y \in \{\underset{˙}{0}\} \to (a \subseteq \{\underset{˙}{0}\} \lor b \subseteq \{\underset{˙}{0}\}))))$
82	81	adantr	$⊢ (R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \to (\{\underset{˙}{0}\} \in PrmIdeal (R) \leftrightarrow (\{\underset{˙}{0}\} \in LIdeal (R) \land \{\underset{˙}{0}\} \neq B \land \forall a \in LIdeal (R) \forall b \in LIdeal (R) (\forall x \in a \forall y \in b x \cdot_{R} y \in \{\underset{˙}{0}\} \to (a \subseteq \{\underset{˙}{0}\} \lor b \subseteq \{\underset{˙}{0}\}))))$
83	9 12 79 82	mpbir3and	$⊢ (R \in NzRing \land U = \{\{\underset{˙}{0}\}, B\}) \to \{\underset{˙}{0}\} \in PrmIdeal (R)$
84		eqid	$⊢ PrmIdeal (R) = PrmIdeal (R)$
85	2 84	isprmrng	Could not format ( R e. PrmRing <-> ( R e. Ring /\ { .0. } e. ( PrmIdeal ` R ) ) ) : No typesetting found for \|- ( R e. PrmRing <-> ( R e. Ring /\ { .0. } e. ( PrmIdeal ` R ) ) ) with typecode \|-
86	5 83 85	sylanbrc	Could not format ( ( R e. NzRing /\ U = { { .0. } , B } ) -> R e. PrmRing ) : No typesetting found for \|- ( ( R e. NzRing /\ U = { { .0. } , B } ) -> R e. PrmRing ) with typecode \|-

Metamath Proof Explorer

Theorem smprngprmrng

Proof