Theorem rngqiprngimf1lem

Description: Lemma for rngqiprngimf1 . (Contributed by AV, 7-Mar-2025)

	Ref	Expression
Hypotheses	rng2idlring.r	⊢ ( 𝜑 → 𝑅 ∈ Rng )
	rng2idlring.i	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
	rng2idlring.j	⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
	rng2idlring.u	⊢ ( 𝜑 → 𝐽 ∈ Ring )
	rng2idlring.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rng2idlring.t	⊢ · = ( .r ‘ 𝑅 )
	rng2idlring.1	⊢ 1 = ( 1r ‘ 𝐽 )
	rngqiprngim.g	⊢ ∼ = ( 𝑅 ~QG 𝐼 )
	rngqiprngim.q	⊢ 𝑄 = ( 𝑅 /s ∼ )
Assertion	rngqiprngimf1lem	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐵 ) → ( ( [ 𝐴 ] ∼ = ( 0g ‘ 𝑄 ) ∧ ( 1 · 𝐴 ) = ( 0g ‘ 𝐽 ) ) → 𝐴 = ( 0g ‘ 𝑅 ) ) )

Proof

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