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	$⊢ C \in 𝑹$
	Assertion	map2psrpr	$⊢ (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} A \leftrightarrow \exists x \in 𝑷 C +_{𝑹} [⟨x, 1_{𝑷}⟩] ~_{𝑹} = A$

Proof

Step	Hyp	Ref	Expression
1		map2psrpr.2	$⊢ C \in 𝑹$
2		ltrelsr	$⊢ <_{𝑹} \subseteq 𝑹 \times 𝑹$
3	2	brel	$⊢ (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} A \to (C +_{𝑹} {-1}_{𝑹} \in 𝑹 \land A \in 𝑹)$
4	3	simprd	$⊢ (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} A \to A \in 𝑹$
5		ltasr	$⊢ C \in 𝑹 \to ({-1}_{𝑹} <_{𝑹} ((C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A) \leftrightarrow (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} (C +_{𝑹} ((C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A)))$
6	1 5	ax-mp	$⊢ {-1}_{𝑹} <_{𝑹} ((C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A) \leftrightarrow (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} (C +_{𝑹} ((C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A))$
7		pn0sr	$⊢ C \in 𝑹 \to C +_{𝑹} (C \cdot_{𝑹} {-1}_{𝑹}) = 0_{𝑹}$
8	1 7	ax-mp	$⊢ C +_{𝑹} (C \cdot_{𝑹} {-1}_{𝑹}) = 0_{𝑹}$
9	8	oveq1i	$⊢ (C +_{𝑹} (C \cdot_{𝑹} {-1}_{𝑹})) +_{𝑹} A = 0_{𝑹} +_{𝑹} A$
10		addasssr	$⊢ (C +_{𝑹} (C \cdot_{𝑹} {-1}_{𝑹})) +_{𝑹} A = C +_{𝑹} ((C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A)$
11		addcomsr	$⊢ 0_{𝑹} +_{𝑹} A = A +_{𝑹} 0_{𝑹}$
12	9 10 11	3eqtr3i	$⊢ C +_{𝑹} ((C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A) = A +_{𝑹} 0_{𝑹}$
13		0idsr	$⊢ A \in 𝑹 \to A +_{𝑹} 0_{𝑹} = A$
14	12 13	syl5eq	$⊢ A \in 𝑹 \to C +_{𝑹} ((C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A) = A$
15	14	breq2d	$⊢ A \in 𝑹 \to ((C +_{𝑹} {-1}_{𝑹}) <_{𝑹} (C +_{𝑹} ((C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A)) \leftrightarrow (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} A)$
16	6 15	syl5bb	$⊢ A \in 𝑹 \to ({-1}_{𝑹} <_{𝑹} ((C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A) \leftrightarrow (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} A)$
17		m1r	$⊢ {-1}_{𝑹} \in 𝑹$
18		mulclsr	$⊢ (C \in 𝑹 \land {-1}_{𝑹} \in 𝑹) \to C \cdot_{𝑹} {-1}_{𝑹} \in 𝑹$
19	1 17 18	mp2an	$⊢ C \cdot_{𝑹} {-1}_{𝑹} \in 𝑹$
20		addclsr	$⊢ (C \cdot_{𝑹} {-1}_{𝑹} \in 𝑹 \land A \in 𝑹) \to (C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A \in 𝑹$
21	19 20	mpan	$⊢ A \in 𝑹 \to (C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A \in 𝑹$
22		df-nr	$⊢ 𝑹 = (𝑷 \times 𝑷) / ~_{𝑹}$
23		breq2	$⊢ [⟨y, z⟩] ~_{𝑹} = (C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A \to ({-1}_{𝑹} <_{𝑹} [⟨y, z⟩] ~_{𝑹} \leftrightarrow {-1}_{𝑹} <_{𝑹} ((C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A))$
24		eqeq2	$⊢ [⟨y, z⟩] ~_{𝑹} = (C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A \to ([⟨x, 1_{𝑷}⟩] ~_{𝑹} = [⟨y, z⟩] ~_{𝑹} \leftrightarrow [⟨x, 1_{𝑷}⟩] ~_{𝑹} = (C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A)$
25	24	rexbidv	$⊢ [⟨y, z⟩] ~_{𝑹} = (C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A \to (\exists x \in 𝑷 [⟨x, 1_{𝑷}⟩] ~_{𝑹} = [⟨y, z⟩] ~_{𝑹} \leftrightarrow \exists x \in 𝑷 [⟨x, 1_{𝑷}⟩] ~_{𝑹} = (C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A)$
26	23 25	imbi12d	$⊢ [⟨y, z⟩] ~_{𝑹} = (C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A \to (({-1}_{𝑹} <_{𝑹} [⟨y, z⟩] ~_{𝑹} \to \exists x \in 𝑷 [⟨x, 1_{𝑷}⟩] ~_{𝑹} = [⟨y, z⟩] ~_{𝑹}) \leftrightarrow ({-1}_{𝑹} <_{𝑹} ((C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A) \to \exists x \in 𝑷 [⟨x, 1_{𝑷}⟩] ~_{𝑹} = (C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A))$
27		df-m1r	$⊢ {-1}_{𝑹} = [⟨1_{𝑷}, 1_{𝑷} +_{𝑷} 1_{𝑷}⟩] ~_{𝑹}$
28	27	breq1i	$⊢ {-1}_{𝑹} <_{𝑹} [⟨y, z⟩] ~_{𝑹} \leftrightarrow [⟨1_{𝑷}, 1_{𝑷} +_{𝑷} 1_{𝑷}⟩] ~_{𝑹} <_{𝑹} [⟨y, z⟩] ~_{𝑹}$
29		addasspr	$⊢ (1_{𝑷} +_{𝑷} 1_{𝑷}) +_{𝑷} y = 1_{𝑷} +_{𝑷} (1_{𝑷} +_{𝑷} y)$
30	29	breq2i	$⊢ (1_{𝑷} +_{𝑷} z) <_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) +_{𝑷} y) \leftrightarrow (1_{𝑷} +_{𝑷} z) <_{𝑷} (1_{𝑷} +_{𝑷} (1_{𝑷} +_{𝑷} y))$
31		ltsrpr	$⊢ [⟨1_{𝑷}, 1_{𝑷} +_{𝑷} 1_{𝑷}⟩] ~_{𝑹} <_{𝑹} [⟨y, z⟩] ~_{𝑹} \leftrightarrow (1_{𝑷} +_{𝑷} z) <_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) +_{𝑷} y)$
32		1pr	$⊢ 1_{𝑷} \in 𝑷$
33		ltapr	$⊢ 1_{𝑷} \in 𝑷 \to (z <_{𝑷} (1_{𝑷} +_{𝑷} y) \leftrightarrow (1_{𝑷} +_{𝑷} z) <_{𝑷} (1_{𝑷} +_{𝑷} (1_{𝑷} +_{𝑷} y)))$
34	32 33	ax-mp	$⊢ z <_{𝑷} (1_{𝑷} +_{𝑷} y) \leftrightarrow (1_{𝑷} +_{𝑷} z) <_{𝑷} (1_{𝑷} +_{𝑷} (1_{𝑷} +_{𝑷} y))$
35	30 31 34	3bitr4i	$⊢ [⟨1_{𝑷}, 1_{𝑷} +_{𝑷} 1_{𝑷}⟩] ~_{𝑹} <_{𝑹} [⟨y, z⟩] ~_{𝑹} \leftrightarrow z <_{𝑷} (1_{𝑷} +_{𝑷} y)$
36	28 35	bitri	$⊢ {-1}_{𝑹} <_{𝑹} [⟨y, z⟩] ~_{𝑹} \leftrightarrow z <_{𝑷} (1_{𝑷} +_{𝑷} y)$
37		ltexpri	$⊢ z <_{𝑷} (1_{𝑷} +_{𝑷} y) \to \exists x \in 𝑷 z +_{𝑷} x = 1_{𝑷} +_{𝑷} y$
38	36 37	sylbi	$⊢ {-1}_{𝑹} <_{𝑹} [⟨y, z⟩] ~_{𝑹} \to \exists x \in 𝑷 z +_{𝑷} x = 1_{𝑷} +_{𝑷} y$
39		enreceq	$⊢ ((x \in 𝑷 \land 1_{𝑷} \in 𝑷) \land (y \in 𝑷 \land z \in 𝑷)) \to ([⟨x, 1_{𝑷}⟩] ~_{𝑹} = [⟨y, z⟩] ~_{𝑹} \leftrightarrow x +_{𝑷} z = 1_{𝑷} +_{𝑷} y)$
40	32 39	mpanl2	$⊢ (x \in 𝑷 \land (y \in 𝑷 \land z \in 𝑷)) \to ([⟨x, 1_{𝑷}⟩] ~_{𝑹} = [⟨y, z⟩] ~_{𝑹} \leftrightarrow x +_{𝑷} z = 1_{𝑷} +_{𝑷} y)$
41		addcompr	$⊢ z +_{𝑷} x = x +_{𝑷} z$
42	41	eqeq1i	$⊢ z +_{𝑷} x = 1_{𝑷} +_{𝑷} y \leftrightarrow x +_{𝑷} z = 1_{𝑷} +_{𝑷} y$
43	40 42	bitr4di	$⊢ (x \in 𝑷 \land (y \in 𝑷 \land z \in 𝑷)) \to ([⟨x, 1_{𝑷}⟩] ~_{𝑹} = [⟨y, z⟩] ~_{𝑹} \leftrightarrow z +_{𝑷} x = 1_{𝑷} +_{𝑷} y)$
44	43	ancoms	$⊢ ((y \in 𝑷 \land z \in 𝑷) \land x \in 𝑷) \to ([⟨x, 1_{𝑷}⟩] ~_{𝑹} = [⟨y, z⟩] ~_{𝑹} \leftrightarrow z +_{𝑷} x = 1_{𝑷} +_{𝑷} y)$
45	44	rexbidva	$⊢ (y \in 𝑷 \land z \in 𝑷) \to (\exists x \in 𝑷 [⟨x, 1_{𝑷}⟩] ~_{𝑹} = [⟨y, z⟩] ~_{𝑹} \leftrightarrow \exists x \in 𝑷 z +_{𝑷} x = 1_{𝑷} +_{𝑷} y)$
46	38 45	syl5ibr	$⊢ (y \in 𝑷 \land z \in 𝑷) \to ({-1}_{𝑹} <_{𝑹} [⟨y, z⟩] ~_{𝑹} \to \exists x \in 𝑷 [⟨x, 1_{𝑷}⟩] ~_{𝑹} = [⟨y, z⟩] ~_{𝑹})$
47	22 26 46	ecoptocl	$⊢ (C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A \in 𝑹 \to ({-1}_{𝑹} <_{𝑹} ((C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A) \to \exists x \in 𝑷 [⟨x, 1_{𝑷}⟩] ~_{𝑹} = (C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A)$
48	21 47	syl	$⊢ A \in 𝑹 \to ({-1}_{𝑹} <_{𝑹} ((C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A) \to \exists x \in 𝑷 [⟨x, 1_{𝑷}⟩] ~_{𝑹} = (C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A)$
49		oveq2	$⊢ [⟨x, 1_{𝑷}⟩] ~_{𝑹} = (C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A \to C +_{𝑹} [⟨x, 1_{𝑷}⟩] ~_{𝑹} = C +_{𝑹} ((C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A)$
50	49 14	sylan9eqr	$⊢ (A \in 𝑹 \land [⟨x, 1_{𝑷}⟩] ~_{𝑹} = (C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A) \to C +_{𝑹} [⟨x, 1_{𝑷}⟩] ~_{𝑹} = A$
51	50	ex	$⊢ A \in 𝑹 \to ([⟨x, 1_{𝑷}⟩] ~_{𝑹} = (C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A \to C +_{𝑹} [⟨x, 1_{𝑷}⟩] ~_{𝑹} = A)$
52	51	reximdv	$⊢ A \in 𝑹 \to (\exists x \in 𝑷 [⟨x, 1_{𝑷}⟩] ~_{𝑹} = (C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A \to \exists x \in 𝑷 C +_{𝑹} [⟨x, 1_{𝑷}⟩] ~_{𝑹} = A)$
53	48 52	syld	$⊢ A \in 𝑹 \to ({-1}_{𝑹} <_{𝑹} ((C \cdot_{𝑹} {-1}_{𝑹}) +_{𝑹} A) \to \exists x \in 𝑷 C +_{𝑹} [⟨x, 1_{𝑷}⟩] ~_{𝑹} = A)$
54	16 53	sylbird	$⊢ A \in 𝑹 \to ((C +_{𝑹} {-1}_{𝑹}) <_{𝑹} A \to \exists x \in 𝑷 C +_{𝑹} [⟨x, 1_{𝑷}⟩] ~_{𝑹} = A)$
55	4 54	mpcom	$⊢ (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} A \to \exists x \in 𝑷 C +_{𝑹} [⟨x, 1_{𝑷}⟩] ~_{𝑹} = A$
56	1	mappsrpr	$⊢ (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} (C +_{𝑹} [⟨x, 1_{𝑷}⟩] ~_{𝑹}) \leftrightarrow x \in 𝑷$
57		breq2	$⊢ C +_{𝑹} [⟨x, 1_{𝑷}⟩] ~_{𝑹} = A \to ((C +_{𝑹} {-1}_{𝑹}) <_{𝑹} (C +_{𝑹} [⟨x, 1_{𝑷}⟩] ~_{𝑹}) \leftrightarrow (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} A)$
58	56 57	bitr3id	$⊢ C +_{𝑹} [⟨x, 1_{𝑷}⟩] ~_{𝑹} = A \to (x \in 𝑷 \leftrightarrow (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} A)$
59	58	biimpac	$⊢ (x \in 𝑷 \land C +_{𝑹} [⟨x, 1_{𝑷}⟩] ~_{𝑹} = A) \to (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} A$
60	59	rexlimiva	$⊢ \exists x \in 𝑷 C +_{𝑹} [⟨x, 1_{𝑷}⟩] ~_{𝑹} = A \to (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} A$
61	55 60	impbii	$⊢ (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} A \leftrightarrow \exists x \in 𝑷 C +_{𝑹} [⟨x, 1_{𝑷}⟩] ~_{𝑹} = A$

Metamath Proof Explorer

Theorem map2psrpr

Proof