qusmnd

Description: Prove that a quotient structure is a monoid. (Contributed by Thierry Arnoux, 31-Aug-2026)

	Ref	Expression
Hypotheses	qusmnd.u	$⊢ φ \to U = R /_{𝑠} \underset{˙}{\sim}$
	qusmnd.v	$⊢ φ \to V = {Base}_{R}$
	qusmnd.p	$⊢ \underset{˙}{+} = +_{R}$
	qusmnd.r	$⊢ φ \to \underset{˙}{\sim} Er V$
	qusmnd.x	$⊢ φ \to R \in X$
	qusmnd.e	$⊢ φ \to ((a \underset{˙}{\sim} p \land b \underset{˙}{\sim} q) \to (a \underset{˙}{+} b) \underset{˙}{\sim} (p \underset{˙}{+} q))$
	qusmnd.1	$⊢ (φ \land x \in V \land y \in V) \to x \underset{˙}{+} y \in V$
	qusmnd.2	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to ((x \underset{˙}{+} y) \underset{˙}{+} z) \underset{˙}{\sim} (x \underset{˙}{+} (y \underset{˙}{+} z))$
	qusmnd.3	$⊢ φ \to \underset{˙}{0} \in V$
	qusmnd.4	$⊢ (φ \land x \in V) \to (\underset{˙}{0} \underset{˙}{+} x) \underset{˙}{\sim} x$
	qusmnd.5	$⊢ (φ \land x \in V) \to (x \underset{˙}{+} \underset{˙}{0}) \underset{˙}{\sim} x$
Assertion	qusmnd	$⊢ φ \to (U \in Mnd \land [\underset{˙}{0}] \underset{˙}{\sim} = 0_{U})$

Proof

Step	Hyp	Ref	Expression
1		qusmnd.u	$⊢ φ \to U = R /_{𝑠} \underset{˙}{\sim}$
2		qusmnd.v	$⊢ φ \to V = {Base}_{R}$
3		qusmnd.p	$⊢ \underset{˙}{+} = +_{R}$
4		qusmnd.r	$⊢ φ \to \underset{˙}{\sim} Er V$
5		qusmnd.x	$⊢ φ \to R \in X$
6		qusmnd.e	$⊢ φ \to ((a \underset{˙}{\sim} p \land b \underset{˙}{\sim} q) \to (a \underset{˙}{+} b) \underset{˙}{\sim} (p \underset{˙}{+} q))$
7		qusmnd.1	$⊢ (φ \land x \in V \land y \in V) \to x \underset{˙}{+} y \in V$
8		qusmnd.2	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to ((x \underset{˙}{+} y) \underset{˙}{+} z) \underset{˙}{\sim} (x \underset{˙}{+} (y \underset{˙}{+} z))$
9		qusmnd.3	$⊢ φ \to \underset{˙}{0} \in V$
10		qusmnd.4	$⊢ (φ \land x \in V) \to (\underset{˙}{0} \underset{˙}{+} x) \underset{˙}{\sim} x$
11		qusmnd.5	$⊢ (φ \land x \in V) \to (x \underset{˙}{+} \underset{˙}{0}) \underset{˙}{\sim} x$
12		eqid	$⊢ (u \in V ⟼ [u] \underset{˙}{\sim}) = (u \in V ⟼ [u] \underset{˙}{\sim})$
13		fvex	$⊢ {Base}_{R} \in V$
14	2 13	eqeltrdi	$⊢ φ \to V \in V$
15		erex	$⊢ \underset{˙}{\sim} Er V \to (V \in V \to \underset{˙}{\sim} \in V)$
16	4 14 15	sylc	$⊢ φ \to \underset{˙}{\sim} \in V$
17	1 2 12 16 5	qusval	$⊢ φ \to U = (u \in V ⟼ [u] \underset{˙}{\sim}) “_{𝑠} R$
18	1 2 12 16 5	quslem	$⊢ φ \to (u \in V ⟼ [u] \underset{˙}{\sim}) : V \underset{onto}{⟶} V / \underset{˙}{\sim}$
19	7	3expb	$⊢ (φ \land (x \in V \land y \in V)) \to x \underset{˙}{+} y \in V$
20	4 14 12 19 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))$
21	4	adantr	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to \underset{˙}{\sim} Er V$
22	21 8	erthi	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to [((x \underset{˙}{+} y) \underset{˙}{+} z)] \underset{˙}{\sim} = [(x \underset{˙}{+} (y \underset{˙}{+} z))] \underset{˙}{\sim}$
23	14	adantr	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to V \in V$
24	21 23 12	divsfval	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to (u \in V ⟼ [u] \underset{˙}{\sim}) ((x \underset{˙}{+} y) \underset{˙}{+} z) = [((x \underset{˙}{+} y) \underset{˙}{+} z)] \underset{˙}{\sim}$
25	21 23 12	divsfval	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to (u \in V ⟼ [u] \underset{˙}{\sim}) (x \underset{˙}{+} (y \underset{˙}{+} z)) = [(x \underset{˙}{+} (y \underset{˙}{+} z))] \underset{˙}{\sim}$
26	22 24 25	3eqtr4d	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to (u \in V ⟼ [u] \underset{˙}{\sim}) ((x \underset{˙}{+} y) \underset{˙}{+} z) = (u \in V ⟼ [u] \underset{˙}{\sim}) (x \underset{˙}{+} (y \underset{˙}{+} z))$
27	4	adantr	$⊢ (φ \land x \in V) \to \underset{˙}{\sim} Er V$
28	27 10	erthi	$⊢ (φ \land x \in V) \to [(\underset{˙}{0} \underset{˙}{+} x)] \underset{˙}{\sim} = [x] \underset{˙}{\sim}$
29	14	adantr	$⊢ (φ \land x \in V) \to V \in V$
30	27 29 12	divsfval	$⊢ (φ \land x \in V) \to (u \in V ⟼ [u] \underset{˙}{\sim}) (\underset{˙}{0} \underset{˙}{+} x) = [(\underset{˙}{0} \underset{˙}{+} x)] \underset{˙}{\sim}$
31	27 29 12	divsfval	$⊢ (φ \land x \in V) \to (u \in V ⟼ [u] \underset{˙}{\sim}) (x) = [x] \underset{˙}{\sim}$
32	28 30 31	3eqtr4d	$⊢ (φ \land x \in V) \to (u \in V ⟼ [u] \underset{˙}{\sim}) (\underset{˙}{0} \underset{˙}{+} x) = (u \in V ⟼ [u] \underset{˙}{\sim}) (x)$
33	27 11	erthi	$⊢ (φ \land x \in V) \to [(x \underset{˙}{+} \underset{˙}{0})] \underset{˙}{\sim} = [x] \underset{˙}{\sim}$
34	27 29 12	divsfval	$⊢ (φ \land x \in V) \to (u \in V ⟼ [u] \underset{˙}{\sim}) (x \underset{˙}{+} \underset{˙}{0}) = [(x \underset{˙}{+} \underset{˙}{0})] \underset{˙}{\sim}$
35	33 34 31	3eqtr4d	$⊢ (φ \land x \in V) \to (u \in V ⟼ [u] \underset{˙}{\sim}) (x \underset{˙}{+} \underset{˙}{0}) = (u \in V ⟼ [u] \underset{˙}{\sim}) (x)$
36	17 2 3 18 20 5 7 26 9 32 35	imasmnd2	$⊢ φ \to (U \in Mnd \land (u \in V ⟼ [u] \underset{˙}{\sim}) (\underset{˙}{0}) = 0_{U})$
37	4 14 12	divsfval	$⊢ φ \to (u \in V ⟼ [u] \underset{˙}{\sim}) (\underset{˙}{0}) = [\underset{˙}{0}] \underset{˙}{\sim}$
38	37	eqcomd	$⊢ φ \to [\underset{˙}{0}] \underset{˙}{\sim} = (u \in V ⟼ [u] \underset{˙}{\sim}) (\underset{˙}{0})$
39	38	eqeq1d	$⊢ φ \to ([\underset{˙}{0}] \underset{˙}{\sim} = 0_{U} \leftrightarrow (u \in V ⟼ [u] \underset{˙}{\sim}) (\underset{˙}{0}) = 0_{U})$
40	39	anbi2d	$⊢ φ \to ((U \in Mnd \land [\underset{˙}{0}] \underset{˙}{\sim} = 0_{U}) \leftrightarrow (U \in Mnd \land (u \in V ⟼ [u] \underset{˙}{\sim}) (\underset{˙}{0}) = 0_{U}))$
41	36 40	mpbird	$⊢ φ \to (U \in Mnd \land [\underset{˙}{0}] \underset{˙}{\sim} = 0_{U})$

Metamath Proof Explorer

Theorem qusmnd

Proof