Theorem smprngopr 26560

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

Hypotheses

Ref	Expression
smprngpr.1	|- G = ( 1st ` R )
smprngpr.2	|- H = ( 2nd ` R )
smprngpr.3	|- X = ran G
smprngpr.4	|- Z = (GId ` G )
smprngpr.5	|- U = (GId ` H )

Assertion

Ref	Expression
smprngopr	|- ( ( R e. RingOps /\ U =/= Z /\ ( Idl ` R ) = { { Z } , X } ) -> R e. PrRing )

Proof of Theorem smprngopr

Dummy variables i j x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp1 957	. 2 |- ( ( R e. RingOps /\ U =/= Z /\ ( Idl ` R ) = { { Z } , X } ) -> R e. RingOps )
2		smprngpr.1	. . . . 5 |- G = ( 1st ` R )
3		smprngpr.4	. . . . 5 |- Z = (GId ` G )
4	2, 3	0idl 26533	. . . 4 |- ( R e. RingOps -> { Z } e. ( Idl ` R ) )
5	4	3ad2ant1 978	. . 3 |- ( ( R e. RingOps /\ U =/= Z /\ ( Idl ` R ) = { { Z } , X } ) -> { Z } e. ( Idl ` R ) )
6		smprngpr.2	. . . . . . . 8 |- H = ( 2nd ` R )
7		smprngpr.3	. . . . . . . 8 |- X = ran G
8		smprngpr.5	. . . . . . . 8 |- U = (GId ` H )
9	2, 6, 7, 3, 8	0rngo 26535	. . . . . . 7 |- ( R e. RingOps -> ( Z = U <-> X = { Z } ) )
10		eqcom 2414	. . . . . . 7 |- ( U = Z <-> Z = U )
11		eqcom 2414	. . . . . . 7 |- ( { Z } = X <-> X = { Z } )
12	9, 10, 11	3bitr4g 280	. . . . . 6 |- ( R e. RingOps -> ( U = Z <-> { Z } = X ) )
13	12	necon3bid 2610	. . . . 5 |- ( R e. RingOps -> ( U =/= Z <-> { Z } =/= X ) )
14	13	biimpa 471	. . . 4 |- ( ( R e. RingOps /\ U =/= Z ) -> { Z } =/= X )
15	14	3adant3 977	. . 3 |- ( ( R e. RingOps /\ U =/= Z /\ ( Idl ` R ) = { { Z } , X } ) -> { Z } =/= X )
16		df-pr 3789	. . . . . . . 8 |- { { Z } , X } = ( { { Z } } u. { X } )
17	16	eqeq2i 2422	. . . . . . 7 |- ( ( Idl ` R ) = { { Z } , X } <-> ( Idl ` R ) = ( { { Z } } u. { X } ) )
18		eleq2 2473	. . . . . . . . 9 |- ( ( Idl ` R ) = ( { { Z } } u. { X } ) -> ( i e. ( Idl ` R ) <-> i e. ( { { Z } } u. { X } ) ) )
19		eleq2 2473	. . . . . . . . 9 |- ( ( Idl ` R ) = ( { { Z } } u. { X } ) -> ( j e. ( Idl ` R ) <-> j e. ( { { Z } } u. { X } ) ) )
20	18, 19	anbi12d 692	. . . . . . . 8 |- ( ( Idl ` R ) = ( { { Z } } u. { X } ) -> ( ( i e. ( Idl ` R ) /\ j e. ( Idl ` R ) ) <-> ( i e. ( { { Z } } u. { X } ) /\ j e. ( { { Z } } u. { X } ) ) ) )
21		elun 3456	. . . . . . . . . 10 |- ( i e. ( { { Z } } u. { X } ) <-> ( i e. { { Z } } \/ i e. { X } ) )
22		elsn 3797	. . . . . . . . . . 11 |- ( i e. { { Z } } <-> i = { Z } )
23		elsn 3797	. . . . . . . . . . 11 |- ( i e. { X } <-> i = X )
24	22, 23	orbi12i 508	. . . . . . . . . 10 |- ( ( i e. { { Z } } \/ i e. { X } ) <-> ( i = { Z } \/ i = X ) )
25	21, 24	bitri 241	. . . . . . . . 9 |- ( i e. ( { { Z } } u. { X } ) <-> ( i = { Z } \/ i = X ) )
26		elun 3456	. . . . . . . . . 10 |- ( j e. ( { { Z } } u. { X } ) <-> ( j e. { { Z } } \/ j e. { X } ) )
27		elsn 3797	. . . . . . . . . . 11 |- ( j e. { { Z } } <-> j = { Z } )
28		elsn 3797	. . . . . . . . . . 11 |- ( j e. { X } <-> j = X )
29	27, 28	orbi12i 508	. . . . . . . . . 10 |- ( ( j e. { { Z } } \/ j e. { X } ) <-> ( j = { Z } \/ j = X ) )
30	26, 29	bitri 241	. . . . . . . . 9 |- ( j e. ( { { Z } } u. { X } ) <-> ( j = { Z } \/ j = X ) )
31	25, 30	anbi12i 679	. . . . . . . 8 |- ( ( i e. ( { { Z } } u. { X } ) /\ j e. ( { { Z } } u. { X } ) ) <-> ( ( i = { Z } \/ i = X ) /\ ( j = { Z } \/ j = X ) ) )
32	20, 31	syl6bb 253	. . . . . . 7 |- ( ( Idl ` R ) = ( { { Z } } u. { X } ) -> ( ( i e. ( Idl ` R ) /\ j e. ( Idl ` R ) ) <-> ( ( i = { Z } \/ i = X ) /\ ( j = { Z } \/ j = X ) ) ) )
33	17, 32	sylbi 188	. . . . . 6 |- ( ( Idl ` R ) = { { Z } , X } -> ( ( i e. ( Idl ` R ) /\ j e. ( Idl ` R ) ) <-> ( ( i = { Z } \/ i = X ) /\ ( j = { Z } \/ j = X ) ) ) )
34	33	3ad2ant3 980	. . . . 5 |- ( ( R e. RingOps /\ U =/= Z /\ ( Idl ` R ) = { { Z } , X } ) -> ( ( i e. ( Idl ` R ) /\ j e. ( Idl ` R ) ) <-> ( ( i = { Z } \/ i = X ) /\ ( j = { Z } \/ j = X ) ) ) )
35		eqimss 3368	. . . . . . . . . . 11 |- ( i = { Z } -> i C_ { Z } )
36	35	orcd 382	. . . . . . . . . 10 |- ( i = { Z } -> ( i C_ { Z } \/ j C_ { Z } ) )
37	36	adantr 452	. . . . . . . . 9 |- ( ( i = { Z } /\ j = { Z } ) -> ( i C_ { Z } \/ j C_ { Z } ) )
38	37	a1d 23	. . . . . . . 8 |- ( ( i = { Z } /\ j = { Z } ) -> ( A. x e. i A. y e. j ( x H y ) e. { Z } -> ( i C_ { Z } \/ j C_ { Z } ) ) )
39	38	a1i 11	. . . . . . 7 |- ( ( R e. RingOps /\ U =/= Z ) -> ( ( i = { Z } /\ j = { Z } ) -> ( A. x e. i A. y e. j ( x H y ) e. { Z } -> ( i C_ { Z } \/ j C_ { Z } ) ) ) )
40		eqimss 3368	. . . . . . . . . . 11 |- ( j = { Z } -> j C_ { Z } )
41	40	olcd 383	. . . . . . . . . 10 |- ( j = { Z } -> ( i C_ { Z } \/ j C_ { Z } ) )
42	41	adantl 453	. . . . . . . . 9 |- ( ( i = X /\ j = { Z } ) -> ( i C_ { Z } \/ j C_ { Z } ) )
43	42	a1d 23	. . . . . . . 8 |- ( ( i = X /\ j = { Z } ) -> ( A. x e. i A. y e. j ( x H y ) e. { Z } -> ( i C_ { Z } \/ j C_ { Z } ) ) )
44	43	a1i 11	. . . . . . 7 |- ( ( R e. RingOps /\ U =/= Z ) -> ( ( i = X /\ j = { Z } ) -> ( A. x e. i A. y e. j ( x H y ) e. { Z } -> ( i C_ { Z } \/ j C_ { Z } ) ) ) )
45	36	adantr 452	. . . . . . . . 9 |- ( ( i = { Z } /\ j = X ) -> ( i C_ { Z } \/ j C_ { Z } ) )
46	45	a1d 23	. . . . . . . 8 |- ( ( i = { Z } /\ j = X ) -> ( A. x e. i A. y e. j ( x H y ) e. { Z } -> ( i C_ { Z } \/ j C_ { Z } ) ) )
47	46	a1i 11	. . . . . . 7 |- ( ( R e. RingOps /\ U =/= Z ) -> ( ( i = { Z } /\ j = X ) -> ( A. x e. i A. y e. j ( x H y ) e. { Z } -> ( i C_ { Z } \/ j C_ { Z } ) ) ) )
48	2	rneqi 5063	. . . . . . . . . . . . . 14 |- ran G = ran ( 1st ` R )
49	7, 48	eqtri 2432	. . . . . . . . . . . . 13 |- X = ran ( 1st ` R )
50	49, 6, 8	rngo1cl 21978	. . . . . . . . . . . 12 |- ( R e. RingOps -> U e. X )
51	50	adantr 452	. . . . . . . . . . 11 |- ( ( R e. RingOps /\ U =/= Z ) -> U e. X )
52	6, 49, 8	rngolidm 21973	. . . . . . . . . . . . . . . 16 |- ( ( R e. RingOps /\ U e. X ) -> ( U H U ) = U )
53	50, 52	mpdan 650	. . . . . . . . . . . . . . 15 |- ( R e. RingOps -> ( U H U ) = U )
54	53	eleq1d 2478	. . . . . . . . . . . . . 14 |- ( R e. RingOps -> ( ( U H U ) e. { Z } <-> U e. { Z } ) )
55		fvex 5709	. . . . . . . . . . . . . . . 16 |- (GId ` H ) e. _V
56	8, 55	eqeltri 2482	. . . . . . . . . . . . . . 15 |- U e. _V
57	56	elsnc 3805	. . . . . . . . . . . . . 14 |- ( U e. { Z } <-> U = Z )
58	54, 57	syl6bb 253	. . . . . . . . . . . . 13 |- ( R e. RingOps -> ( ( U H U ) e. { Z } <-> U = Z ) )
59	58	necon3bbid 2609	. . . . . . . . . . . 12 |- ( R e. RingOps -> ( -. ( U H U ) e. { Z } <-> U =/= Z ) )
60	59	biimpar 472	. . . . . . . . . . 11 |- ( ( R e. RingOps /\ U =/= Z ) -> -. ( U H U ) e. { Z } )
61		oveq1 6055	. . . . . . . . . . . . . 14 |- ( x = U -> ( x H y ) = ( U H y ) )
62	61	eleq1d 2478	. . . . . . . . . . . . 13 |- ( x = U -> ( ( x H y ) e. { Z } <-> ( U H y ) e. { Z } ) )
63	62	notbid 286	. . . . . . . . . . . 12 |- ( x = U -> ( -. ( x H y ) e. { Z } <-> -. ( U H y ) e. { Z } ) )
64		oveq2 6056	. . . . . . . . . . . . . 14 |- ( y = U -> ( U H y ) = ( U H U ) )
65	64	eleq1d 2478	. . . . . . . . . . . . 13 |- ( y = U -> ( ( U H y ) e. { Z } <-> ( U H U ) e. { Z } ) )
66	65	notbid 286	. . . . . . . . . . . 12 |- ( y = U -> ( -. ( U H y ) e. { Z } <-> -. ( U H U ) e. { Z } ) )
67	63, 66	rspc2ev 3028	. . . . . . . . . . 11 |- ( ( U e. X /\ U e. X /\ -. ( U H U ) e. { Z } ) -> E. x e. X E. y e. X -. ( x H y ) e. { Z } )
68	51, 51, 60, 67	syl3anc 1184	. . . . . . . . . 10 |- ( ( R e. RingOps /\ U =/= Z ) -> E. x e. X E. y e. X -. ( x H y ) e. { Z } )
69		rexnal 2685	. . . . . . . . . . . 12 |- ( E. y e. X -. ( x H y ) e. { Z } <-> -. A. y e. X ( x H y ) e. { Z } )
70	69	rexbii 2699	. . . . . . . . . . 11 |- ( E. x e. X E. y e. X -. ( x H y ) e. { Z } <-> E. x e. X -. A. y e. X ( x H y ) e. { Z } )
71		rexnal 2685	. . . . . . . . . . 11 |- ( E. x e. X -. A. y e. X ( x H y ) e. { Z } <-> -. A. x e. X A. y e. X ( x H y ) e. { Z } )
72	70, 71	bitri 241	. . . . . . . . . 10 |- ( E. x e. X E. y e. X -. ( x H y ) e. { Z } <-> -. A. x e. X A. y e. X ( x H y ) e. { Z } )
73	68, 72	sylib 189	. . . . . . . . 9 |- ( ( R e. RingOps /\ U =/= Z ) -> -. A. x e. X A. y e. X ( x H y ) e. { Z } )
74	73	pm2.21d 100	. . . . . . . 8 |- ( ( R e. RingOps /\ U =/= Z ) -> ( A. x e. X A. y e. X ( x H y ) e. { Z } -> ( i C_ { Z } \/ j C_ { Z } ) ) )
75		raleq 2872	. . . . . . . . . 10 |- ( i = X -> ( A. x e. i A. y e. j ( x H y ) e. { Z } <-> A. x e. X A. y e. j ( x H y ) e. { Z } ) )
76		raleq 2872	. . . . . . . . . . 11 |- ( j = X -> ( A. y e. j ( x H y ) e. { Z } <-> A. y e. X ( x H y ) e. { Z } ) )
77	76	ralbidv 2694	. . . . . . . . . 10 |- ( j = X -> ( A. x e. X A. y e. j ( x H y ) e. { Z } <-> A. x e. X A. y e. X ( x H y ) e. { Z } ) )
78	75, 77	sylan9bb 681	. . . . . . . . 9 |- ( ( i = X /\ j = X ) -> ( A. x e. i A. y e. j ( x H y ) e. { Z } <-> A. x e. X A. y e. X ( x H y ) e. { Z } ) )
79	78	imbi1d 309	. . . . . . . 8 |- ( ( i = X /\ j = X ) -> ( ( A. x e. i A. y e. j ( x H y ) e. { Z } -> ( i C_ { Z } \/ j C_ { Z } ) ) <-> ( A. x e. X A. y e. X ( x H y ) e. { Z } -> ( i C_ { Z } \/ j C_ { Z } ) ) ) )
80	74, 79	syl5ibrcom 214	. . . . . . 7 |- ( ( R e. RingOps /\ U =/= Z ) -> ( ( i = X /\ j = X ) -> ( A. x e. i A. y e. j ( x H y ) e. { Z } -> ( i C_ { Z } \/ j C_ { Z } ) ) ) )
81	39, 44, 47, 80	ccased 914	. . . . . 6 |- ( ( R e. RingOps /\ U =/= Z ) -> ( ( ( i = { Z } \/ i = X ) /\ ( j = { Z } \/ j = X ) ) -> ( A. x e. i A. y e. j ( x H y ) e. { Z } -> ( i C_ { Z } \/ j C_ { Z } ) ) ) )
82	81	3adant3 977	. . . . 5 |- ( ( R e. RingOps /\ U =/= Z /\ ( Idl ` R ) = { { Z } , X } ) -> ( ( ( i = { Z } \/ i = X ) /\ ( j = { Z } \/ j = X ) ) -> ( A. x e. i A. y e. j ( x H y ) e. { Z } -> ( i C_ { Z } \/ j C_ { Z } ) ) ) )
83	34, 82	sylbid 207	. . . 4 |- ( ( R e. RingOps /\ U =/= Z /\ ( Idl ` R ) = { { Z } , X } ) -> ( ( i e. ( Idl ` R ) /\ j e. ( Idl ` R ) ) -> ( A. x e. i A. y e. j ( x H y ) e. { Z } -> ( i C_ { Z } \/ j C_ { Z } ) ) ) )
84	83	ralrimivv 2765	. . 3 |- ( ( R e. RingOps /\ U =/= Z /\ ( Idl ` R ) = { { Z } , X } ) -> A. i e. ( Idl ` R ) A. j e. ( Idl ` R ) ( A. x e. i A. y e. j ( x H y ) e. { Z } -> ( i C_ { Z } \/ j C_ { Z } ) ) )
85	2, 6, 7	ispridl 26542	. . . 4 |- ( R e. RingOps -> ( { Z } e. ( PrIdl ` R ) <-> ( { Z } e. ( Idl ` R ) /\ { Z } =/= X /\ A. i e. ( Idl ` R ) A. j e. ( Idl ` R ) ( A. x e. i A. y e. j ( x H y ) e. { Z } -> ( i C_ { Z } \/ j C_ { Z } ) ) ) ) )
86	85	3ad2ant1 978	. . 3 |- ( ( R e. RingOps /\ U =/= Z /\ ( Idl ` R ) = { { Z } , X } ) -> ( { Z } e. ( PrIdl ` R ) <-> ( { Z } e. ( Idl ` R ) /\ { Z } =/= X /\ A. i e. ( Idl ` R ) A. j e. ( Idl ` R ) ( A. x e. i A. y e. j ( x H y ) e. { Z } -> ( i C_ { Z } \/ j C_ { Z } ) ) ) ) )
87	5, 15, 84, 86	mpbir3and 1137	. 2 |- ( ( R e. RingOps /\ U =/= Z /\ ( Idl ` R ) = { { Z } , X } ) -> { Z } e. ( PrIdl ` R ) )
88	2, 3	isprrngo 26558	. 2 |- ( R e. PrRing <-> ( R e. RingOps /\ { Z } e. ( PrIdl ` R ) ) )
89	1, 87, 88	sylanbrc 646	1 |- ( ( R e. RingOps /\ U =/= Z /\ ( Idl ` R ) = { { Z } , X } ) -> R e. PrRing )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   \/ wo 358   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   =/= wne 2575   A.wral 2674   E.wrex 2675   _Vcvv 2924   u. cun 3286   C_ wss 3288   {csn 3782   {cpr 3783   ran crn 4846   ` cfv 5421  (class class class)co 6048   1stc1st 6314   2ndc2nd 6315  GIdcgi 21736   RingOpscrngo 21924   Idlcidl 26515   PrIdlcpridl 26516   PrRingcprrng 26554

This theorem is referenced by:  divrngpr  26561

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-rep 4288  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-reu 2681  df-rmo 2682  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-iun 4063  df-br 4181  df-opab 4235  df-mpt 4236  df-id 4466  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-ov 6051  df-1st 6316  df-2nd 6317  df-riota 6516  df-grpo 21740  df-gid 21741  df-ginv 21742  df-ablo 21831  df-ass 21862  df-exid 21864  df-mgm 21868  df-sgr 21880  df-mndo 21887  df-rngo 21925  df-idl 26518  df-pridl 26519  df-prrngo 26556