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

Theorem mulsasslem1 28073
Description: Lemma for mulsass 28076. 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, 2mulscut2 28043 . . 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 lltropt 27791 . . . 4 ( L ‘𝐶) <<s ( R ‘𝐶)
54a1i 11 . . 3 (𝜑 → ( L ‘𝐶) <<s ( R ‘𝐶))
6 mulsval2 28021 . . . 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 584 . . 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 27822 . . . . 5 (𝐶 No → (( L ‘𝐶) |s ( R ‘𝐶)) = 𝐶)
108, 9syl 17 . . . 4 (𝜑 → (( L ‘𝐶) |s ( R ‘𝐶)) = 𝐶)
1110eqcomd 2736 . . 3 (𝜑𝐶 = (( L ‘𝐶) |s ( R ‘𝐶)))
123, 5, 7, 11mulsunif 28060 . 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 4274 . . . . 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 4162 . . . . . . 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 2734 . . . . . . . . . . 11 (𝑏 = 𝑡 → (𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) ↔ 𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿))))
16152rexbidv 3203 . . . . . . . . . 10 (𝑏 = 𝑡 → (∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) ↔ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿))))
1716rexab 3669 . . . . . . . . 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 3265 . . . . . . . . . 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 3265 . . . . . . . . . . . 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 7423 . . . . . . . . . . . . . 14 (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) ∈ V
21 oveq1 7397 . . . . . . . . . . . . . . . . . 18 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) → (𝑡 ·s 𝐶) = ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶))
2221oveq1d 7405 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) = (((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)))
23 oveq1 7397 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) → (𝑡 ·s 𝑧𝐿) = ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿))
2422, 23oveq12d 7408 . . . . . . . . . . . . . . . 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 2741 . . . . . . . . . . . . . . 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 3158 . . . . . . . . . . . . . 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 3501 . . . . . . . . . . . . 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 3077 . . . . . . . . . . . 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 277 . . . . . . . . . . 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 3077 . . . . . . . . . 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 3208 . . . . . . . . . . 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 1848 . . . . . . . . . 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 302 . . . . . . . . 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 275 . . . . . . . 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 2734 . . . . . . . . . . 11 (𝑏 = 𝑡 → (𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) ↔ 𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅))))
36352rexbidv 3203 . . . . . . . . . 10 (𝑏 = 𝑡 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅))))
3736rexab 3669 . . . . . . . . 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 3265 . . . . . . . . . 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 3265 . . . . . . . . . . . 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 7423 . . . . . . . . . . . . . 14 (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) ∈ V
41 oveq1 7397 . . . . . . . . . . . . . . . . . 18 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) → (𝑡 ·s 𝐶) = ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶))
4241oveq1d 7405 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) = (((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)))
43 oveq1 7397 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) → (𝑡 ·s 𝑧𝐿) = ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿))
4442, 43oveq12d 7408 . . . . . . . . . . . . . . . 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 2741 . . . . . . . . . . . . . . 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 3158 . . . . . . . . . . . . . 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 3501 . . . . . . . . . . . . 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 3077 . . . . . . . . . . . 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 277 . . . . . . . . . . 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 3077 . . . . . . . . . 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 3208 . . . . . . . . . . 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 1848 . . . . . . . . . 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 302 . . . . . . . . 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 275 . . . . . . . 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 914 . . . . . . 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 276 . . . . . 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 2797 . . . . 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 2753 . . . 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 4274 . . . . 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 4162 . . . . . . 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 2734 . . . . . . . . . . 11 (𝑏 = 𝑡 → (𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) ↔ 𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅))))
62612rexbidv 3203 . . . . . . . . . 10 (𝑏 = 𝑡 → (∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) ↔ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅))))
6362rexab 3669 . . . . . . . . 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 3265 . . . . . . . . . 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 3265 . . . . . . . . . . . 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 7423 . . . . . . . . . . . . . 14 (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) ∈ V
67 oveq1 7397 . . . . . . . . . . . . . . . . . 18 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) → (𝑡 ·s 𝐶) = ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶))
6867oveq1d 7405 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) = (((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)))
69 oveq1 7397 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) → (𝑡 ·s 𝑧𝑅) = ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅))
7068, 69oveq12d 7408 . . . . . . . . . . . . . . . 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 2741 . . . . . . . . . . . . . . 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 3158 . . . . . . . . . . . . . 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 3501 . . . . . . . . . . . . 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 3077 . . . . . . . . . . . 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 277 . . . . . . . . . . 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 3077 . . . . . . . . . 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 3208 . . . . . . . . . . 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 1848 . . . . . . . . . 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 302 . . . . . . . . 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 275 . . . . . . . 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 2734 . . . . . . . . . . 11 (𝑏 = 𝑡 → (𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) ↔ 𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿))))
82812rexbidv 3203 . . . . . . . . . 10 (𝑏 = 𝑡 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿))))
8382rexab 3669 . . . . . . . . 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 3265 . . . . . . . . . 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 3265 . . . . . . . . . . . 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 7423 . . . . . . . . . . . . . 14 (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) ∈ V
87 oveq1 7397 . . . . . . . . . . . . . . . . . 18 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) → (𝑡 ·s 𝐶) = ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶))
8887oveq1d 7405 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) = (((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)))
89 oveq1 7397 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) → (𝑡 ·s 𝑧𝑅) = ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅))
9088, 89oveq12d 7408 . . . . . . . . . . . . . . . 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 2741 . . . . . . . . . . . . . . 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 3158 . . . . . . . . . . . . . 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 3501 . . . . . . . . . . . . 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 3077 . . . . . . . . . . . 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 277 . . . . . . . . . . 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 3077 . . . . . . . . . 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 3208 . . . . . . . . . . 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 1848 . . . . . . . . . 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 302 . . . . . . . . 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 275 . . . . . . . 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 914 . . . . . . 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 276 . . . . . 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 2797 . . . . 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 2753 . . . 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 4132 . . 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 4274 . . . . 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 4162 . . . . . . 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 3669 . . . . . . . . 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 3265 . . . . . . . . . 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 3265 . . . . . . . . . . . 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 7405 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) = (((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)))
112 oveq1 7397 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) → (𝑡 ·s 𝑧𝑅) = ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅))
113111, 112oveq12d 7408 . . . . . . . . . . . . . . . 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 2741 . . . . . . . . . . . . . . 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 3158 . . . . . . . . . . . . . 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 3501 . . . . . . . . . . . . 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 3077 . . . . . . . . . . . 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 277 . . . . . . . . . . 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 3077 . . . . . . . . . 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 3208 . . . . . . . . . . 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 1848 . . . . . . . . . 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 302 . . . . . . . . 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 275 . . . . . . . 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 3669 . . . . . . . . 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 3265 . . . . . . . . . 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 3265 . . . . . . . . . . . 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 7405 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) = (((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)))
128 oveq1 7397 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) → (𝑡 ·s 𝑧𝑅) = ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅))
129127, 128oveq12d 7408 . . . . . . . . . . . . . . . 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 2741 . . . . . . . . . . . . . . 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 3158 . . . . . . . . . . . . . 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 3501 . . . . . . . . . . . . 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 3077 . . . . . . . . . . . 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 277 . . . . . . . . . . 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 3077 . . . . . . . . . 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 3208 . . . . . . . . . . 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 1848 . . . . . . . . . 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 302 . . . . . . . . 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 275 . . . . . . . 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 914 . . . . . . 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 276 . . . . . 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 2797 . . . . 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 2753 . . . 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 4274 . . . . 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 4162 . . . . . . 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 3669 . . . . . . . . 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 3265 . . . . . . . . . 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 3265 . . . . . . . . . . . 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 7405 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) = (((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)))
150 oveq1 7397 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) → (𝑡 ·s 𝑧𝐿) = ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿))
151149, 150oveq12d 7408 . . . . . . . . . . . . . . . 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 2741 . . . . . . . . . . . . . . 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 3158 . . . . . . . . . . . . . 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 3501 . . . . . . . . . . . . 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 3077 . . . . . . . . . . . 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 277 . . . . . . . . . . 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 3077 . . . . . . . . . 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 3208 . . . . . . . . . . 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 1848 . . . . . . . . . 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 302 . . . . . . . . 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 275 . . . . . . . 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 3669 . . . . . . . . 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 3265 . . . . . . . . . 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 3265 . . . . . . . . . . . 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 7405 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) = (((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)))
166 oveq1 7397 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) → (𝑡 ·s 𝑧𝐿) = ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿))
167165, 166oveq12d 7408 . . . . . . . . . . . . . . . 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 2741 . . . . . . . . . . . . . . 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 3158 . . . . . . . . . . . . . 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 3501 . . . . . . . . . . . . 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 3077 . . . . . . . . . . . 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 277 . . . . . . . . . . 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 3077 . . . . . . . . . 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 3208 . . . . . . . . . . 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 1848 . . . . . . . . . 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 302 . . . . . . . . 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 275 . . . . . . . 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 914 . . . . . . 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 276 . . . . . 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 2797 . . . . 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 2753 . . . 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 4132 . . 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 7402 . 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 2783 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
Syntax hints:  wi 4  wa 395  wo 847   = wceq 1540  wex 1779  wcel 2109  {cab 2708  wrex 3054  cun 3915   class class class wbr 5110  cfv 6514  (class class class)co 7390   No csur 27558   <<s csslt 27699   |s cscut 27701   L cleft 27760   R cright 27761   +s cadds 27873   -s csubs 27933   ·s cmuls 28016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-tp 4597  df-op 4599  df-ot 4601  df-uni 4875  df-int 4914  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-se 5595  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-1st 7971  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-1o 8437  df-2o 8438  df-nadd 8633  df-no 27561  df-slt 27562  df-bday 27563  df-sle 27664  df-sslt 27700  df-scut 27702  df-0s 27743  df-made 27762  df-old 27763  df-left 27765  df-right 27766  df-norec 27852  df-norec2 27863  df-adds 27874  df-negs 27934  df-subs 27935  df-muls 28017
This theorem is referenced by:  mulsass  28076
  Copyright terms: Public domain W3C validator