prsrlem1

Description: Decomposing signed reals into positive reals. Lemma for addsrpr and mulsrpr . (Contributed by Jim Kingdon, 30-Dec-2019)

		Ref	Expression
	Assertion	prsrlem1	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to ((((w \in 𝑷 \land v \in 𝑷) \land (s \in 𝑷 \land f \in 𝑷)) \land ((u \in 𝑷 \land t \in 𝑷) \land (g \in 𝑷 \land h \in 𝑷))) \land (w +_{𝑷} f = v +_{𝑷} s \land u +_{𝑷} h = t +_{𝑷} g))$

Proof

Step	Hyp	Ref	Expression
1		enrer	$⊢ ~_{𝑹} Er (𝑷 \times 𝑷)$
2		erdm	$⊢ ~_{𝑹} Er (𝑷 \times 𝑷) \to dom ~_{𝑹} = 𝑷 \times 𝑷$
3	1 2	ax-mp	$⊢ dom ~_{𝑹} = 𝑷 \times 𝑷$
4		simprll	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to A = [⟨w, v⟩] ~_{𝑹}$
5		simpll	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to A \in ((𝑷 \times 𝑷) / ~_{𝑹})$
6	4 5	eqeltrrd	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to [⟨w, v⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹})$
7		ecelqsdm	$⊢ (dom ~_{𝑹} = 𝑷 \times 𝑷 \land [⟨w, v⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹})) \to ⟨w, v⟩ \in (𝑷 \times 𝑷)$
8	3 6 7	sylancr	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to ⟨w, v⟩ \in (𝑷 \times 𝑷)$
9		opelxp	$⊢ ⟨w, v⟩ \in (𝑷 \times 𝑷) \leftrightarrow (w \in 𝑷 \land v \in 𝑷)$
10	8 9	sylib	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to (w \in 𝑷 \land v \in 𝑷)$
11		simprrl	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to A = [⟨s, f⟩] ~_{𝑹}$
12	11 5	eqeltrrd	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to [⟨s, f⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹})$
13		ecelqsdm	$⊢ (dom ~_{𝑹} = 𝑷 \times 𝑷 \land [⟨s, f⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹})) \to ⟨s, f⟩ \in (𝑷 \times 𝑷)$
14	3 12 13	sylancr	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to ⟨s, f⟩ \in (𝑷 \times 𝑷)$
15		opelxp	$⊢ ⟨s, f⟩ \in (𝑷 \times 𝑷) \leftrightarrow (s \in 𝑷 \land f \in 𝑷)$
16	14 15	sylib	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to (s \in 𝑷 \land f \in 𝑷)$
17	10 16	jca	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to ((w \in 𝑷 \land v \in 𝑷) \land (s \in 𝑷 \land f \in 𝑷))$
18		simprlr	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to B = [⟨u, t⟩] ~_{𝑹}$
19		simplr	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to B \in ((𝑷 \times 𝑷) / ~_{𝑹})$
20	18 19	eqeltrrd	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to [⟨u, t⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹})$
21		ecelqsdm	$⊢ (dom ~_{𝑹} = 𝑷 \times 𝑷 \land [⟨u, t⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹})) \to ⟨u, t⟩ \in (𝑷 \times 𝑷)$
22	3 20 21	sylancr	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to ⟨u, t⟩ \in (𝑷 \times 𝑷)$
23		opelxp	$⊢ ⟨u, t⟩ \in (𝑷 \times 𝑷) \leftrightarrow (u \in 𝑷 \land t \in 𝑷)$
24	22 23	sylib	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to (u \in 𝑷 \land t \in 𝑷)$
25		simprrr	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to B = [⟨g, h⟩] ~_{𝑹}$
26	25 19	eqeltrrd	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to [⟨g, h⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹})$
27		ecelqsdm	$⊢ (dom ~_{𝑹} = 𝑷 \times 𝑷 \land [⟨g, h⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹})) \to ⟨g, h⟩ \in (𝑷 \times 𝑷)$
28	3 26 27	sylancr	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to ⟨g, h⟩ \in (𝑷 \times 𝑷)$
29		opelxp	$⊢ ⟨g, h⟩ \in (𝑷 \times 𝑷) \leftrightarrow (g \in 𝑷 \land h \in 𝑷)$
30	28 29	sylib	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to (g \in 𝑷 \land h \in 𝑷)$
31	24 30	jca	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to ((u \in 𝑷 \land t \in 𝑷) \land (g \in 𝑷 \land h \in 𝑷))$
32	4 11	eqtr3d	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to [⟨w, v⟩] ~_{𝑹} = [⟨s, f⟩] ~_{𝑹}$
33	1	a1i	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to ~_{𝑹} Er (𝑷 \times 𝑷)$
34	33 8	erth	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to (⟨w, v⟩ ~_{𝑹} ⟨s, f⟩ \leftrightarrow [⟨w, v⟩] ~_{𝑹} = [⟨s, f⟩] ~_{𝑹})$
35	32 34	mpbird	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to ⟨w, v⟩ ~_{𝑹} ⟨s, f⟩$
36		df-enr	$⊢ ~_{𝑹} = \{⟨x, y⟩ \| ((x \in (𝑷 \times 𝑷) \land y \in (𝑷 \times 𝑷)) \land \exists a \exists b \exists c \exists d ((x = ⟨a, b⟩ \land y = ⟨c, d⟩) \land a +_{𝑷} d = b +_{𝑷} c))\}$
37	36	ecopoveq	$⊢ ((w \in 𝑷 \land v \in 𝑷) \land (s \in 𝑷 \land f \in 𝑷)) \to (⟨w, v⟩ ~_{𝑹} ⟨s, f⟩ \leftrightarrow w +_{𝑷} f = v +_{𝑷} s)$
38	10 16 37	syl2anc	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to (⟨w, v⟩ ~_{𝑹} ⟨s, f⟩ \leftrightarrow w +_{𝑷} f = v +_{𝑷} s)$
39	35 38	mpbid	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to w +_{𝑷} f = v +_{𝑷} s$
40	18 25	eqtr3d	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to [⟨u, t⟩] ~_{𝑹} = [⟨g, h⟩] ~_{𝑹}$
41	33 22	erth	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to (⟨u, t⟩ ~_{𝑹} ⟨g, h⟩ \leftrightarrow [⟨u, t⟩] ~_{𝑹} = [⟨g, h⟩] ~_{𝑹})$
42	40 41	mpbird	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to ⟨u, t⟩ ~_{𝑹} ⟨g, h⟩$
43	36	ecopoveq	$⊢ ((u \in 𝑷 \land t \in 𝑷) \land (g \in 𝑷 \land h \in 𝑷)) \to (⟨u, t⟩ ~_{𝑹} ⟨g, h⟩ \leftrightarrow u +_{𝑷} h = t +_{𝑷} g)$
44	24 30 43	syl2anc	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to (⟨u, t⟩ ~_{𝑹} ⟨g, h⟩ \leftrightarrow u +_{𝑷} h = t +_{𝑷} g)$
45	42 44	mpbid	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to u +_{𝑷} h = t +_{𝑷} g$
46	39 45	jca	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to (w +_{𝑷} f = v +_{𝑷} s \land u +_{𝑷} h = t +_{𝑷} g)$
47	17 31 46	jca31	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to ((((w \in 𝑷 \land v \in 𝑷) \land (s \in 𝑷 \land f \in 𝑷)) \land ((u \in 𝑷 \land t \in 𝑷) \land (g \in 𝑷 \land h \in 𝑷))) \land (w +_{𝑷} f = v +_{𝑷} s \land u +_{𝑷} h = t +_{𝑷} g))$

Metamath Proof Explorer

Theorem prsrlem1

Proof