Theorem qusmnd

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

	Ref	Expression
Hypotheses	qusmnd.u	⊢ ( 𝜑 → 𝑈 = ( 𝑅 /s ∼ ) )
	qusmnd.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
	qusmnd.p	⊢ + = ( +g ‘ 𝑅 )
	qusmnd.r	⊢ ( 𝜑 → ∼ Er 𝑉 )
	qusmnd.x	⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
	qusmnd.e	⊢ ( 𝜑 → ( ( 𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞 ) → ( 𝑎 + 𝑏 ) ∼ ( 𝑝 + 𝑞 ) ) )
	qusmnd.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
	qusmnd.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) ∼ ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
	qusmnd.3	⊢ ( 𝜑 → 0 ∈ 𝑉 )
	qusmnd.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 0 + 𝑥 ) ∼ 𝑥 )
	qusmnd.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝑥 + 0 ) ∼ 𝑥 )
Assertion	qusmnd	⊢ ( 𝜑 → ( 𝑈 ∈ Mnd ∧ [ 0 ] ∼ = ( 0g ‘ 𝑈 ) ) )

Proof

Step	Hyp	Ref	Expression
1		qusmnd.u	⊢ ( 𝜑 → 𝑈 = ( 𝑅 /s ∼ ) )
2		qusmnd.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3		qusmnd.p	⊢ + = ( +g ‘ 𝑅 )
4		qusmnd.r	⊢ ( 𝜑 → ∼ Er 𝑉 )
5		qusmnd.x	⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
6		qusmnd.e	⊢ ( 𝜑 → ( ( 𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞 ) → ( 𝑎 + 𝑏 ) ∼ ( 𝑝 + 𝑞 ) ) )
7		qusmnd.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
8		qusmnd.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) ∼ ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
9		qusmnd.3	⊢ ( 𝜑 → 0 ∈ 𝑉 )
10		qusmnd.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 0 + 𝑥 ) ∼ 𝑥 )
11		qusmnd.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝑥 + 0 ) ∼ 𝑥 )
12		eqid	⊢ ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) = ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ )
13		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
14	2 13	eqeltrdi	⊢ ( 𝜑 → 𝑉 ∈ V )
15		erex	⊢ ( ∼ Er 𝑉 → ( 𝑉 ∈ V → ∼ ∈ V ) )
16	4 14 15	sylc	⊢ ( 𝜑 → ∼ ∈ V )
17	1 2 12 16 5	qusval	⊢ ( 𝜑 → 𝑈 = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) “s 𝑅 ) )
18	1 2 12 16 5	quslem	⊢ ( 𝜑 → ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) : 𝑉 –onto→ ( 𝑉 / ∼ ) )
19	7	3expb	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
20	4 14 12 19 6	ercpbl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 𝑎 ) = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 𝑝 ) ∧ ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 𝑏 ) = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 𝑞 ) ) → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( 𝑎 + 𝑏 ) ) = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( 𝑝 + 𝑞 ) ) ) )
21	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ∼ Er 𝑉 )
22	21 8	erthi	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → [ ( ( 𝑥 + 𝑦 ) + 𝑧 ) ] ∼ = [ ( 𝑥 + ( 𝑦 + 𝑧 ) ) ] ∼ )
23	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑉 ∈ V )
24	21 23 12	divsfval	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( ( 𝑥 + 𝑦 ) + 𝑧 ) ) = [ ( ( 𝑥 + 𝑦 ) + 𝑧 ) ] ∼ )
25	21 23 12	divsfval	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) = [ ( 𝑥 + ( 𝑦 + 𝑧 ) ) ] ∼ )
26	22 24 25	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( ( 𝑥 + 𝑦 ) + 𝑧 ) ) = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) )
27	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ∼ Er 𝑉 )
28	27 10	erthi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → [ ( 0 + 𝑥 ) ] ∼ = [ 𝑥 ] ∼ )
29	14	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑉 ∈ V )
30	27 29 12	divsfval	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( 0 + 𝑥 ) ) = [ ( 0 + 𝑥 ) ] ∼ )
31	27 29 12	divsfval	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 𝑥 ) = [ 𝑥 ] ∼ )
32	28 30 31	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( 0 + 𝑥 ) ) = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 𝑥 ) )
33	27 11	erthi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → [ ( 𝑥 + 0 ) ] ∼ = [ 𝑥 ] ∼ )
34	27 29 12	divsfval	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( 𝑥 + 0 ) ) = [ ( 𝑥 + 0 ) ] ∼ )
35	33 34 31	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( 𝑥 + 0 ) ) = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 𝑥 ) )
36	17 2 3 18 20 5 7 26 9 32 35	imasmnd2	⊢ ( 𝜑 → ( 𝑈 ∈ Mnd ∧ ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 0 ) = ( 0g ‘ 𝑈 ) ) )
37	4 14 12	divsfval	⊢ ( 𝜑 → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 0 ) = [ 0 ] ∼ )
38	37	eqcomd	⊢ ( 𝜑 → [ 0 ] ∼ = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 0 ) )
39	38	eqeq1d	⊢ ( 𝜑 → ( [ 0 ] ∼ = ( 0g ‘ 𝑈 ) ↔ ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 0 ) = ( 0g ‘ 𝑈 ) ) )
40	39	anbi2d	⊢ ( 𝜑 → ( ( 𝑈 ∈ Mnd ∧ [ 0 ] ∼ = ( 0g ‘ 𝑈 ) ) ↔ ( 𝑈 ∈ Mnd ∧ ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) )
41	36 40	mpbird	⊢ ( 𝜑 → ( 𝑈 ∈ Mnd ∧ [ 0 ] ∼ = ( 0g ‘ 𝑈 ) ) )