Theorem map2psrpr 11147

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 11105	. . . . 5 ⊢ <R ⊆ (R × R)
2	1	brel 5753	. . . 4 ⊢ ((𝐶 +R -1R) <R 𝐴 → ((𝐶 +R -1R) ∈ R ∧ 𝐴 ∈ R))
3	2	simprd 495	. . 3 ⊢ ((𝐶 +R -1R) <R 𝐴 → 𝐴 ∈ R)
4		map2psrpr.2	. . . . . 6 ⊢ 𝐶 ∈ R
5		ltasr 11137	. . . . . 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 11138	. . . . . . . . . 10 ⊢ (𝐶 ∈ R → (𝐶 +R (𝐶 ·R -1R)) = 0R)
8	4, 7	ax-mp 5	. . . . . . . . 9 ⊢ (𝐶 +R (𝐶 ·R -1R)) = 0R
9	8	oveq1i 7440	. . . . . . . 8 ⊢ ((𝐶 +R (𝐶 ·R -1R)) +R 𝐴) = (0R +R 𝐴)
10		addasssr 11125	. . . . . . . 8 ⊢ ((𝐶 +R (𝐶 ·R -1R)) +R 𝐴) = (𝐶 +R ((𝐶 ·R -1R) +R 𝐴))
11		addcomsr 11124	. . . . . . . 8 ⊢ (0R +R 𝐴) = (𝐴 +R 0R)
12	9, 10, 11	3eqtr3i 2770	. . . . . . 7 ⊢ (𝐶 +R ((𝐶 ·R -1R) +R 𝐴)) = (𝐴 +R 0R)
13		0idsr 11134	. . . . . . 7 ⊢ (𝐴 ∈ R → (𝐴 +R 0R) = 𝐴)
14	12, 13	eqtrid 2786	. . . . . 6 ⊢ (𝐴 ∈ R → (𝐶 +R ((𝐶 ·R -1R) +R 𝐴)) = 𝐴)
15	14	breq2d 5159	. . . . 5 ⊢ (𝐴 ∈ R → ((𝐶 +R -1R) <R (𝐶 +R ((𝐶 ·R -1R) +R 𝐴)) ↔ (𝐶 +R -1R) <R 𝐴))
16	6, 15	bitrid 283	. . . 4 ⊢ (𝐴 ∈ R → (-1R <R ((𝐶 ·R -1R) +R 𝐴) ↔ (𝐶 +R -1R) <R 𝐴))
17		m1r 11119	. . . . . . . 8 ⊢ -1R ∈ R
18		mulclsr 11121	. . . . . . . 8 ⊢ ((𝐶 ∈ R ∧ -1R ∈ R) → (𝐶 ·R -1R) ∈ R)
19	4, 17, 18	mp2an 692	. . . . . . 7 ⊢ (𝐶 ·R -1R) ∈ R
20		addclsr 11120	. . . . . . 7 ⊢ (((𝐶 ·R -1R) ∈ R ∧ 𝐴 ∈ R) → ((𝐶 ·R -1R) +R 𝐴) ∈ R)
21	19, 20	mpan 690	. . . . . 6 ⊢ (𝐴 ∈ R → ((𝐶 ·R -1R) +R 𝐴) ∈ R)
22		df-nr 11093	. . . . . . 7 ⊢ R = ((P × P) / ~R )
23		breq2 5151	. . . . . . . 8 ⊢ ([⟨𝑦, 𝑧⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → (-1R <R [⟨𝑦, 𝑧⟩] ~R ↔ -1R <R ((𝐶 ·R -1R) +R 𝐴)))
24		eqeq2 2746	. . . . . . . . 9 ⊢ ([⟨𝑦, 𝑧⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → ([⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴)))
25	24	rexbidv 3176	. . . . . . . 8 ⊢ ([⟨𝑦, 𝑧⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → (∃𝑥 ∈ P [⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ ∃𝑥 ∈ P [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴)))
26	23, 25	imbi12d 344	. . . . . . 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 11099	. . . . . . . . . . 11 ⊢ -1R = [⟨1P, (1P +P 1P)⟩] ~R
28	27	breq1i 5154	. . . . . . . . . 10 ⊢ (-1R <R [⟨𝑦, 𝑧⟩] ~R ↔ [⟨1P, (1P +P 1P)⟩] ~R <R [⟨𝑦, 𝑧⟩] ~R )
29		addasspr 11059	. . . . . . . . . . . 12 ⊢ ((1P +P 1P) +P 𝑦) = (1P +P (1P +P 𝑦))
30	29	breq2i 5155	. . . . . . . . . . 11 ⊢ ((1P +P 𝑧)<P ((1P +P 1P) +P 𝑦) ↔ (1P +P 𝑧)<P (1P +P (1P +P 𝑦)))
31		ltsrpr 11114	. . . . . . . . . . 11 ⊢ ([⟨1P, (1P +P 1P)⟩] ~R <R [⟨𝑦, 𝑧⟩] ~R ↔ (1P +P 𝑧)<P ((1P +P 1P) +P 𝑦))
32		1pr 11052	. . . . . . . . . . . 12 ⊢ 1P ∈ P
33		ltapr 11082	. . . . . . . . . . . 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 303	. . . . . . . . . 10 ⊢ ([⟨1P, (1P +P 1P)⟩] ~R <R [⟨𝑦, 𝑧⟩] ~R ↔ 𝑧<P (1P +P 𝑦))
36	28, 35	bitri 275	. . . . . . . . 9 ⊢ (-1R <R [⟨𝑦, 𝑧⟩] ~R ↔ 𝑧<P (1P +P 𝑦))
37		ltexpri 11080	. . . . . . . . 9 ⊢ (𝑧<P (1P +P 𝑦) → ∃𝑥 ∈ P (𝑧 +P 𝑥) = (1P +P 𝑦))
38	36, 37	sylbi 217	. . . . . . . 8 ⊢ (-1R <R [⟨𝑦, 𝑧⟩] ~R → ∃𝑥 ∈ P (𝑧 +P 𝑥) = (1P +P 𝑦))
39		enreceq 11103	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ P ∧ 1P ∈ P) ∧ (𝑦 ∈ P ∧ 𝑧 ∈ P)) → ([⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ (𝑥 +P 𝑧) = (1P +P 𝑦)))
40	32, 39	mpanl2 701	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ P ∧ (𝑦 ∈ P ∧ 𝑧 ∈ P)) → ([⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ (𝑥 +P 𝑧) = (1P +P 𝑦)))
41		addcompr 11058	. . . . . . . . . . . 12 ⊢ (𝑧 +P 𝑥) = (𝑥 +P 𝑧)
42	41	eqeq1i 2739	. . . . . . . . . . 11 ⊢ ((𝑧 +P 𝑥) = (1P +P 𝑦) ↔ (𝑥 +P 𝑧) = (1P +P 𝑦))
43	40, 42	bitr4di 289	. . . . . . . . . 10 ⊢ ((𝑥 ∈ P ∧ (𝑦 ∈ P ∧ 𝑧 ∈ P)) → ([⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ (𝑧 +P 𝑥) = (1P +P 𝑦)))
44	43	ancoms 458	. . . . . . . . 9 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ 𝑥 ∈ P) → ([⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ (𝑧 +P 𝑥) = (1P +P 𝑦)))
45	44	rexbidva 3174	. . . . . . . 8 ⊢ ((𝑦 ∈ P ∧ 𝑧 ∈ P) → (∃𝑥 ∈ P [⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ ∃𝑥 ∈ P (𝑧 +P 𝑥) = (1P +P 𝑦)))
46	38, 45	imbitrrid 246	. . . . . . 7 ⊢ ((𝑦 ∈ P ∧ 𝑧 ∈ P) → (-1R <R [⟨𝑦, 𝑧⟩] ~R → ∃𝑥 ∈ P [⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ))
47	22, 26, 46	ecoptocl 8845	. . . . . 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 7438	. . . . . . . 8 ⊢ ([⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = (𝐶 +R ((𝐶 ·R -1R) +R 𝐴)))
50	49, 14	sylan9eqr 2796	. . . . . . 7 ⊢ ((𝐴 ∈ R ∧ [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴)) → (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴)
51	50	ex 412	. . . . . 6 ⊢ (𝐴 ∈ R → ([⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴))
52	51	reximdv 3167	. . . . 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 260	. . 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 11145	. . . . 5 ⊢ ((𝐶 +R -1R) <R (𝐶 +R [⟨𝑥, 1P⟩] ~R ) ↔ 𝑥 ∈ P)
57		breq2 5151	. . . . 5 ⊢ ((𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴 → ((𝐶 +R -1R) <R (𝐶 +R [⟨𝑥, 1P⟩] ~R ) ↔ (𝐶 +R -1R) <R 𝐴))
58	56, 57	bitr3id 285	. . . 4 ⊢ ((𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴 → (𝑥 ∈ P ↔ (𝐶 +R -1R) <R 𝐴))
59	58	biimpac 478	. . 3 ⊢ ((𝑥 ∈ P ∧ (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴) → (𝐶 +R -1R) <R 𝐴)
60	59	rexlimiva 3144	. 2 ⊢ (∃𝑥 ∈ P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴 → (𝐶 +R -1R) <R 𝐴)
61	55, 60	impbii 209	1 ⊢ ((𝐶 +R -1R) <R 𝐴 ↔ ∃𝑥 ∈ P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536   ∈ wcel 2105  ∃wrex 3067  ⟨cop 4636   class class class wbr 5147  (class class class)co 7430  [cec 8741  Pcnp 10896  1_Pc1p 10897   +_P cpp 10898  <_P cltp 10900   ~_R cer 10901  Rcnr 10902  0_Rc0r 10903  -1_Rcm1r 10905   +_R cplr 10906   ·_R cmr 10907   <_R cltr 10908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-oadd 8508  df-omul 8509  df-er 8743  df-ec 8745  df-qs 8749  df-ni 10909  df-pli 10910  df-mi 10911  df-lti 10912  df-plpq 10945  df-mpq 10946  df-ltpq 10947  df-enq 10948  df-nq 10949  df-erq 10950  df-plq 10951  df-mq 10952  df-1nq 10953  df-rq 10954  df-ltnq 10955  df-np 11018  df-1p 11019  df-plp 11020  df-mp 11021  df-ltp 11022  df-enr 11092  df-nr 11093  df-plr 11094  df-mr 11095  df-ltr 11096  df-0r 11097  df-1r 11098  df-m1r 11099

This theorem is referenced by:  supsrlem  11148