| Step |
Hyp |
Ref |
Expression |
| 1 |
|
rngqiprngfu.r |
|- ( ph -> R e. Rng ) |
| 2 |
|
rngqiprngfu.i |
|- ( ph -> I e. ( 2Ideal ` R ) ) |
| 3 |
|
rngqiprngfu.j |
|- J = ( R |`s I ) |
| 4 |
|
rngqiprngfu.u |
|- ( ph -> J e. Ring ) |
| 5 |
|
rngqiprngfu.b |
|- B = ( Base ` R ) |
| 6 |
|
rngqiprngfu.t |
|- .x. = ( .r ` R ) |
| 7 |
|
rngqiprngfu.1 |
|- .1. = ( 1r ` J ) |
| 8 |
|
rngqiprngfu.g |
|- .~ = ( R ~QG I ) |
| 9 |
|
rngqiprngfu.q |
|- Q = ( R /s .~ ) |
| 10 |
|
rngqiprngfu.v |
|- ( ph -> Q e. Ring ) |
| 11 |
|
rngqiprngfu.e |
|- ( ph -> E e. ( 1r ` Q ) ) |
| 12 |
1 2 3 4 5 6 7 8 9 10
|
rngqiprngfulem1 |
|- ( ph -> E. x e. B ( 1r ` Q ) = [ x ] .~ ) |
| 13 |
11
|
adantr |
|- ( ( ph /\ x e. B ) -> E e. ( 1r ` Q ) ) |
| 14 |
|
eleq2 |
|- ( ( 1r ` Q ) = [ x ] .~ -> ( E e. ( 1r ` Q ) <-> E e. [ x ] .~ ) ) |
| 15 |
14
|
adantl |
|- ( ( ( ph /\ x e. B ) /\ ( 1r ` Q ) = [ x ] .~ ) -> ( E e. ( 1r ` Q ) <-> E e. [ x ] .~ ) ) |
| 16 |
|
elecg |
|- ( ( E e. ( 1r ` Q ) /\ x e. B ) -> ( E e. [ x ] .~ <-> x .~ E ) ) |
| 17 |
11 16
|
sylan |
|- ( ( ph /\ x e. B ) -> ( E e. [ x ] .~ <-> x .~ E ) ) |
| 18 |
|
rngabl |
|- ( R e. Rng -> R e. Abel ) |
| 19 |
1 18
|
syl |
|- ( ph -> R e. Abel ) |
| 20 |
|
eqid |
|- ( 2Ideal ` R ) = ( 2Ideal ` R ) |
| 21 |
5 20
|
2idlss |
|- ( I e. ( 2Ideal ` R ) -> I C_ B ) |
| 22 |
2 21
|
syl |
|- ( ph -> I C_ B ) |
| 23 |
19 22
|
jca |
|- ( ph -> ( R e. Abel /\ I C_ B ) ) |
| 24 |
23
|
adantr |
|- ( ( ph /\ x e. B ) -> ( R e. Abel /\ I C_ B ) ) |
| 25 |
|
eqid |
|- ( -g ` R ) = ( -g ` R ) |
| 26 |
5 25 8
|
eqgabl |
|- ( ( R e. Abel /\ I C_ B ) -> ( x .~ E <-> ( x e. B /\ E e. B /\ ( E ( -g ` R ) x ) e. I ) ) ) |
| 27 |
24 26
|
syl |
|- ( ( ph /\ x e. B ) -> ( x .~ E <-> ( x e. B /\ E e. B /\ ( E ( -g ` R ) x ) e. I ) ) ) |
| 28 |
|
simp2 |
|- ( ( x e. B /\ E e. B /\ ( E ( -g ` R ) x ) e. I ) -> E e. B ) |
| 29 |
27 28
|
biimtrdi |
|- ( ( ph /\ x e. B ) -> ( x .~ E -> E e. B ) ) |
| 30 |
17 29
|
sylbid |
|- ( ( ph /\ x e. B ) -> ( E e. [ x ] .~ -> E e. B ) ) |
| 31 |
30
|
adantr |
|- ( ( ( ph /\ x e. B ) /\ ( 1r ` Q ) = [ x ] .~ ) -> ( E e. [ x ] .~ -> E e. B ) ) |
| 32 |
15 31
|
sylbid |
|- ( ( ( ph /\ x e. B ) /\ ( 1r ` Q ) = [ x ] .~ ) -> ( E e. ( 1r ` Q ) -> E e. B ) ) |
| 33 |
32
|
ex |
|- ( ( ph /\ x e. B ) -> ( ( 1r ` Q ) = [ x ] .~ -> ( E e. ( 1r ` Q ) -> E e. B ) ) ) |
| 34 |
13 33
|
mpid |
|- ( ( ph /\ x e. B ) -> ( ( 1r ` Q ) = [ x ] .~ -> E e. B ) ) |
| 35 |
34
|
rexlimdva |
|- ( ph -> ( E. x e. B ( 1r ` Q ) = [ x ] .~ -> E e. B ) ) |
| 36 |
12 35
|
mpd |
|- ( ph -> E e. B ) |