Theorem dfcnqs 5282

Description: Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in CC from those in R.. The trick involves qsid 4319, which shows that the coset of the converse epsilon 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 5260), and allows us to reuse some of the equivalence class lemmas we developed for the transition from positive reals to signed reals, etc.

Assertion

Ref	Expression
dfcnqs	|- CC = ((R. X. R.)/.`'E)

Proof of Theorem dfcnqs

Step	Hyp	Ref	Expression
1		df-c 5260	. 2 |- CC = (R. X. R.)
2		qsid 4319	. 2 |- ((R. X. R.)/.`'E) = (R. X. R.)
3	1, 2	eqtr4i 1505	1 |- CC = ((R. X. R.)/.`'E)

Syntax hints:   = wceq 960  Ecep 2846   X. cxp 3184  `'ccnv 3185  /.cqs 4276  R.cnr 5013  CCcc 5252

This theorem is referenced by:  axaddcom 5295  axmulcom 5296  axaddass 5297  axmulass 5298  axdistr 5299

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-10o 1144  ax-16 1214  ax-11o 1222  ax-ext 1464  ax-sep 2718  ax-pow 2758  ax-pr 2795

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 985  df-sb 1176  df-eu 1386  df-mo 1387  df-clab 1470  df-cleq 1475  df-clel 1478  df-ne 1594  df-rex 1657  df-v 1819  df-dif 2060  df-un 2061  df-in 2062  df-ss 2064  df-nul 2292  df-pw 2414  df-sn 2424  df-pr 2425  df-op 2428  df-br 2635  df-opab 2682  df-eprel 2848  df-xp 3200  df-cnv 3202  df-dm 3204  df-rn 3205  df-res 3206  df-ima 3207  df-ec 4279  df-qs 4282  df-c 5260

Copyright terms: Public domain