This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qsnzr

Description: A quotient of a nonzero ring by a proper ideal is a nonzero ring. (Contributed by Thierry Arnoux, 9-Mar-2025)

Ref Expression
Hypotheses qsnzr.q 
|- Q = ( R /s ( R ~QG I ) )
qsnzr.1 
|- B = ( Base ` R )
qsnzr.r 
|- ( ph -> R e. Ring )
qsnzr.z 
|- ( ph -> R e. NzRing )
qsnzr.i 
|- ( ph -> I e. ( 2Ideal ` R ) )
qsnzr.2 
|- ( ph -> I =/= B )
Assertion qsnzr 
|- ( ph -> Q e. NzRing )

Proof

Step Hyp Ref Expression
1 qsnzr.q 
 |-  Q = ( R /s ( R ~QG I ) )
2 qsnzr.1 
 |-  B = ( Base ` R )
3 qsnzr.r 
 |-  ( ph -> R e. Ring )
4 qsnzr.z 
 |-  ( ph -> R e. NzRing )
5 qsnzr.i 
 |-  ( ph -> I e. ( 2Ideal ` R ) )
6 qsnzr.2 
 |-  ( ph -> I =/= B )
7 eqid 
 |-  ( 2Ideal ` R ) = ( 2Ideal ` R )
8 1 7 qusring 
 |-  ( ( R e. Ring /\ I e. ( 2Ideal ` R ) ) -> Q e. Ring )
9 3 5 8 syl2anc 
 |-  ( ph -> Q e. Ring )
10 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
11 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
12 eqid 
 |-  ( invg ` R ) = ( invg ` R )
13 11 12 grpinvid 
 |-  ( R e. Grp -> ( ( invg ` R ) ` ( 0g ` R ) ) = ( 0g ` R ) )
14 3 10 13 3syl 
 |-  ( ph -> ( ( invg ` R ) ` ( 0g ` R ) ) = ( 0g ` R ) )
15 14 oveq1d 
 |-  ( ph -> ( ( ( invg ` R ) ` ( 0g ` R ) ) ( +g ` R ) ( 1r ` R ) ) = ( ( 0g ` R ) ( +g ` R ) ( 1r ` R ) ) )
16 eqid 
 |-  ( +g ` R ) = ( +g ` R )
17 3 10 syl 
 |-  ( ph -> R e. Grp )
18 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
19 2 18 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
20 3 19 syl 
 |-  ( ph -> ( 1r ` R ) e. B )
21 2 16 11 17 20 grplidd 
 |-  ( ph -> ( ( 0g ` R ) ( +g ` R ) ( 1r ` R ) ) = ( 1r ` R ) )
22 15 21 eqtrd 
 |-  ( ph -> ( ( ( invg ` R ) ` ( 0g ` R ) ) ( +g ` R ) ( 1r ` R ) ) = ( 1r ` R ) )
23 5 2idllidld 
 |-  ( ph -> I e. ( LIdeal ` R ) )
24 2 18 pridln1 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> -. ( 1r ` R ) e. I )
25 3 23 6 24 syl3anc 
 |-  ( ph -> -. ( 1r ` R ) e. I )
26 22 25 eqneltrd 
 |-  ( ph -> -. ( ( ( invg ` R ) ` ( 0g ` R ) ) ( +g ` R ) ( 1r ` R ) ) e. I )
27 3 adantr 
 |-  ( ( ph /\ ( 1r ` R ) ( R ~QG I ) ( 0g ` R ) ) -> R e. Ring )
28 lidlnsg 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) -> I e. ( NrmSGrp ` R ) )
29 3 23 28 syl2anc 
 |-  ( ph -> I e. ( NrmSGrp ` R ) )
30 nsgsubg 
 |-  ( I e. ( NrmSGrp ` R ) -> I e. ( SubGrp ` R ) )
31 29 30 syl 
 |-  ( ph -> I e. ( SubGrp ` R ) )
32 2 subgss 
 |-  ( I e. ( SubGrp ` R ) -> I C_ B )
33 31 32 syl 
 |-  ( ph -> I C_ B )
34 33 adantr 
 |-  ( ( ph /\ ( 1r ` R ) ( R ~QG I ) ( 0g ` R ) ) -> I C_ B )
35 eqid 
 |-  ( R ~QG I ) = ( R ~QG I )
36 2 35 eqger 
 |-  ( I e. ( SubGrp ` R ) -> ( R ~QG I ) Er B )
37 31 36 syl 
 |-  ( ph -> ( R ~QG I ) Er B )
38 37 adantr 
 |-  ( ( ph /\ ( 1r ` R ) ( R ~QG I ) ( 0g ` R ) ) -> ( R ~QG I ) Er B )
39 simpr 
 |-  ( ( ph /\ ( 1r ` R ) ( R ~QG I ) ( 0g ` R ) ) -> ( 1r ` R ) ( R ~QG I ) ( 0g ` R ) )
40 38 39 ersym 
 |-  ( ( ph /\ ( 1r ` R ) ( R ~QG I ) ( 0g ` R ) ) -> ( 0g ` R ) ( R ~QG I ) ( 1r ` R ) )
41 2 12 16 35 eqgval 
 |-  ( ( R e. Ring /\ I C_ B ) -> ( ( 0g ` R ) ( R ~QG I ) ( 1r ` R ) <-> ( ( 0g ` R ) e. B /\ ( 1r ` R ) e. B /\ ( ( ( invg ` R ) ` ( 0g ` R ) ) ( +g ` R ) ( 1r ` R ) ) e. I ) ) )
42 41 biimpa 
 |-  ( ( ( R e. Ring /\ I C_ B ) /\ ( 0g ` R ) ( R ~QG I ) ( 1r ` R ) ) -> ( ( 0g ` R ) e. B /\ ( 1r ` R ) e. B /\ ( ( ( invg ` R ) ` ( 0g ` R ) ) ( +g ` R ) ( 1r ` R ) ) e. I ) )
43 42 simp3d 
 |-  ( ( ( R e. Ring /\ I C_ B ) /\ ( 0g ` R ) ( R ~QG I ) ( 1r ` R ) ) -> ( ( ( invg ` R ) ` ( 0g ` R ) ) ( +g ` R ) ( 1r ` R ) ) e. I )
44 27 34 40 43 syl21anc 
 |-  ( ( ph /\ ( 1r ` R ) ( R ~QG I ) ( 0g ` R ) ) -> ( ( ( invg ` R ) ` ( 0g ` R ) ) ( +g ` R ) ( 1r ` R ) ) e. I )
45 26 44 mtand 
 |-  ( ph -> -. ( 1r ` R ) ( R ~QG I ) ( 0g ` R ) )
46 37 20 erth 
 |-  ( ph -> ( ( 1r ` R ) ( R ~QG I ) ( 0g ` R ) <-> [ ( 1r ` R ) ] ( R ~QG I ) = [ ( 0g ` R ) ] ( R ~QG I ) ) )
47 45 46 mtbid 
 |-  ( ph -> -. [ ( 1r ` R ) ] ( R ~QG I ) = [ ( 0g ` R ) ] ( R ~QG I ) )
48 47 neqned 
 |-  ( ph -> [ ( 1r ` R ) ] ( R ~QG I ) =/= [ ( 0g ` R ) ] ( R ~QG I ) )
49 1 7 18 qus1 
 |-  ( ( R e. Ring /\ I e. ( 2Ideal ` R ) ) -> ( Q e. Ring /\ [ ( 1r ` R ) ] ( R ~QG I ) = ( 1r ` Q ) ) )
50 3 5 49 syl2anc 
 |-  ( ph -> ( Q e. Ring /\ [ ( 1r ` R ) ] ( R ~QG I ) = ( 1r ` Q ) ) )
51 50 simprd 
 |-  ( ph -> [ ( 1r ` R ) ] ( R ~QG I ) = ( 1r ` Q ) )
52 1 11 qus0 
 |-  ( I e. ( NrmSGrp ` R ) -> [ ( 0g ` R ) ] ( R ~QG I ) = ( 0g ` Q ) )
53 29 52 syl 
 |-  ( ph -> [ ( 0g ` R ) ] ( R ~QG I ) = ( 0g ` Q ) )
54 48 51 53 3netr3d 
 |-  ( ph -> ( 1r ` Q ) =/= ( 0g ` Q ) )
55 eqid 
 |-  ( 1r ` Q ) = ( 1r ` Q )
56 eqid 
 |-  ( 0g ` Q ) = ( 0g ` Q )
57 55 56 isnzr 
 |-  ( Q e. NzRing <-> ( Q e. Ring /\ ( 1r ` Q ) =/= ( 0g ` Q ) ) )
58 9 54 57 sylanbrc 
 |-  ( ph -> Q e. NzRing )