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 )