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 /_{𝑠} (R ~_{QG} I)$
	qsnzr.1	$⊢ B = {Base}_{R}$
	qsnzr.r	$⊢ φ \to R \in Ring$
	qsnzr.z	$⊢ φ \to R \in NzRing$
	qsnzr.i	$⊢ φ \to I \in 2Ideal (R)$
	qsnzr.2	$⊢ φ \to I \neq B$
Assertion	qsnzr	$⊢ φ \to Q \in NzRing$

Proof

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

Metamath Proof Explorer

Theorem qsnzr

Proof