Theorem smprngopr 26662

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 26635	. . . 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 26637	. . . . . . 7 |- ( R e. RingOps -> ( Z = U <-> X = { Z } ) )
10		eqcom 2438	. . . . . . 7 |- ( U = Z <-> Z = U )
11		eqcom 2438	. . . . . . 7 |- ( { Z } = X <-> X = { Z } )
12	9, 10, 11	3bitr4g 280	. . . . . 6 |- ( R e. RingOps -> ( U = Z <-> { Z } = X ) )
13	12	necon3bid 2636	. . . . 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 3821	. . . . . . . 8 |- { { Z } , X } = ( { { Z } } u. { X } )
17	16	eqeq2i 2446	. . . . . . 7 |- ( ( Idl ` R ) = { { Z } , X } <-> ( Idl ` R ) = ( { { Z } } u. { X } ) )
18		eleq2 2497	. . . . . . . . 9 |- ( ( Idl ` R ) = ( { { Z } } u. { X } ) -> ( i e. ( Idl ` R ) <-> i e. ( { { Z } } u. { X } ) ) )
19		eleq2 2497	. . . . . . . . 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 3488	. . . . . . . . . 10 |- ( i e. ( { { Z } } u. { X } ) <-> ( i e. { { Z } } \/ i e. { X } ) )
22		elsn 3829	. . . . . . . . . . 11 |- ( i e. { { Z } } <-> i = { Z } )
23		elsn 3829	. . . . . . . . . . 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 3488	. . . . . . . . . 10 |- ( j e. ( { { Z } } u. { X } ) <-> ( j e. { { Z } } \/ j e. { X } ) )
27		elsn 3829	. . . . . . . . . . 11 |- ( j e. { { Z } } <-> j = { Z } )
28		elsn 3829	. . . . . . . . . . 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 3400	. . . . . . . . . . 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 3400	. . . . . . . . . . 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 5096	. . . . . . . . . . . . . 14 |- ran G = ran ( 1st ` R )
49	7, 48	eqtri 2456	. . . . . . . . . . . . 13 |- X = ran ( 1st ` R )
50	49, 6, 8	rngo1cl 22017	. . . . . . . . . . . 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 22012	. . . . . . . . . . . . . . . 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 2502	. . . . . . . . . . . . . 14 |- ( R e. RingOps -> ( ( U H U ) e. { Z } <-> U e. { Z } ) )
55		fvex 5742	. . . . . . . . . . . . . . . 16 |- (GId ` H ) e. _V
56	8, 55	eqeltri 2506	. . . . . . . . . . . . . . 15 |- U e. _V
57	56	elsnc 3837	. . . . . . . . . . . . . 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 2635	. . . . . . . . . . . 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 6088	. . . . . . . . . . . . . 14 |- ( x = U -> ( x H y ) = ( U H y ) )
62	61	eleq1d 2502	. . . . . . . . . . . . 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 6089	. . . . . . . . . . . . . 14 |- ( y = U -> ( U H y ) = ( U H U ) )
65	64	eleq1d 2502	. . . . . . . . . . . . 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 3060	. . . . . . . . . . 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 2716	. . . . . . . . . . . 12 |- ( E. y e. X -. ( x H y ) e. { Z } <-> -. A. y e. X ( x H y ) e. { Z } )
70	69	rexbii 2730	. . . . . . . . . . 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 2716	. . . . . . . . . . 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 2904	. . . . . . . . . 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 2904	. . . . . . . . . . 11 |- ( j = X -> ( A. y e. j ( x H y ) e. { Z } <-> A. y e. X ( x H y ) e. { Z } ) )
77	76	ralbidv 2725	. . . . . . . . . 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 2797	. . 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 26644	. . . 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 26660	. 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 1652   e. wcel 1725   =/= wne 2599   A.wral 2705   E.wrex 2706   _Vcvv 2956   u. cun 3318   C_ wss 3320   {csn 3814   {cpr 3815   ran crn 4879   ` cfv 5454  (class class class)co 6081   1stc1st 6347   2ndc2nd 6348  GIdcgi 21775   RingOpscrngo 21963   Idlcidl 26617   PrIdlcpridl 26618   PrRingcprrng 26656

This theorem is referenced by:  divrngpr  26663

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-rep 4320  ax-sep 4330  ax-nul 4338  ax-pow 4377  ax-pr 4403  ax-un 4701

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2958  df-sbc 3162  df-csb 3252  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-pw 3801  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-iun 4095  df-br 4213  df-opab 4267  df-mpt 4268  df-id 4498  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-rn 4889  df-res 4890  df-ima 4891  df-iota 5418  df-fun 5456  df-fn 5457  df-f 5458  df-f1 5459  df-fo 5460  df-f1o 5461  df-fv 5462  df-ov 6084  df-1st 6349  df-2nd 6350  df-riota 6549  df-grpo 21779  df-gid 21780  df-ginv 21781  df-ablo 21870  df-ass 21901  df-exid 21903  df-mgm 21907  df-sgr 21919  df-mndo 21926  df-rngo 21964  df-idl 26620  df-pridl 26621  df-prrngo 26658