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 syl6bb 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 syl6bb 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