mulsrmo

Description: There is at most one result from multiplying signed reals. (Contributed by Jim Kingdon, 30-Dec-2019)

		Ref	Expression
	Assertion	mulsrmo	$⊢ (A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \to \exists^{*} z \exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹})$

Proof

Step	Hyp	Ref	Expression
1		enrer	$⊢ ~_{𝑹} Er (𝑷 \times 𝑷)$
2	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 𝑷)$
3		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))$
4		mulcmpblnr	$⊢ (((w \in 𝑷 \land v \in 𝑷) \land (s \in 𝑷 \land f \in 𝑷)) \land ((u \in 𝑷 \land t \in 𝑷) \land (g \in 𝑷 \land h \in 𝑷))) \to ((w +_{𝑷} f = v +_{𝑷} s \land u +_{𝑷} h = t +_{𝑷} g) \to ⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩ ~_{𝑹} ⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩)$
5	4	imp	$⊢ ((((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)) \to ⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩ ~_{𝑹} ⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩$
6	3 5	syl	$⊢ ((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 \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩ ~_{𝑹} ⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩$
7	2 6	erthi	$⊢ ((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 \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹} = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹}$
8	7	adantrlr	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land (((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \land (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))) \to [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹} = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹}$
9	8	adantrrr	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land (((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \land ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹}))) \to [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹} = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹}$
10		simprlr	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land (((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \land ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹}))) \to z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}$
11		simprrr	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land (((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \land ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹}))) \to q = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹}$
12	9 10 11	3eqtr4d	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land (((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \land ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹}))) \to z = q$
13	12	expr	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹})) \to (((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹}) \to z = q)$
14	13	exlimdvv	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹})) \to (\exists g \exists h ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹}) \to z = q)$
15	14	exlimdvv	$⊢ ((A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \land ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹})) \to (\exists s \exists f \exists g \exists h ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹}) \to z = q)$
16	15	ex	$⊢ (A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \to (((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \to (\exists s \exists f \exists g \exists h ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹}) \to z = q))$
17	16	exlimdvv	$⊢ (A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \to (\exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \to (\exists s \exists f \exists g \exists h ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹}) \to z = q))$
18	17	exlimdvv	$⊢ (A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \to (\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \to (\exists s \exists f \exists g \exists h ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹}) \to z = q))$
19	18	impd	$⊢ (A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \to ((\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \land \exists s \exists f \exists g \exists h ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹})) \to z = q)$
20	19	alrimivv	$⊢ (A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \to \forall z \forall q ((\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \land \exists s \exists f \exists g \exists h ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹})) \to z = q)$
21		opeq12	$⊢ (w = s \land v = f) \to ⟨w, v⟩ = ⟨s, f⟩$
22	21	eceq1d	$⊢ (w = s \land v = f) \to [⟨w, v⟩] ~_{𝑹} = [⟨s, f⟩] ~_{𝑹}$
23	22	eqeq2d	$⊢ (w = s \land v = f) \to (A = [⟨w, v⟩] ~_{𝑹} \leftrightarrow A = [⟨s, f⟩] ~_{𝑹})$
24	23	anbi1d	$⊢ (w = s \land v = f) \to ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \leftrightarrow (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}))$
25		simpl	$⊢ (w = s \land v = f) \to w = s$
26	25	oveq1d	$⊢ (w = s \land v = f) \to w \cdot_{𝑷} u = s \cdot_{𝑷} u$
27		simpr	$⊢ (w = s \land v = f) \to v = f$
28	27	oveq1d	$⊢ (w = s \land v = f) \to v \cdot_{𝑷} t = f \cdot_{𝑷} t$
29	26 28	oveq12d	$⊢ (w = s \land v = f) \to (w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t) = (s \cdot_{𝑷} u) +_{𝑷} (f \cdot_{𝑷} t)$
30	25	oveq1d	$⊢ (w = s \land v = f) \to w \cdot_{𝑷} t = s \cdot_{𝑷} t$
31	27	oveq1d	$⊢ (w = s \land v = f) \to v \cdot_{𝑷} u = f \cdot_{𝑷} u$
32	30 31	oveq12d	$⊢ (w = s \land v = f) \to (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u) = (s \cdot_{𝑷} t) +_{𝑷} (f \cdot_{𝑷} u)$
33	29 32	opeq12d	$⊢ (w = s \land v = f) \to ⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩ = ⟨(s \cdot_{𝑷} u) +_{𝑷} (f \cdot_{𝑷} t), (s \cdot_{𝑷} t) +_{𝑷} (f \cdot_{𝑷} u)⟩$
34	33	eceq1d	$⊢ (w = s \land v = f) \to [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹} = [⟨(s \cdot_{𝑷} u) +_{𝑷} (f \cdot_{𝑷} t), (s \cdot_{𝑷} t) +_{𝑷} (f \cdot_{𝑷} u)⟩] ~_{𝑹}$
35	34	eqeq2d	$⊢ (w = s \land v = f) \to (q = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹} \leftrightarrow q = [⟨(s \cdot_{𝑷} u) +_{𝑷} (f \cdot_{𝑷} t), (s \cdot_{𝑷} t) +_{𝑷} (f \cdot_{𝑷} u)⟩] ~_{𝑹})$
36	24 35	anbi12d	$⊢ (w = s \land v = f) \to (((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land q = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \leftrightarrow ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land q = [⟨(s \cdot_{𝑷} u) +_{𝑷} (f \cdot_{𝑷} t), (s \cdot_{𝑷} t) +_{𝑷} (f \cdot_{𝑷} u)⟩] ~_{𝑹}))$
37		opeq12	$⊢ (u = g \land t = h) \to ⟨u, t⟩ = ⟨g, h⟩$
38	37	eceq1d	$⊢ (u = g \land t = h) \to [⟨u, t⟩] ~_{𝑹} = [⟨g, h⟩] ~_{𝑹}$
39	38	eqeq2d	$⊢ (u = g \land t = h) \to (B = [⟨u, t⟩] ~_{𝑹} \leftrightarrow B = [⟨g, h⟩] ~_{𝑹})$
40	39	anbi2d	$⊢ (u = g \land t = h) \to ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \leftrightarrow (A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}))$
41		simpl	$⊢ (u = g \land t = h) \to u = g$
42	41	oveq2d	$⊢ (u = g \land t = h) \to s \cdot_{𝑷} u = s \cdot_{𝑷} g$
43		simpr	$⊢ (u = g \land t = h) \to t = h$
44	43	oveq2d	$⊢ (u = g \land t = h) \to f \cdot_{𝑷} t = f \cdot_{𝑷} h$
45	42 44	oveq12d	$⊢ (u = g \land t = h) \to (s \cdot_{𝑷} u) +_{𝑷} (f \cdot_{𝑷} t) = (s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h)$
46	43	oveq2d	$⊢ (u = g \land t = h) \to s \cdot_{𝑷} t = s \cdot_{𝑷} h$
47	41	oveq2d	$⊢ (u = g \land t = h) \to f \cdot_{𝑷} u = f \cdot_{𝑷} g$
48	46 47	oveq12d	$⊢ (u = g \land t = h) \to (s \cdot_{𝑷} t) +_{𝑷} (f \cdot_{𝑷} u) = (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)$
49	45 48	opeq12d	$⊢ (u = g \land t = h) \to ⟨(s \cdot_{𝑷} u) +_{𝑷} (f \cdot_{𝑷} t), (s \cdot_{𝑷} t) +_{𝑷} (f \cdot_{𝑷} u)⟩ = ⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩$
50	49	eceq1d	$⊢ (u = g \land t = h) \to [⟨(s \cdot_{𝑷} u) +_{𝑷} (f \cdot_{𝑷} t), (s \cdot_{𝑷} t) +_{𝑷} (f \cdot_{𝑷} u)⟩] ~_{𝑹} = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹}$
51	50	eqeq2d	$⊢ (u = g \land t = h) \to (q = [⟨(s \cdot_{𝑷} u) +_{𝑷} (f \cdot_{𝑷} t), (s \cdot_{𝑷} t) +_{𝑷} (f \cdot_{𝑷} u)⟩] ~_{𝑹} \leftrightarrow q = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹})$
52	40 51	anbi12d	$⊢ (u = g \land t = h) \to (((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land q = [⟨(s \cdot_{𝑷} u) +_{𝑷} (f \cdot_{𝑷} t), (s \cdot_{𝑷} t) +_{𝑷} (f \cdot_{𝑷} u)⟩] ~_{𝑹}) \leftrightarrow ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹}))$
53	36 52	cbvex4vw	$⊢ \exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land q = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \leftrightarrow \exists s \exists f \exists g \exists h ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹})$
54	53	anbi2i	$⊢ (\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \land \exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land q = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹})) \leftrightarrow (\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \land \exists s \exists f \exists g \exists h ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹}))$
55	54	imbi1i	$⊢ ((\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \land \exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land q = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹})) \to z = q) \leftrightarrow ((\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \land \exists s \exists f \exists g \exists h ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹})) \to z = q)$
56	55	2albii	$⊢ \forall z \forall q ((\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \land \exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land q = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹})) \to z = q) \leftrightarrow \forall z \forall q ((\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \land \exists s \exists f \exists g \exists h ((A = [⟨s, f⟩] ~_{𝑹} \land B = [⟨g, h⟩] ~_{𝑹}) \land q = [⟨(s \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h), (s \cdot_{𝑷} h) +_{𝑷} (f \cdot_{𝑷} g)⟩] ~_{𝑹})) \to z = q)$
57	20 56	sylibr	$⊢ (A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \to \forall z \forall q ((\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \land \exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land q = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹})) \to z = q)$
58		eqeq1	$⊢ z = q \to (z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹} \leftrightarrow q = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹})$
59	58	anbi2d	$⊢ z = q \to (((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \leftrightarrow ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land q = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}))$
60	59	4exbidv	$⊢ z = q \to (\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \leftrightarrow \exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land q = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}))$
61	60	mo4	$⊢ \exists^{*} z \exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \leftrightarrow \forall z \forall q ((\exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}) \land \exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land q = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹})) \to z = q)$
62	57 61	sylibr	$⊢ (A \in ((𝑷 \times 𝑷) / ~_{𝑹}) \land B \in ((𝑷 \times 𝑷) / ~_{𝑹})) \to \exists^{*} z \exists w \exists v \exists u \exists t ((A = [⟨w, v⟩] ~_{𝑹} \land B = [⟨u, t⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} t), (w \cdot_{𝑷} t) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹})$

Metamath Proof Explorer

Theorem mulsrmo

Proof