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

Theorem mulsasslem1 28071
Description: Lemma for mulsass 28074. 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 28041 . . 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 27786 . . . 4 ( L ‘𝐶) <<s ( R ‘𝐶)
54a1i 11 . . 3 (𝜑 → ( L ‘𝐶) <<s ( R ‘𝐶))
6 mulsval2 28019 . . . 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 27818 . . . . 5 (𝐶 No → (( L ‘𝐶) |s ( R ‘𝐶)) = 𝐶)
108, 9syl 17 . . . 4 (𝜑 → (( L ‘𝐶) |s ( R ‘𝐶)) = 𝐶)
1110eqcomd 2735 . . 3 (𝜑𝐶 = (( L ‘𝐶) |s ( R ‘𝐶)))
123, 5, 7, 11mulsunif 28058 . 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 4259 . . . . 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 4147 . . . . . . 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 2733 . . . . . . . . . . 11 (𝑏 = 𝑡 → (𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) ↔ 𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿))))
16152rexbidv 3194 . . . . . . . . . 10 (𝑏 = 𝑡 → (∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) ↔ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿))))
1716rexab 3655 . . . . . . . . 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 3256 . . . . . . . . . 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 3256 . . . . . . . . . . . 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 7382 . . . . . . . . . . . . . 14 (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) ∈ V
21 oveq1 7356 . . . . . . . . . . . . . . . . . 18 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) → (𝑡 ·s 𝐶) = ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶))
2221oveq1d 7364 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) = (((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)))
23 oveq1 7356 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) → (𝑡 ·s 𝑧𝐿) = ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿))
2422, 23oveq12d 7367 . . . . . . . . . . . . . . . 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 2740 . . . . . . . . . . . . . . 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 3153 . . . . . . . . . . . . . 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 3487 . . . . . . . . . . . . 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 3076 . . . . . . . . . . . 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 3076 . . . . . . . . . 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 3199 . . . . . . . . . . 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 2733 . . . . . . . . . . 11 (𝑏 = 𝑡 → (𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) ↔ 𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅))))
36352rexbidv 3194 . . . . . . . . . 10 (𝑏 = 𝑡 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅))))
3736rexab 3655 . . . . . . . . 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 3256 . . . . . . . . . 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 3256 . . . . . . . . . . . 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 7382 . . . . . . . . . . . . . 14 (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) ∈ V
41 oveq1 7356 . . . . . . . . . . . . . . . . . 18 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) → (𝑡 ·s 𝐶) = ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶))
4241oveq1d 7364 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) = (((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)))
43 oveq1 7356 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) → (𝑡 ·s 𝑧𝐿) = ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿))
4442, 43oveq12d 7367 . . . . . . . . . . . . . . . 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 2740 . . . . . . . . . . . . . . 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 3153 . . . . . . . . . . . . . 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 3487 . . . . . . . . . . . . 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 3076 . . . . . . . . . . . 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 3076 . . . . . . . . . 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 3199 . . . . . . . . . . 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 2796 . . . . 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 2752 . . . 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 4259 . . . . 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 4147 . . . . . . 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 2733 . . . . . . . . . . 11 (𝑏 = 𝑡 → (𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) ↔ 𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅))))
62612rexbidv 3194 . . . . . . . . . 10 (𝑏 = 𝑡 → (∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) ↔ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅))))
6362rexab 3655 . . . . . . . . 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 3256 . . . . . . . . . 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 3256 . . . . . . . . . . . 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 7382 . . . . . . . . . . . . . 14 (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) ∈ V
67 oveq1 7356 . . . . . . . . . . . . . . . . . 18 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) → (𝑡 ·s 𝐶) = ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶))
6867oveq1d 7364 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) = (((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)))
69 oveq1 7356 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) → (𝑡 ·s 𝑧𝑅) = ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅))
7068, 69oveq12d 7367 . . . . . . . . . . . . . . . 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 2740 . . . . . . . . . . . . . . 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 3153 . . . . . . . . . . . . . 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 3487 . . . . . . . . . . . . 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 3076 . . . . . . . . . . . 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 3076 . . . . . . . . . 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 3199 . . . . . . . . . . 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 2733 . . . . . . . . . . 11 (𝑏 = 𝑡 → (𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) ↔ 𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿))))
82812rexbidv 3194 . . . . . . . . . 10 (𝑏 = 𝑡 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿))))
8382rexab 3655 . . . . . . . . 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 3256 . . . . . . . . . 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 3256 . . . . . . . . . . . 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 7382 . . . . . . . . . . . . . 14 (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) ∈ V
87 oveq1 7356 . . . . . . . . . . . . . . . . . 18 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) → (𝑡 ·s 𝐶) = ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶))
8887oveq1d 7364 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) = (((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)))
89 oveq1 7356 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) → (𝑡 ·s 𝑧𝑅) = ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅))
9088, 89oveq12d 7367 . . . . . . . . . . . . . . . 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 2740 . . . . . . . . . . . . . . 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 3153 . . . . . . . . . . . . . 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 3487 . . . . . . . . . . . . 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 3076 . . . . . . . . . . . 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 3076 . . . . . . . . . 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 3199 . . . . . . . . . . 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 2796 . . . . 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 2752 . . . 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 4117 . . 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 4259 . . . . 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 4147 . . . . . . 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 3655 . . . . . . . . 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 3256 . . . . . . . . . 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 3256 . . . . . . . . . . . 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 7364 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) = (((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)))
112 oveq1 7356 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) → (𝑡 ·s 𝑧𝑅) = ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅))
113111, 112oveq12d 7367 . . . . . . . . . . . . . . . 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 2740 . . . . . . . . . . . . . . 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 3153 . . . . . . . . . . . . . 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 3487 . . . . . . . . . . . . 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 3076 . . . . . . . . . . . 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 3076 . . . . . . . . . 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 3199 . . . . . . . . . . 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 3655 . . . . . . . . 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 3256 . . . . . . . . . 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 3256 . . . . . . . . . . . 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 7364 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) = (((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)))
128 oveq1 7356 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) → (𝑡 ·s 𝑧𝑅) = ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅))
129127, 128oveq12d 7367 . . . . . . . . . . . . . . . 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 2740 . . . . . . . . . . . . . . 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 3153 . . . . . . . . . . . . . 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 3487 . . . . . . . . . . . . 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 3076 . . . . . . . . . . . 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 3076 . . . . . . . . . 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 3199 . . . . . . . . . . 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 2796 . . . . 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 2752 . . . 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 4259 . . . . 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 4147 . . . . . . 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 3655 . . . . . . . . 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 3256 . . . . . . . . . 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 3256 . . . . . . . . . . . 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 7364 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) = (((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)))
150 oveq1 7356 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) → (𝑡 ·s 𝑧𝐿) = ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿))
151149, 150oveq12d 7367 . . . . . . . . . . . . . . . 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 2740 . . . . . . . . . . . . . . 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 3153 . . . . . . . . . . . . . 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 3487 . . . . . . . . . . . . 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 3076 . . . . . . . . . . . 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 3076 . . . . . . . . . 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 3199 . . . . . . . . . . 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 3655 . . . . . . . . 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 3256 . . . . . . . . . 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 3256 . . . . . . . . . . . 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 7364 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) → ((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) = (((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)))
166 oveq1 7356 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) → (𝑡 ·s 𝑧𝐿) = ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿))
167165, 166oveq12d 7367 . . . . . . . . . . . . . . . 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 2740 . . . . . . . . . . . . . . 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 3153 . . . . . . . . . . . . . 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 3487 . . . . . . . . . . . . 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 3076 . . . . . . . . . . . 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 3076 . . . . . . . . . 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 3199 . . . . . . . . . . 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 2796 . . . . 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 2752 . . . 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 4117 . . 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 7361 . 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 2782 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 2707  wrex 3053  cun 3901   class class class wbr 5092  cfv 6482  (class class class)co 7349   No csur 27549   <<s csslt 27691   |s cscut 27693   L cleft 27755   R cright 27756   +s cadds 27871   -s csubs 27931   ·s cmuls 28014
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 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671
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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-tp 4582  df-op 4584  df-ot 4586  df-uni 4859  df-int 4897  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-se 5573  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-1st 7924  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-1o 8388  df-2o 8389  df-nadd 8584  df-no 27552  df-slt 27553  df-bday 27554  df-sle 27655  df-sslt 27692  df-scut 27694  df-0s 27738  df-made 27757  df-old 27758  df-left 27760  df-right 27761  df-norec 27850  df-norec2 27861  df-adds 27872  df-negs 27932  df-subs 27933  df-muls 28015
This theorem is referenced by:  mulsass  28074
  Copyright terms: Public domain W3C validator