Metamath Proof Explorer

Theorem smprngopr

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

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

Proof

Step Hyp Ref Expression
1 smprngpr.1 
 |-  G = ( 1st ` R )
2 smprngpr.2 
 |-  H = ( 2nd ` R )
3 smprngpr.3 
 |-  X = ran G
4 smprngpr.4 
 |-  Z = ( GId ` G )
5 smprngpr.5 
 |-  U = ( GId ` H )
6 simp1 
 |-  ( ( R e. RingOps /\ U =/= Z /\ ( Idl ` R ) = { { Z } , X } ) -> R e. RingOps )
7 1 4 0idl 
 |-  ( R e. RingOps -> { Z } e. ( Idl ` R ) )
8 7 3ad2ant1 
 |-  ( ( R e. RingOps /\ U =/= Z /\ ( Idl ` R ) = { { Z } , X } ) -> { Z } e. ( Idl ` R ) )
9 1 2 3 4 5 0rngo 
 |-  ( R e. RingOps -> ( Z = U <-> X = { Z } ) )
10 eqcom 
 |-  ( U = Z <-> Z = U )
11 eqcom 
 |-  ( { Z } = X <-> X = { Z } )
12 9 10 11 3bitr4g 
 |-  ( R e. RingOps -> ( U = Z <-> { Z } = X ) )
13 12 necon3bid 
 |-  ( R e. RingOps -> ( U =/= Z <-> { Z } =/= X ) )
14 13 biimpa 
 |-  ( ( R e. RingOps /\ U =/= Z ) -> { Z } =/= X )
15 14 3adant3 
 |-  ( ( R e. RingOps /\ U =/= Z /\ ( Idl ` R ) = { { Z } , X } ) -> { Z } =/= X )
16 df-pr 
 |-  { { Z } , X } = ( { { Z } } u. { X } )
17 16 eqeq2i 
 |-  ( ( Idl ` R ) = { { Z } , X } <-> ( Idl ` R ) = ( { { Z } } u. { X } ) )
18 eleq2 
 |-  ( ( Idl ` R ) = ( { { Z } } u. { X } ) -> ( i e. ( Idl ` R ) <-> i e. ( { { Z } } u. { X } ) ) )
19 eleq2 
 |-  ( ( Idl ` R ) = ( { { Z } } u. { X } ) -> ( j e. ( Idl ` R ) <-> j e. ( { { Z } } u. { X } ) ) )
20 18 19 anbi12d 
 |-  ( ( 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 
 |-  ( i e. ( { { Z } } u. { X } ) <-> ( i e. { { Z } } \/ i e. { X } ) )
22 velsn 
 |-  ( i e. { { Z } } <-> i = { Z } )
23 velsn 
 |-  ( i e. { X } <-> i = X )
24 22 23 orbi12i 
 |-  ( ( i e. { { Z } } \/ i e. { X } ) <-> ( i = { Z } \/ i = X ) )
25 21 24 bitri 
 |-  ( i e. ( { { Z } } u. { X } ) <-> ( i = { Z } \/ i = X ) )
26 elun 
 |-  ( j e. ( { { Z } } u. { X } ) <-> ( j e. { { Z } } \/ j e. { X } ) )
27 velsn 
 |-  ( j e. { { Z } } <-> j = { Z } )
28 velsn 
 |-  ( j e. { X } <-> j = X )
29 27 28 orbi12i 
 |-  ( ( j e. { { Z } } \/ j e. { X } ) <-> ( j = { Z } \/ j = X ) )
30 26 29 bitri 
 |-  ( j e. ( { { Z } } u. { X } ) <-> ( j = { Z } \/ j = X ) )
31 25 30 anbi12i 
 |-  ( ( i e. ( { { Z } } u. { X } ) /\ j e. ( { { Z } } u. { X } ) ) <-> ( ( i = { Z } \/ i = X ) /\ ( j = { Z } \/ j = X ) ) )
32 20 31 bitrdi 
 |-  ( ( 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 
 |-  ( ( Idl ` R ) = { { Z } , X } -> ( ( i e. ( Idl ` R ) /\ j e. ( Idl ` R ) ) <-> ( ( i = { Z } \/ i = X ) /\ ( j = { Z } \/ j = X ) ) ) )
34 33 3ad2ant3 
 |-  ( ( 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 
 |-  ( i = { Z } -> i C_ { Z } )
36 35 orcd 
 |-  ( i = { Z } -> ( i C_ { Z } \/ j C_ { Z } ) )
37 36 adantr 
 |-  ( ( i = { Z } /\ j = { Z } ) -> ( i C_ { Z } \/ j C_ { Z } ) )
38 37 a1d 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( j = { Z } -> j C_ { Z } )
41 40 olcd 
 |-  ( j = { Z } -> ( i C_ { Z } \/ j C_ { Z } ) )
42 41 adantl 
 |-  ( ( i = X /\ j = { Z } ) -> ( i C_ { Z } \/ j C_ { Z } ) )
43 42 a1d 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( ( i = { Z } /\ j = X ) -> ( i C_ { Z } \/ j C_ { Z } ) )
46 45 a1d 
 |-  ( ( 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 
 |-  ( ( 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 1 rneqi 
 |-  ran G = ran ( 1st ` R )
49 3 48 eqtri 
 |-  X = ran ( 1st ` R )
50 49 2 5 rngo1cl 
 |-  ( R e. RingOps -> U e. X )
51 50 adantr 
 |-  ( ( R e. RingOps /\ U =/= Z ) -> U e. X )
52 2 49 5 rngolidm 
 |-  ( ( R e. RingOps /\ U e. X ) -> ( U H U ) = U )
53 50 52 mpdan 
 |-  ( R e. RingOps -> ( U H U ) = U )
54 53 eleq1d 
 |-  ( R e. RingOps -> ( ( U H U ) e. { Z } <-> U e. { Z } ) )
55 5 fvexi 
 |-  U e. _V
56 55 elsn 
 |-  ( U e. { Z } <-> U = Z )
57 54 56 bitrdi 
 |-  ( R e. RingOps -> ( ( U H U ) e. { Z } <-> U = Z ) )
58 57 necon3bbid 
 |-  ( R e. RingOps -> ( -. ( U H U ) e. { Z } <-> U =/= Z ) )
59 58 biimpar 
 |-  ( ( R e. RingOps /\ U =/= Z ) -> -. ( U H U ) e. { Z } )
60 oveq1 
 |-  ( x = U -> ( x H y ) = ( U H y ) )
61 60 eleq1d 
 |-  ( x = U -> ( ( x H y ) e. { Z } <-> ( U H y ) e. { Z } ) )
62 61 notbid 
 |-  ( x = U -> ( -. ( x H y ) e. { Z } <-> -. ( U H y ) e. { Z } ) )
63 oveq2 
 |-  ( y = U -> ( U H y ) = ( U H U ) )
64 63 eleq1d 
 |-  ( y = U -> ( ( U H y ) e. { Z } <-> ( U H U ) e. { Z } ) )
65 64 notbid 
 |-  ( y = U -> ( -. ( U H y ) e. { Z } <-> -. ( U H U ) e. { Z } ) )
66 62 65 rspc2ev 
 |-  ( ( U e. X /\ U e. X /\ -. ( U H U ) e. { Z } ) -> E. x e. X E. y e. X -. ( x H y ) e. { Z } )
67 51 51 59 66 syl3anc 
 |-  ( ( R e. RingOps /\ U =/= Z ) -> E. x e. X E. y e. X -. ( x H y ) e. { Z } )
68 rexnal2 
 |-  ( 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 } )
69 67 68 sylib 
 |-  ( ( R e. RingOps /\ U =/= Z ) -> -. A. x e. X A. y e. X ( x H y ) e. { Z } )
70 69 pm2.21d 
 |-  ( ( R e. RingOps /\ U =/= Z ) -> ( A. x e. X A. y e. X ( x H y ) e. { Z } -> ( i C_ { Z } \/ j C_ { Z } ) ) )
71 raleq 
 |-  ( 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 } ) )
72 raleq 
 |-  ( j = X -> ( A. y e. j ( x H y ) e. { Z } <-> A. y e. X ( x H y ) e. { Z } ) )
73 72 ralbidv 
 |-  ( 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 } ) )
74 71 73 sylan9bb 
 |-  ( ( 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 } ) )
75 74 imbi1d 
 |-  ( ( 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 } ) ) ) )
76 70 75 syl5ibrcom 
 |-  ( ( 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 } ) ) ) )
77 39 44 47 76 ccased 
 |-  ( ( 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 } ) ) ) )
78 77 3adant3 
 |-  ( ( 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 } ) ) ) )
79 34 78 sylbid 
 |-  ( ( 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 } ) ) ) )
80 79 ralrimivv 
 |-  ( ( 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 } ) ) )
81 1 2 3 ispridl 
 |-  ( 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 } ) ) ) ) )
82 81 3ad2ant1 
 |-  ( ( 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 } ) ) ) ) )
83 8 15 80 82 mpbir3and 
 |-  ( ( R e. RingOps /\ U =/= Z /\ ( Idl ` R ) = { { Z } , X } ) -> { Z } e. ( PrIdl ` R ) )
84 1 4 isprrngo 
 |-  ( R e. PrRing <-> ( R e. RingOps /\ { Z } e. ( PrIdl ` R ) ) )
85 6 83 84 sylanbrc 
 |-  ( ( R e. RingOps /\ U =/= Z /\ ( Idl ` R ) = { { Z } , X } ) -> R e. PrRing )