Theorem qusaddflem

Description: The operation of a quotient structure is a function. (Contributed by Mario Carneiro, 24-Feb-2015)

	Ref	Expression
Hypotheses	qusaddf.u	⊢ ( 𝜑 → 𝑈 = ( 𝑅 /s ∼ ) )
	qusaddf.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
	qusaddf.r	⊢ ( 𝜑 → ∼ Er 𝑉 )
	qusaddf.z	⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
	qusaddf.e	⊢ ( 𝜑 → ( ( 𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞 ) → ( 𝑎 · 𝑏 ) ∼ ( 𝑝 · 𝑞 ) ) )
	qusaddf.c	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( 𝑝 · 𝑞 ) ∈ 𝑉 )
	qusaddflem.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ )
	qusaddflem.g	⊢ ( 𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
Assertion	qusaddflem	⊢ ( 𝜑 → ∙ : ( ( 𝑉 / ∼ ) × ( 𝑉 / ∼ ) ) ⟶ ( 𝑉 / ∼ ) )

Proof

Step	Hyp	Ref	Expression
1		qusaddf.u	⊢ ( 𝜑 → 𝑈 = ( 𝑅 /s ∼ ) )
2		qusaddf.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3		qusaddf.r	⊢ ( 𝜑 → ∼ Er 𝑉 )
4		qusaddf.z	⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
5		qusaddf.e	⊢ ( 𝜑 → ( ( 𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞 ) → ( 𝑎 · 𝑏 ) ∼ ( 𝑝 · 𝑞 ) ) )
6		qusaddf.c	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( 𝑝 · 𝑞 ) ∈ 𝑉 )
7		qusaddflem.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ )
8		qusaddflem.g	⊢ ( 𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
9		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
10	2 9	eqeltrdi	⊢ ( 𝜑 → 𝑉 ∈ V )
11		erex	⊢ ( ∼ Er 𝑉 → ( 𝑉 ∈ V → ∼ ∈ V ) )
12	3 10 11	sylc	⊢ ( 𝜑 → ∼ ∈ V )
13	1 2 7 12 4	quslem	⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ ( 𝑉 / ∼ ) )
14	3 10 7 6 5	ercpbl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
15	13 14 8 6	imasaddflem	⊢ ( 𝜑 → ∙ : ( ( 𝑉 / ∼ ) × ( 𝑉 / ∼ ) ) ⟶ ( 𝑉 / ∼ ) )