Theorem rngqiprngimf1

Description: F is a one-to-one function from (the base set of) a non-unital ring to the product of the (base set of the) quotient with a two-sided ideal and the (base set of the) two-sided ideal. (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 ∼ )
	rngqiprngim.c	⊢ 𝐶 = ( Base ‘ 𝑄 )
	rngqiprngim.p	⊢ 𝑃 = ( 𝑄 ×s 𝐽 )
	rngqiprngim.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ )
Assertion	rngqiprngimf1	⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1→ ( 𝐶 × 𝐼 ) )

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		rngqiprngim.c	⊢ 𝐶 = ( Base ‘ 𝑄 )
11		rngqiprngim.p	⊢ 𝑃 = ( 𝑄 ×s 𝐽 )
12		rngqiprngim.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ )
13		ringrng	⊢ ( 𝐽 ∈ Ring → 𝐽 ∈ Rng )
14	4 13	syl	⊢ ( 𝜑 → 𝐽 ∈ Rng )
15	3 14	eqeltrrid	⊢ ( 𝜑 → ( 𝑅 ↾s 𝐼 ) ∈ Rng )
16	1 2 15	rng2idlnsg	⊢ ( 𝜑 → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )
17		nsgsubg	⊢ ( 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
18	16 17	syl	⊢ ( 𝜑 → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
19	8	oveq2i	⊢ ( 𝑅 /s ∼ ) = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
20	9 19	eqtri	⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
21		eqid	⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
22	20 21	qus2idrng	⊢ ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝑄 ∈ Rng )
23	1 2 18 22	syl3anc	⊢ ( 𝜑 → 𝑄 ∈ Rng )
24		rnggrp	⊢ ( 𝑄 ∈ Rng → 𝑄 ∈ Grp )
25	24	grpmndd	⊢ ( 𝑄 ∈ Rng → 𝑄 ∈ Mnd )
26	23 25	syl	⊢ ( 𝜑 → 𝑄 ∈ Mnd )
27		ringmnd	⊢ ( 𝐽 ∈ Ring → 𝐽 ∈ Mnd )
28	4 27	syl	⊢ ( 𝜑 → 𝐽 ∈ Mnd )
29	11	xpsmnd0	⊢ ( ( 𝑄 ∈ Mnd ∧ 𝐽 ∈ Mnd ) → ( 0g ‘ 𝑃 ) = ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ )
30	26 28 29	syl2anc	⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) = ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ )
31	30	sneqd	⊢ ( 𝜑 → { ( 0g ‘ 𝑃 ) } = { ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ } )
32	31	imaeq2d	⊢ ( 𝜑 → ( ◡ 𝐹 “ { ( 0g ‘ 𝑃 ) } ) = ( ◡ 𝐹 “ { ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ } ) )
33		nfv	⊢ Ⅎ 𝑥 𝜑
34		opex	⊢ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ∈ V
35	34	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ∈ V )
36	33 35 12	fnmptd	⊢ ( 𝜑 → 𝐹 Fn 𝐵 )
37		fncnvima2	⊢ ( 𝐹 Fn 𝐵 → ( ◡ 𝐹 “ { ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ } ) = { 𝑎 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑎 ) ∈ { ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ } } )
38	36 37	syl	⊢ ( 𝜑 → ( ◡ 𝐹 “ { ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ } ) = { 𝑎 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑎 ) ∈ { ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ } } )
39	1 2 3 4 5 6 7 8 9 10 11 12	rngqiprngimfv	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑎 ) = ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ )
40	39	eleq1d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑎 ) ∈ { ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ } ↔ ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ∈ { ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ } ) )
41	40	rabbidva	⊢ ( 𝜑 → { 𝑎 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑎 ) ∈ { ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ } } = { 𝑎 ∈ 𝐵 ∣ ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ∈ { ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ } } )
42		eceq1	⊢ ( 𝑎 = ( 0g ‘ 𝑅 ) → [ 𝑎 ] ∼ = [ ( 0g ‘ 𝑅 ) ] ∼ )
43		oveq2	⊢ ( 𝑎 = ( 0g ‘ 𝑅 ) → ( 1 · 𝑎 ) = ( 1 · ( 0g ‘ 𝑅 ) ) )
44	42 43	opeq12d	⊢ ( 𝑎 = ( 0g ‘ 𝑅 ) → ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ = ⟨ [ ( 0g ‘ 𝑅 ) ] ∼ , ( 1 · ( 0g ‘ 𝑅 ) ) ⟩ )
45	44	eleq1d	⊢ ( 𝑎 = ( 0g ‘ 𝑅 ) → ( ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ∈ { ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ } ↔ ⟨ [ ( 0g ‘ 𝑅 ) ] ∼ , ( 1 · ( 0g ‘ 𝑅 ) ) ⟩ ∈ { ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ } ) )
46		rnggrp	⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Grp )
47	1 46	syl	⊢ ( 𝜑 → 𝑅 ∈ Grp )
48	47	grpmndd	⊢ ( 𝜑 → 𝑅 ∈ Mnd )
49		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
50	5 49	mndidcl	⊢ ( 𝑅 ∈ Mnd → ( 0g ‘ 𝑅 ) ∈ 𝐵 )
51	48 50	syl	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ 𝐵 )
52	8	eceq2i	⊢ [ ( 0g ‘ 𝑅 ) ] ∼ = [ ( 0g ‘ 𝑅 ) ] ( 𝑅 ~QG 𝐼 )
53	20 49	qus0	⊢ ( 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) → [ ( 0g ‘ 𝑅 ) ] ( 𝑅 ~QG 𝐼 ) = ( 0g ‘ 𝑄 ) )
54	16 53	syl	⊢ ( 𝜑 → [ ( 0g ‘ 𝑅 ) ] ( 𝑅 ~QG 𝐼 ) = ( 0g ‘ 𝑄 ) )
55	52 54	eqtrid	⊢ ( 𝜑 → [ ( 0g ‘ 𝑅 ) ] ∼ = ( 0g ‘ 𝑄 ) )
56	1 2 15	rng2idl0	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ 𝐼 )
57	5 21	2idlss	⊢ ( 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) → 𝐼 ⊆ 𝐵 )
58	2 57	syl	⊢ ( 𝜑 → 𝐼 ⊆ 𝐵 )
59	3 5 49	ress0g	⊢ ( ( 𝑅 ∈ Mnd ∧ ( 0g ‘ 𝑅 ) ∈ 𝐼 ∧ 𝐼 ⊆ 𝐵 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝐽 ) )
60	48 56 58 59	syl3anc	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝐽 ) )
61	60	oveq2d	⊢ ( 𝜑 → ( 1 · ( 0g ‘ 𝑅 ) ) = ( 1 · ( 0g ‘ 𝐽 ) ) )
62	3 6	ressmulr	⊢ ( 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) → · = ( .r ‘ 𝐽 ) )
63	2 62	syl	⊢ ( 𝜑 → · = ( .r ‘ 𝐽 ) )
64	63	oveqd	⊢ ( 𝜑 → ( 1 · ( 0g ‘ 𝐽 ) ) = ( 1 ( .r ‘ 𝐽 ) ( 0g ‘ 𝐽 ) ) )
65		eqid	⊢ ( Base ‘ 𝐽 ) = ( Base ‘ 𝐽 )
66	65 7	ringidcl	⊢ ( 𝐽 ∈ Ring → 1 ∈ ( Base ‘ 𝐽 ) )
67		eqid	⊢ ( .r ‘ 𝐽 ) = ( .r ‘ 𝐽 )
68		eqid	⊢ ( 0g ‘ 𝐽 ) = ( 0g ‘ 𝐽 )
69	65 67 68	ringrz	⊢ ( ( 𝐽 ∈ Ring ∧ 1 ∈ ( Base ‘ 𝐽 ) ) → ( 1 ( .r ‘ 𝐽 ) ( 0g ‘ 𝐽 ) ) = ( 0g ‘ 𝐽 ) )
70	4 66 69	syl2anc2	⊢ ( 𝜑 → ( 1 ( .r ‘ 𝐽 ) ( 0g ‘ 𝐽 ) ) = ( 0g ‘ 𝐽 ) )
71	61 64 70	3eqtrd	⊢ ( 𝜑 → ( 1 · ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝐽 ) )
72	55 71	opeq12d	⊢ ( 𝜑 → ⟨ [ ( 0g ‘ 𝑅 ) ] ∼ , ( 1 · ( 0g ‘ 𝑅 ) ) ⟩ = ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ )
73		opex	⊢ ⟨ [ ( 0g ‘ 𝑅 ) ] ∼ , ( 1 · ( 0g ‘ 𝑅 ) ) ⟩ ∈ V
74	73	elsn	⊢ ( ⟨ [ ( 0g ‘ 𝑅 ) ] ∼ , ( 1 · ( 0g ‘ 𝑅 ) ) ⟩ ∈ { ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ } ↔ ⟨ [ ( 0g ‘ 𝑅 ) ] ∼ , ( 1 · ( 0g ‘ 𝑅 ) ) ⟩ = ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ )
75	72 74	sylibr	⊢ ( 𝜑 → ⟨ [ ( 0g ‘ 𝑅 ) ] ∼ , ( 1 · ( 0g ‘ 𝑅 ) ) ⟩ ∈ { ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ } )
76		opex	⊢ ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ∈ V
77	76	elsn	⊢ ( ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ∈ { ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ } ↔ ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ = ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ )
78	8	ovexi	⊢ ∼ ∈ V
79		ecexg	⊢ ( ∼ ∈ V → [ 𝑎 ] ∼ ∈ V )
80	78 79	ax-mp	⊢ [ 𝑎 ] ∼ ∈ V
81		ovex	⊢ ( 1 · 𝑎 ) ∈ V
82	80 81	opth	⊢ ( ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ = ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ ↔ ( [ 𝑎 ] ∼ = ( 0g ‘ 𝑄 ) ∧ ( 1 · 𝑎 ) = ( 0g ‘ 𝐽 ) ) )
83	77 82	bitri	⊢ ( ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ∈ { ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ } ↔ ( [ 𝑎 ] ∼ = ( 0g ‘ 𝑄 ) ∧ ( 1 · 𝑎 ) = ( 0g ‘ 𝐽 ) ) )
84	1 2 3 4 5 6 7 8 9	rngqiprngimf1lem	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( [ 𝑎 ] ∼ = ( 0g ‘ 𝑄 ) ∧ ( 1 · 𝑎 ) = ( 0g ‘ 𝐽 ) ) → 𝑎 = ( 0g ‘ 𝑅 ) ) )
85	83 84	biimtrid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ∈ { ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ } → 𝑎 = ( 0g ‘ 𝑅 ) ) )
86	85	imp	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ∈ { ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ } ) → 𝑎 = ( 0g ‘ 𝑅 ) )
87	45 51 75 86	rabeqsnd	⊢ ( 𝜑 → { 𝑎 ∈ 𝐵 ∣ ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ∈ { ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ } } = { ( 0g ‘ 𝑅 ) } )
88	41 87	eqtrd	⊢ ( 𝜑 → { 𝑎 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑎 ) ∈ { ⟨ ( 0g ‘ 𝑄 ) , ( 0g ‘ 𝐽 ) ⟩ } } = { ( 0g ‘ 𝑅 ) } )
89	32 38 88	3eqtrd	⊢ ( 𝜑 → ( ◡ 𝐹 “ { ( 0g ‘ 𝑃 ) } ) = { ( 0g ‘ 𝑅 ) } )
90	1 2 3 4 5 6 7 8 9 10 11 12	rngqiprngghm	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 GrpHom 𝑃 ) )
91		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
92		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
93	5 91 49 92	kerf1ghm	⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑃 ) → ( 𝐹 : 𝐵 –1-1→ ( Base ‘ 𝑃 ) ↔ ( ◡ 𝐹 “ { ( 0g ‘ 𝑃 ) } ) = { ( 0g ‘ 𝑅 ) } ) )
94	90 93	syl	⊢ ( 𝜑 → ( 𝐹 : 𝐵 –1-1→ ( Base ‘ 𝑃 ) ↔ ( ◡ 𝐹 “ { ( 0g ‘ 𝑃 ) } ) = { ( 0g ‘ 𝑅 ) } ) )
95	89 94	mpbird	⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1→ ( Base ‘ 𝑃 ) )
96		eqidd	⊢ ( 𝜑 → 𝐹 = 𝐹 )
97		eqidd	⊢ ( 𝜑 → 𝐵 = 𝐵 )
98	1 2 3 4 5 6 7 8 9 10 11	rngqipbas	⊢ ( 𝜑 → ( Base ‘ 𝑃 ) = ( 𝐶 × 𝐼 ) )
99	96 97 98	f1eq123d	⊢ ( 𝜑 → ( 𝐹 : 𝐵 –1-1→ ( Base ‘ 𝑃 ) ↔ 𝐹 : 𝐵 –1-1→ ( 𝐶 × 𝐼 ) ) )
100	95 99	mpbid	⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1→ ( 𝐶 × 𝐼 ) )