Theorem mappsrpr

Description: Mapping from positive signed reals to positive reals. (Contributed by NM, 17-May-1996) (Revised by Mario Carneiro, 15-Jun-2013) (New usage is discouraged.)

	Ref	Expression
Hypothesis	mappsrpr.2	|- C e. R.
Assertion	mappsrpr	|- ( ( C +R -1R ) . ] ~R ) <-> A e. P. )

Proof

Step	Hyp	Ref	Expression
1		mappsrpr.2	|- C e. R.
2		df-m1r	|- -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
3	2	breq1i	|- ( -1R . ] ~R <-> [ <. 1P , ( 1P +P. 1P ) >. ] ~R . ] ~R )
4		ltsrpr	|- ( [ <. 1P , ( 1P +P. 1P ) >. ] ~R . ] ~R <-> ( 1P +P. 1P )
5	3 4	bitri	|- ( -1R . ] ~R <-> ( 1P +P. 1P )
6		ltasr	|- ( C e. R. -> ( -1R . ] ~R <-> ( C +R -1R ) . ] ~R ) ) )
7	1 6	ax-mp	|- ( -1R . ] ~R <-> ( C +R -1R ) . ] ~R ) )
8		ltrelpr	|-
9	8	brel	|- ( ( 1P +P. 1P ) ( ( 1P +P. 1P ) e. P. /\ ( ( 1P +P. 1P ) +P. A ) e. P. ) )
10		dmplp	|- dom +P. = ( P. X. P. )
11		0npr	|- -. (/) e. P.
12	10 11	ndmovrcl	|- ( ( ( 1P +P. 1P ) +P. A ) e. P. -> ( ( 1P +P. 1P ) e. P. /\ A e. P. ) )
13	12	simprd	|- ( ( ( 1P +P. 1P ) +P. A ) e. P. -> A e. P. )
14	9 13	simpl2im	|- ( ( 1P +P. 1P ) A e. P. )
15		1pr	|- 1P e. P.
16		addclpr	|- ( ( 1P e. P. /\ 1P e. P. ) -> ( 1P +P. 1P ) e. P. )
17	15 15 16	mp2an	|- ( 1P +P. 1P ) e. P.
18		ltaddpr	|- ( ( ( 1P +P. 1P ) e. P. /\ A e. P. ) -> ( 1P +P. 1P )
19	17 18	mpan	|- ( A e. P. -> ( 1P +P. 1P )
20	14 19	impbii	|- ( ( 1P +P. 1P ) A e. P. )
21	5 7 20	3bitr3i	|- ( ( C +R -1R ) . ] ~R ) <-> A e. P. )