Theorem erov2

Description: The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010)

	Ref	Expression
Hypotheses	eropr2.1	$$⊢J=A/\underset{\dot{}}{\sim }$$
	eropr2.2	$$⊢\underset{\dot{}}{⨣}=\left\{⟨⟨x,y⟩,z⟩|\exists p\in A\exists q\in A\left(\left(x=\left[p\right]\underset{\dot{}}{\sim }\wedge y=\left[q\right]\underset{\dot{}}{\sim }\right)\wedge z=\left[\left(p\underset{\dot{}}{+}q\right)\right]\underset{\dot{}}{\sim }\right)\right\}$$
	eropr2.3	$$⊢\phi \to \underset{\dot{}}{\sim }\in X$$
	eropr2.4	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}U$$
	eropr2.5	$$⊢\phi \to A\subseteq U$$
	eropr2.6	$$⊢\phi \to \underset{\dot{}}{+}:A\times A⟶A$$
	eropr2.7	$$⊢\left(\phi \wedge \left(\left(r\in A\wedge s\in A\right)\wedge \left(t\in A\wedge u\in A\right)\right)\right)\to \left(\left(r\underset{\dot{}}{\sim }s\wedge t\underset{\dot{}}{\sim }u\right)\to \left(r\underset{\dot{}}{+}t\right)\underset{\dot{}}{\sim }\left(s\underset{\dot{}}{+}u\right)\right)$$
Assertion	erov2	$$⊢\left(\phi \wedge P\in A\wedge Q\in A\right)\to \left[P\right]\underset{\dot{}}{\sim }\underset{\dot{}}{⨣}\left[Q\right]\underset{\dot{}}{\sim }=\left[\left(P\underset{\dot{}}{+}Q\right)\right]\underset{\dot{}}{\sim }$$

Proof

Step	Hyp	Ref	Expression
1		eropr2.1	$$⊢J=A/\underset{\dot{}}{\sim }$$
2		eropr2.2	$$⊢\underset{\dot{}}{⨣}=\left\{⟨⟨x,y⟩,z⟩|\exists p\in A\exists q\in A\left(\left(x=\left[p\right]\underset{\dot{}}{\sim }\wedge y=\left[q\right]\underset{\dot{}}{\sim }\right)\wedge z=\left[\left(p\underset{\dot{}}{+}q\right)\right]\underset{\dot{}}{\sim }\right)\right\}$$
3		eropr2.3	$$⊢\phi \to \underset{\dot{}}{\sim }\in X$$
4		eropr2.4	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}U$$
5		eropr2.5	$$⊢\phi \to A\subseteq U$$
6		eropr2.6	$$⊢\phi \to \underset{\dot{}}{+}:A\times A⟶A$$
7		eropr2.7	$$⊢\left(\phi \wedge \left(\left(r\in A\wedge s\in A\right)\wedge \left(t\in A\wedge u\in A\right)\right)\right)\to \left(\left(r\underset{\dot{}}{\sim }s\wedge t\underset{\dot{}}{\sim }u\right)\to \left(r\underset{\dot{}}{+}t\right)\underset{\dot{}}{\sim }\left(s\underset{\dot{}}{+}u\right)\right)$$
8	1 1 3 4 4 4 5 5 5 6 7 2 3 3	erov	$$⊢\left(\phi \wedge P\in A\wedge Q\in A\right)\to \left[P\right]\underset{\dot{}}{\sim }\underset{\dot{}}{⨣}\left[Q\right]\underset{\dot{}}{\sim }=\left[\left(P\underset{\dot{}}{+}Q\right)\right]\underset{\dot{}}{\sim }$$