qusring2

Description: The quotient structure of a ring is a ring. (Contributed by Mario Carneiro, 14-Jun-2015)

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

Proof

Step	Hyp	Ref	Expression
1		qusring2.u	$⊢ φ \to U = R /_{𝑠} \underset{˙}{\sim}$
2		qusring2.v	$⊢ φ \to V = {Base}_{R}$
3		qusring2.p	$⊢ \underset{˙}{+} = +_{R}$
4		qusring2.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		qusring2.o	$⊢ \underset{˙}{1} = 1_{R}$
6		qusring2.r	$⊢ φ \to \underset{˙}{\sim} Er V$
7		qusring2.e1	$⊢ φ \to ((a \underset{˙}{\sim} p \land b \underset{˙}{\sim} q) \to (a \underset{˙}{+} b) \underset{˙}{\sim} (p \underset{˙}{+} q))$
8		qusring2.e2	$⊢ φ \to ((a \underset{˙}{\sim} p \land b \underset{˙}{\sim} q) \to (a \underset{˙}{\cdot} b) \underset{˙}{\sim} (p \underset{˙}{\cdot} q))$
9		qusring2.x	$⊢ φ \to R \in Ring$
10		eqid	$⊢ (u \in V ⟼ [u] \underset{˙}{\sim}) = (u \in V ⟼ [u] \underset{˙}{\sim})$
11		fvex	$⊢ {Base}_{R} \in V$
12	2 11	eqeltrdi	$⊢ φ \to V \in V$
13		erex	$⊢ \underset{˙}{\sim} Er V \to (V \in V \to \underset{˙}{\sim} \in V)$
14	6 12 13	sylc	$⊢ φ \to \underset{˙}{\sim} \in V$
15	1 2 10 14 9	qusval	$⊢ φ \to U = (u \in V ⟼ [u] \underset{˙}{\sim}) “_{𝑠} R$
16	1 2 10 14 9	quslem	$⊢ φ \to (u \in V ⟼ [u] \underset{˙}{\sim}) : V \underset{onto}{⟶} V / \underset{˙}{\sim}$
17	9	adantr	$⊢ (φ \land (x \in V \land y \in V)) \to R \in Ring$
18		simprl	$⊢ (φ \land (x \in V \land y \in V)) \to x \in V$
19	2	adantr	$⊢ (φ \land (x \in V \land y \in V)) \to V = {Base}_{R}$
20	18 19	eleqtrd	$⊢ (φ \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	21 19	eleqtrd	$⊢ (φ \land (x \in V \land y \in V)) \to y \in {Base}_{R}$
23		eqid	$⊢ {Base}_{R} = {Base}_{R}$
24	23 3	ringacl	$⊢ (R \in Ring \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x \underset{˙}{+} y \in {Base}_{R}$
25	17 20 22 24	syl3anc	$⊢ (φ \land (x \in V \land y \in V)) \to x \underset{˙}{+} y \in {Base}_{R}$
26	25 19	eleqtrrd	$⊢ (φ \land (x \in V \land y \in V)) \to x \underset{˙}{+} y \in V$
27	6 12 10 26 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{˙}{+} b) = (u \in V ⟼ [u] \underset{˙}{\sim}) (p \underset{˙}{+} q))$
28	23 4	ringcl	$⊢ (R \in Ring \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x \underset{˙}{\cdot} y \in {Base}_{R}$
29	17 20 22 28	syl3anc	$⊢ (φ \land (x \in V \land y \in V)) \to x \underset{˙}{\cdot} y \in {Base}_{R}$
30	29 19	eleqtrrd	$⊢ (φ \land (x \in V \land y \in V)) \to x \underset{˙}{\cdot} y \in V$
31	6 12 10 30 8	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))$
32	15 2 3 4 5 16 27 31 9	imasring	$⊢ φ \to (U \in Ring \land (u \in V ⟼ [u] \underset{˙}{\sim}) (\underset{˙}{1}) = 1_{U})$
33	6 12 10	divsfval	$⊢ φ \to (u \in V ⟼ [u] \underset{˙}{\sim}) (\underset{˙}{1}) = [\underset{˙}{1}] \underset{˙}{\sim}$
34	33	eqcomd	$⊢ φ \to [\underset{˙}{1}] \underset{˙}{\sim} = (u \in V ⟼ [u] \underset{˙}{\sim}) (\underset{˙}{1})$
35	34	eqeq1d	$⊢ φ \to ([\underset{˙}{1}] \underset{˙}{\sim} = 1_{U} \leftrightarrow (u \in V ⟼ [u] \underset{˙}{\sim}) (\underset{˙}{1}) = 1_{U})$
36	35	anbi2d	$⊢ φ \to ((U \in Ring \land [\underset{˙}{1}] \underset{˙}{\sim} = 1_{U}) \leftrightarrow (U \in Ring \land (u \in V ⟼ [u] \underset{˙}{\sim}) (\underset{˙}{1}) = 1_{U}))$
37	32 36	mpbird	$⊢ φ \to (U \in Ring \land [\underset{˙}{1}] \underset{˙}{\sim} = 1_{U})$

Metamath Proof Explorer

Theorem qusring2

Proof