Theorem map2psrpr 11234

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 11192	. . . . 5 ⊢ <R ⊆ (R × R)
2	1	brel 5723	. . . 4 ⊢ ((𝐶 +R -1R) <R 𝐴 → ((𝐶 +R -1R) ∈ R ∧ 𝐴 ∈ R))
3	2	simprd 501	. . 3 ⊢ ((𝐶 +R -1R) <R 𝐴 → 𝐴 ∈ R)
4		map2psrpr.2	. . . . . 6 ⊢ 𝐶 ∈ R
5		ltasr 11224	. . . . . 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 11225	. . . . . . . . . 10 ⊢ (𝐶 ∈ R → (𝐶 +R (𝐶 ·R -1R)) = 0R)
8	4, 7	ax-mp 5	. . . . . . . . 9 ⊢ (𝐶 +R (𝐶 ·R -1R)) = 0R
9	8	oveq1i 7461	. . . . . . . 8 ⊢ ((𝐶 +R (𝐶 ·R -1R)) +R 𝐴) = (0R +R 𝐴)
10		addasssr 11212	. . . . . . . 8 ⊢ ((𝐶 +R (𝐶 ·R -1R)) +R 𝐴) = (𝐶 +R ((𝐶 ·R -1R) +R 𝐴))
11		addcomsr 11211	. . . . . . . 8 ⊢ (0R +R 𝐴) = (𝐴 +R 0R)
12	9, 10, 11	3eqtr3i 2794	. . . . . . 7 ⊢ (𝐶 +R ((𝐶 ·R -1R) +R 𝐴)) = (𝐴 +R 0R)
13		0idsr 11221	. . . . . . 7 ⊢ (𝐴 ∈ R → (𝐴 +R 0R) = 𝐴)
14	12, 13	eqtrid 2810	. . . . . 6 ⊢ (𝐴 ∈ R → (𝐶 +R ((𝐶 ·R -1R) +R 𝐴)) = 𝐴)
15	14	breq2d 5120	. . . . 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 11206	. . . . . . . 8 ⊢ -1R ∈ R
18		mulclsr 11208	. . . . . . . 8 ⊢ ((𝐶 ∈ R ∧ -1R ∈ R) → (𝐶 ·R -1R) ∈ R)
19	4, 17, 18	mp2an 705	. . . . . . 7 ⊢ (𝐶 ·R -1R) ∈ R
20		addclsr 11207	. . . . . . 7 ⊢ (((𝐶 ·R -1R) ∈ R ∧ 𝐴 ∈ R) → ((𝐶 ·R -1R) +R 𝐴) ∈ R)
21	19, 20	mpan 703	. . . . . 6 ⊢ (𝐴 ∈ R → ((𝐶 ·R -1R) +R 𝐴) ∈ R)
22		df-nr 11180	. . . . . . 7 ⊢ R = ((P × P) / ~R )
23		breq2 5112	. . . . . . . 8 ⊢ ([⟨𝑦, 𝑧⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → (-1R <R [⟨𝑦, 𝑧⟩] ~R ↔ -1R <R ((𝐶 ·R -1R) +R 𝐴)))
24		eqeq2 2775	. . . . . . . . 9 ⊢ ([⟨𝑦, 𝑧⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → ([⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴)))
25	24	rexbidv 3190	. . . . . . . 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 11186	. . . . . . . . . . 11 ⊢ -1R = [⟨1P, (1P +P 1P)⟩] ~R
28	27	breq1i 5115	. . . . . . . . . 10 ⊢ (-1R <R [⟨𝑦, 𝑧⟩] ~R ↔ [⟨1P, (1P +P 1P)⟩] ~R <R [⟨𝑦, 𝑧⟩] ~R )
29		addasspr 11146	. . . . . . . . . . . 12 ⊢ ((1P +P 1P) +P 𝑦) = (1P +P (1P +P 𝑦))
30	29	breq2i 5116	. . . . . . . . . . 11 ⊢ ((1P +P 𝑧)<P ((1P +P 1P) +P 𝑦) ↔ (1P +P 𝑧)<P (1P +P (1P +P 𝑦)))
31		ltsrpr 11201	. . . . . . . . . . 11 ⊢ ([⟨1P, (1P +P 1P)⟩] ~R <R [⟨𝑦, 𝑧⟩] ~R ↔ (1P +P 𝑧)<P ((1P +P 1P) +P 𝑦))
32		1pr 11139	. . . . . . . . . . . 12 ⊢ 1P ∈ P
33		ltapr 11169	. . . . . . . . . . . 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 11167	. . . . . . . . 9 ⊢ (𝑧<P (1P +P 𝑦) → ∃𝑥 ∈ P (𝑧 +P 𝑥) = (1P +P 𝑦))
38	36, 37	sylbi 220	. . . . . . . 8 ⊢ (-1R <R [⟨𝑦, 𝑧⟩] ~R → ∃𝑥 ∈ P (𝑧 +P 𝑥) = (1P +P 𝑦))
39		enreceq 11190	. . . . . . . . . . . 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 11145	. . . . . . . . . . . 12 ⊢ (𝑧 +P 𝑥) = (𝑥 +P 𝑧)
42	41	eqeq1i 2768	. . . . . . . . . . 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 3188	. . . . . . . 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 8866	. . . . . 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 7459	. . . . . . . 8 ⊢ ([⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = (𝐶 +R ((𝐶 ·R -1R) +R 𝐴)))
50	49, 14	sylan9eqr 2820	. . . . . . 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 3181	. . . . 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 11232	. . . . 5 ⊢ ((𝐶 +R -1R) <R (𝐶 +R [⟨𝑥, 1P⟩] ~R ) ↔ 𝑥 ∈ P)
57		breq2 5112	. . . . 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 3159	. 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 2147  ∃wrex 3090  ⟨cop 4840   class class class wbr 5108  (class class class)co 7451  [cec 8753  Pcnp 10983  1_Pc1p 10984   +_P cpp 10985  <_P cltp 10987   ~_R cer 10988  Rcnr 10989  0_Rc0r 10990  -1_Rcm1r 10992   +_R cplr 10993   ·_R cmr 10994   <_R cltr 10995

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-inf2 9679

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-int 4913  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ov 7454  df-oprab 7455  df-mpo 7456  df-om 7912  df-1st 8035  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-1o 8514  df-oadd 8518  df-omul 8519  df-er 8755  df-ec 8757  df-qs 8761  df-ni 10996  df-pli 10997  df-mi 10998  df-lti 10999  df-plpq 11032  df-mpq 11033  df-ltpq 11034  df-enq 11035  df-nq 11036  df-erq 11037  df-plq 11038  df-mq 11039  df-1nq 11040  df-rq 11041  df-ltnq 11042  df-np 11105  df-1p 11106  df-plp 11107  df-mp 11108  df-ltp 11109  df-enr 11179  df-nr 11180  df-plr 11181  df-mr 11182  df-ltr 11183  df-0r 11184  df-1r 11185  df-m1r 11186

This theorem is used by:  supsrlem  11235