Theorem map2psrpr 10535

Description: Equivalence for positive signed real. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.)

Hypothesis

Ref	Expression
map2psrpr.2	⊢ 𝐶 ∈ R

Assertion

Ref	Expression
map2psrpr	⊢ ((𝐶 +R -1R) <R 𝐴 ↔ ∃𝑥 ∈ P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶

Proof of Theorem map2psrpr

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ltrelsr 10493	. . . . 5 ⊢ <R ⊆ (R × R)
2	1	brel 5620	. . . 4 ⊢ ((𝐶 +R -1R) <R 𝐴 → ((𝐶 +R -1R) ∈ R ∧ 𝐴 ∈ R))
3	2	simprd 498	. . 3 ⊢ ((𝐶 +R -1R) <R 𝐴 → 𝐴 ∈ R)
4		map2psrpr.2	. . . . . 6 ⊢ 𝐶 ∈ R
5		ltasr 10525	. . . . . 6 ⊢ (𝐶 ∈ R → (-1R <R ((𝐶 ·R -1R) +R 𝐴) ↔ (𝐶 +R -1R) <R (𝐶 +R ((𝐶 ·R -1R) +R 𝐴))))
6	4, 5	ax-mp 5	. . . . 5 ⊢ (-1R <R ((𝐶 ·R -1R) +R 𝐴) ↔ (𝐶 +R -1R) <R (𝐶 +R ((𝐶 ·R -1R) +R 𝐴)))
7		pn0sr 10526	. . . . . . . . . 10 ⊢ (𝐶 ∈ R → (𝐶 +R (𝐶 ·R -1R)) = 0R)
8	4, 7	ax-mp 5	. . . . . . . . 9 ⊢ (𝐶 +R (𝐶 ·R -1R)) = 0R
9	8	oveq1i 7169	. . . . . . . 8 ⊢ ((𝐶 +R (𝐶 ·R -1R)) +R 𝐴) = (0R +R 𝐴)
10		addasssr 10513	. . . . . . . 8 ⊢ ((𝐶 +R (𝐶 ·R -1R)) +R 𝐴) = (𝐶 +R ((𝐶 ·R -1R) +R 𝐴))
11		addcomsr 10512	. . . . . . . 8 ⊢ (0R +R 𝐴) = (𝐴 +R 0R)
12	9, 10, 11	3eqtr3i 2855	. . . . . . 7 ⊢ (𝐶 +R ((𝐶 ·R -1R) +R 𝐴)) = (𝐴 +R 0R)
13		0idsr 10522	. . . . . . 7 ⊢ (𝐴 ∈ R → (𝐴 +R 0R) = 𝐴)
14	12, 13	syl5eq 2871	. . . . . 6 ⊢ (𝐴 ∈ R → (𝐶 +R ((𝐶 ·R -1R) +R 𝐴)) = 𝐴)
15	14	breq2d 5081	. . . . 5 ⊢ (𝐴 ∈ R → ((𝐶 +R -1R) <R (𝐶 +R ((𝐶 ·R -1R) +R 𝐴)) ↔ (𝐶 +R -1R) <R 𝐴))
16	6, 15	syl5bb 285	. . . 4 ⊢ (𝐴 ∈ R → (-1R <R ((𝐶 ·R -1R) +R 𝐴) ↔ (𝐶 +R -1R) <R 𝐴))
17		m1r 10507	. . . . . . . 8 ⊢ -1R ∈ R
18		mulclsr 10509	. . . . . . . 8 ⊢ ((𝐶 ∈ R ∧ -1R ∈ R) → (𝐶 ·R -1R) ∈ R)
19	4, 17, 18	mp2an 690	. . . . . . 7 ⊢ (𝐶 ·R -1R) ∈ R
20		addclsr 10508	. . . . . . 7 ⊢ (((𝐶 ·R -1R) ∈ R ∧ 𝐴 ∈ R) → ((𝐶 ·R -1R) +R 𝐴) ∈ R)
21	19, 20	mpan 688	. . . . . 6 ⊢ (𝐴 ∈ R → ((𝐶 ·R -1R) +R 𝐴) ∈ R)
22		df-nr 10481	. . . . . . 7 ⊢ R = ((P × P) / ~R )
23		breq2 5073	. . . . . . . 8 ⊢ ([⟨𝑦, 𝑧⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → (-1R <R [⟨𝑦, 𝑧⟩] ~R ↔ -1R <R ((𝐶 ·R -1R) +R 𝐴)))
24		eqeq2 2836	. . . . . . . . 9 ⊢ ([⟨𝑦, 𝑧⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → ([⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴)))
25	24	rexbidv 3300	. . . . . . . 8 ⊢ ([⟨𝑦, 𝑧⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → (∃𝑥 ∈ P [⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ ∃𝑥 ∈ P [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴)))
26	23, 25	imbi12d 347	. . . . . . 7 ⊢ ([⟨𝑦, 𝑧⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → ((-1R <R [⟨𝑦, 𝑧⟩] ~R → ∃𝑥 ∈ P [⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ) ↔ (-1R <R ((𝐶 ·R -1R) +R 𝐴) → ∃𝑥 ∈ P [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴))))
27		df-m1r 10487	. . . . . . . . . . 11 ⊢ -1R = [⟨1P, (1P +P 1P)⟩] ~R
28	27	breq1i 5076	. . . . . . . . . 10 ⊢ (-1R <R [⟨𝑦, 𝑧⟩] ~R ↔ [⟨1P, (1P +P 1P)⟩] ~R <R [⟨𝑦, 𝑧⟩] ~R )
29		addasspr 10447	. . . . . . . . . . . 12 ⊢ ((1P +P 1P) +P 𝑦) = (1P +P (1P +P 𝑦))
30	29	breq2i 5077	. . . . . . . . . . 11 ⊢ ((1P +P 𝑧)<P ((1P +P 1P) +P 𝑦) ↔ (1P +P 𝑧)<P (1P +P (1P +P 𝑦)))
31		ltsrpr 10502	. . . . . . . . . . 11 ⊢ ([⟨1P, (1P +P 1P)⟩] ~R <R [⟨𝑦, 𝑧⟩] ~R ↔ (1P +P 𝑧)<P ((1P +P 1P) +P 𝑦))
32		1pr 10440	. . . . . . . . . . . 12 ⊢ 1P ∈ P
33		ltapr 10470	. . . . . . . . . . . 12 ⊢ (1P ∈ P → (𝑧<P (1P +P 𝑦) ↔ (1P +P 𝑧)<P (1P +P (1P +P 𝑦))))
34	32, 33	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝑧<P (1P +P 𝑦) ↔ (1P +P 𝑧)<P (1P +P (1P +P 𝑦)))
35	30, 31, 34	3bitr4i 305	. . . . . . . . . 10 ⊢ ([⟨1P, (1P +P 1P)⟩] ~R <R [⟨𝑦, 𝑧⟩] ~R ↔ 𝑧<P (1P +P 𝑦))
36	28, 35	bitri 277	. . . . . . . . 9 ⊢ (-1R <R [⟨𝑦, 𝑧⟩] ~R ↔ 𝑧<P (1P +P 𝑦))
37		ltexpri 10468	. . . . . . . . 9 ⊢ (𝑧<P (1P +P 𝑦) → ∃𝑥 ∈ P (𝑧 +P 𝑥) = (1P +P 𝑦))
38	36, 37	sylbi 219	. . . . . . . 8 ⊢ (-1R <R [⟨𝑦, 𝑧⟩] ~R → ∃𝑥 ∈ P (𝑧 +P 𝑥) = (1P +P 𝑦))
39		enreceq 10491	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ P ∧ 1P ∈ P) ∧ (𝑦 ∈ P ∧ 𝑧 ∈ P)) → ([⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ (𝑥 +P 𝑧) = (1P +P 𝑦)))
40	32, 39	mpanl2 699	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ P ∧ (𝑦 ∈ P ∧ 𝑧 ∈ P)) → ([⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ (𝑥 +P 𝑧) = (1P +P 𝑦)))
41		addcompr 10446	. . . . . . . . . . . 12 ⊢ (𝑧 +P 𝑥) = (𝑥 +P 𝑧)
42	41	eqeq1i 2829	. . . . . . . . . . 11 ⊢ ((𝑧 +P 𝑥) = (1P +P 𝑦) ↔ (𝑥 +P 𝑧) = (1P +P 𝑦))
43	40, 42	syl6bbr 291	. . . . . . . . . 10 ⊢ ((𝑥 ∈ P ∧ (𝑦 ∈ P ∧ 𝑧 ∈ P)) → ([⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ (𝑧 +P 𝑥) = (1P +P 𝑦)))
44	43	ancoms 461	. . . . . . . . 9 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ 𝑥 ∈ P) → ([⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ (𝑧 +P 𝑥) = (1P +P 𝑦)))
45	44	rexbidva 3299	. . . . . . . 8 ⊢ ((𝑦 ∈ P ∧ 𝑧 ∈ P) → (∃𝑥 ∈ P [⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ ∃𝑥 ∈ P (𝑧 +P 𝑥) = (1P +P 𝑦)))
46	38, 45	syl5ibr 248	. . . . . . 7 ⊢ ((𝑦 ∈ P ∧ 𝑧 ∈ P) → (-1R <R [⟨𝑦, 𝑧⟩] ~R → ∃𝑥 ∈ P [⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ))
47	22, 26, 46	ecoptocl 8390	. . . . . 6 ⊢ (((𝐶 ·R -1R) +R 𝐴) ∈ R → (-1R <R ((𝐶 ·R -1R) +R 𝐴) → ∃𝑥 ∈ P [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴)))
48	21, 47	syl 17	. . . . 5 ⊢ (𝐴 ∈ R → (-1R <R ((𝐶 ·R -1R) +R 𝐴) → ∃𝑥 ∈ P [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴)))
49		oveq2 7167	. . . . . . . 8 ⊢ ([⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = (𝐶 +R ((𝐶 ·R -1R) +R 𝐴)))
50	49, 14	sylan9eqr 2881	. . . . . . 7 ⊢ ((𝐴 ∈ R ∧ [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴)) → (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴)
51	50	ex 415	. . . . . 6 ⊢ (𝐴 ∈ R → ([⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴))
52	51	reximdv 3276	. . . . 5 ⊢ (𝐴 ∈ R → (∃𝑥 ∈ P [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → ∃𝑥 ∈ P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴))
53	48, 52	syld 47	. . . 4 ⊢ (𝐴 ∈ R → (-1R <R ((𝐶 ·R -1R) +R 𝐴) → ∃𝑥 ∈ P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴))
54	16, 53	sylbird 262	. . 3 ⊢ (𝐴 ∈ R → ((𝐶 +R -1R) <R 𝐴 → ∃𝑥 ∈ P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴))
55	3, 54	mpcom 38	. 2 ⊢ ((𝐶 +R -1R) <R 𝐴 → ∃𝑥 ∈ P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴)
56	4	mappsrpr 10533	. . . . 5 ⊢ ((𝐶 +R -1R) <R (𝐶 +R [⟨𝑥, 1P⟩] ~R ) ↔ 𝑥 ∈ P)
57		breq2 5073	. . . . 5 ⊢ ((𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴 → ((𝐶 +R -1R) <R (𝐶 +R [⟨𝑥, 1P⟩] ~R ) ↔ (𝐶 +R -1R) <R 𝐴))
58	56, 57	syl5bbr 287	. . . 4 ⊢ ((𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴 → (𝑥 ∈ P ↔ (𝐶 +R -1R) <R 𝐴))
59	58	biimpac 481	. . 3 ⊢ ((𝑥 ∈ P ∧ (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴) → (𝐶 +R -1R) <R 𝐴)
60	59	rexlimiva 3284	. 2 ⊢ (∃𝑥 ∈ P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴 → (𝐶 +R -1R) <R 𝐴)
61	55, 60	impbii 211	1 ⊢ ((𝐶 +R -1R) <R 𝐴 ↔ ∃𝑥 ∈ P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1536   ∈ wcel 2113  ∃wrex 3142  ⟨cop 4576   class class class wbr 5069  (class class class)co 7159  [cec 8290  Pcnp 10284  1_Pc1p 10285   +_P cpp 10286  <_P cltp 10288   ~_R cer 10289  Rcnr 10290  0_Rc0r 10291  -1_Rcm1r 10293   +_R cplr 10294   ·_R cmr 10295   <_R cltr 10296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464  ax-inf2 9107

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-reu 3148  df-rmo 3149  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-tp 4575  df-op 4577  df-uni 4842  df-int 4880  df-iun 4924  df-br 5070  df-opab 5132  df-mpt 5150  df-tr 5176  df-id 5463  df-eprel 5468  df-po 5477  df-so 5478  df-fr 5517  df-we 5519  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-pred 6151  df-ord 6197  df-on 6198  df-lim 6199  df-suc 6200  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-ov 7162  df-oprab 7163  df-mpo 7164  df-om 7584  df-1st 7692  df-2nd 7693  df-wrecs 7950  df-recs 8011  df-rdg 8049  df-1o 8105  df-oadd 8109  df-omul 8110  df-er 8292  df-ec 8294  df-qs 8298  df-ni 10297  df-pli 10298  df-mi 10299  df-lti 10300  df-plpq 10333  df-mpq 10334  df-ltpq 10335  df-enq 10336  df-nq 10337  df-erq 10338  df-plq 10339  df-mq 10340  df-1nq 10341  df-rq 10342  df-ltnq 10343  df-np 10406  df-1p 10407  df-plp 10408  df-mp 10409  df-ltp 10410  df-enr 10480  df-nr 10481  df-plr 10482  df-mr 10483  df-ltr 10484  df-0r 10485  df-1r 10486  df-m1r 10487

This theorem is referenced by:  supsrlem  10536