smprngopr - Mathbox for Jeff Madsen

	Mathbox for Jeff Madsen		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > smprngopr		Structured version Visualization version GIF version

Theorem smprngopr 33851

Description: A simple ring (one whose only ideals are 0 and 𝑅) is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.)

**Hypotheses**
Ref	Expression
smprngpr.1	⊢ 𝐺 = (1^st ‘𝑅)
smprngpr.2	⊢ 𝐻 = (2^nd ‘𝑅)
smprngpr.3	⊢ 𝑋 = ran 𝐺
smprngpr.4	⊢ 𝑍 = (GId‘𝐺)
smprngpr.5	⊢ 𝑈 = (GId‘𝐻)

**Assertion**
Ref	Expression
smprngopr	⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → 𝑅 ∈ PrRing)

Proof of Theorem smprngopr Dummy variables 𝑖 𝑗 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp1 1061	. 2 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → 𝑅 ∈ RingOps)
2		smprngpr.1	. . . . 5 ⊢ 𝐺 = (1^st ‘𝑅)
3		smprngpr.4	. . . . 5 ⊢ 𝑍 = (GId‘𝐺)
4	2, 3	0idl 33824	. . . 4 ⊢ (𝑅 ∈ RingOps → {𝑍} ∈ (Idl‘𝑅))
5	4	3ad2ant1 1082	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → {𝑍} ∈ (Idl‘𝑅))
6		smprngpr.2	. . . . . . . 8 ⊢ 𝐻 = (2^nd ‘𝑅)
7		smprngpr.3	. . . . . . . 8 ⊢ 𝑋 = ran 𝐺
8		smprngpr.5	. . . . . . . 8 ⊢ 𝑈 = (GId‘𝐻)
9	2, 6, 7, 3, 8	0rngo 33826	. . . . . . 7 ⊢ (𝑅 ∈ RingOps → (𝑍 = 𝑈 ↔ 𝑋 = {𝑍}))
10		eqcom 2629	. . . . . . 7 ⊢ (𝑈 = 𝑍 ↔ 𝑍 = 𝑈)
11		eqcom 2629	. . . . . . 7 ⊢ ({𝑍} = 𝑋 ↔ 𝑋 = {𝑍})
12	9, 10, 11	3bitr4g 303	. . . . . 6 ⊢ (𝑅 ∈ RingOps → (𝑈 = 𝑍 ↔ {𝑍} = 𝑋))
13	12	necon3bid 2838	. . . . 5 ⊢ (𝑅 ∈ RingOps → (𝑈 ≠ 𝑍 ↔ {𝑍} ≠ 𝑋))
14	13	biimpa 501	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → {𝑍} ≠ 𝑋)
15	14	3adant3 1081	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → {𝑍} ≠ 𝑋)
16		df-pr 4180	. . . . . . . 8 ⊢ {{𝑍}, 𝑋} = ({{𝑍}} ∪ {𝑋})
17	16	eqeq2i 2634	. . . . . . 7 ⊢ ((Idl‘𝑅) = {{𝑍}, 𝑋} ↔ (Idl‘𝑅) = ({{𝑍}} ∪ {𝑋}))
18		eleq2 2690	. . . . . . . . 9 ⊢ ((Idl‘𝑅) = ({{𝑍}} ∪ {𝑋}) → (𝑖 ∈ (Idl‘𝑅) ↔ 𝑖 ∈ ({{𝑍}} ∪ {𝑋})))
19		eleq2 2690	. . . . . . . . 9 ⊢ ((Idl‘𝑅) = ({{𝑍}} ∪ {𝑋}) → (𝑗 ∈ (Idl‘𝑅) ↔ 𝑗 ∈ ({{𝑍}} ∪ {𝑋})))
20	18, 19	anbi12d 747	. . . . . . . 8 ⊢ ((Idl‘𝑅) = ({{𝑍}} ∪ {𝑋}) → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) ↔ (𝑖 ∈ ({{𝑍}} ∪ {𝑋}) ∧ 𝑗 ∈ ({{𝑍}} ∪ {𝑋}))))
21		elun 3753	. . . . . . . . . 10 ⊢ (𝑖 ∈ ({{𝑍}} ∪ {𝑋}) ↔ (𝑖 ∈ {{𝑍}} ∨ 𝑖 ∈ {𝑋}))
22		velsn 4193	. . . . . . . . . . 11 ⊢ (𝑖 ∈ {{𝑍}} ↔ 𝑖 = {𝑍})
23		velsn 4193	. . . . . . . . . . 11 ⊢ (𝑖 ∈ {𝑋} ↔ 𝑖 = 𝑋)
24	22, 23	orbi12i 543	. . . . . . . . . 10 ⊢ ((𝑖 ∈ {{𝑍}} ∨ 𝑖 ∈ {𝑋}) ↔ (𝑖 = {𝑍} ∨ 𝑖 = 𝑋))
25	21, 24	bitri 264	. . . . . . . . 9 ⊢ (𝑖 ∈ ({{𝑍}} ∪ {𝑋}) ↔ (𝑖 = {𝑍} ∨ 𝑖 = 𝑋))
26		elun 3753	. . . . . . . . . 10 ⊢ (𝑗 ∈ ({{𝑍}} ∪ {𝑋}) ↔ (𝑗 ∈ {{𝑍}} ∨ 𝑗 ∈ {𝑋}))
27		velsn 4193	. . . . . . . . . . 11 ⊢ (𝑗 ∈ {{𝑍}} ↔ 𝑗 = {𝑍})
28		velsn 4193	. . . . . . . . . . 11 ⊢ (𝑗 ∈ {𝑋} ↔ 𝑗 = 𝑋)
29	27, 28	orbi12i 543	. . . . . . . . . 10 ⊢ ((𝑗 ∈ {{𝑍}} ∨ 𝑗 ∈ {𝑋}) ↔ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋))
30	26, 29	bitri 264	. . . . . . . . 9 ⊢ (𝑗 ∈ ({{𝑍}} ∪ {𝑋}) ↔ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋))
31	25, 30	anbi12i 733	. . . . . . . 8 ⊢ ((𝑖 ∈ ({{𝑍}} ∪ {𝑋}) ∧ 𝑗 ∈ ({{𝑍}} ∪ {𝑋})) ↔ ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)))
32	20, 31	syl6bb 276	. . . . . . 7 ⊢ ((Idl‘𝑅) = ({{𝑍}} ∪ {𝑋}) → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) ↔ ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋))))
33	17, 32	sylbi 207	. . . . . 6 ⊢ ((Idl‘𝑅) = {{𝑍}, 𝑋} → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) ↔ ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋))))
34	33	3ad2ant3 1084	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) ↔ ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋))))
35		eqimss 3657	. . . . . . . . . . 11 ⊢ (𝑖 = {𝑍} → 𝑖 ⊆ {𝑍})
36	35	orcd 407	. . . . . . . . . 10 ⊢ (𝑖 = {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))
37	36	adantr 481	. . . . . . . . 9 ⊢ ((𝑖 = {𝑍} ∧ 𝑗 = {𝑍}) → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))
38	37	a1d 25	. . . . . . . 8 ⊢ ((𝑖 = {𝑍} ∧ 𝑗 = {𝑍}) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))
39	38	a1i 11	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → ((𝑖 = {𝑍} ∧ 𝑗 = {𝑍}) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
40		eqimss 3657	. . . . . . . . . . 11 ⊢ (𝑗 = {𝑍} → 𝑗 ⊆ {𝑍})
41	40	olcd 408	. . . . . . . . . 10 ⊢ (𝑗 = {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))
42	41	adantl 482	. . . . . . . . 9 ⊢ ((𝑖 = 𝑋 ∧ 𝑗 = {𝑍}) → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))
43	42	a1d 25	. . . . . . . 8 ⊢ ((𝑖 = 𝑋 ∧ 𝑗 = {𝑍}) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))
44	43	a1i 11	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → ((𝑖 = 𝑋 ∧ 𝑗 = {𝑍}) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
45	36	adantr 481	. . . . . . . . 9 ⊢ ((𝑖 = {𝑍} ∧ 𝑗 = 𝑋) → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))
46	45	a1d 25	. . . . . . . 8 ⊢ ((𝑖 = {𝑍} ∧ 𝑗 = 𝑋) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))
47	46	a1i 11	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → ((𝑖 = {𝑍} ∧ 𝑗 = 𝑋) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
48	2	rneqi 5352	. . . . . . . . . . . . . 14 ⊢ ran 𝐺 = ran (1^st ‘𝑅)
49	7, 48	eqtri 2644	. . . . . . . . . . . . 13 ⊢ 𝑋 = ran (1^st ‘𝑅)
50	49, 6, 8	rngo1cl 33738	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ RingOps → 𝑈 ∈ 𝑋)
51	50	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → 𝑈 ∈ 𝑋)
52	6, 49, 8	rngolidm 33736	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ∈ 𝑋) → (𝑈𝐻𝑈) = 𝑈)
53	50, 52	mpdan 702	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ RingOps → (𝑈𝐻𝑈) = 𝑈)
54	53	eleq1d 2686	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ RingOps → ((𝑈𝐻𝑈) ∈ {𝑍} ↔ 𝑈 ∈ {𝑍}))
55		fvex 6201	. . . . . . . . . . . . . . . 16 ⊢ (GId‘𝐻) ∈ V
56	8, 55	eqeltri 2697	. . . . . . . . . . . . . . 15 ⊢ 𝑈 ∈ V
57	56	elsn 4192	. . . . . . . . . . . . . 14 ⊢ (𝑈 ∈ {𝑍} ↔ 𝑈 = 𝑍)
58	54, 57	syl6bb 276	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ RingOps → ((𝑈𝐻𝑈) ∈ {𝑍} ↔ 𝑈 = 𝑍))
59	58	necon3bbid 2831	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ RingOps → (¬ (𝑈𝐻𝑈) ∈ {𝑍} ↔ 𝑈 ≠ 𝑍))
60	59	biimpar 502	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → ¬ (𝑈𝐻𝑈) ∈ {𝑍})
61		oveq1 6657	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑈 → (𝑥𝐻𝑦) = (𝑈𝐻𝑦))
62	61	eleq1d 2686	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑈 → ((𝑥𝐻𝑦) ∈ {𝑍} ↔ (𝑈𝐻𝑦) ∈ {𝑍}))
63	62	notbid 308	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑈 → (¬ (𝑥𝐻𝑦) ∈ {𝑍} ↔ ¬ (𝑈𝐻𝑦) ∈ {𝑍}))
64		oveq2 6658	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑈 → (𝑈𝐻𝑦) = (𝑈𝐻𝑈))
65	64	eleq1d 2686	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑈 → ((𝑈𝐻𝑦) ∈ {𝑍} ↔ (𝑈𝐻𝑈) ∈ {𝑍}))
66	65	notbid 308	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑈 → (¬ (𝑈𝐻𝑦) ∈ {𝑍} ↔ ¬ (𝑈𝐻𝑈) ∈ {𝑍}))
67	63, 66	rspc2ev 3324	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ 𝑋 ∧ 𝑈 ∈ 𝑋 ∧ ¬ (𝑈𝐻𝑈) ∈ {𝑍}) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ (𝑥𝐻𝑦) ∈ {𝑍})
68	51, 51, 60, 67	syl3anc 1326	. . . . . . . . . 10 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ (𝑥𝐻𝑦) ∈ {𝑍})
69		rexnal2 3043	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ (𝑥𝐻𝑦) ∈ {𝑍} ↔ ¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) ∈ {𝑍})
70	68, 69	sylib 208	. . . . . . . . 9 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → ¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) ∈ {𝑍})
71	70	pm2.21d 118	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))
72		raleq 3138	. . . . . . . . . 10 ⊢ (𝑖 = 𝑋 → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍}))
73		raleq 3138	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑋 → (∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} ↔ ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) ∈ {𝑍}))
74	73	ralbidv 2986	. . . . . . . . . 10 ⊢ (𝑗 = 𝑋 → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) ∈ {𝑍}))
75	72, 74	sylan9bb 736	. . . . . . . . 9 ⊢ ((𝑖 = 𝑋 ∧ 𝑗 = 𝑋) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) ∈ {𝑍}))
76	75	imbi1d 331	. . . . . . . 8 ⊢ ((𝑖 = 𝑋 ∧ 𝑗 = 𝑋) → ((∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})) ↔ (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
77	71, 76	syl5ibrcom 237	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → ((𝑖 = 𝑋 ∧ 𝑗 = 𝑋) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
78	39, 44, 47, 77	ccased 988	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → (((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
79	78	3adant3 1081	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → (((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
80	34, 79	sylbid 230	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
81	80	ralrimivv 2970	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → ∀𝑖 ∈ (Idl‘𝑅)∀𝑗 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))
82	2, 6, 7	ispridl 33833	. . . 4 ⊢ (𝑅 ∈ RingOps → ({𝑍} ∈ (PrIdl‘𝑅) ↔ ({𝑍} ∈ (Idl‘𝑅) ∧ {𝑍} ≠ 𝑋 ∧ ∀𝑖 ∈ (Idl‘𝑅)∀𝑗 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))))
83	82	3ad2ant1 1082	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → ({𝑍} ∈ (PrIdl‘𝑅) ↔ ({𝑍} ∈ (Idl‘𝑅) ∧ {𝑍} ≠ 𝑋 ∧ ∀𝑖 ∈ (Idl‘𝑅)∀𝑗 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))))
84	5, 15, 81, 83	mpbir3and 1245	. 2 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → {𝑍} ∈ (PrIdl‘𝑅))
85	2, 3	isprrngo 33849	. 2 ⊢ (𝑅 ∈ PrRing ↔ (𝑅 ∈ RingOps ∧ {𝑍} ∈ (PrIdl‘𝑅)))
86	1, 84, 85	sylanbrc 698	1 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → 𝑅 ∈ PrRing)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∨ wo 383 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 ∃wrex 2913 Vcvv 3200 ∪ cun 3572 ⊆ wss 3574 {csn 4177 {cpr 4179 ran crn 5115 ‘cfv 5888 (class class class)co 6650 1^st c1st 7166 2^nd c2nd 7167 GIdcgi 27344 RingOpscrngo 33693 Idlcidl 33806 PrIdlcpridl 33807 PrRingcprrng 33845

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-1st 7168 df-2nd 7169 df-grpo 27347 df-gid 27348 df-ginv 27349 df-ablo 27399 df-ass 33642 df-exid 33644 df-mgmOLD 33648 df-sgrOLD 33660 df-mndo 33666 df-rngo 33694 df-idl 33809 df-pridl 33810 df-prrngo 33847

This theorem is referenced by: divrngpr 33852

W3C validator