qusrng

Description: The quotient structure of a non-unital ring is a non-unital ring ( qusring2 analog). (Contributed by AV, 23-Feb-2025)

	Ref	Expression
Hypotheses	qusrng.u	$⊢ φ \to U = R /_{𝑠} \underset{˙}{\sim}$
	qusrng.v	$⊢ φ \to V = {Base}_{R}$
	qusrng.p	$⊢ \underset{˙}{+} = +_{R}$
	qusrng.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	qusrng.r	$⊢ φ \to \underset{˙}{\sim} Er V$
	qusrng.e1	$⊢ φ \to ((a \underset{˙}{\sim} p \land b \underset{˙}{\sim} q) \to (a \underset{˙}{+} b) \underset{˙}{\sim} (p \underset{˙}{+} q))$
	qusrng.e2	$⊢ φ \to ((a \underset{˙}{\sim} p \land b \underset{˙}{\sim} q) \to (a \underset{˙}{\cdot} b) \underset{˙}{\sim} (p \underset{˙}{\cdot} q))$
	qusrng.x	$⊢ φ \to R \in Rng$
Assertion	qusrng	$⊢ φ \to U \in Rng$

Proof

Step	Hyp	Ref	Expression
1		qusrng.u	$⊢ φ \to U = R /_{𝑠} \underset{˙}{\sim}$
2		qusrng.v	$⊢ φ \to V = {Base}_{R}$
3		qusrng.p	$⊢ \underset{˙}{+} = +_{R}$
4		qusrng.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		qusrng.r	$⊢ φ \to \underset{˙}{\sim} Er V$
6		qusrng.e1	$⊢ φ \to ((a \underset{˙}{\sim} p \land b \underset{˙}{\sim} q) \to (a \underset{˙}{+} b) \underset{˙}{\sim} (p \underset{˙}{+} q))$
7		qusrng.e2	$⊢ φ \to ((a \underset{˙}{\sim} p \land b \underset{˙}{\sim} q) \to (a \underset{˙}{\cdot} b) \underset{˙}{\sim} (p \underset{˙}{\cdot} q))$
8		qusrng.x	$⊢ φ \to R \in Rng$
9		eqid	$⊢ (u \in V ⟼ [u] \underset{˙}{\sim}) = (u \in V ⟼ [u] \underset{˙}{\sim})$
10		fvex	$⊢ {Base}_{R} \in V$
11	2 10	eqeltrdi	$⊢ φ \to V \in V$
12		erex	$⊢ \underset{˙}{\sim} Er V \to (V \in V \to \underset{˙}{\sim} \in V)$
13	5 11 12	sylc	$⊢ φ \to \underset{˙}{\sim} \in V$
14	1 2 9 13 8	qusval	$⊢ φ \to U = (u \in V ⟼ [u] \underset{˙}{\sim}) “_{𝑠} R$
15	1 2 9 13 8	quslem	$⊢ φ \to (u \in V ⟼ [u] \underset{˙}{\sim}) : V \underset{onto}{⟶} V / \underset{˙}{\sim}$
16	8	adantr	$⊢ (φ \land (x \in V \land y \in V)) \to R \in Rng$
17		simprl	$⊢ (φ \land (x \in V \land y \in V)) \to x \in V$
18	2	eleq2d	$⊢ φ \to (x \in V \leftrightarrow x \in {Base}_{R})$
19	18	adantr	$⊢ (φ \land (x \in V \land y \in V)) \to (x \in V \leftrightarrow x \in {Base}_{R})$
20	17 19	mpbid	$⊢ (φ \land (x \in V \land y \in V)) \to x \in {Base}_{R}$
21		simprr	$⊢ (φ \land (x \in V \land y \in V)) \to y \in V$
22	2	eleq2d	$⊢ φ \to (y \in V \leftrightarrow y \in {Base}_{R})$
23	22	adantr	$⊢ (φ \land (x \in V \land y \in V)) \to (y \in V \leftrightarrow y \in {Base}_{R})$
24	21 23	mpbid	$⊢ (φ \land (x \in V \land y \in V)) \to y \in {Base}_{R}$
25		eqid	$⊢ {Base}_{R} = {Base}_{R}$
26	25 3	rngacl	$⊢ (R \in Rng \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x \underset{˙}{+} y \in {Base}_{R}$
27	16 20 24 26	syl3anc	$⊢ (φ \land (x \in V \land y \in V)) \to x \underset{˙}{+} y \in {Base}_{R}$
28	2	eleq2d	$⊢ φ \to (x \underset{˙}{+} y \in V \leftrightarrow x \underset{˙}{+} y \in {Base}_{R})$
29	28	adantr	$⊢ (φ \land (x \in V \land y \in V)) \to (x \underset{˙}{+} y \in V \leftrightarrow x \underset{˙}{+} y \in {Base}_{R})$
30	27 29	mpbird	$⊢ (φ \land (x \in V \land y \in V)) \to x \underset{˙}{+} y \in V$
31	5 11 9 30 6	ercpbl	$⊢ (φ \land (a \in V \land b \in V) \land (p \in V \land q \in V)) \to (((u \in V ⟼ [u] \underset{˙}{\sim}) (a) = (u \in V ⟼ [u] \underset{˙}{\sim}) (p) \land (u \in V ⟼ [u] \underset{˙}{\sim}) (b) = (u \in V ⟼ [u] \underset{˙}{\sim}) (q)) \to (u \in V ⟼ [u] \underset{˙}{\sim}) (a \underset{˙}{+} b) = (u \in V ⟼ [u] \underset{˙}{\sim}) (p \underset{˙}{+} q))$
32	25 4	rngcl	$⊢ (R \in Rng \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x \underset{˙}{\cdot} y \in {Base}_{R}$
33	16 20 24 32	syl3anc	$⊢ (φ \land (x \in V \land y \in V)) \to x \underset{˙}{\cdot} y \in {Base}_{R}$
34	2	eleq2d	$⊢ φ \to (x \underset{˙}{\cdot} y \in V \leftrightarrow x \underset{˙}{\cdot} y \in {Base}_{R})$
35	34	adantr	$⊢ (φ \land (x \in V \land y \in V)) \to (x \underset{˙}{\cdot} y \in V \leftrightarrow x \underset{˙}{\cdot} y \in {Base}_{R})$
36	33 35	mpbird	$⊢ (φ \land (x \in V \land y \in V)) \to x \underset{˙}{\cdot} y \in V$
37	5 11 9 36 7	ercpbl	$⊢ (φ \land (a \in V \land b \in V) \land (p \in V \land q \in V)) \to (((u \in V ⟼ [u] \underset{˙}{\sim}) (a) = (u \in V ⟼ [u] \underset{˙}{\sim}) (p) \land (u \in V ⟼ [u] \underset{˙}{\sim}) (b) = (u \in V ⟼ [u] \underset{˙}{\sim}) (q)) \to (u \in V ⟼ [u] \underset{˙}{\sim}) (a \underset{˙}{\cdot} b) = (u \in V ⟼ [u] \underset{˙}{\sim}) (p \underset{˙}{\cdot} q))$
38	14 2 3 4 15 31 37 8	imasrng	$⊢ φ \to U \in Rng$

Metamath Proof Explorer

Theorem qusrng

Proof