Theorem map2psrpr 11195

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 11153	. . . . 5 ⊢ <R ⊆ (R × R)
2	1	brel 5716	. . . 4 ⊢ ((𝐶 +R -1R) <R 𝐴 → ((𝐶 +R -1R) ∈ R ∧ 𝐴 ∈ R))
3	2	simprd 501	. . 3 ⊢ ((𝐶 +R -1R) <R 𝐴 → 𝐴 ∈ R)
4		map2psrpr.2	. . . . . 6 ⊢ 𝐶 ∈ R
5		ltasr 11185	. . . . . 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 11186	. . . . . . . . . 10 ⊢ (𝐶 ∈ R → (𝐶 +R (𝐶 ·R -1R)) = 0R)
8	4, 7	ax-mp 5	. . . . . . . . 9 ⊢ (𝐶 +R (𝐶 ·R -1R)) = 0R
9	8	oveq1i 7430	. . . . . . . 8 ⊢ ((𝐶 +R (𝐶 ·R -1R)) +R 𝐴) = (0R +R 𝐴)
10		addasssr 11173	. . . . . . . 8 ⊢ ((𝐶 +R (𝐶 ·R -1R)) +R 𝐴) = (𝐶 +R ((𝐶 ·R -1R) +R 𝐴))
11		addcomsr 11172	. . . . . . . 8 ⊢ (0R +R 𝐴) = (𝐴 +R 0R)
12	9, 10, 11	3eqtr3i 2792	. . . . . . 7 ⊢ (𝐶 +R ((𝐶 ·R -1R) +R 𝐴)) = (𝐴 +R 0R)
13		0idsr 11182	. . . . . . 7 ⊢ (𝐴 ∈ R → (𝐴 +R 0R) = 𝐴)
14	12, 13	eqtrid 2808	. . . . . 6 ⊢ (𝐴 ∈ R → (𝐶 +R ((𝐶 ·R -1R) +R 𝐴)) = 𝐴)
15	14	breq2d 5115	. . . . 5 ⊢ (𝐴 ∈ R → ((𝐶 +R -1R) <R (𝐶 +R ((𝐶 ·R -1R) +R 𝐴)) ↔ (𝐶 +R -1R) <R 𝐴))
16	6, 15	bitrid 286	. . . 4 ⊢ (𝐴 ∈ R → (-1R <R ((𝐶 ·R -1R) +R 𝐴) ↔ (𝐶 +R -1R) <R 𝐴))
17		m1r 11167	. . . . . . . 8 ⊢ -1R ∈ R
18		mulclsr 11169	. . . . . . . 8 ⊢ ((𝐶 ∈ R ∧ -1R ∈ R) → (𝐶 ·R -1R) ∈ R)
19	4, 17, 18	mp2an 705	. . . . . . 7 ⊢ (𝐶 ·R -1R) ∈ R
20		addclsr 11168	. . . . . . 7 ⊢ (((𝐶 ·R -1R) ∈ R ∧ 𝐴 ∈ R) → ((𝐶 ·R -1R) +R 𝐴) ∈ R)
21	19, 20	mpan 703	. . . . . 6 ⊢ (𝐴 ∈ R → ((𝐶 ·R -1R) +R 𝐴) ∈ R)
22		df-nr 11141	. . . . . . 7 ⊢ R = ((P × P) / ~R )
23		breq2 5107	. . . . . . . 8 ⊢ ([⟨𝑦, 𝑧⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → (-1R <R [⟨𝑦, 𝑧⟩] ~R ↔ -1R <R ((𝐶 ·R -1R) +R 𝐴)))
24		eqeq2 2773	. . . . . . . . 9 ⊢ ([⟨𝑦, 𝑧⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → ([⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴)))
25	24	rexbidv 3187	. . . . . . . 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 11147	. . . . . . . . . . 11 ⊢ -1R = [⟨1P, (1P +P 1P)⟩] ~R
28	27	breq1i 5110	. . . . . . . . . 10 ⊢ (-1R <R [⟨𝑦, 𝑧⟩] ~R ↔ [⟨1P, (1P +P 1P)⟩] ~R <R [⟨𝑦, 𝑧⟩] ~R )
29		addasspr 11107	. . . . . . . . . . . 12 ⊢ ((1P +P 1P) +P 𝑦) = (1P +P (1P +P 𝑦))
30	29	breq2i 5111	. . . . . . . . . . 11 ⊢ ((1P +P 𝑧)<P ((1P +P 1P) +P 𝑦) ↔ (1P +P 𝑧)<P (1P +P (1P +P 𝑦)))
31		ltsrpr 11162	. . . . . . . . . . 11 ⊢ ([⟨1P, (1P +P 1P)⟩] ~R <R [⟨𝑦, 𝑧⟩] ~R ↔ (1P +P 𝑧)<P ((1P +P 1P) +P 𝑦))
32		1pr 11100	. . . . . . . . . . . 12 ⊢ 1P ∈ P
33		ltapr 11130	. . . . . . . . . . . 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 306	. . . . . . . . . 10 ⊢ ([⟨1P, (1P +P 1P)⟩] ~R <R [⟨𝑦, 𝑧⟩] ~R ↔ 𝑧<P (1P +P 𝑦))
36	28, 35	bitri 278	. . . . . . . . 9 ⊢ (-1R <R [⟨𝑦, 𝑧⟩] ~R ↔ 𝑧<P (1P +P 𝑦))
37		ltexpri 11128	. . . . . . . . 9 ⊢ (𝑧<P (1P +P 𝑦) → ∃𝑥 ∈ P (𝑧 +P 𝑥) = (1P +P 𝑦))
38	36, 37	sylbi 220	. . . . . . . 8 ⊢ (-1R <R [⟨𝑦, 𝑧⟩] ~R → ∃𝑥 ∈ P (𝑧 +P 𝑥) = (1P +P 𝑦))
39		enreceq 11151	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ P ∧ 1P ∈ P) ∧ (𝑦 ∈ P ∧ 𝑧 ∈ P)) → ([⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ (𝑥 +P 𝑧) = (1P +P 𝑦)))
40	32, 39	mpanl2 714	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ P ∧ (𝑦 ∈ P ∧ 𝑧 ∈ P)) → ([⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ (𝑥 +P 𝑧) = (1P +P 𝑦)))
41		addcompr 11106	. . . . . . . . . . . 12 ⊢ (𝑧 +P 𝑥) = (𝑥 +P 𝑧)
42	41	eqeq1i 2766	. . . . . . . . . . 11 ⊢ ((𝑧 +P 𝑥) = (1P +P 𝑦) ↔ (𝑥 +P 𝑧) = (1P +P 𝑦))
43	40, 42	bitr4di 292	. . . . . . . . . 10 ⊢ ((𝑥 ∈ P ∧ (𝑦 ∈ P ∧ 𝑧 ∈ P)) → ([⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ (𝑧 +P 𝑥) = (1P +P 𝑦)))
44	43	ancoms 464	. . . . . . . . 9 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ 𝑥 ∈ P) → ([⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ (𝑧 +P 𝑥) = (1P +P 𝑦)))
45	44	rexbidva 3185	. . . . . . . 8 ⊢ ((𝑦 ∈ P ∧ 𝑧 ∈ P) → (∃𝑥 ∈ P [⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ ∃𝑥 ∈ P (𝑧 +P 𝑥) = (1P +P 𝑦)))
46	38, 45	imbitrrid 249	. . . . . . 7 ⊢ ((𝑦 ∈ P ∧ 𝑧 ∈ P) → (-1R <R [⟨𝑦, 𝑧⟩] ~R → ∃𝑥 ∈ P [⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ))
47	22, 26, 46	ecoptocl 8828	. . . . . 6 ⊢ (((𝐶 ·R -1R) +R 𝐴) ∈ R → (-1R <R ((𝐶 ·R -1R) +R 𝐴) → ∃𝑥 ∈ P [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴)))
48	21, 47	syl 18	. . . . 5 ⊢ (𝐴 ∈ R → (-1R <R ((𝐶 ·R -1R) +R 𝐴) → ∃𝑥 ∈ P [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴)))
49		oveq2 7428	. . . . . . . 8 ⊢ ([⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = (𝐶 +R ((𝐶 ·R -1R) +R 𝐴)))
50	49, 14	sylan9eqr 2818	. . . . . . 7 ⊢ ((𝐴 ∈ R ∧ [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴)) → (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴)
51	50	ex 418	. . . . . 6 ⊢ (𝐴 ∈ R → ([⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴))
52	51	reximdv 3178	. . . . 5 ⊢ (𝐴 ∈ R → (∃𝑥 ∈ P [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → ∃𝑥 ∈ P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴))
53	48, 52	syld 48	. . . 4 ⊢ (𝐴 ∈ R → (-1R <R ((𝐶 ·R -1R) +R 𝐴) → ∃𝑥 ∈ P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴))
54	16, 53	sylbird 263	. . 3 ⊢ (𝐴 ∈ R → ((𝐶 +R -1R) <R 𝐴 → ∃𝑥 ∈ P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴))
55	3, 54	mpcom 39	. 2 ⊢ ((𝐶 +R -1R) <R 𝐴 → ∃𝑥 ∈ P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴)
56	4	mappsrpr 11193	. . . . 5 ⊢ ((𝐶 +R -1R) <R (𝐶 +R [⟨𝑥, 1P⟩] ~R ) ↔ 𝑥 ∈ P)
57		breq2 5107	. . . . 5 ⊢ ((𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴 → ((𝐶 +R -1R) <R (𝐶 +R [⟨𝑥, 1P⟩] ~R ) ↔ (𝐶 +R -1R) <R 𝐴))
58	56, 57	bitr3id 288	. . . 4 ⊢ ((𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴 → (𝑥 ∈ P ↔ (𝐶 +R -1R) <R 𝐴))
59	58	biimpac 484	. . 3 ⊢ ((𝑥 ∈ P ∧ (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴) → (𝐶 +R -1R) <R 𝐴)
60	59	rexlimiva 3156	. 2 ⊢ (∃𝑥 ∈ P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴 → (𝐶 +R -1R) <R 𝐴)
61	55, 60	impbii 212	1 ⊢ ((𝐶 +R -1R) <R 𝐴 ↔ ∃𝑥 ∈ P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∃wrex 3087  ⟨cop 4590   class class class wbr 5103  (class class class)co 7420  [cec 8715  Pcnp 10944  1_Pc1p 10945   +_P cpp 10946  <_P cltp 10948   ~_R cer 10949  Rcnr 10950  0_Rc0r 10951  -1_Rcm1r 10953   +_R cplr 10954   ·_R cmr 10955   <_R cltr 10956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751  ax-inf2 9642

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-1o 8476  df-oadd 8480  df-omul 8481  df-er 8717  df-ec 8719  df-qs 8723  df-ni 10957  df-pli 10958  df-mi 10959  df-lti 10960  df-plpq 10993  df-mpq 10994  df-ltpq 10995  df-enq 10996  df-nq 10997  df-erq 10998  df-plq 10999  df-mq 11000  df-1nq 11001  df-rq 11002  df-ltnq 11003  df-np 11066  df-1p 11067  df-plp 11068  df-mp 11069  df-ltp 11070  df-enr 11140  df-nr 11141  df-plr 11142  df-mr 11143  df-ltr 11144  df-0r 11145  df-1r 11146  df-m1r 11147

This theorem is used by:  supsrlem  11196