rngqiprngimf1lem

	Ref	Expression
Hypotheses	rng2idlring.r	$⊢ φ \to R \in Rng$
	rng2idlring.i	$⊢ φ \to I \in 2Ideal (R)$
	rng2idlring.j	$⊢ J = R ↾_{𝑠} I$
	rng2idlring.u	$⊢ φ \to J \in Ring$
	rng2idlring.b	$⊢ B = {Base}_{R}$
	rng2idlring.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	rng2idlring.1	$⊢ \underset{˙}{1} = 1_{J}$
	rngqiprngim.g	$⊢ \underset{˙}{\sim} = R ~_{QG} I$
	rngqiprngim.q	$⊢ Q = R /_{𝑠} \underset{˙}{\sim}$
Assertion	rngqiprngimf1lem	$⊢ (φ \land A \in B) \to (([A] \underset{˙}{\sim} = 0_{Q} \land \underset{˙}{1} \underset{˙}{\cdot} A = 0_{J}) \to A = 0_{R})$

Proof

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

Metamath Proof Explorer

Theorem rngqiprngimf1lem

Proof