# Metamath Proof Explorer

## Theorem mulsrmo

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

Ref Expression
Assertion mulsrmo ${⊢}\left({A}\in \left(\left(𝑷×𝑷\right)/{~}_{𝑹}\right)\wedge {B}\in \left(\left(𝑷×𝑷\right)/{~}_{𝑹}\right)\right)\to {\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\exists {t}\phantom{\rule{.4em}{0ex}}\left(\left({A}=\left[⟨{w},{v}⟩\right]{~}_{𝑹}\wedge {B}=\left[⟨{u},{t}⟩\right]{~}_{𝑹}\right)\wedge {z}=\left[⟨\left({w}{\cdot }_{𝑷}{u}\right){+}_{𝑷}\left({v}{\cdot }_{𝑷}{t}\right),\left({w}{\cdot }_{𝑷}{t}\right){+}_{𝑷}\left({v}{\cdot }_{𝑷}{u}\right)⟩\right]{~}_{𝑹}\right)$

### Proof

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