Theorem qusmulval

Description: The multiplication in a quotient structure. (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	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( 𝑝 · 𝑞 ) ∈ 𝑉 )
	qusmulf.p	⊢ · = ( .r ‘ 𝑅 )
	qusmulf.a	⊢ ∙ = ( .r ‘ 𝑈 )
Assertion	qusmulval	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( [ 𝑋 ] ∼ ∙ [ 𝑌 ] ∼ ) = [ ( 𝑋 · 𝑌 ) ] ∼ )

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		qusmulf.p	⊢ · = ( .r ‘ 𝑅 )
8		qusmulf.a	⊢ ∙ = ( .r ‘ 𝑈 )
9		eqid	⊢ ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ )
10		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
11	2 10	eqeltrdi	⊢ ( 𝜑 → 𝑉 ∈ V )
12		erex	⊢ ( ∼ Er 𝑉 → ( 𝑉 ∈ V → ∼ ∈ V ) )
13	3 11 12	sylc	⊢ ( 𝜑 → ∼ ∈ V )
14	1 2 9 13 4	qusval	⊢ ( 𝜑 → 𝑈 = ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) “s 𝑅 ) )
15	1 2 9 13 4	quslem	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) : 𝑉 –onto→ ( 𝑉 / ∼ ) )
16	14 2 15 4 7 8	imasmulr	⊢ ( 𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) ‘ 𝑝 ) , ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) ‘ 𝑞 ) ⟩ , ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
17	1 2 3 4 5 6 9 16	qusaddvallem	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( [ 𝑋 ] ∼ ∙ [ 𝑌 ] ∼ ) = [ ( 𝑋 · 𝑌 ) ] ∼ )