Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  smprngopr Structured version   Unicode version

Theorem smprngopr 26662
 Description: A simple ring (one whose only ideals are and ) is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.)
Hypotheses
Ref Expression
smprngpr.1
smprngpr.2
smprngpr.3
smprngpr.4 GId
smprngpr.5 GId
Assertion
Ref Expression
smprngopr

Proof of Theorem smprngopr
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp1 957 . 2
2 smprngpr.1 . . . . 5
3 smprngpr.4 . . . . 5 GId
42, 30idl 26635 . . . 4
6 smprngpr.2 . . . . . . . 8
7 smprngpr.3 . . . . . . . 8
8 smprngpr.5 . . . . . . . 8 GId
92, 6, 7, 3, 80rngo 26637 . . . . . . 7
10 eqcom 2438 . . . . . . 7
11 eqcom 2438 . . . . . . 7
129, 10, 113bitr4g 280 . . . . . 6
1312necon3bid 2636 . . . . 5
1413biimpa 471 . . . 4
16 df-pr 3821 . . . . . . . 8
1716eqeq2i 2446 . . . . . . 7
18 eleq2 2497 . . . . . . . . 9
19 eleq2 2497 . . . . . . . . 9
2018, 19anbi12d 692 . . . . . . . 8
21 elun 3488 . . . . . . . . . 10
22 elsn 3829 . . . . . . . . . . 11
23 elsn 3829 . . . . . . . . . . 11
2422, 23orbi12i 508 . . . . . . . . . 10
2521, 24bitri 241 . . . . . . . . 9
26 elun 3488 . . . . . . . . . 10
27 elsn 3829 . . . . . . . . . . 11
28 elsn 3829 . . . . . . . . . . 11
2927, 28orbi12i 508 . . . . . . . . . 10
3026, 29bitri 241 . . . . . . . . 9
3125, 30anbi12i 679 . . . . . . . 8
3220, 31syl6bb 253 . . . . . . 7
3317, 32sylbi 188 . . . . . 6
34333ad2ant3 980 . . . . 5
35 eqimss 3400 . . . . . . . . . . 11
3635orcd 382 . . . . . . . . . 10
3736adantr 452 . . . . . . . . 9
3837a1d 23 . . . . . . . 8
3938a1i 11 . . . . . . 7
40 eqimss 3400 . . . . . . . . . . 11
4140olcd 383 . . . . . . . . . 10
4241adantl 453 . . . . . . . . 9
4342a1d 23 . . . . . . . 8
4443a1i 11 . . . . . . 7
4536adantr 452 . . . . . . . . 9
4645a1d 23 . . . . . . . 8
4746a1i 11 . . . . . . 7
482rneqi 5096 . . . . . . . . . . . . . 14
497, 48eqtri 2456 . . . . . . . . . . . . 13
5049, 6, 8rngo1cl 22017 . . . . . . . . . . . 12
5150adantr 452 . . . . . . . . . . 11
526, 49, 8rngolidm 22012 . . . . . . . . . . . . . . . 16
5350, 52mpdan 650 . . . . . . . . . . . . . . 15
5453eleq1d 2502 . . . . . . . . . . . . . 14
55 fvex 5742 . . . . . . . . . . . . . . . 16 GId
568, 55eqeltri 2506 . . . . . . . . . . . . . . 15
5756elsnc 3837 . . . . . . . . . . . . . 14
5854, 57syl6bb 253 . . . . . . . . . . . . 13
5958necon3bbid 2635 . . . . . . . . . . . 12
6059biimpar 472 . . . . . . . . . . 11
61 oveq1 6088 . . . . . . . . . . . . . 14
6261eleq1d 2502 . . . . . . . . . . . . 13
6362notbid 286 . . . . . . . . . . . 12
64 oveq2 6089 . . . . . . . . . . . . . 14
6564eleq1d 2502 . . . . . . . . . . . . 13
6665notbid 286 . . . . . . . . . . . 12
6763, 66rspc2ev 3060 . . . . . . . . . . 11
6851, 51, 60, 67syl3anc 1184 . . . . . . . . . 10
69 rexnal 2716 . . . . . . . . . . . 12
7069rexbii 2730 . . . . . . . . . . 11
71 rexnal 2716 . . . . . . . . . . 11
7270, 71bitri 241 . . . . . . . . . 10
7368, 72sylib 189 . . . . . . . . 9
7473pm2.21d 100 . . . . . . . 8
75 raleq 2904 . . . . . . . . . 10
76 raleq 2904 . . . . . . . . . . 11
7776ralbidv 2725 . . . . . . . . . 10
7875, 77sylan9bb 681 . . . . . . . . 9
7978imbi1d 309 . . . . . . . 8
8074, 79syl5ibrcom 214 . . . . . . 7
8139, 44, 47, 80ccased 914 . . . . . 6
82813adant3 977 . . . . 5
8334, 82sylbid 207 . . . 4
8483ralrimivv 2797 . . 3
852, 6, 7ispridl 26644 . . . 4