Theorem dfcnqs

Description: Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in CC from those in R. . The trick involves qsid , which shows that the coset of the converse membership relation (which is not an equivalence relation) acts as an identity divisor for the quotient set operation. This lets us "pretend" that CC is a quotient set, even though it is not (compare df-c ), and allows to reuse some of the equivalence class lemmas we developed for the transition from positive reals to signed reals, etc. (Contributed by NM, 13-Aug-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	dfcnqs	$$⊢ℂ=\left(𝑹\times 𝑹\right)/{\mathrm{E}}^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		df-c	$$⊢ℂ=𝑹\times 𝑹$$
2		qsid	$$⊢\left(𝑹\times 𝑹\right)/{\mathrm{E}}^{-1}=𝑹\times 𝑹$$
3	1 2	eqtr4i	$$⊢ℂ=\left(𝑹\times 𝑹\right)/{\mathrm{E}}^{-1}$$