Theorem qusmgm

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

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

Proof

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