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 ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
qsnzr.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
qsnzr.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
qsnzr.z ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
qsnzr.i ⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
qsnzr.2 ⊢ ( 𝜑 → 𝐼 ≠ 𝐵 )
Assertion qsnzr ( 𝜑 → 𝑄 ∈ NzRing )

Proof

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