Theorem qusmgm

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

	Ref	Expression
Hypotheses	qusmgm.u	$$⊢\phi \to U=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
	qusmgm.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
	qusmgm.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	qusmgm.r	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}V$$
	qusmgm.x	$$⊢\phi \to R\in X$$
	qusmgm.e	$$⊢\phi \to \left(\left(a\underset{\dot{}}{\sim }p\wedge b\underset{\dot{}}{\sim }q\right)\to \left(a\underset{\dot{}}{+}b\right)\underset{\dot{}}{\sim }\left(p\underset{\dot{}}{+}q\right)\right)$$
	qusmgm.1	$$⊢\left(\phi \wedge x\in V\wedge y\in V\right)\to x\underset{\dot{}}{+}y\in V$$
	qusmgm.2	$$⊢\phi \to \underset{\dot{}}{0}\in V$$
	qusmgm.3	$$⊢\left(\phi \wedge x\in V\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{+}x\right)\underset{\dot{}}{\sim }x$$
	qusmgm.4	$$⊢\left(\phi \wedge x\in V\right)\to \left(x\underset{\dot{}}{+}\underset{\dot{}}{0}\right)\underset{\dot{}}{\sim }x$$
Assertion	qusmgm	$$⊢\phi \to \left(U\in \mathrm{Mgm}\wedge \left[\underset{\dot{}}{0}\right]\underset{\dot{}}{\sim }=0_U\right)$$

Proof

Step	Hyp	Ref	Expression
1		qusmgm.u	$$⊢\phi \to U=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
2		qusmgm.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
3		qusmgm.p	$$⊢\underset{\dot{}}{+}={+}_R$$
4		qusmgm.r	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}V$$
5		qusmgm.x	$$⊢\phi \to R\in X$$
6		qusmgm.e	$$⊢\phi \to \left(\left(a\underset{\dot{}}{\sim }p\wedge b\underset{\dot{}}{\sim }q\right)\to \left(a\underset{\dot{}}{+}b\right)\underset{\dot{}}{\sim }\left(p\underset{\dot{}}{+}q\right)\right)$$
7		qusmgm.1	$$⊢\left(\phi \wedge x\in V\wedge y\in V\right)\to x\underset{\dot{}}{+}y\in V$$
8		qusmgm.2	$$⊢\phi \to \underset{\dot{}}{0}\in V$$
9		qusmgm.3	$$⊢\left(\phi \wedge x\in V\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{+}x\right)\underset{\dot{}}{\sim }x$$
10		qusmgm.4	$$⊢\left(\phi \wedge x\in V\right)\to \left(x\underset{\dot{}}{+}\underset{\dot{}}{0}\right)\underset{\dot{}}{\sim }x$$
11		eqid	$$⊢\left(u\in V⟼\left[u\right]\underset{\dot{}}{\sim }\right)=\left(u\in V⟼\left[u\right]\underset{\dot{}}{\sim }\right)$$
12		fvex	$$⊢{\mathrm{Base}}_R\in \mathrm{V}$$
13	2 12	eqeltrdi	$$⊢\phi \to V\in \mathrm{V}$$
14		erex	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}V\to \left(V\in \mathrm{V}\to \underset{\dot{}}{\sim }\in \mathrm{V}\right)$$
15	4 13 14	sylc	$$⊢\phi \to \underset{\dot{}}{\sim }\in \mathrm{V}$$
16	1 2 11 15 5	qusval	$$⊢\phi \to U=\left(u\in V⟼\left[u\right]\underset{\dot{}}{\sim }\right){“}_{𝑠}R$$
17	1 2 11 15 5	quslem	$$⊢\phi \to \left(u\in V⟼\left[u\right]\underset{\dot{}}{\sim }\right):V\underset{onto}{⟶}V/\underset{\dot{}}{\sim }$$
18	7	3expb	$$⊢\left(\phi \wedge \left(x\in V\wedge y\in V\right)\right)\to x\underset{\dot{}}{+}y\in V$$
19	4 13 11 18 6	ercpbl	$$⊢\left(\phi \wedge \left(a\in V\wedge b\in V\right)\wedge \left(p\in V\wedge q\in V\right)\right)\to \left(\left(\left(u\in V⟼\left[u\right]\underset{\dot{}}{\sim }\right)\left(a\right)=\left(u\in V⟼\left[u\right]\underset{\dot{}}{\sim }\right)\left(p\right)\wedge \left(u\in V⟼\left[u\right]\underset{\dot{}}{\sim }\right)\left(b\right)=\left(u\in V⟼\left[u\right]\underset{\dot{}}{\sim }\right)\left(q\right)\right)\to \left(u\in V⟼\left[u\right]\underset{\dot{}}{\sim }\right)\left(a\underset{\dot{}}{+}b\right)=\left(u\in V⟼\left[u\right]\underset{\dot{}}{\sim }\right)\left(p\underset{\dot{}}{+}q\right)\right)$$
20	4	adantr	$$⊢\left(\phi \wedge x\in V\right)\to \underset{\dot{}}{\sim }\mathrm{Er}V$$
21	20 9	erthi	$$⊢\left(\phi \wedge x\in V\right)\to \left[\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x\right)\right]\underset{\dot{}}{\sim }=\left[x\right]\underset{\dot{}}{\sim }$$
22	13	adantr	$$⊢\left(\phi \wedge x\in V\right)\to V\in \mathrm{V}$$
23	20 22 11	divsfval	$$⊢\left(\phi \wedge x\in V\right)\to \left(u\in V⟼\left[u\right]\underset{\dot{}}{\sim }\right)\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x\right)=\left[\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x\right)\right]\underset{\dot{}}{\sim }$$
24	20 22 11	divsfval	$$⊢\left(\phi \wedge x\in V\right)\to \left(u\in V⟼\left[u\right]\underset{\dot{}}{\sim }\right)\left(x\right)=\left[x\right]\underset{\dot{}}{\sim }$$
25	21 23 24	3eqtr4d	$$⊢\left(\phi \wedge x\in V\right)\to \left(u\in V⟼\left[u\right]\underset{\dot{}}{\sim }\right)\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x\right)=\left(u\in V⟼\left[u\right]\underset{\dot{}}{\sim }\right)\left(x\right)$$
26	20 10	erthi	$$⊢\left(\phi \wedge x\in V\right)\to \left[\left(x\underset{\dot{}}{+}\underset{\dot{}}{0}\right)\right]\underset{\dot{}}{\sim }=\left[x\right]\underset{\dot{}}{\sim }$$
27	20 22 11	divsfval	$$⊢\left(\phi \wedge x\in V\right)\to \left(u\in V⟼\left[u\right]\underset{\dot{}}{\sim }\right)\left(x\underset{\dot{}}{+}\underset{\dot{}}{0}\right)=\left[\left(x\underset{\dot{}}{+}\underset{\dot{}}{0}\right)\right]\underset{\dot{}}{\sim }$$
28	26 27 24	3eqtr4d	$$⊢\left(\phi \wedge x\in V\right)\to \left(u\in V⟼\left[u\right]\underset{\dot{}}{\sim }\right)\left(x\underset{\dot{}}{+}\underset{\dot{}}{0}\right)=\left(u\in V⟼\left[u\right]\underset{\dot{}}{\sim }\right)\left(x\right)$$
29	16 2 3 17 19 5 7 8 25 28	imasmgm2	$$⊢\phi \to \left(U\in \mathrm{Mgm}\wedge \left(u\in V⟼\left[u\right]\underset{\dot{}}{\sim }\right)\left(\underset{\dot{}}{0}\right)=0_U\right)$$
30	4 13 11	divsfval	$$⊢\phi \to \left(u\in V⟼\left[u\right]\underset{\dot{}}{\sim }\right)\left(\underset{\dot{}}{0}\right)=\left[\underset{\dot{}}{0}\right]\underset{\dot{}}{\sim }$$
31	30	eqcomd	$$⊢\phi \to \left[\underset{\dot{}}{0}\right]\underset{\dot{}}{\sim }=\left(u\in V⟼\left[u\right]\underset{\dot{}}{\sim }\right)\left(\underset{\dot{}}{0}\right)$$
32	31	eqeq1d	$$⊢\phi \to \left(\left[\underset{\dot{}}{0}\right]\underset{\dot{}}{\sim }=0_U\leftrightarrow \left(u\in V⟼\left[u\right]\underset{\dot{}}{\sim }\right)\left(\underset{\dot{}}{0}\right)=0_U\right)$$
33	32	anbi2d	$$⊢\phi \to \left(\left(U\in \mathrm{Mgm}\wedge \left[\underset{\dot{}}{0}\right]\underset{\dot{}}{\sim }=0_U\right)\leftrightarrow \left(U\in \mathrm{Mgm}\wedge \left(u\in V⟼\left[u\right]\underset{\dot{}}{\sim }\right)\left(\underset{\dot{}}{0}\right)=0_U\right)\right)$$
34	29 33	mpbird	$$⊢\phi \to \left(U\in \mathrm{Mgm}\wedge \left[\underset{\dot{}}{0}\right]\underset{\dot{}}{\sim }=0_U\right)$$