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∈RingOps∧U≠Z∧Idl⁡R=ZX→R∈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∈RingOps∧U≠Z∧Idl⁡R=ZX→R∈RingOps
7 1 4 0idl ⊢R∈RingOps→Z∈Idl⁡R
8 7 3ad2ant1 ⊢R∈RingOps∧U≠Z∧Idl⁡R=ZX→Z∈Idl⁡R
9 1 2 3 4 5 0rngo ⊢R∈RingOps→Z=U↔X=Z
10 eqcom ⊢U=Z↔Z=U
11 eqcom ⊢Z=X↔X=Z
12 9 10 11 3bitr4g ⊢R∈RingOps→U=Z↔Z=X
13 12 necon3bid ⊢R∈RingOps→U≠Z↔Z≠X
14 13 biimpa ⊢R∈RingOps∧U≠Z→Z≠X
15 14 3adant3 ⊢R∈RingOps∧U≠Z∧Idl⁡R=ZX→Z≠X
16 df-pr ⊢ZX=Z∪X
17 16 eqeq2i ⊢Idl⁡R=ZX↔Idl⁡R=Z∪X
18 eleq2 ⊢Idl⁡R=Z∪X→i∈Idl⁡R↔i∈Z∪X
19 eleq2 ⊢Idl⁡R=Z∪X→j∈Idl⁡R↔j∈Z∪X
20 18 19 anbi12d ⊢Idl⁡R=Z∪X→i∈Idl⁡R∧j∈Idl⁡R↔i∈Z∪X∧j∈Z∪X
21 elun ⊢i∈Z∪X↔i∈Z∨i∈X
22 velsn ⊢i∈Z↔i=Z
23 velsn ⊢i∈X↔i=X
24 22 23 orbi12i ⊢i∈Z∨i∈X↔i=Z∨i=X
25 21 24 bitri ⊢i∈Z∪X↔i=Z∨i=X
26 elun ⊢j∈Z∪X↔j∈Z∨j∈X
27 velsn ⊢j∈Z↔j=Z
28 velsn ⊢j∈X↔j=X
29 27 28 orbi12i ⊢j∈Z∨j∈X↔j=Z∨j=X
30 26 29 bitri ⊢j∈Z∪X↔j=Z∨j=X
31 25 30 anbi12i ⊢i∈Z∪X∧j∈Z∪X↔i=Z∨i=X∧j=Z∨j=X
32 20 31 bitrdi ⊢Idl⁡R=Z∪X→i∈Idl⁡R∧j∈Idl⁡R↔i=Z∨i=X∧j=Z∨j=X
33 17 32 sylbi ⊢Idl⁡R=ZX→i∈Idl⁡R∧j∈Idl⁡R↔i=Z∨i=X∧j=Z∨j=X
34 33 3ad2ant3 ⊢R∈RingOps∧U≠Z∧Idl⁡R=ZX→i∈Idl⁡R∧j∈Idl⁡R↔i=Z∨i=X∧j=Z∨j=X
35 eqimss ⊢i=Z→i⊆Z
36 35 orcd ⊢i=Z→i⊆Z∨j⊆Z
37 36 adantr ⊢i=Z∧j=Z→i⊆Z∨j⊆Z
38 37 a1d ⊢i=Z∧j=Z→∀x∈i∀y∈jxHy∈Z→i⊆Z∨j⊆Z
39 38 a1i ⊢R∈RingOps∧U≠Z→i=Z∧j=Z→∀x∈i∀y∈jxHy∈Z→i⊆Z∨j⊆Z
40 eqimss ⊢j=Z→j⊆Z
41 40 olcd ⊢j=Z→i⊆Z∨j⊆Z
42 41 adantl ⊢i=X∧j=Z→i⊆Z∨j⊆Z
43 42 a1d ⊢i=X∧j=Z→∀x∈i∀y∈jxHy∈Z→i⊆Z∨j⊆Z
44 43 a1i ⊢R∈RingOps∧U≠Z→i=X∧j=Z→∀x∈i∀y∈jxHy∈Z→i⊆Z∨j⊆Z
45 36 adantr ⊢i=Z∧j=X→i⊆Z∨j⊆Z
46 45 a1d ⊢i=Z∧j=X→∀x∈i∀y∈jxHy∈Z→i⊆Z∨j⊆Z
47 46 a1i ⊢R∈RingOps∧U≠Z→i=Z∧j=X→∀x∈i∀y∈jxHy∈Z→i⊆Z∨j⊆Z
48 1 rneqi ⊢ran⁡G=ran⁡1st⁡R
49 3 48 eqtri ⊢X=ran⁡1st⁡R
50 49 2 5 rngo1cl ⊢R∈RingOps→U∈X
51 50 adantr ⊢R∈RingOps∧U≠Z→U∈X
52 2 49 5 rngolidm ⊢R∈RingOps∧U∈X→UHU=U
53 50 52 mpdan ⊢R∈RingOps→UHU=U
54 53 eleq1d ⊢R∈RingOps→UHU∈Z↔U∈Z
55 5 fvexi ⊢U∈V
56 55 elsn ⊢U∈Z↔U=Z
57 54 56 bitrdi ⊢R∈RingOps→UHU∈Z↔U=Z
58 57 necon3bbid ⊢R∈RingOps→¬UHU∈Z↔U≠Z
59 58 biimpar ⊢R∈RingOps∧U≠Z→¬UHU∈Z
60 oveq1 ⊢x=U→xHy=UHy
61 60 eleq1d ⊢x=U→xHy∈Z↔UHy∈Z
62 61 notbid ⊢x=U→¬xHy∈Z↔¬UHy∈Z
63 oveq2 ⊢y=U→UHy=UHU
64 63 eleq1d ⊢y=U→UHy∈Z↔UHU∈Z
65 64 notbid ⊢y=U→¬UHy∈Z↔¬UHU∈Z
66 62 65 rspc2ev ⊢U∈X∧U∈X∧¬UHU∈Z→∃x∈X∃y∈X¬xHy∈Z
67 51 51 59 66 syl3anc ⊢R∈RingOps∧U≠Z→∃x∈X∃y∈X¬xHy∈Z
68 rexnal2 ⊢∃x∈X∃y∈X¬xHy∈Z↔¬∀x∈X∀y∈XxHy∈Z
69 67 68 sylib ⊢R∈RingOps∧U≠Z→¬∀x∈X∀y∈XxHy∈Z
70 69 pm2.21d ⊢R∈RingOps∧U≠Z→∀x∈X∀y∈XxHy∈Z→i⊆Z∨j⊆Z
71 raleq ⊢i=X→∀x∈i∀y∈jxHy∈Z↔∀x∈X∀y∈jxHy∈Z
72 raleq ⊢j=X→∀y∈jxHy∈Z↔∀y∈XxHy∈Z
73 72 ralbidv ⊢j=X→∀x∈X∀y∈jxHy∈Z↔∀x∈X∀y∈XxHy∈Z
74 71 73 sylan9bb ⊢i=X∧j=X→∀x∈i∀y∈jxHy∈Z↔∀x∈X∀y∈XxHy∈Z
75 74 imbi1d ⊢i=X∧j=X→∀x∈i∀y∈jxHy∈Z→i⊆Z∨j⊆Z↔∀x∈X∀y∈XxHy∈Z→i⊆Z∨j⊆Z
76 70 75 syl5ibrcom ⊢R∈RingOps∧U≠Z→i=X∧j=X→∀x∈i∀y∈jxHy∈Z→i⊆Z∨j⊆Z
77 39 44 47 76 ccased ⊢R∈RingOps∧U≠Z→i=Z∨i=X∧j=Z∨j=X→∀x∈i∀y∈jxHy∈Z→i⊆Z∨j⊆Z
78 77 3adant3 ⊢R∈RingOps∧U≠Z∧Idl⁡R=ZX→i=Z∨i=X∧j=Z∨j=X→∀x∈i∀y∈jxHy∈Z→i⊆Z∨j⊆Z
79 34 78 sylbid ⊢R∈RingOps∧U≠Z∧Idl⁡R=ZX→i∈Idl⁡R∧j∈Idl⁡R→∀x∈i∀y∈jxHy∈Z→i⊆Z∨j⊆Z
80 79 ralrimivv ⊢R∈RingOps∧U≠Z∧Idl⁡R=ZX→∀i∈Idl⁡R∀j∈Idl⁡R∀x∈i∀y∈jxHy∈Z→i⊆Z∨j⊆Z
81 1 2 3 ispridl ⊢R∈RingOps→Z∈PrIdl⁡R↔Z∈Idl⁡R∧Z≠X∧∀i∈Idl⁡R∀j∈Idl⁡R∀x∈i∀y∈jxHy∈Z→i⊆Z∨j⊆Z
82 81 3ad2ant1 ⊢R∈RingOps∧U≠Z∧Idl⁡R=ZX→Z∈PrIdl⁡R↔Z∈Idl⁡R∧Z≠X∧∀i∈Idl⁡R∀j∈Idl⁡R∀x∈i∀y∈jxHy∈Z→i⊆Z∨j⊆Z
83 8 15 80 82 mpbir3and ⊢R∈RingOps∧U≠Z∧Idl⁡R=ZX→Z∈PrIdl⁡R
84 1 4 isprrngo ⊢R∈PrRing↔R∈RingOps∧Z∈PrIdl⁡R
85 6 83 84 sylanbrc ⊢R∈RingOps∧U≠Z∧Idl⁡R=ZX→R∈PrRing