Metamath Proof Explorer

Theorem rngqiprngfulem2

Description: Lemma 2 for rngqiprngfu (and lemma for rngqiprngu ). (Contributed by AV, 16-Mar-2025)

Ref Expression
Hypotheses rngqiprngfu.r 
|- ( ph -> R e. Rng )
rngqiprngfu.i 
|- ( ph -> I e. ( 2Ideal ` R ) )
rngqiprngfu.j 
|- J = ( R |`s I )
rngqiprngfu.u 
|- ( ph -> J e. Ring )
rngqiprngfu.b 
|- B = ( Base ` R )
rngqiprngfu.t 
|- .x. = ( .r ` R )
rngqiprngfu.1 
|- .1. = ( 1r ` J )
rngqiprngfu.g 
|- .~ = ( R ~QG I )
rngqiprngfu.q 
|- Q = ( R /s .~ )
rngqiprngfu.v 
|- ( ph -> Q e. Ring )
rngqiprngfu.e 
|- ( ph -> E e. ( 1r ` Q ) )
Assertion rngqiprngfulem2 
|- ( ph -> E e. B )

Proof

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 )