Theorem qusaddval

Description: The addition in a quotient structure. (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$$
	qusaddf.p	$$⊢\underset{\dot{}}{·}={+}_R$$
	qusaddf.a	$$⊢\underset{\dot{}}{\bullet }={+}_U$$
Assertion	qusaddval	$$⊢\left(\phi \wedge X\in V\wedge Y\in V\right)\to \left[X\right]\underset{\dot{}}{\sim }\underset{\dot{}}{\bullet }\left[Y\right]\underset{\dot{}}{\sim }=\left[\left(X\underset{\dot{}}{·}Y\right)\right]\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		qusaddf.p	$$⊢\underset{\dot{}}{·}={+}_R$$
8		qusaddf.a	$$⊢\underset{\dot{}}{\bullet }={+}_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	imasplusg	$$⊢\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	qusaddvallem	$$⊢\left(\phi \wedge X\in V\wedge Y\in V\right)\to \left[X\right]\underset{\dot{}}{\sim }\underset{\dot{}}{\bullet }\left[Y\right]\underset{\dot{}}{\sim }=\left[\left(X\underset{\dot{}}{·}Y\right)\right]\underset{\dot{}}{\sim }$$