Metamath Proof Explorer

Theorem 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 
|- .0. = ( 0g ` R )
smprngprmrng.u 
|- U = ( LIdeal ` R )
Assertion smprngprmrng 
|- ( ( R e. NzRing /\ U = { { .0. } , B } ) -> R e. PrmRing )

Proof

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