rngqiprngimfo

Description: F is a function from (the base set of) a non-unital ring onto 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, 5-Mar-2025) (Proof shortened by AV, 24-Mar-2025)

	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}$
	rngqiprngim.c	$⊢ C = {Base}_{Q}$
	rngqiprngim.p	$⊢ P = Q \times_{𝑠} J$
	rngqiprngim.f	$⊢ F = (x \in B ⟼ ⟨[x] \underset{˙}{\sim}, \underset{˙}{1} \underset{˙}{\cdot} x⟩)$
Assertion	rngqiprngimfo	$⊢ φ \to F : B \underset{onto}{⟶} C \times I$

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		rngqiprngim.c	$⊢ C = {Base}_{Q}$
11		rngqiprngim.p	$⊢ P = Q \times_{𝑠} J$
12		rngqiprngim.f	$⊢ F = (x \in B ⟼ ⟨[x] \underset{˙}{\sim}, \underset{˙}{1} \underset{˙}{\cdot} x⟩)$
13	1 2 3 4 5 6 7 8 9 10 11 12	rngqiprngimf	$⊢ φ \to F : B ⟶ C \times I$
14		elxpi	$⊢ b \in (C \times I) \to \exists p \exists q (b = ⟨p, q⟩ \land (p \in C \land q \in I))$
15	10	eleq2i	$⊢ p \in C \leftrightarrow p \in {Base}_{Q}$
16		vex	$⊢ p \in V$
17	8 9 5	quselbas	$⊢ (R \in Rng \land p \in V) \to (p \in {Base}_{Q} \leftrightarrow \exists c \in B p = [c] \underset{˙}{\sim})$
18	1 16 17	sylancl	$⊢ φ \to (p \in {Base}_{Q} \leftrightarrow \exists c \in B p = [c] \underset{˙}{\sim})$
19	15 18	bitrid	$⊢ φ \to (p \in C \leftrightarrow \exists c \in B p = [c] \underset{˙}{\sim})$
20		eqid	$⊢ +_{R} = +_{R}$
21		rnggrp	$⊢ R \in Rng \to R \in Grp$
22	1 21	syl	$⊢ φ \to R \in Grp$
23	22	ad2antrr	$⊢ ((φ \land q \in I) \land c \in B) \to R \in Grp$
24		simpr	$⊢ ((φ \land q \in I) \land c \in B) \to c \in B$
25	1	ad2antrr	$⊢ ((φ \land q \in I) \land c \in B) \to R \in Rng$
26	1 2 3 4 5 6 7	rngqiprng1elbas	$⊢ φ \to \underset{˙}{1} \in B$
27	26	ad2antrr	$⊢ ((φ \land q \in I) \land c \in B) \to \underset{˙}{1} \in B$
28	5 6	rngcl	$⊢ (R \in Rng \land \underset{˙}{1} \in B \land c \in B) \to \underset{˙}{1} \underset{˙}{\cdot} c \in B$
29	25 27 24 28	syl3anc	$⊢ ((φ \land q \in I) \land c \in B) \to \underset{˙}{1} \underset{˙}{\cdot} c \in B$
30		eqid	$⊢ -_{R} = -_{R}$
31	5 30	grpsubcl	$⊢ (R \in Grp \land c \in B \land \underset{˙}{1} \underset{˙}{\cdot} c \in B) \to c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c) \in B$
32	23 24 29 31	syl3anc	$⊢ ((φ \land q \in I) \land c \in B) \to c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c) \in B$
33		eqid	$⊢ 2Ideal (R) = 2Ideal (R)$
34	5 33	2idlss	$⊢ I \in 2Ideal (R) \to I \subseteq B$
35	2 34	syl	$⊢ φ \to I \subseteq B$
36	35	sselda	$⊢ (φ \land q \in I) \to q \in B$
37	36	adantr	$⊢ ((φ \land q \in I) \land c \in B) \to q \in B$
38	5 20 23 32 37	grpcld	$⊢ ((φ \land q \in I) \land c \in B) \to (c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q \in B$
39	38	adantr	$⊢ (((φ \land q \in I) \land c \in B) \land p = [c] \underset{˙}{\sim}) \to (c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q \in B$
40		opeq1	$⊢ p = [c] \underset{˙}{\sim} \to ⟨p, q⟩ = ⟨[c] \underset{˙}{\sim}, q⟩$
41	40	adantl	$⊢ (((φ \land q \in I) \land c \in B) \land p = [c] \underset{˙}{\sim}) \to ⟨p, q⟩ = ⟨[c] \underset{˙}{\sim}, q⟩$
42		eceq1	$⊢ a = (c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q \to [a] \underset{˙}{\sim} = [((c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q)] \underset{˙}{\sim}$
43		oveq2	$⊢ a = (c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q \to \underset{˙}{1} \underset{˙}{\cdot} a = \underset{˙}{1} \underset{˙}{\cdot} ((c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q)$
44	42 43	opeq12d	$⊢ a = (c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q \to ⟨[a] \underset{˙}{\sim}, \underset{˙}{1} \underset{˙}{\cdot} a⟩ = ⟨[((c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q)] \underset{˙}{\sim}, \underset{˙}{1} \underset{˙}{\cdot} ((c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q)⟩$
45	41 44	eqeqan12d	$⊢ ((((φ \land q \in I) \land c \in B) \land p = [c] \underset{˙}{\sim}) \land a = (c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q) \to (⟨p, q⟩ = ⟨[a] \underset{˙}{\sim}, \underset{˙}{1} \underset{˙}{\cdot} a⟩ \leftrightarrow ⟨[c] \underset{˙}{\sim}, q⟩ = ⟨[((c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q)] \underset{˙}{\sim}, \underset{˙}{1} \underset{˙}{\cdot} ((c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q)⟩)$
46		rngabl	$⊢ R \in Rng \to R \in Abel$
47	1 46	syl	$⊢ φ \to R \in Abel$
48	47	ad2antrr	$⊢ ((φ \land q \in I) \land c \in B) \to R \in Abel$
49	5 20 30	ablsubaddsub	$⊢ (R \in Abel \land (c \in B \land \underset{˙}{1} \underset{˙}{\cdot} c \in B \land q \in B)) \to ((c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q) -_{R} c = q -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)$
50	48 24 29 37 49	syl13anc	$⊢ ((φ \land q \in I) \land c \in B) \to ((c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q) -_{R} c = q -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)$
51	4	ringgrpd	$⊢ φ \to J \in Grp$
52	51	ad2antrr	$⊢ ((φ \land q \in I) \land c \in B) \to J \in Grp$
53		eqid	$⊢ {Base}_{J} = {Base}_{J}$
54	2 3 53	2idlbas	$⊢ φ \to {Base}_{J} = I$
55	54	eqcomd	$⊢ φ \to I = {Base}_{J}$
56	55	eleq2d	$⊢ φ \to (q \in I \leftrightarrow q \in {Base}_{J})$
57	56	biimpa	$⊢ (φ \land q \in I) \to q \in {Base}_{J}$
58	57	adantr	$⊢ ((φ \land q \in I) \land c \in B) \to q \in {Base}_{J}$
59	1 2 3 4 5 6 7	rngqiprngghmlem1	$⊢ (φ \land c \in B) \to \underset{˙}{1} \underset{˙}{\cdot} c \in {Base}_{J}$
60	59	adantlr	$⊢ ((φ \land q \in I) \land c \in B) \to \underset{˙}{1} \underset{˙}{\cdot} c \in {Base}_{J}$
61		eqid	$⊢ -_{J} = -_{J}$
62	53 61	grpsubcl	$⊢ (J \in Grp \land q \in {Base}_{J} \land \underset{˙}{1} \underset{˙}{\cdot} c \in {Base}_{J}) \to q -_{J} (\underset{˙}{1} \underset{˙}{\cdot} c) \in {Base}_{J}$
63	52 58 60 62	syl3anc	$⊢ ((φ \land q \in I) \land c \in B) \to q -_{J} (\underset{˙}{1} \underset{˙}{\cdot} c) \in {Base}_{J}$
64		ringrng	$⊢ J \in Ring \to J \in Rng$
65	4 64	syl	$⊢ φ \to J \in Rng$
66	3 65	eqeltrrid	$⊢ φ \to R ↾_{𝑠} I \in Rng$
67	1 2 66	rng2idlnsg	$⊢ φ \to I \in NrmSGrp (R)$
68		nsgsubg	$⊢ I \in NrmSGrp (R) \to I \in SubGrp (R)$
69	67 68	syl	$⊢ φ \to I \in SubGrp (R)$
70	69	ad2antrr	$⊢ ((φ \land q \in I) \land c \in B) \to I \in SubGrp (R)$
71		simplr	$⊢ ((φ \land q \in I) \land c \in B) \to q \in I$
72	54	ad2antrr	$⊢ ((φ \land q \in I) \land c \in B) \to {Base}_{J} = I$
73	60 72	eleqtrd	$⊢ ((φ \land q \in I) \land c \in B) \to \underset{˙}{1} \underset{˙}{\cdot} c \in I$
74	30 3 61	subgsub	$⊢ (I \in SubGrp (R) \land q \in I \land \underset{˙}{1} \underset{˙}{\cdot} c \in I) \to q -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c) = q -_{J} (\underset{˙}{1} \underset{˙}{\cdot} c)$
75	70 71 73 74	syl3anc	$⊢ ((φ \land q \in I) \land c \in B) \to q -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c) = q -_{J} (\underset{˙}{1} \underset{˙}{\cdot} c)$
76	55	ad2antrr	$⊢ ((φ \land q \in I) \land c \in B) \to I = {Base}_{J}$
77	63 75 76	3eltr4d	$⊢ ((φ \land q \in I) \land c \in B) \to q -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c) \in I$
78	50 77	eqeltrd	$⊢ ((φ \land q \in I) \land c \in B) \to ((c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q) -_{R} c \in I$
79	5 30 8	qusecsub	$⊢ ((R \in Abel \land I \in SubGrp (R)) \land (c \in B \land (c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q \in B)) \to ([c] \underset{˙}{\sim} = [((c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q)] \underset{˙}{\sim} \leftrightarrow ((c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q) -_{R} c \in I)$
80	48 70 24 38 79	syl22anc	$⊢ ((φ \land q \in I) \land c \in B) \to ([c] \underset{˙}{\sim} = [((c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q)] \underset{˙}{\sim} \leftrightarrow ((c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q) -_{R} c \in I)$
81	78 80	mpbird	$⊢ ((φ \land q \in I) \land c \in B) \to [c] \underset{˙}{\sim} = [((c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q)] \underset{˙}{\sim}$
82	1 2 3 4 5 6 7	rngqiprngimfolem	$⊢ (φ \land q \in I \land c \in B) \to \underset{˙}{1} \underset{˙}{\cdot} ((c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q) = q$
83	82	3expa	$⊢ ((φ \land q \in I) \land c \in B) \to \underset{˙}{1} \underset{˙}{\cdot} ((c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q) = q$
84	83	eqcomd	$⊢ ((φ \land q \in I) \land c \in B) \to q = \underset{˙}{1} \underset{˙}{\cdot} ((c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q)$
85	81 84	opeq12d	$⊢ ((φ \land q \in I) \land c \in B) \to ⟨[c] \underset{˙}{\sim}, q⟩ = ⟨[((c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q)] \underset{˙}{\sim}, \underset{˙}{1} \underset{˙}{\cdot} ((c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q)⟩$
86	85	adantr	$⊢ (((φ \land q \in I) \land c \in B) \land p = [c] \underset{˙}{\sim}) \to ⟨[c] \underset{˙}{\sim}, q⟩ = ⟨[((c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q)] \underset{˙}{\sim}, \underset{˙}{1} \underset{˙}{\cdot} ((c -_{R} (\underset{˙}{1} \underset{˙}{\cdot} c)) +_{R} q)⟩$
87	39 45 86	rspcedvd	$⊢ (((φ \land q \in I) \land c \in B) \land p = [c] \underset{˙}{\sim}) \to \exists a \in B ⟨p, q⟩ = ⟨[a] \underset{˙}{\sim}, \underset{˙}{1} \underset{˙}{\cdot} a⟩$
88	87	rexlimdva2	$⊢ (φ \land q \in I) \to (\exists c \in B p = [c] \underset{˙}{\sim} \to \exists a \in B ⟨p, q⟩ = ⟨[a] \underset{˙}{\sim}, \underset{˙}{1} \underset{˙}{\cdot} a⟩)$
89	88	ex	$⊢ φ \to (q \in I \to (\exists c \in B p = [c] \underset{˙}{\sim} \to \exists a \in B ⟨p, q⟩ = ⟨[a] \underset{˙}{\sim}, \underset{˙}{1} \underset{˙}{\cdot} a⟩))$
90	89	com23	$⊢ φ \to (\exists c \in B p = [c] \underset{˙}{\sim} \to (q \in I \to \exists a \in B ⟨p, q⟩ = ⟨[a] \underset{˙}{\sim}, \underset{˙}{1} \underset{˙}{\cdot} a⟩))$
91	19 90	sylbid	$⊢ φ \to (p \in C \to (q \in I \to \exists a \in B ⟨p, q⟩ = ⟨[a] \underset{˙}{\sim}, \underset{˙}{1} \underset{˙}{\cdot} a⟩))$
92	91	impd	$⊢ φ \to ((p \in C \land q \in I) \to \exists a \in B ⟨p, q⟩ = ⟨[a] \underset{˙}{\sim}, \underset{˙}{1} \underset{˙}{\cdot} a⟩)$
93	92	com12	$⊢ (p \in C \land q \in I) \to (φ \to \exists a \in B ⟨p, q⟩ = ⟨[a] \underset{˙}{\sim}, \underset{˙}{1} \underset{˙}{\cdot} a⟩)$
94	93	adantl	$⊢ (b = ⟨p, q⟩ \land (p \in C \land q \in I)) \to (φ \to \exists a \in B ⟨p, q⟩ = ⟨[a] \underset{˙}{\sim}, \underset{˙}{1} \underset{˙}{\cdot} a⟩)$
95	94	imp	$⊢ ((b = ⟨p, q⟩ \land (p \in C \land q \in I)) \land φ) \to \exists a \in B ⟨p, q⟩ = ⟨[a] \underset{˙}{\sim}, \underset{˙}{1} \underset{˙}{\cdot} a⟩$
96		simplll	$⊢ (((b = ⟨p, q⟩ \land (p \in C \land q \in I)) \land φ) \land a \in B) \to b = ⟨p, q⟩$
97	1 2 3 4 5 6 7 8 9 10 11 12	rngqiprngimfv	$⊢ (φ \land a \in B) \to F (a) = ⟨[a] \underset{˙}{\sim}, \underset{˙}{1} \underset{˙}{\cdot} a⟩$
98	97	adantll	$⊢ (((b = ⟨p, q⟩ \land (p \in C \land q \in I)) \land φ) \land a \in B) \to F (a) = ⟨[a] \underset{˙}{\sim}, \underset{˙}{1} \underset{˙}{\cdot} a⟩$
99	96 98	eqeq12d	$⊢ (((b = ⟨p, q⟩ \land (p \in C \land q \in I)) \land φ) \land a \in B) \to (b = F (a) \leftrightarrow ⟨p, q⟩ = ⟨[a] \underset{˙}{\sim}, \underset{˙}{1} \underset{˙}{\cdot} a⟩)$
100	99	rexbidva	$⊢ ((b = ⟨p, q⟩ \land (p \in C \land q \in I)) \land φ) \to (\exists a \in B b = F (a) \leftrightarrow \exists a \in B ⟨p, q⟩ = ⟨[a] \underset{˙}{\sim}, \underset{˙}{1} \underset{˙}{\cdot} a⟩)$
101	95 100	mpbird	$⊢ ((b = ⟨p, q⟩ \land (p \in C \land q \in I)) \land φ) \to \exists a \in B b = F (a)$
102	101	ex	$⊢ (b = ⟨p, q⟩ \land (p \in C \land q \in I)) \to (φ \to \exists a \in B b = F (a))$
103	102	exlimivv	$⊢ \exists p \exists q (b = ⟨p, q⟩ \land (p \in C \land q \in I)) \to (φ \to \exists a \in B b = F (a))$
104	14 103	syl	$⊢ b \in (C \times I) \to (φ \to \exists a \in B b = F (a))$
105	104	impcom	$⊢ (φ \land b \in (C \times I)) \to \exists a \in B b = F (a)$
106	105	ralrimiva	$⊢ φ \to \forall b \in (C \times I) \exists a \in B b = F (a)$
107		dffo3	$⊢ F : B \underset{onto}{⟶} C \times I \leftrightarrow (F : B ⟶ C \times I \land \forall b \in (C \times I) \exists a \in B b = F (a))$
108	13 106 107	sylanbrc	$⊢ φ \to F : B \underset{onto}{⟶} C \times I$

Metamath Proof Explorer

Theorem rngqiprngimfo

Proof