Theorem qusmulf

Description: The multiplication in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015)

	Ref	Expression
Hypotheses	qusaddf.u	$$⊢\phi \to U=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
	qusaddf.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
	qusaddf.r	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}V$$
	qusaddf.z	$$⊢\phi \to R\in Z$$
	qusaddf.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)$$
	qusaddf.c	$$⊢\left(\phi \wedge \left(p\in V\wedge q\in V\right)\right)\to p\underset{\dot{}}{·}q\in V$$
	qusmulf.p	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	qusmulf.a	$$⊢\underset{\dot{}}{\bullet }={\cdot }_U$$
Assertion	qusmulf	$$⊢\phi \to \underset{\dot{}}{\bullet }:\left(V/\underset{\dot{}}{\sim }\right)\times \left(V/\underset{\dot{}}{\sim }\right)⟶V/\underset{\dot{}}{\sim }$$

Proof

Step	Hyp	Ref	Expression
1		qusaddf.u	$$⊢\phi \to U=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
2		qusaddf.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
3		qusaddf.r	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}V$$
4		qusaddf.z	$$⊢\phi \to R\in Z$$
5		qusaddf.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)$$
6		qusaddf.c	$$⊢\left(\phi \wedge \left(p\in V\wedge q\in V\right)\right)\to p\underset{\dot{}}{·}q\in V$$
7		qusmulf.p	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
8		qusmulf.a	$$⊢\underset{\dot{}}{\bullet }={\cdot }_U$$
9		eqid	$$⊢\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)=\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)$$
10		fvex	$$⊢{\mathrm{Base}}_R\in \mathrm{V}$$
11	2 10	eqeltrdi	$$⊢\phi \to V\in \mathrm{V}$$
12		erex	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}V\to \left(V\in \mathrm{V}\to \underset{\dot{}}{\sim }\in \mathrm{V}\right)$$
13	3 11 12	sylc	$$⊢\phi \to \underset{\dot{}}{\sim }\in \mathrm{V}$$
14	1 2 9 13 4	qusval	$$⊢\phi \to U=\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right){“}_{𝑠}R$$
15	1 2 9 13 4	quslem	$$⊢\phi \to \left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right):V\underset{onto}{⟶}V/\underset{\dot{}}{\sim }$$
16	14 2 15 4 7 8	imasmulr	$$⊢\phi \to \underset{\dot{}}{\bullet }=\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)\left(p\right),\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)\left(q\right)⟩,\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)\left(p\underset{\dot{}}{·}q\right)⟩\right\}$$
17	1 2 3 4 5 6 9 16	qusaddflem	$$⊢\phi \to \underset{\dot{}}{\bullet }:\left(V/\underset{\dot{}}{\sim }\right)\times \left(V/\underset{\dot{}}{\sim }\right)⟶V/\underset{\dot{}}{\sim }$$