Metamath Proof Explorer

Theorem rngqiprngimf1lem

Description: Lemma for rngqiprngimf1 . (Contributed by AV, 7-Mar-2025)

Ref Expression
Hypotheses rng2idlring.r 
|- ( ph -> R e. Rng )
rng2idlring.i 
|- ( ph -> I e. ( 2Ideal ` R ) )
rng2idlring.j 
|- J = ( R |`s I )
rng2idlring.u 
|- ( ph -> J e. Ring )
rng2idlring.b 
|- B = ( Base ` R )
rng2idlring.t 
|- .x. = ( .r ` R )
rng2idlring.1 
|- .1. = ( 1r ` J )
rngqiprngim.g 
|- .~ = ( R ~QG I )
rngqiprngim.q 
|- Q = ( R /s .~ )
Assertion rngqiprngimf1lem 
|- ( ( ph /\ A e. B ) -> ( ( [ A ] .~ = ( 0g ` Q ) /\ ( .1. .x. A ) = ( 0g ` J ) ) -> A = ( 0g ` R ) ) )

Proof

Step Hyp Ref Expression
1 rng2idlring.r 
 |-  ( ph -> R e. Rng )
2 rng2idlring.i 
 |-  ( ph -> I e. ( 2Ideal ` R ) )
3 rng2idlring.j 
 |-  J = ( R |`s I )
4 rng2idlring.u 
 |-  ( ph -> J e. Ring )
5 rng2idlring.b 
 |-  B = ( Base ` R )
6 rng2idlring.t 
 |-  .x. = ( .r ` R )
7 rng2idlring.1 
 |-  .1. = ( 1r ` J )
8 rngqiprngim.g 
 |-  .~ = ( R ~QG I )
9 rngqiprngim.q 
 |-  Q = ( R /s .~ )
10 ringrng 
 |-  ( J e. Ring -> J e. Rng )
11 4 10 syl 
 |-  ( ph -> J e. Rng )
12 3 11 eqeltrrid 
 |-  ( ph -> ( R |`s I ) e. Rng )
13 1 2 12 rng2idlnsg 
 |-  ( ph -> I e. ( NrmSGrp ` R ) )
14 13 adantr 
 |-  ( ( ph /\ A e. B ) -> I e. ( NrmSGrp ` R ) )
15 8 oveq2i 
 |-  ( R /s .~ ) = ( R /s ( R ~QG I ) )
16 9 15 eqtri 
 |-  Q = ( R /s ( R ~QG I ) )
17 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
18 16 17 qus0 
 |-  ( I e. ( NrmSGrp ` R ) -> [ ( 0g ` R ) ] ( R ~QG I ) = ( 0g ` Q ) )
19 14 18 syl 
 |-  ( ( ph /\ A e. B ) -> [ ( 0g ` R ) ] ( R ~QG I ) = ( 0g ` Q ) )
20 19 eqcomd 
 |-  ( ( ph /\ A e. B ) -> ( 0g ` Q ) = [ ( 0g ` R ) ] ( R ~QG I ) )
21 20 eqeq2d 
 |-  ( ( ph /\ A e. B ) -> ( [ A ] .~ = ( 0g ` Q ) <-> [ A ] .~ = [ ( 0g ` R ) ] ( R ~QG I ) ) )
22 8 eqcomi 
 |-  ( R ~QG I ) = .~
23 22 eceq2i 
 |-  [ ( 0g ` R ) ] ( R ~QG I ) = [ ( 0g ` R ) ] .~
24 23 a1i 
 |-  ( ( ph /\ A e. B ) -> [ ( 0g ` R ) ] ( R ~QG I ) = [ ( 0g ` R ) ] .~ )
25 24 eqeq2d 
 |-  ( ( ph /\ A e. B ) -> ( [ A ] .~ = [ ( 0g ` R ) ] ( R ~QG I ) <-> [ A ] .~ = [ ( 0g ` R ) ] .~ ) )
26 eqcom 
 |-  ( [ A ] .~ = [ ( 0g ` R ) ] .~ <-> [ ( 0g ` R ) ] .~ = [ A ] .~ )
27 rngabl 
 |-  ( R e. Rng -> R e. Abel )
28 1 27 syl 
 |-  ( ph -> R e. Abel )
29 nsgsubg 
 |-  ( I e. ( NrmSGrp ` R ) -> I e. ( SubGrp ` R ) )
30 13 29 syl 
 |-  ( ph -> I e. ( SubGrp ` R ) )
31 28 30 jca 
 |-  ( ph -> ( R e. Abel /\ I e. ( SubGrp ` R ) ) )
32 5 17 rng0cl 
 |-  ( R e. Rng -> ( 0g ` R ) e. B )
33 1 32 syl 
 |-  ( ph -> ( 0g ` R ) e. B )
34 33 anim1i 
 |-  ( ( ph /\ A e. B ) -> ( ( 0g ` R ) e. B /\ A e. B ) )
35 eqid 
 |-  ( -g ` R ) = ( -g ` R )
36 5 35 8 qusecsub 
 |-  ( ( ( R e. Abel /\ I e. ( SubGrp ` R ) ) /\ ( ( 0g ` R ) e. B /\ A e. B ) ) -> ( [ ( 0g ` R ) ] .~ = [ A ] .~ <-> ( A ( -g ` R ) ( 0g ` R ) ) e. I ) )
37 31 34 36 syl2an2r 
 |-  ( ( ph /\ A e. B ) -> ( [ ( 0g ` R ) ] .~ = [ A ] .~ <-> ( A ( -g ` R ) ( 0g ` R ) ) e. I ) )
38 26 37 bitrid 
 |-  ( ( ph /\ A e. B ) -> ( [ A ] .~ = [ ( 0g ` R ) ] .~ <-> ( A ( -g ` R ) ( 0g ` R ) ) e. I ) )
39 21 25 38 3bitrd 
 |-  ( ( ph /\ A e. B ) -> ( [ A ] .~ = ( 0g ` Q ) <-> ( A ( -g ` R ) ( 0g ` R ) ) e. I ) )
40 rnggrp 
 |-  ( R e. Rng -> R e. Grp )
41 1 40 syl 
 |-  ( ph -> R e. Grp )
42 5 17 35 grpsubid1 
 |-  ( ( R e. Grp /\ A e. B ) -> ( A ( -g ` R ) ( 0g ` R ) ) = A )
43 41 42 sylan 
 |-  ( ( ph /\ A e. B ) -> ( A ( -g ` R ) ( 0g ` R ) ) = A )
44 43 eleq1d 
 |-  ( ( ph /\ A e. B ) -> ( ( A ( -g ` R ) ( 0g ` R ) ) e. I <-> A e. I ) )
45 eqid 
 |-  ( Base ` J ) = ( Base ` J )
46 eqid 
 |-  ( 0g ` J ) = ( 0g ` J )
47 eqid 
 |-  ( .r ` J ) = ( .r ` J )
48 4 adantr 
 |-  ( ( ph /\ A e. ( Base ` J ) ) -> J e. Ring )
49 simpr 
 |-  ( ( ph /\ A e. ( Base ` J ) ) -> A e. ( Base ` J ) )
50 eqid 
 |-  ( 1r ` J ) = ( 1r ` J )
51 45 46 47 48 49 50 ring1nzdiv 
 |-  ( ( ph /\ A e. ( Base ` J ) ) -> ( ( ( 1r ` J ) ( .r ` J ) A ) = ( 0g ` J ) <-> A = ( 0g ` J ) ) )
52 51 biimpd 
 |-  ( ( ph /\ A e. ( Base ` J ) ) -> ( ( ( 1r ` J ) ( .r ` J ) A ) = ( 0g ` J ) -> A = ( 0g ` J ) ) )
53 52 ex 
 |-  ( ph -> ( A e. ( Base ` J ) -> ( ( ( 1r ` J ) ( .r ` J ) A ) = ( 0g ` J ) -> A = ( 0g ` J ) ) ) )
54 2 3 45 2idlbas 
 |-  ( ph -> ( Base ` J ) = I )
55 54 eqcomd 
 |-  ( ph -> I = ( Base ` J ) )
56 55 eleq2d 
 |-  ( ph -> ( A e. I <-> A e. ( Base ` J ) ) )
57 3 6 ressmulr 
 |-  ( I e. ( 2Ideal ` R ) -> .x. = ( .r ` J ) )
58 2 57 syl 
 |-  ( ph -> .x. = ( .r ` J ) )
59 7 a1i 
 |-  ( ph -> .1. = ( 1r ` J ) )
60 eqidd 
 |-  ( ph -> A = A )
61 58 59 60 oveq123d 
 |-  ( ph -> ( .1. .x. A ) = ( ( 1r ` J ) ( .r ` J ) A ) )
62 61 eqeq1d 
 |-  ( ph -> ( ( .1. .x. A ) = ( 0g ` J ) <-> ( ( 1r ` J ) ( .r ` J ) A ) = ( 0g ` J ) ) )
63 3 17 subg0 
 |-  ( I e. ( SubGrp ` R ) -> ( 0g ` R ) = ( 0g ` J ) )
64 30 63 syl 
 |-  ( ph -> ( 0g ` R ) = ( 0g ` J ) )
65 64 eqeq2d 
 |-  ( ph -> ( A = ( 0g ` R ) <-> A = ( 0g ` J ) ) )
66 62 65 imbi12d 
 |-  ( ph -> ( ( ( .1. .x. A ) = ( 0g ` J ) -> A = ( 0g ` R ) ) <-> ( ( ( 1r ` J ) ( .r ` J ) A ) = ( 0g ` J ) -> A = ( 0g ` J ) ) ) )
67 53 56 66 3imtr4d 
 |-  ( ph -> ( A e. I -> ( ( .1. .x. A ) = ( 0g ` J ) -> A = ( 0g ` R ) ) ) )
68 67 adantr 
 |-  ( ( ph /\ A e. B ) -> ( A e. I -> ( ( .1. .x. A ) = ( 0g ` J ) -> A = ( 0g ` R ) ) ) )
69 44 68 sylbid 
 |-  ( ( ph /\ A e. B ) -> ( ( A ( -g ` R ) ( 0g ` R ) ) e. I -> ( ( .1. .x. A ) = ( 0g ` J ) -> A = ( 0g ` R ) ) ) )
70 39 69 sylbid 
 |-  ( ( ph /\ A e. B ) -> ( [ A ] .~ = ( 0g ` Q ) -> ( ( .1. .x. A ) = ( 0g ` J ) -> A = ( 0g ` R ) ) ) )
71 70 impd 
 |-  ( ( ph /\ A e. B ) -> ( ( [ A ] .~ = ( 0g ` Q ) /\ ( .1. .x. A ) = ( 0g ` J ) ) -> A = ( 0g ` R ) ) )