Theorem map2psrpr

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

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

Proof

Step	Hyp	Ref	Expression
1		map2psrpr.2	⊢ 𝐶 ∈ R
2		ltrelsr	⊢ <R ⊆ ( R × R )
3	2	brel	⊢ ( ( 𝐶 +R -1R ) <R 𝐴 → ( ( 𝐶 +R -1R ) ∈ R ∧ 𝐴 ∈ R ) )
4	3	simprd	⊢ ( ( 𝐶 +R -1R ) <R 𝐴 → 𝐴 ∈ R )
5		ltasr	⊢ ( 𝐶 ∈ R → ( -1R <R ( ( 𝐶 ·R -1R ) +R 𝐴 ) ↔ ( 𝐶 +R -1R ) <R ( 𝐶 +R ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) ) )
6	1 5	ax-mp	⊢ ( -1R <R ( ( 𝐶 ·R -1R ) +R 𝐴 ) ↔ ( 𝐶 +R -1R ) <R ( 𝐶 +R ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) )
7		pn0sr	⊢ ( 𝐶 ∈ R → ( 𝐶 +R ( 𝐶 ·R -1R ) ) = 0R )
8	1 7	ax-mp	⊢ ( 𝐶 +R ( 𝐶 ·R -1R ) ) = 0R
9	8	oveq1i	⊢ ( ( 𝐶 +R ( 𝐶 ·R -1R ) ) +R 𝐴 ) = ( 0R +R 𝐴 )
10		addasssr	⊢ ( ( 𝐶 +R ( 𝐶 ·R -1R ) ) +R 𝐴 ) = ( 𝐶 +R ( ( 𝐶 ·R -1R ) +R 𝐴 ) )
11		addcomsr	⊢ ( 0R +R 𝐴 ) = ( 𝐴 +R 0R )
12	9 10 11	3eqtr3i	⊢ ( 𝐶 +R ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) = ( 𝐴 +R 0R )
13		0idsr	⊢ ( 𝐴 ∈ R → ( 𝐴 +R 0R ) = 𝐴 )
14	12 13	eqtrid	⊢ ( 𝐴 ∈ R → ( 𝐶 +R ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) = 𝐴 )
15	14	breq2d	⊢ ( 𝐴 ∈ R → ( ( 𝐶 +R -1R ) <R ( 𝐶 +R ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) ↔ ( 𝐶 +R -1R ) <R 𝐴 ) )
16	6 15	syl5bb	⊢ ( 𝐴 ∈ R → ( -1R <R ( ( 𝐶 ·R -1R ) +R 𝐴 ) ↔ ( 𝐶 +R -1R ) <R 𝐴 ) )
17		m1r	⊢ -1R ∈ R
18		mulclsr	⊢ ( ( 𝐶 ∈ R ∧ -1R ∈ R ) → ( 𝐶 ·R -1R ) ∈ R )
19	1 17 18	mp2an	⊢ ( 𝐶 ·R -1R ) ∈ R
20		addclsr	⊢ ( ( ( 𝐶 ·R -1R ) ∈ R ∧ 𝐴 ∈ R ) → ( ( 𝐶 ·R -1R ) +R 𝐴 ) ∈ R )
21	19 20	mpan	⊢ ( 𝐴 ∈ R → ( ( 𝐶 ·R -1R ) +R 𝐴 ) ∈ R )
22		df-nr	⊢ R = ( ( P × P ) / ~R )
23		breq2	⊢ ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) → ( -1R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ -1R <R ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) )
24		eqeq2	⊢ ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) → ( [ ⟨ 𝑥 , 1P ⟩ ] ~R = [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ [ ⟨ 𝑥 , 1P ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) )
25	24	rexbidv	⊢ ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) → ( ∃ 𝑥 ∈ P [ ⟨ 𝑥 , 1P ⟩ ] ~R = [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ ∃ 𝑥 ∈ P [ ⟨ 𝑥 , 1P ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) )
26	23 25	imbi12d	⊢ ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~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	⊢ -1R = [ ⟨ 1P , ( 1P +P 1P ) ⟩ ] ~R
28	27	breq1i	⊢ ( -1R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ [ ⟨ 1P , ( 1P +P 1P ) ⟩ ] ~R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R )
29		addasspr	⊢ ( ( 1P +P 1P ) +P 𝑦 ) = ( 1P +P ( 1P +P 𝑦 ) )
30	29	breq2i	⊢ ( ( 1P +P 𝑧 ) <P ( ( 1P +P 1P ) +P 𝑦 ) ↔ ( 1P +P 𝑧 ) <P ( 1P +P ( 1P +P 𝑦 ) ) )
31		ltsrpr	⊢ ( [ ⟨ 1P , ( 1P +P 1P ) ⟩ ] ~R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ ( 1P +P 𝑧 ) <P ( ( 1P +P 1P ) +P 𝑦 ) )
32		1pr	⊢ 1P ∈ P
33		ltapr	⊢ ( 1P ∈ P → ( 𝑧 <P ( 1P +P 𝑦 ) ↔ ( 1P +P 𝑧 ) <P ( 1P +P ( 1P +P 𝑦 ) ) ) )
34	32 33	ax-mp	⊢ ( 𝑧 <P ( 1P +P 𝑦 ) ↔ ( 1P +P 𝑧 ) <P ( 1P +P ( 1P +P 𝑦 ) ) )
35	30 31 34	3bitr4i	⊢ ( [ ⟨ 1P , ( 1P +P 1P ) ⟩ ] ~R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ 𝑧 <P ( 1P +P 𝑦 ) )
36	28 35	bitri	⊢ ( -1R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ 𝑧 <P ( 1P +P 𝑦 ) )
37		ltexpri	⊢ ( 𝑧 <P ( 1P +P 𝑦 ) → ∃ 𝑥 ∈ P ( 𝑧 +P 𝑥 ) = ( 1P +P 𝑦 ) )
38	36 37	sylbi	⊢ ( -1R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R → ∃ 𝑥 ∈ P ( 𝑧 +P 𝑥 ) = ( 1P +P 𝑦 ) )
39		enreceq	⊢ ( ( ( 𝑥 ∈ P ∧ 1P ∈ P ) ∧ ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ) → ( [ ⟨ 𝑥 , 1P ⟩ ] ~R = [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ ( 𝑥 +P 𝑧 ) = ( 1P +P 𝑦 ) ) )
40	32 39	mpanl2	⊢ ( ( 𝑥 ∈ P ∧ ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ) → ( [ ⟨ 𝑥 , 1P ⟩ ] ~R = [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ ( 𝑥 +P 𝑧 ) = ( 1P +P 𝑦 ) ) )
41		addcompr	⊢ ( 𝑧 +P 𝑥 ) = ( 𝑥 +P 𝑧 )
42	41	eqeq1i	⊢ ( ( 𝑧 +P 𝑥 ) = ( 1P +P 𝑦 ) ↔ ( 𝑥 +P 𝑧 ) = ( 1P +P 𝑦 ) )
43	40 42	bitr4di	⊢ ( ( 𝑥 ∈ P ∧ ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ) → ( [ ⟨ 𝑥 , 1P ⟩ ] ~R = [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ ( 𝑧 +P 𝑥 ) = ( 1P +P 𝑦 ) ) )
44	43	ancoms	⊢ ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑥 ∈ P ) → ( [ ⟨ 𝑥 , 1P ⟩ ] ~R = [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ ( 𝑧 +P 𝑥 ) = ( 1P +P 𝑦 ) ) )
45	44	rexbidva	⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( ∃ 𝑥 ∈ P [ ⟨ 𝑥 , 1P ⟩ ] ~R = [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ ∃ 𝑥 ∈ P ( 𝑧 +P 𝑥 ) = ( 1P +P 𝑦 ) ) )
46	38 45	syl5ibr	⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( -1R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R → ∃ 𝑥 ∈ P [ ⟨ 𝑥 , 1P ⟩ ] ~R = [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ) )
47	22 26 46	ecoptocl	⊢ ( ( ( 𝐶 ·R -1R ) +R 𝐴 ) ∈ R → ( -1R <R ( ( 𝐶 ·R -1R ) +R 𝐴 ) → ∃ 𝑥 ∈ P [ ⟨ 𝑥 , 1P ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) )
48	21 47	syl	⊢ ( 𝐴 ∈ R → ( -1R <R ( ( 𝐶 ·R -1R ) +R 𝐴 ) → ∃ 𝑥 ∈ P [ ⟨ 𝑥 , 1P ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) )
49		oveq2	⊢ ( [ ⟨ 𝑥 , 1P ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) → ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = ( 𝐶 +R ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) )
50	49 14	sylan9eqr	⊢ ( ( 𝐴 ∈ R ∧ [ ⟨ 𝑥 , 1P ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) → ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 )
51	50	ex	⊢ ( 𝐴 ∈ R → ( [ ⟨ 𝑥 , 1P ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) → ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 ) )
52	51	reximdv	⊢ ( 𝐴 ∈ R → ( ∃ 𝑥 ∈ P [ ⟨ 𝑥 , 1P ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) → ∃ 𝑥 ∈ P ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 ) )
53	48 52	syld	⊢ ( 𝐴 ∈ R → ( -1R <R ( ( 𝐶 ·R -1R ) +R 𝐴 ) → ∃ 𝑥 ∈ P ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 ) )
54	16 53	sylbird	⊢ ( 𝐴 ∈ R → ( ( 𝐶 +R -1R ) <R 𝐴 → ∃ 𝑥 ∈ P ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 ) )
55	4 54	mpcom	⊢ ( ( 𝐶 +R -1R ) <R 𝐴 → ∃ 𝑥 ∈ P ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 )
56	1	mappsrpr	⊢ ( ( 𝐶 +R -1R ) <R ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) ↔ 𝑥 ∈ P )
57		breq2	⊢ ( ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 → ( ( 𝐶 +R -1R ) <R ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) ↔ ( 𝐶 +R -1R ) <R 𝐴 ) )
58	56 57	bitr3id	⊢ ( ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 → ( 𝑥 ∈ P ↔ ( 𝐶 +R -1R ) <R 𝐴 ) )
59	58	biimpac	⊢ ( ( 𝑥 ∈ P ∧ ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 ) → ( 𝐶 +R -1R ) <R 𝐴 )
60	59	rexlimiva	⊢ ( ∃ 𝑥 ∈ P ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 → ( 𝐶 +R -1R ) <R 𝐴 )
61	55 60	impbii	⊢ ( ( 𝐶 +R -1R ) <R 𝐴 ↔ ∃ 𝑥 ∈ P ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 )