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

Theorem mulsasslem3 27600
Description: Lemma for mulsass 27601. Demonstrate the central equality. (Contributed by Scott Fenton, 10-Mar-2025.)
Hypotheses
Ref Expression
mulsasslem3.1 (𝜑𝐴 No )
mulsasslem3.2 (𝜑𝐵 No )
mulsasslem3.3 (𝜑𝐶 No )
mulsasslem3.4 𝑃 ⊆ (( L ‘𝐴) ∪ ( R ‘𝐴))
mulsasslem3.5 𝑄 ⊆ (( L ‘𝐵) ∪ ( R ‘𝐵))
mulsasslem3.6 𝑅 ⊆ (( L ‘𝐶) ∪ ( R ‘𝐶))
mulsasslem3.7 (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)))
mulsasslem3.8 (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)))
mulsasslem3.9 (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)))
mulsasslem3.10 (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)))
mulsasslem3.11 (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))((𝑥𝑂 ·s 𝐵) ·s 𝐶) = (𝑥𝑂 ·s (𝐵 ·s 𝐶)))
mulsasslem3.12 (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝐴 ·s 𝑦𝑂) ·s 𝐶) = (𝐴 ·s (𝑦𝑂 ·s 𝐶)))
mulsasslem3.13 (𝜑 → ∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝐵) ·s 𝑧𝑂) = (𝐴 ·s (𝐵 ·s 𝑧𝑂)))
Assertion
Ref Expression
mulsasslem3 (𝜑 → (∃𝑥𝑃𝑦𝑄𝑧𝑅 𝑎 = ((((((𝑥 ·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 (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))))))
Distinct variable groups:   𝑥𝑂,𝑦𝑂,𝑧𝑂,𝐴   𝐵,𝑥𝑂,𝑦𝑂,𝑧𝑂   𝐶,𝑥𝑂,𝑦𝑂,𝑧𝑂   𝑥,𝑥𝑂,𝑦𝑂,𝑧𝑂   𝑦,𝑦𝑂,𝑧𝑂   𝑧,𝑧𝑂,𝑦   𝑦,𝑃,𝑧   𝑧,𝑄   𝑥,𝑦,𝑧,𝜑
Allowed substitution hints:   𝜑(𝑎,𝑥𝑂,𝑦𝑂,𝑧𝑂)   𝐴(𝑥,𝑦,𝑧,𝑎)   𝐵(𝑥,𝑦,𝑧,𝑎)   𝐶(𝑥,𝑦,𝑧,𝑎)   𝑃(𝑥,𝑎,𝑥𝑂,𝑦𝑂,𝑧𝑂)   𝑄(𝑥,𝑦,𝑎,𝑥𝑂,𝑦𝑂,𝑧𝑂)   𝑅(𝑥,𝑦,𝑧,𝑎,𝑥𝑂,𝑦𝑂,𝑧𝑂)

Proof of Theorem mulsasslem3
StepHypRef Expression
1 oveq1 7411 . . . . . . . . . . 11 (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s 𝐵) = (𝑥 ·s 𝐵))
21oveq1d 7419 . . . . . . . . . 10 (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝐵) ·s 𝐶) = ((𝑥 ·s 𝐵) ·s 𝐶))
3 oveq1 7411 . . . . . . . . . 10 (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝐵 ·s 𝐶)) = (𝑥 ·s (𝐵 ·s 𝐶)))
42, 3eqeq12d 2749 . . . . . . . . 9 (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝐵) ·s 𝐶) = (𝑥𝑂 ·s (𝐵 ·s 𝐶)) ↔ ((𝑥 ·s 𝐵) ·s 𝐶) = (𝑥 ·s (𝐵 ·s 𝐶))))
5 mulsasslem3.11 . . . . . . . . . 10 (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))((𝑥𝑂 ·s 𝐵) ·s 𝐶) = (𝑥𝑂 ·s (𝐵 ·s 𝐶)))
65adantr 482 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))((𝑥𝑂 ·s 𝐵) ·s 𝐶) = (𝑥𝑂 ·s (𝐵 ·s 𝐶)))
7 mulsasslem3.4 . . . . . . . . . 10 𝑃 ⊆ (( L ‘𝐴) ∪ ( R ‘𝐴))
8 simprll 778 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → 𝑥𝑃)
97, 8sselid 3979 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → 𝑥 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
104, 6, 9rspcdva 3613 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝑥 ·s 𝐵) ·s 𝐶) = (𝑥 ·s (𝐵 ·s 𝐶)))
11 oveq2 7412 . . . . . . . . . . . . 13 (𝑦𝑂 = 𝑦 → (𝐴 ·s 𝑦𝑂) = (𝐴 ·s 𝑦))
1211oveq1d 7419 . . . . . . . . . . . 12 (𝑦𝑂 = 𝑦 → ((𝐴 ·s 𝑦𝑂) ·s 𝐶) = ((𝐴 ·s 𝑦) ·s 𝐶))
13 oveq1 7411 . . . . . . . . . . . . 13 (𝑦𝑂 = 𝑦 → (𝑦𝑂 ·s 𝐶) = (𝑦 ·s 𝐶))
1413oveq2d 7420 . . . . . . . . . . . 12 (𝑦𝑂 = 𝑦 → (𝐴 ·s (𝑦𝑂 ·s 𝐶)) = (𝐴 ·s (𝑦 ·s 𝐶)))
1512, 14eqeq12d 2749 . . . . . . . . . . 11 (𝑦𝑂 = 𝑦 → (((𝐴 ·s 𝑦𝑂) ·s 𝐶) = (𝐴 ·s (𝑦𝑂 ·s 𝐶)) ↔ ((𝐴 ·s 𝑦) ·s 𝐶) = (𝐴 ·s (𝑦 ·s 𝐶))))
16 mulsasslem3.12 . . . . . . . . . . . 12 (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝐴 ·s 𝑦𝑂) ·s 𝐶) = (𝐴 ·s (𝑦𝑂 ·s 𝐶)))
1716adantr 482 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝐴 ·s 𝑦𝑂) ·s 𝐶) = (𝐴 ·s (𝑦𝑂 ·s 𝐶)))
18 mulsasslem3.5 . . . . . . . . . . . 12 𝑄 ⊆ (( L ‘𝐵) ∪ ( R ‘𝐵))
19 simprlr 779 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → 𝑦𝑄)
2018, 19sselid 3979 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → 𝑦 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵)))
2115, 17, 20rspcdva 3613 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝐴 ·s 𝑦) ·s 𝐶) = (𝐴 ·s (𝑦 ·s 𝐶)))
22 oveq2 7412 . . . . . . . . . . . . . 14 (𝑧𝑂 = 𝑧 → ((𝐴 ·s 𝐵) ·s 𝑧𝑂) = ((𝐴 ·s 𝐵) ·s 𝑧))
23 oveq2 7412 . . . . . . . . . . . . . . 15 (𝑧𝑂 = 𝑧 → (𝐵 ·s 𝑧𝑂) = (𝐵 ·s 𝑧))
2423oveq2d 7420 . . . . . . . . . . . . . 14 (𝑧𝑂 = 𝑧 → (𝐴 ·s (𝐵 ·s 𝑧𝑂)) = (𝐴 ·s (𝐵 ·s 𝑧)))
2522, 24eqeq12d 2749 . . . . . . . . . . . . 13 (𝑧𝑂 = 𝑧 → (((𝐴 ·s 𝐵) ·s 𝑧𝑂) = (𝐴 ·s (𝐵 ·s 𝑧𝑂)) ↔ ((𝐴 ·s 𝐵) ·s 𝑧) = (𝐴 ·s (𝐵 ·s 𝑧))))
26 mulsasslem3.13 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝐵) ·s 𝑧𝑂) = (𝐴 ·s (𝐵 ·s 𝑧𝑂)))
2726adantr 482 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝐵) ·s 𝑧𝑂) = (𝐴 ·s (𝐵 ·s 𝑧𝑂)))
28 mulsasslem3.6 . . . . . . . . . . . . . 14 𝑅 ⊆ (( L ‘𝐶) ∪ ( R ‘𝐶))
29 simprr 772 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → 𝑧𝑅)
3028, 29sselid 3979 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → 𝑧 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶)))
3125, 27, 30rspcdva 3613 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝐴 ·s 𝐵) ·s 𝑧) = (𝐴 ·s (𝐵 ·s 𝑧)))
32 leftssno 27355 . . . . . . . . . . . . . . . . . . . . . 22 ( L ‘𝐴) ⊆ No
33 rightssno 27356 . . . . . . . . . . . . . . . . . . . . . 22 ( R ‘𝐴) ⊆ No
3432, 33unssi 4184 . . . . . . . . . . . . . . . . . . . . 21 (( L ‘𝐴) ∪ ( R ‘𝐴)) ⊆ No
357, 34sstri 3990 . . . . . . . . . . . . . . . . . . . 20 𝑃 No
3635, 8sselid 3979 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → 𝑥 No )
37 mulsasslem3.2 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 No )
3837adantr 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → 𝐵 No )
3936, 38mulscld 27571 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (𝑥 ·s 𝐵) ∈ No )
40 leftssno 27355 . . . . . . . . . . . . . . . . . . . . 21 ( L ‘𝐶) ⊆ No
41 rightssno 27356 . . . . . . . . . . . . . . . . . . . . 21 ( R ‘𝐶) ⊆ No
4240, 41unssi 4184 . . . . . . . . . . . . . . . . . . . 20 (( L ‘𝐶) ∪ ( R ‘𝐶)) ⊆ No
4328, 42sstri 3990 . . . . . . . . . . . . . . . . . . 19 𝑅 No
4443, 29sselid 3979 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → 𝑧 No )
4539, 44mulscld 27571 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝑥 ·s 𝐵) ·s 𝑧) ∈ No )
46 mulsasslem3.1 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 No )
4746adantr 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → 𝐴 No )
48 leftssno 27355 . . . . . . . . . . . . . . . . . . . . . 22 ( L ‘𝐵) ⊆ No
49 rightssno 27356 . . . . . . . . . . . . . . . . . . . . . 22 ( R ‘𝐵) ⊆ No
5048, 49unssi 4184 . . . . . . . . . . . . . . . . . . . . 21 (( L ‘𝐵) ∪ ( R ‘𝐵)) ⊆ No
5118, 50sstri 3990 . . . . . . . . . . . . . . . . . . . 20 𝑄 No
5251, 19sselid 3979 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → 𝑦 No )
5347, 52mulscld 27571 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (𝐴 ·s 𝑦) ∈ No )
5453, 44mulscld 27571 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝐴 ·s 𝑦) ·s 𝑧) ∈ No )
5545, 54addscomd 27431 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) = (((𝐴 ·s 𝑦) ·s 𝑧) +s ((𝑥 ·s 𝐵) ·s 𝑧)))
5655oveq1d 7419 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = ((((𝐴 ·s 𝑦) ·s 𝑧) +s ((𝑥 ·s 𝐵) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))
5736, 52mulscld 27571 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (𝑥 ·s 𝑦) ∈ No )
5857, 44mulscld 27571 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝑥 ·s 𝑦) ·s 𝑧) ∈ No )
5954, 45, 58addsubsassd 27528 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝐴 ·s 𝑦) ·s 𝑧) +s ((𝑥 ·s 𝐵) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = (((𝐴 ·s 𝑦) ·s 𝑧) +s (((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧))))
6056, 59eqtrd 2773 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = (((𝐴 ·s 𝑦) ·s 𝑧) +s (((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧))))
6160oveq1d 7419 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) +s ((𝑥 ·s 𝑦) ·s 𝐶)) = ((((𝐴 ·s 𝑦) ·s 𝑧) +s (((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧))) +s ((𝑥 ·s 𝑦) ·s 𝐶)))
6245, 58subscld 27515 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) ∈ No )
63 mulsasslem3.3 . . . . . . . . . . . . . . . 16 (𝜑𝐶 No )
6463adantr 482 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → 𝐶 No )
6557, 64mulscld 27571 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝑥 ·s 𝑦) ·s 𝐶) ∈ No )
6654, 62, 65addsassd 27469 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝐴 ·s 𝑦) ·s 𝑧) +s (((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧))) +s ((𝑥 ·s 𝑦) ·s 𝐶)) = (((𝐴 ·s 𝑦) ·s 𝑧) +s ((((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) +s ((𝑥 ·s 𝑦) ·s 𝐶))))
6711oveq1d 7419 . . . . . . . . . . . . . . . 16 (𝑦𝑂 = 𝑦 → ((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = ((𝐴 ·s 𝑦) ·s 𝑧𝑂))
68 oveq1 7411 . . . . . . . . . . . . . . . . 17 (𝑦𝑂 = 𝑦 → (𝑦𝑂 ·s 𝑧𝑂) = (𝑦 ·s 𝑧𝑂))
6968oveq2d 7420 . . . . . . . . . . . . . . . 16 (𝑦𝑂 = 𝑦 → (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)) = (𝐴 ·s (𝑦 ·s 𝑧𝑂)))
7067, 69eqeq12d 2749 . . . . . . . . . . . . . . 15 (𝑦𝑂 = 𝑦 → (((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)) ↔ ((𝐴 ·s 𝑦) ·s 𝑧𝑂) = (𝐴 ·s (𝑦 ·s 𝑧𝑂))))
71 oveq2 7412 . . . . . . . . . . . . . . . 16 (𝑧𝑂 = 𝑧 → ((𝐴 ·s 𝑦) ·s 𝑧𝑂) = ((𝐴 ·s 𝑦) ·s 𝑧))
72 oveq2 7412 . . . . . . . . . . . . . . . . 17 (𝑧𝑂 = 𝑧 → (𝑦 ·s 𝑧𝑂) = (𝑦 ·s 𝑧))
7372oveq2d 7420 . . . . . . . . . . . . . . . 16 (𝑧𝑂 = 𝑧 → (𝐴 ·s (𝑦 ·s 𝑧𝑂)) = (𝐴 ·s (𝑦 ·s 𝑧)))
7471, 73eqeq12d 2749 . . . . . . . . . . . . . . 15 (𝑧𝑂 = 𝑧 → (((𝐴 ·s 𝑦) ·s 𝑧𝑂) = (𝐴 ·s (𝑦 ·s 𝑧𝑂)) ↔ ((𝐴 ·s 𝑦) ·s 𝑧) = (𝐴 ·s (𝑦 ·s 𝑧))))
75 mulsasslem3.10 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)))
7675adantr 482 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)))
7770, 74, 76, 20, 30rspc2dv 3625 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝐴 ·s 𝑦) ·s 𝑧) = (𝐴 ·s (𝑦 ·s 𝑧)))
7845, 65, 58addsubsd 27529 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝑥 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = ((((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) +s ((𝑥 ·s 𝑦) ·s 𝐶)))
791oveq1d 7419 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = ((𝑥 ·s 𝐵) ·s 𝑧𝑂))
80 oveq1 7411 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)) = (𝑥 ·s (𝐵 ·s 𝑧𝑂)))
8179, 80eqeq12d 2749 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝐵) ·s 𝑧𝑂) = (𝑥 ·s (𝐵 ·s 𝑧𝑂))))
82 oveq2 7412 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝑂 = 𝑧 → ((𝑥 ·s 𝐵) ·s 𝑧𝑂) = ((𝑥 ·s 𝐵) ·s 𝑧))
8323oveq2d 7420 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝑂 = 𝑧 → (𝑥 ·s (𝐵 ·s 𝑧𝑂)) = (𝑥 ·s (𝐵 ·s 𝑧)))
8482, 83eqeq12d 2749 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑂 = 𝑧 → (((𝑥 ·s 𝐵) ·s 𝑧𝑂) = (𝑥 ·s (𝐵 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝐵) ·s 𝑧) = (𝑥 ·s (𝐵 ·s 𝑧))))
85 mulsasslem3.9 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)))
8685adantr 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)))
8781, 84, 86, 9, 30rspc2dv 3625 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝑥 ·s 𝐵) ·s 𝑧) = (𝑥 ·s (𝐵 ·s 𝑧)))
88 oveq1 7411 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s 𝑦𝑂) = (𝑥 ·s 𝑦𝑂))
8988oveq1d 7419 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = ((𝑥 ·s 𝑦𝑂) ·s 𝐶))
90 oveq1 7411 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)) = (𝑥 ·s (𝑦𝑂 ·s 𝐶)))
9189, 90eqeq12d 2749 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)) ↔ ((𝑥 ·s 𝑦𝑂) ·s 𝐶) = (𝑥 ·s (𝑦𝑂 ·s 𝐶))))
92 oveq2 7412 . . . . . . . . . . . . . . . . . . . . 21 (𝑦𝑂 = 𝑦 → (𝑥 ·s 𝑦𝑂) = (𝑥 ·s 𝑦))
9392oveq1d 7419 . . . . . . . . . . . . . . . . . . . 20 (𝑦𝑂 = 𝑦 → ((𝑥 ·s 𝑦𝑂) ·s 𝐶) = ((𝑥 ·s 𝑦) ·s 𝐶))
9413oveq2d 7420 . . . . . . . . . . . . . . . . . . . 20 (𝑦𝑂 = 𝑦 → (𝑥 ·s (𝑦𝑂 ·s 𝐶)) = (𝑥 ·s (𝑦 ·s 𝐶)))
9593, 94eqeq12d 2749 . . . . . . . . . . . . . . . . . . 19 (𝑦𝑂 = 𝑦 → (((𝑥 ·s 𝑦𝑂) ·s 𝐶) = (𝑥 ·s (𝑦𝑂 ·s 𝐶)) ↔ ((𝑥 ·s 𝑦) ·s 𝐶) = (𝑥 ·s (𝑦 ·s 𝐶))))
96 mulsasslem3.8 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)))
9796adantr 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)))
9891, 95, 97, 9, 20rspc2dv 3625 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝑥 ·s 𝑦) ·s 𝐶) = (𝑥 ·s (𝑦 ·s 𝐶)))
9987, 98oveq12d 7422 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝑥 ·s 𝑦) ·s 𝐶)) = ((𝑥 ·s (𝐵 ·s 𝑧)) +s (𝑥 ·s (𝑦 ·s 𝐶))))
10038, 44mulscld 27571 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (𝐵 ·s 𝑧) ∈ No )
10136, 100mulscld 27571 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (𝑥 ·s (𝐵 ·s 𝑧)) ∈ No )
10252, 64mulscld 27571 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (𝑦 ·s 𝐶) ∈ No )
10336, 102mulscld 27571 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (𝑥 ·s (𝑦 ·s 𝐶)) ∈ No )
104101, 103addscomd 27431 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝑥 ·s (𝐵 ·s 𝑧)) +s (𝑥 ·s (𝑦 ·s 𝐶))) = ((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))))
10599, 104eqtrd 2773 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝑥 ·s 𝑦) ·s 𝐶)) = ((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))))
10688oveq1d 7419 . . . . . . . . . . . . . . . . . 18 (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = ((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂))
107 oveq1 7411 . . . . . . . . . . . . . . . . . 18 (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)) = (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂)))
108106, 107eqeq12d 2749 . . . . . . . . . . . . . . . . 17 (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂))))
10992oveq1d 7419 . . . . . . . . . . . . . . . . . 18 (𝑦𝑂 = 𝑦 → ((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂) = ((𝑥 ·s 𝑦) ·s 𝑧𝑂))
11068oveq2d 7420 . . . . . . . . . . . . . . . . . 18 (𝑦𝑂 = 𝑦 → (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂)) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))
111109, 110eqeq12d 2749 . . . . . . . . . . . . . . . . 17 (𝑦𝑂 = 𝑦 → (((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂))))
112 oveq2 7412 . . . . . . . . . . . . . . . . . 18 (𝑧𝑂 = 𝑧 → ((𝑥 ·s 𝑦) ·s 𝑧𝑂) = ((𝑥 ·s 𝑦) ·s 𝑧))
11372oveq2d 7420 . . . . . . . . . . . . . . . . . 18 (𝑧𝑂 = 𝑧 → (𝑥 ·s (𝑦 ·s 𝑧𝑂)) = (𝑥 ·s (𝑦 ·s 𝑧)))
114112, 113eqeq12d 2749 . . . . . . . . . . . . . . . . 17 (𝑧𝑂 = 𝑧 → (((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝑦) ·s 𝑧) = (𝑥 ·s (𝑦 ·s 𝑧))))
115 mulsasslem3.7 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)))
116115adantr 482 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)))
117108, 111, 114, 116, 9, 20, 30rspc3dv 3628 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝑥 ·s 𝑦) ·s 𝑧) = (𝑥 ·s (𝑦 ·s 𝑧)))
118105, 117oveq12d 7422 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝑥 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
11978, 118eqtr3d 2775 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) +s ((𝑥 ·s 𝑦) ·s 𝐶)) = (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
12077, 119oveq12d 7422 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((𝐴 ·s 𝑦) ·s 𝑧) +s ((((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) +s ((𝑥 ·s 𝑦) ·s 𝐶))) = ((𝐴 ·s (𝑦 ·s 𝑧)) +s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧)))))
12161, 66, 1203eqtrd 2777 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) +s ((𝑥 ·s 𝑦) ·s 𝐶)) = ((𝐴 ·s (𝑦 ·s 𝑧)) +s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧)))))
12231, 121oveq12d 7422 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((𝐴 ·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 (𝑦 ·s 𝑧))))))
12347, 38mulscld 27571 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (𝐴 ·s 𝐵) ∈ No )
124123, 44mulscld 27571 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝐴 ·s 𝐵) ·s 𝑧) ∈ No )
12545, 54addscld 27444 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) ∈ No )
126125, 58subscld 27515 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) ∈ No )
127124, 126, 65subsubs4d 27540 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝐴 ·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 𝑦) ·s 𝐶))))
12847, 100mulscld 27571 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (𝐴 ·s (𝐵 ·s 𝑧)) ∈ No )
12952, 44mulscld 27571 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (𝑦 ·s 𝑧) ∈ No )
13047, 129mulscld 27571 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (𝐴 ·s (𝑦 ·s 𝑧)) ∈ No )
131103, 101addscld 27444 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) ∈ No )
13236, 129mulscld 27571 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (𝑥 ·s (𝑦 ·s 𝑧)) ∈ No )
133131, 132subscld 27515 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))) ∈ No )
134128, 130, 133subsubs4d 27540 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((𝐴 ·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 (𝑦 ·s 𝑧))))))
135122, 127, 1343eqtr4d 2783 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝐴 ·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 (𝑦 ·s 𝑧)))))
13621, 135oveq12d 7422 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((𝐴 ·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 (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))))
13753, 64mulscld 27571 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝐴 ·s 𝑦) ·s 𝐶) ∈ No )
138124, 126subscld 27515 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧))) ∈ No )
139137, 138, 65addsubsd 27529 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝐴 ·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 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))))
140137, 138, 65addsubsassd 27528 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝐴 ·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 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧))) -s ((𝑥 ·s 𝑦) ·s 𝐶))))
141139, 140eqtr3d 2775 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝐴 ·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 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧))) -s ((𝑥 ·s 𝑦) ·s 𝐶))))
14247, 102mulscld 27571 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (𝐴 ·s (𝑦 ·s 𝐶)) ∈ No )
143142, 128, 130addsubsassd 27528 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))) = ((𝐴 ·s (𝑦 ·s 𝐶)) +s ((𝐴 ·s (𝐵 ·s 𝑧)) -s (𝐴 ·s (𝑦 ·s 𝑧)))))
144143oveq1d 7419 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝐴 ·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 (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧)))))
145128, 130subscld 27515 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝐴 ·s (𝐵 ·s 𝑧)) -s (𝐴 ·s (𝑦 ·s 𝑧))) ∈ No )
146142, 145, 133addsubsassd 27528 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((𝐴 ·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 (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))))
147144, 146eqtrd 2773 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝐴 ·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 (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))))
148136, 141, 1473eqtr4d 2783 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝐴 ·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 (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧)))))
14910, 148oveq12d 7422 . . . . . . 7 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((𝑥 ·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 (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))) -s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))))
15039, 64mulscld 27571 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝑥 ·s 𝐵) ·s 𝐶) ∈ No )
151150, 137addscld 27444 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) ∈ No )
152151, 65subscld 27515 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)) ∈ No )
153152, 124, 126addsubsassd 27528 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((((𝑥 ·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 𝑦) ·s 𝐶)) +s (((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))))
154150, 137, 65addsubsassd 27528 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)) = (((𝑥 ·s 𝐵) ·s 𝐶) +s (((𝐴 ·s 𝑦) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶))))
155154oveq1d 7419 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((((𝑥 ·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 𝑦) ·s 𝐶))) +s (((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))))
156137, 65subscld 27515 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((𝐴 ·s 𝑦) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶)) ∈ No )
157150, 156, 138addsassd 27469 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝑥 ·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 𝑦) ·s 𝐶)) +s (((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧))))))
158153, 155, 1573eqtrd 2777 . . . . . . 7 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((((𝑥 ·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 𝑦) ·s 𝐶)) +s (((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧))))))
15938, 64mulscld 27571 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (𝐵 ·s 𝐶) ∈ No )
16036, 159mulscld 27571 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (𝑥 ·s (𝐵 ·s 𝐶)) ∈ No )
161142, 128addscld 27444 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) ∈ No )
162161, 130subscld 27515 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))) ∈ No )
163160, 162, 133addsubsassd 27528 . . . . . . 7 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((𝑥 ·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 (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))) -s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))))
164149, 158, 1633eqtr4d 2783 . . . . . 6 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((((𝑥 ·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 (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧)))) -s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧)))))
16539, 53addscld 27444 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ∈ No )
166165, 57, 64subsdird 27594 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝐶) = ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶)))
16739, 53, 64addsdird 27592 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝐶) = (((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)))
168167oveq1d 7419 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶)) = ((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)))
169166, 168eqtrd 2773 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝐶) = ((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)))
170169oveq1d 7419 . . . . . . 7 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧)) = (((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)) +s ((𝐴 ·s 𝐵) ·s 𝑧)))
171165, 57, 44subsdird 27594 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝑧) = ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)))
17239, 53, 44addsdird 27592 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝑧) = (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)))
173172oveq1d 7419 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))
174171, 173eqtrd 2773 . . . . . . 7 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝑧) = ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))
175170, 174oveq12d 7422 . . . . . 6 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((((𝑥 ·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 𝑧)) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧))))
176102, 100addscld 27444 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) ∈ No )
17747, 176, 129subsdid 27593 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (𝐴 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))) = ((𝐴 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))))
17847, 102, 100addsdid 27591 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (𝐴 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) = ((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))))
179178oveq1d 7419 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝐴 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))) = (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))))
180177, 179eqtrd 2773 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (𝐴 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))) = (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))))
181180oveq2d 7420 . . . . . . 7 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝑥 ·s (𝐵 ·s 𝐶)) +s (𝐴 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧)))) = ((𝑥 ·s (𝐵 ·s 𝐶)) +s (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧)))))
18236, 176, 129subsdid 27593 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (𝑥 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))) = ((𝑥 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
18336, 102, 100addsdid 27591 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (𝑥 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) = ((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))))
184183oveq1d 7419 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((𝑥 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))) = (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
185182, 184eqtrd 2773 . . . . . . 7 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (𝑥 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))) = (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
186181, 185oveq12d 7422 . . . . . 6 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (((𝑥 ·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 𝑧)))) -s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧)))))
187164, 175, 1863eqtr4d 2783 . . . . 5 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → ((((((𝑥 ·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 (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧)))))
188187eqeq2d 2744 . . . 4 ((𝜑 ∧ ((𝑥𝑃𝑦𝑄) ∧ 𝑧𝑅)) → (𝑎 = ((((((𝑥 ·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 (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))))))
189188anassrs 469 . . 3 (((𝜑 ∧ (𝑥𝑃𝑦𝑄)) ∧ 𝑧𝑅) → (𝑎 = ((((((𝑥 ·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 (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))))))
190189rexbidva 3177 . 2 ((𝜑 ∧ (𝑥𝑃𝑦𝑄)) → (∃𝑧𝑅 𝑎 = ((((((𝑥 ·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 (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))))))
1911902rexbidva 3218 1 (𝜑 → (∃𝑥𝑃𝑦𝑄𝑧𝑅 𝑎 = ((((((𝑥 ·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 (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wral 3062  wrex 3071  cun 3945  wss 3947  cfv 6540  (class class class)co 7404   No csur 27123   L cleft 27320   R cright 27321   +s cadds 27423   -s csubs 27475   ·s cmuls 27542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-ot 4636  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-1st 7970  df-2nd 7971  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-1o 8461  df-2o 8462  df-nadd 8661  df-no 27126  df-slt 27127  df-bday 27128  df-sle 27228  df-sslt 27263  df-scut 27265  df-0s 27305  df-made 27322  df-old 27323  df-left 27325  df-right 27326  df-norec 27402  df-norec2 27413  df-adds 27424  df-negs 27476  df-subs 27477  df-muls 27543
This theorem is referenced by:  mulsass  27601
  Copyright terms: Public domain W3C validator