MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulsasslem1 Structured version   Visualization version   GIF version

Theorem mulsasslem1 28606
Description: Lemma for mulsass 28609. Expand the left hand side of the formula. (Contributed by Scott Fenton, 9-Mar-2025.)
Hypotheses
Ref Expression
mulsasslem.1 (𝜑 → 𝐴 ∈ No)
mulsasslem.2 (𝜑 → 𝐵 ∈ No)
mulsasslem.3 (𝜑 → 𝐶 ∈ No)
Assertion
Ref Expression
mulsasslem1 (𝜑 → ((𝐴 ·s 𝐵) ·s 𝐶) = ((({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿))}) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅))})) |s (({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅))}) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿))}))))
Distinct variable groups:   𝐴,𝑎,𝑥𝐿,𝑥𝑅,𝑦𝐿,𝑦𝑅,𝑧𝐿,𝑧𝑅   𝐵,𝑎,𝑥𝐿,𝑥𝑅,𝑦𝐿,𝑦𝑅,𝑧𝐿,𝑧𝑅   𝐶,𝑎,𝑥𝐿,𝑥𝑅,𝑦𝐿,𝑦𝑅,𝑧𝐿,𝑧𝑅
Allowed substitution hints:   𝜑(𝑎, 𝑥𝐿, 𝑥𝑅, 𝑦𝐿, 𝑦𝑅, 𝑧𝐿, 𝑧𝑅)

Proof of Theorem mulsasslem1
Dummy variables 𝑏 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mulsasslem.1 . . . 4 (𝜑 → 𝐴 ∈ No)
2 mulsasslem.2 . . . 4 (𝜑 → 𝐵 ∈ No)
31, 2mulcut2 28576 . . 3 (𝜑 → ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))}) <<s ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))}))
4 lltr 28305 . . . 4 (L‘𝐶) <<s (R‘𝐶)
54a1i 11 . . 3 (𝜑 → (L‘𝐶) <<s (R‘𝐶))
6 mulsval2 28554 . . . 4 ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (𝐴 ·s 𝐵) = (({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))}) |s ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))})))
71, 2, 6syl2anc 596 . . 3 (𝜑 → (𝐴 ·s 𝐵) = (({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))}) |s ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))})))
8 mulsasslem.3 . . . . 5 (𝜑 → 𝐶 ∈ No)
9 lrcut 28347 . . . . 5 (𝐶 ∈ No → ((L‘𝐶) |s (R‘𝐶)) = 𝐶)
108, 9syl 18 . . . 4 (𝜑 → ((L‘𝐶) |s (R‘𝐶)) = 𝐶)
1110eqcomd 2769 . . 3 (𝜑 → 𝐶 = ((L‘𝐶) |s (R‘𝐶)))
123, 5, 7, 11mulsunif 28593 . 2 (𝜑 → ((𝐴 ·s 𝐵) ·s 𝐶) = (({𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))})∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))} ∪ {𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))})∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))}) |s ({𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))})∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))} ∪ {𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))})∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))})))
13 unab 4256 . . . . 5 ({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿))}) = {𝑎 ∣ (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿)) ∨ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿)))}
14 rexun 4197 . . . . . . 7 (∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))})∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) ↔ (∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))}∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) ∨ ∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))}∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))))
15 eqeq1 2767 . . . . . . . . . . 11 (𝑏 = 𝑡 → (𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ↔ 𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))))
16152rexbidv 3231 . . . . . . . . . 10 (𝑏 = 𝑡 → (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ↔ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))))
1716rexab 3656 . . . . . . . . 9 (∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))}∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) ↔ ∃𝑡(∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))))
18 rexcom4 3293 . . . . . . . . . 10 (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑡∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑡∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))))
19 rexcom4 3293 . . . . . . . . . . . 12 (∃𝑦𝐿 ∈ (L‘𝐵)∃𝑡(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑡∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))))
20 ovex 7484 . . . . . . . . . . . . . 14 (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∈ V
21 oveq1 7458 . . . . . . . . . . . . . . . . . 18 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) → (𝑡 ·s 𝐶) = ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶))
2221oveq1d 7466 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) = (((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)))
23 oveq1 7458 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) → (𝑡 ·s 𝑧𝐿) = ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿))
2422, 23oveq12d 7469 . . . . . . . . . . . . . . . 16 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) → (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿)))
2524eqeq2d 2774 . . . . . . . . . . . . . . 15 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) → (𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) ↔ 𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿))))
2625rexbidv 3190 . . . . . . . . . . . . . 14 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) → (∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) ↔ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿))))
2720, 26ceqsexv 3502 . . . . . . . . . . . . 13 (∃𝑡(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿)))
2827rexbii 3113 . . . . . . . . . . . 12 (∃𝑦𝐿 ∈ (L‘𝐵)∃𝑡(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿)))
2919, 28bitr3i 280 . . . . . . . . . . 11 (∃𝑡∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿)))
3029rexbii 3113 . . . . . . . . . 10 (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑡∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿)))
31 r19.41vv 3236 . . . . . . . . . . 11 (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))))
3231exbii 1881 . . . . . . . . . 10 (∃𝑡∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑡(∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))))
3318, 30, 323bitr3ri 305 . . . . . . . . 9 (∃𝑡(∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿)))
3417, 33bitri 278 . . . . . . . 8 (∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))}∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) ↔ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿)))
35 eqeq1 2767 . . . . . . . . . . 11 (𝑏 = 𝑡 → (𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ↔ 𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))))
36352rexbidv 3231 . . . . . . . . . 10 (𝑏 = 𝑡 → (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ↔ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))))
3736rexab 3656 . . . . . . . . 9 (∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))}∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) ↔ ∃𝑡(∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))))
38 rexcom4 3293 . . . . . . . . . 10 (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑡∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑡∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))))
39 rexcom4 3293 . . . . . . . . . . . 12 (∃𝑦𝑅 ∈ (R‘𝐵)∃𝑡(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑡∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))))
40 ovex 7484 . . . . . . . . . . . . . 14 (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∈ V
41 oveq1 7458 . . . . . . . . . . . . . . . . . 18 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) → (𝑡 ·s 𝐶) = ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶))
4241oveq1d 7466 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) = (((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)))
43 oveq1 7458 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) → (𝑡 ·s 𝑧𝐿) = ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿))
4442, 43oveq12d 7469 . . . . . . . . . . . . . . . 16 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) → (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿)))
4544eqeq2d 2774 . . . . . . . . . . . . . . 15 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) → (𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) ↔ 𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿))))
4645rexbidv 3190 . . . . . . . . . . . . . 14 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) → (∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) ↔ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿))))
4740, 46ceqsexv 3502 . . . . . . . . . . . . 13 (∃𝑡(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿)))
4847rexbii 3113 . . . . . . . . . . . 12 (∃𝑦𝑅 ∈ (R‘𝐵)∃𝑡(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿)))
4939, 48bitr3i 280 . . . . . . . . . . 11 (∃𝑡∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿)))
5049rexbii 3113 . . . . . . . . . 10 (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑡∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿)))
51 r19.41vv 3236 . . . . . . . . . . 11 (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))))
5251exbii 1881 . . . . . . . . . 10 (∃𝑡∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑡(∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))))
5338, 50, 523bitr3ri 305 . . . . . . . . 9 (∃𝑡(∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿)))
5437, 53bitri 278 . . . . . . . 8 (∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))}∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) ↔ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿)))
5534, 54orbi12i 928 . . . . . . 7 ((∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))}∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) ∨ ∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))}∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿)) ∨ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿))))
5614, 55bitr2i 279 . . . . . 6 ((∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿)) ∨ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿))) ↔ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))})∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)))
5756abbii 2830 . . . . 5 {𝑎 ∣ (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿)) ∨ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿)))} = {𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))})∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))}
5813, 57eqtri 2786 . . . 4 ({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿))}) = {𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))})∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))}
59 unab 4256 . . . . 5 ({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅))}) = {𝑎 ∣ (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅)) ∨ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅)))}
60 rexun 4197 . . . . . . 7 (∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))})∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) ↔ (∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))}∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) ∨ ∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))}∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))))
61 eqeq1 2767 . . . . . . . . . . 11 (𝑏 = 𝑡 → (𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ↔ 𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))))
62612rexbidv 3231 . . . . . . . . . 10 (𝑏 = 𝑡 → (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ↔ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))))
6362rexab 3656 . . . . . . . . 9 (∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))}∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) ↔ ∃𝑡(∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))))
64 rexcom4 3293 . . . . . . . . . 10 (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑡∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑡∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))))
65 rexcom4 3293 . . . . . . . . . . . 12 (∃𝑦𝑅 ∈ (R‘𝐵)∃𝑡(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑡∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))))
66 ovex 7484 . . . . . . . . . . . . . 14 (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∈ V
67 oveq1 7458 . . . . . . . . . . . . . . . . . 18 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) → (𝑡 ·s 𝐶) = ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶))
6867oveq1d 7466 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) = (((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)))
69 oveq1 7458 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) → (𝑡 ·s 𝑧𝑅) = ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅))
7068, 69oveq12d 7469 . . . . . . . . . . . . . . . 16 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) → (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅)))
7170eqeq2d 2774 . . . . . . . . . . . . . . 15 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) → (𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) ↔ 𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅))))
7271rexbidv 3190 . . . . . . . . . . . . . 14 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) → (∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) ↔ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅))))
7366, 72ceqsexv 3502 . . . . . . . . . . . . 13 (∃𝑡(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅)))
7473rexbii 3113 . . . . . . . . . . . 12 (∃𝑦𝑅 ∈ (R‘𝐵)∃𝑡(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅)))
7565, 74bitr3i 280 . . . . . . . . . . 11 (∃𝑡∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅)))
7675rexbii 3113 . . . . . . . . . 10 (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑡∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅)))
77 r19.41vv 3236 . . . . . . . . . . 11 (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))))
7877exbii 1881 . . . . . . . . . 10 (∃𝑡∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑡(∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))))
7964, 76, 783bitr3ri 305 . . . . . . . . 9 (∃𝑡(∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅)))
8063, 79bitri 278 . . . . . . . 8 (∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))}∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) ↔ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅)))
81 eqeq1 2767 . . . . . . . . . . 11 (𝑏 = 𝑡 → (𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ↔ 𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))))
82812rexbidv 3231 . . . . . . . . . 10 (𝑏 = 𝑡 → (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ↔ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))))
8382rexab 3656 . . . . . . . . 9 (∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))}∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) ↔ ∃𝑡(∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))))
84 rexcom4 3293 . . . . . . . . . 10 (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑡∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑡∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))))
85 rexcom4 3293 . . . . . . . . . . . 12 (∃𝑦𝐿 ∈ (L‘𝐵)∃𝑡(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑡∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))))
86 ovex 7484 . . . . . . . . . . . . . 14 (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∈ V
87 oveq1 7458 . . . . . . . . . . . . . . . . . 18 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) → (𝑡 ·s 𝐶) = ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶))
8887oveq1d 7466 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) = (((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)))
89 oveq1 7458 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) → (𝑡 ·s 𝑧𝑅) = ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅))
9088, 89oveq12d 7469 . . . . . . . . . . . . . . . 16 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) → (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅)))
9190eqeq2d 2774 . . . . . . . . . . . . . . 15 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) → (𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) ↔ 𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅))))
9291rexbidv 3190 . . . . . . . . . . . . . 14 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) → (∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) ↔ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅))))
9386, 92ceqsexv 3502 . . . . . . . . . . . . 13 (∃𝑡(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅)))
9493rexbii 3113 . . . . . . . . . . . 12 (∃𝑦𝐿 ∈ (L‘𝐵)∃𝑡(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅)))
9585, 94bitr3i 280 . . . . . . . . . . 11 (∃𝑡∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅)))
9695rexbii 3113 . . . . . . . . . 10 (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑡∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅)))
97 r19.41vv 3236 . . . . . . . . . . 11 (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))))
9897exbii 1881 . . . . . . . . . 10 (∃𝑡∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑡(∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))))
9984, 96, 983bitr3ri 305 . . . . . . . . 9 (∃𝑡(∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅)))
10083, 99bitri 278 . . . . . . . 8 (∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))}∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) ↔ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅)))
10180, 100orbi12i 928 . . . . . . 7 ((∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))}∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) ∨ ∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))}∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅)) ∨ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅))))
10260, 101bitr2i 279 . . . . . 6 ((∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅)) ∨ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅))) ↔ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))})∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)))
103102abbii 2830 . . . . 5 {𝑎 ∣ (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅)) ∨ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅)))} = {𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))})∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))}
10459, 103eqtri 2786 . . . 4 ({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅))}) = {𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))})∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))}
10558, 104uneq12i 4168 . . 3 (({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿))}) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅))})) = ({𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))})∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))} ∪ {𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))})∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))})
106 unab 4256 . . . . 5 ({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅))}) = {𝑎 ∣ (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅)) ∨ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅)))}
107 rexun 4197 . . . . . . 7 (∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))})∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) ↔ (∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))}∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) ∨ ∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))}∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))))
10816rexab 3656 . . . . . . . . 9 (∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))}∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) ↔ ∃𝑡(∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))))
109 rexcom4 3293 . . . . . . . . . 10 (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑡∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑡∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))))
110 rexcom4 3293 . . . . . . . . . . . 12 (∃𝑦𝐿 ∈ (L‘𝐵)∃𝑡(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑡∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))))
11121oveq1d 7466 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) = (((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)))
112 oveq1 7458 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) → (𝑡 ·s 𝑧𝑅) = ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅))
113111, 112oveq12d 7469 . . . . . . . . . . . . . . . 16 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) → (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅)))
114113eqeq2d 2774 . . . . . . . . . . . . . . 15 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) → (𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) ↔ 𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅))))
115114rexbidv 3190 . . . . . . . . . . . . . 14 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) → (∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) ↔ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅))))
11620, 115ceqsexv 3502 . . . . . . . . . . . . 13 (∃𝑡(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅)))
117116rexbii 3113 . . . . . . . . . . . 12 (∃𝑦𝐿 ∈ (L‘𝐵)∃𝑡(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅)))
118110, 117bitr3i 280 . . . . . . . . . . 11 (∃𝑡∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅)))
119118rexbii 3113 . . . . . . . . . 10 (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑡∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅)))
120 r19.41vv 3236 . . . . . . . . . . 11 (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))))
121120exbii 1881 . . . . . . . . . 10 (∃𝑡∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑡(∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))))
122109, 119, 1213bitr3ri 305 . . . . . . . . 9 (∃𝑡(∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅)))
123108, 122bitri 278 . . . . . . . 8 (∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))}∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) ↔ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅)))
12436rexab 3656 . . . . . . . . 9 (∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))}∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) ↔ ∃𝑡(∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))))
125 rexcom4 3293 . . . . . . . . . 10 (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑡∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑡∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))))
126 rexcom4 3293 . . . . . . . . . . . 12 (∃𝑦𝑅 ∈ (R‘𝐵)∃𝑡(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑡∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))))
12741oveq1d 7466 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) = (((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)))
128 oveq1 7458 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) → (𝑡 ·s 𝑧𝑅) = ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅))
129127, 128oveq12d 7469 . . . . . . . . . . . . . . . 16 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) → (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅)))
130129eqeq2d 2774 . . . . . . . . . . . . . . 15 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) → (𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) ↔ 𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅))))
131130rexbidv 3190 . . . . . . . . . . . . . 14 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) → (∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) ↔ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅))))
13240, 131ceqsexv 3502 . . . . . . . . . . . . 13 (∃𝑡(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅)))
133132rexbii 3113 . . . . . . . . . . . 12 (∃𝑦𝑅 ∈ (R‘𝐵)∃𝑡(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅)))
134126, 133bitr3i 280 . . . . . . . . . . 11 (∃𝑡∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅)))
135134rexbii 3113 . . . . . . . . . 10 (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑡∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅)))
136 r19.41vv 3236 . . . . . . . . . . 11 (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))))
137136exbii 1881 . . . . . . . . . 10 (∃𝑡∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑡(∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))))
138125, 135, 1373bitr3ri 305 . . . . . . . . 9 (∃𝑡(∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ∧ ∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅)))
139124, 138bitri 278 . . . . . . . 8 (∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))}∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) ↔ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅)))
140123, 139orbi12i 928 . . . . . . 7 ((∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))}∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)) ∨ ∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))}∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))) ↔ (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅)) ∨ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅))))
141107, 140bitr2i 279 . . . . . 6 ((∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅)) ∨ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅))) ↔ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))})∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅)))
142141abbii 2830 . . . . 5 {𝑎 ∣ (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅)) ∨ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅)))} = {𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))})∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))}
143106, 142eqtri 2786 . . . 4 ({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅))}) = {𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))})∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))}
144 unab 4256 . . . . 5 ({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿))}) = {𝑎 ∣ (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿)) ∨ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿)))}
145 rexun 4197 . . . . . . 7 (∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))})∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) ↔ (∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))}∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) ∨ ∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))}∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))))
14662rexab 3656 . . . . . . . . 9 (∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))}∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) ↔ ∃𝑡(∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))))
147 rexcom4 3293 . . . . . . . . . 10 (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑡∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑡∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))))
148 rexcom4 3293 . . . . . . . . . . . 12 (∃𝑦𝑅 ∈ (R‘𝐵)∃𝑡(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑡∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))))
14967oveq1d 7466 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) = (((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)))
150 oveq1 7458 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) → (𝑡 ·s 𝑧𝐿) = ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿))
151149, 150oveq12d 7469 . . . . . . . . . . . . . . . 16 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) → (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿)))
152151eqeq2d 2774 . . . . . . . . . . . . . . 15 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) → (𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) ↔ 𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿))))
153152rexbidv 3190 . . . . . . . . . . . . . 14 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) → (∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) ↔ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿))))
15466, 153ceqsexv 3502 . . . . . . . . . . . . 13 (∃𝑡(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿)))
155154rexbii 3113 . . . . . . . . . . . 12 (∃𝑦𝑅 ∈ (R‘𝐵)∃𝑡(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿)))
156148, 155bitr3i 280 . . . . . . . . . . 11 (∃𝑡∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿)))
157156rexbii 3113 . . . . . . . . . 10 (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑡∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿)))
158 r19.41vv 3236 . . . . . . . . . . 11 (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))))
159158exbii 1881 . . . . . . . . . 10 (∃𝑡∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)(𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑡(∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))))
160147, 157, 1593bitr3ri 305 . . . . . . . . 9 (∃𝑡(∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿)))
161146, 160bitri 278 . . . . . . . 8 (∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))}∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) ↔ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿)))
16282rexab 3656 . . . . . . . . 9 (∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))}∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) ↔ ∃𝑡(∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))))
163 rexcom4 3293 . . . . . . . . . 10 (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑡∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑡∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))))
164 rexcom4 3293 . . . . . . . . . . . 12 (∃𝑦𝐿 ∈ (L‘𝐵)∃𝑡(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑡∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))))
16587oveq1d 7466 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) = (((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)))
166 oveq1 7458 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) → (𝑡 ·s 𝑧𝐿) = ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿))
167165, 166oveq12d 7469 . . . . . . . . . . . . . . . 16 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) → (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿)))
168167eqeq2d 2774 . . . . . . . . . . . . . . 15 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) → (𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) ↔ 𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿))))
169168rexbidv 3190 . . . . . . . . . . . . . 14 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) → (∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) ↔ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿))))
17086, 169ceqsexv 3502 . . . . . . . . . . . . 13 (∃𝑡(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿)))
171170rexbii 3113 . . . . . . . . . . . 12 (∃𝑦𝐿 ∈ (L‘𝐵)∃𝑡(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿)))
172164, 171bitr3i 280 . . . . . . . . . . 11 (∃𝑡∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿)))
173172rexbii 3113 . . . . . . . . . 10 (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑡∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿)))
174 r19.41vv 3236 . . . . . . . . . . 11 (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))))
175174exbii 1881 . . . . . . . . . 10 (∃𝑡∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)(𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑡(∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))))
176163, 173, 1753bitr3ri 305 . . . . . . . . 9 (∃𝑡(∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ∧ ∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿)))
177162, 176bitri 278 . . . . . . . 8 (∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))}∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) ↔ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿)))
178161, 177orbi12i 928 . . . . . . 7 ((∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))}∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)) ∨ ∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))}∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))) ↔ (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿)) ∨ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿))))
179145, 178bitr2i 279 . . . . . 6 ((∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿)) ∨ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿))) ↔ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))})∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿)))
180179abbii 2830 . . . . 5 {𝑎 ∣ (∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿)) ∨ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿)))} = {𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))})∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))}
181144, 180eqtri 2786 . . . 4 ({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿))}) = {𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))})∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))}
182143, 181uneq12i 4168 . . 3 (({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅))}) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿))})) = ({𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))})∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))} ∪ {𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))})∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))})
183105, 182oveq12i 7463 . 2 ((({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿))}) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅))})) |s (({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅))}) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿))}))) = (({𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))})∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))} ∪ {𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))})∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))}) |s ({𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅))})∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s (𝑡 ·s 𝑧𝑅))} ∪ {𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅))} ∪ {𝑏 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿))})∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s (𝑡 ·s 𝑧𝐿))}))
18412, 183eqtr4di 2816 1 (𝜑 → ((𝐴 ·s 𝐵) ·s 𝐶) = ((({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿))}) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅))})) |s (({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝑅 ∈ (R‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅))}) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ (L‘𝐴)∃𝑦𝑅 ∈ (R‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) −s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (L‘𝐵)∃𝑧𝐿 ∈ (L‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) −s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) −s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿))}))))
Colors of variables:    wff setvar class
This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861   = wceq 1570  ∃wex 1812   ∈ wcel 2147  {cab 2741  ∃wrex 3090   ∪ cun 4152   class class class wbr 5108  ‘cfv 6566  (class class class)co 7451  Nocsur 28054   <<s cslts 28200   |s ccuts 28202  Lcleft 28268  Rcright 28269   +s cadds 28402   −s csubs 28463   ·s cmuls 28549
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5238  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783
This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4841  df-ot 4864  df-uni 4873  df-int 4913  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-se 5612  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-riota 7408  df-ov 7454  df-oprab 7455  df-mpo 7456  df-1st 8035  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-1o 8514  df-2o 8515  df-nadd 8713  df-no 28057  df-lts 28058  df-bday 28059  df-les 28159  df-slts 28201  df-cuts 28203  df-0s 28250  df-made 28270  df-old 28271  df-left 28273  df-right 28274  df-norec 28381  df-norec2 28392  df-adds 28403  df-negs 28464  df-subs 28465  df-muls 28550
This theorem is used by:  mulsass  28609
  Copyright terms: Public domain W3C validator