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 = 1 st ⁡ R
smprngpr.2 ⊢ H = 2 nd ⁡ R
smprngpr.3 ⊢ X = ran ⁡ G
smprngpr.4 ⊢ Z = GId ⁡ G
smprngpr.5 ⊢ U = GId ⁡ H
Assertion smprngopr ⊢ R ∈ RingOps ∧ U ≠ Z ∧ Idl ⁡ R = Z X → R ∈ PrRing

Proof

Step Hyp Ref Expression
1 smprngpr.1 ⊢ G = 1 st ⁡ R
2 smprngpr.2 ⊢ H = 2 nd ⁡ 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 = Z X → R ∈ RingOps
7 1 4 0idl ⊢ R ∈ RingOps → Z ∈ Idl ⁡ R
8 7 3ad2ant1 ⊢ R ∈ RingOps ∧ U ≠ Z ∧ Idl ⁡ R = Z X → 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 = Z X → Z ≠ X
16 df-pr ⊢ Z X = Z ∪ X
17 16 eqeq2i ⊢ Idl ⁡ R = Z X ↔ 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 = Z X → i ∈ Idl ⁡ R ∧ j ∈ Idl ⁡ R ↔ i = Z ∨ i = X ∧ j = Z ∨ j = X
34 33 3ad2ant3 ⊢ R ∈ RingOps ∧ U ≠ Z ∧ Idl ⁡ R = Z X → 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 ∈ j x H y ∈ Z → i ⊆ Z ∨ j ⊆ Z
39 38 a1i ⊢ R ∈ RingOps ∧ U ≠ Z → i = Z ∧ j = Z → ∀ x ∈ i ∀ y ∈ j x H y ∈ 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 ∈ j x H y ∈ Z → i ⊆ Z ∨ j ⊆ Z
44 43 a1i ⊢ R ∈ RingOps ∧ U ≠ Z → i = X ∧ j = Z → ∀ x ∈ i ∀ y ∈ j x H y ∈ 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 ∈ j x H y ∈ Z → i ⊆ Z ∨ j ⊆ Z
47 46 a1i ⊢ R ∈ RingOps ∧ U ≠ Z → i = Z ∧ j = X → ∀ x ∈ i ∀ y ∈ j x H y ∈ Z → i ⊆ Z ∨ j ⊆ Z
48 1 rneqi ⊢ ran ⁡ G = ran ⁡ 1 st ⁡ R
49 3 48 eqtri ⊢ X = ran ⁡ 1 st ⁡ 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 → U H U = U
53 50 52 mpdan ⊢ R ∈ RingOps → U H U = U
54 53 eleq1d ⊢ R ∈ RingOps → U H U ∈ Z ↔ U ∈ Z
55 5 fvexi ⊢ U ∈ V
56 55 elsn ⊢ U ∈ Z ↔ U = Z
57 54 56 bitrdi ⊢ R ∈ RingOps → U H U ∈ Z ↔ U = Z
58 57 necon3bbid ⊢ R ∈ RingOps → ¬ U H U ∈ Z ↔ U ≠ Z
59 58 biimpar ⊢ R ∈ RingOps ∧ U ≠ Z → ¬ U H U ∈ Z
60 oveq1 ⊢ x = U → x H y = U H y
61 60 eleq1d ⊢ x = U → x H y ∈ Z ↔ U H y ∈ Z
62 61 notbid ⊢ x = U → ¬ x H y ∈ Z ↔ ¬ U H y ∈ Z
63 oveq2 ⊢ y = U → U H y = U H U
64 63 eleq1d ⊢ y = U → U H y ∈ Z ↔ U H U ∈ Z
65 64 notbid ⊢ y = U → ¬ U H y ∈ Z ↔ ¬ U H U ∈ Z
66 62 65 rspc2ev ⊢ U ∈ X ∧ U ∈ X ∧ ¬ U H U ∈ Z → ∃ x ∈ X ∃ y ∈ X ¬ x H y ∈ Z
67 51 51 59 66 syl3anc ⊢ R ∈ RingOps ∧ U ≠ Z → ∃ x ∈ X ∃ y ∈ X ¬ x H y ∈ Z
68 rexnal2 ⊢ ∃ x ∈ X ∃ y ∈ X ¬ x H y ∈ Z ↔ ¬ ∀ x ∈ X ∀ y ∈ X x H y ∈ Z
69 67 68 sylib ⊢ R ∈ RingOps ∧ U ≠ Z → ¬ ∀ x ∈ X ∀ y ∈ X x H y ∈ Z
70 69 pm2.21d ⊢ R ∈ RingOps ∧ U ≠ Z → ∀ x ∈ X ∀ y ∈ X x H y ∈ Z → i ⊆ Z ∨ j ⊆ Z
71 raleq ⊢ i = X → ∀ x ∈ i ∀ y ∈ j x H y ∈ Z ↔ ∀ x ∈ X ∀ y ∈ j x H y ∈ Z
72 raleq ⊢ j = X → ∀ y ∈ j x H y ∈ Z ↔ ∀ y ∈ X x H y ∈ Z
73 72 ralbidv ⊢ j = X → ∀ x ∈ X ∀ y ∈ j x H y ∈ Z ↔ ∀ x ∈ X ∀ y ∈ X x H y ∈ Z
74 71 73 sylan9bb ⊢ i = X ∧ j = X → ∀ x ∈ i ∀ y ∈ j x H y ∈ Z ↔ ∀ x ∈ X ∀ y ∈ X x H y ∈ Z
75 74 imbi1d ⊢ i = X ∧ j = X → ∀ x ∈ i ∀ y ∈ j x H y ∈ Z → i ⊆ Z ∨ j ⊆ Z ↔ ∀ x ∈ X ∀ y ∈ X x H y ∈ Z → i ⊆ Z ∨ j ⊆ Z
76 70 75 syl5ibrcom ⊢ R ∈ RingOps ∧ U ≠ Z → i = X ∧ j = X → ∀ x ∈ i ∀ y ∈ j x H y ∈ 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 ∈ j x H y ∈ Z → i ⊆ Z ∨ j ⊆ Z
78 77 3adant3 ⊢ R ∈ RingOps ∧ U ≠ Z ∧ Idl ⁡ R = Z X → i = Z ∨ i = X ∧ j = Z ∨ j = X → ∀ x ∈ i ∀ y ∈ j x H y ∈ Z → i ⊆ Z ∨ j ⊆ Z
79 34 78 sylbid ⊢ R ∈ RingOps ∧ U ≠ Z ∧ Idl ⁡ R = Z X → i ∈ Idl ⁡ R ∧ j ∈ Idl ⁡ R → ∀ x ∈ i ∀ y ∈ j x H y ∈ Z → i ⊆ Z ∨ j ⊆ Z
80 79 ralrimivv ⊢ R ∈ RingOps ∧ U ≠ Z ∧ Idl ⁡ R = Z X → ∀ i ∈ Idl ⁡ R ∀ j ∈ Idl ⁡ R ∀ x ∈ i ∀ y ∈ j x H y ∈ 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 ∈ j x H y ∈ Z → i ⊆ Z ∨ j ⊆ Z
82 81 3ad2ant1 ⊢ R ∈ RingOps ∧ U ≠ Z ∧ Idl ⁡ R = Z X → Z ∈ PrIdl ⁡ R ↔ Z ∈ Idl ⁡ R ∧ Z ≠ X ∧ ∀ i ∈ Idl ⁡ R ∀ j ∈ Idl ⁡ R ∀ x ∈ i ∀ y ∈ j x H y ∈ Z → i ⊆ Z ∨ j ⊆ Z
83 8 15 80 82 mpbir3and ⊢ R ∈ RingOps ∧ U ≠ Z ∧ Idl ⁡ R = Z X → 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 = Z X → R ∈ PrRing