Metamath Proof Explorer

Theorem mulsasslem3

Description: Lemma for mulsass . Demonstrate the central equality. (Contributed by Scott Fenton, 10-Mar-2025)

Ref Expression
Hypotheses 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 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 𝑧 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mulsasslem3.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
2 mulsasslem3.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
3 mulsasslem3.3 ⊢ ( 𝜑 → 𝐶 ∈ No )
4 mulsasslem3.4 ⊢ 𝑃 ⊆ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) )
5 mulsasslem3.5 ⊢ 𝑄 ⊆ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) )
6 mulsasslem3.6 ⊢ 𝑅 ⊆ ( ( L ‘ 𝐶 ) ∪ ( R ‘ 𝐶 ) )
7 mulsasslem3.7 ⊢ ( 𝜑 → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝐶 ) ∪ ( R ‘ 𝐶 ) ) ( ( 𝑥𝑂 ·s 𝑦𝑂 ) ·s 𝑧𝑂 ) = ( 𝑥𝑂 ·s ( 𝑦𝑂 ·s 𝑧𝑂 ) ) )
8 mulsasslem3.8 ⊢ ( 𝜑 → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ( ( 𝑥𝑂 ·s 𝑦𝑂 ) ·s 𝐶 ) = ( 𝑥𝑂 ·s ( 𝑦𝑂 ·s 𝐶 ) ) )
9 mulsasslem3.9 ⊢ ( 𝜑 → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝐶 ) ∪ ( R ‘ 𝐶 ) ) ( ( 𝑥𝑂 ·s 𝐵 ) ·s 𝑧𝑂 ) = ( 𝑥𝑂 ·s ( 𝐵 ·s 𝑧𝑂 ) ) )
10 mulsasslem3.10 ⊢ ( 𝜑 → ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝐶 ) ∪ ( R ‘ 𝐶 ) ) ( ( 𝐴 ·s 𝑦𝑂 ) ·s 𝑧𝑂 ) = ( 𝐴 ·s ( 𝑦𝑂 ·s 𝑧𝑂 ) ) )
11 mulsasslem3.11 ⊢ ( 𝜑 → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( ( 𝑥𝑂 ·s 𝐵 ) ·s 𝐶 ) = ( 𝑥𝑂 ·s ( 𝐵 ·s 𝐶 ) ) )
12 mulsasslem3.12 ⊢ ( 𝜑 → ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ( ( 𝐴 ·s 𝑦𝑂 ) ·s 𝐶 ) = ( 𝐴 ·s ( 𝑦𝑂 ·s 𝐶 ) ) )
13 mulsasslem3.13 ⊢ ( 𝜑 → ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝐶 ) ∪ ( R ‘ 𝐶 ) ) ( ( 𝐴 ·s 𝐵 ) ·s 𝑧𝑂 ) = ( 𝐴 ·s ( 𝐵 ·s 𝑧𝑂 ) ) )
14 oveq1 ⊢ ( 𝑥𝑂 = 𝑥 → ( 𝑥𝑂 ·s 𝐵 ) = ( 𝑥 ·s 𝐵 ) )
15 14 oveq1d ⊢ ( 𝑥𝑂 = 𝑥 → ( ( 𝑥𝑂 ·s 𝐵 ) ·s 𝐶 ) = ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) )
16 oveq1 ⊢ ( 𝑥𝑂 = 𝑥 → ( 𝑥𝑂 ·s ( 𝐵 ·s 𝐶 ) ) = ( 𝑥 ·s ( 𝐵 ·s 𝐶 ) ) )
17 15 16 eqeq12d ⊢ ( 𝑥𝑂 = 𝑥 → ( ( ( 𝑥𝑂 ·s 𝐵 ) ·s 𝐶 ) = ( 𝑥𝑂 ·s ( 𝐵 ·s 𝐶 ) ) ↔ ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) = ( 𝑥 ·s ( 𝐵 ·s 𝐶 ) ) ) )
18 11 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( ( 𝑥𝑂 ·s 𝐵 ) ·s 𝐶 ) = ( 𝑥𝑂 ·s ( 𝐵 ·s 𝐶 ) ) )
19 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → 𝑥 ∈ 𝑃 )
20 4 19 sselid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → 𝑥 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
21 17 18 20 rspcdva ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) = ( 𝑥 ·s ( 𝐵 ·s 𝐶 ) ) )
22 oveq2 ⊢ ( 𝑦𝑂 = 𝑦 → ( 𝐴 ·s 𝑦𝑂 ) = ( 𝐴 ·s 𝑦 ) )
23 22 oveq1d ⊢ ( 𝑦𝑂 = 𝑦 → ( ( 𝐴 ·s 𝑦𝑂 ) ·s 𝐶 ) = ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) )
24 oveq1 ⊢ ( 𝑦𝑂 = 𝑦 → ( 𝑦𝑂 ·s 𝐶 ) = ( 𝑦 ·s 𝐶 ) )
25 24 oveq2d ⊢ ( 𝑦𝑂 = 𝑦 → ( 𝐴 ·s ( 𝑦𝑂 ·s 𝐶 ) ) = ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) )
26 23 25 eqeq12d ⊢ ( 𝑦𝑂 = 𝑦 → ( ( ( 𝐴 ·s 𝑦𝑂 ) ·s 𝐶 ) = ( 𝐴 ·s ( 𝑦𝑂 ·s 𝐶 ) ) ↔ ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) = ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) ) )
27 12 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ( ( 𝐴 ·s 𝑦𝑂 ) ·s 𝐶 ) = ( 𝐴 ·s ( 𝑦𝑂 ·s 𝐶 ) ) )
28 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → 𝑦 ∈ 𝑄 )
29 5 28 sselid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → 𝑦 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) )
30 26 27 29 rspcdva ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) = ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) )
31 oveq2 ⊢ ( 𝑧𝑂 = 𝑧 → ( ( 𝐴 ·s 𝐵 ) ·s 𝑧𝑂 ) = ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) )
32 oveq2 ⊢ ( 𝑧𝑂 = 𝑧 → ( 𝐵 ·s 𝑧𝑂 ) = ( 𝐵 ·s 𝑧 ) )
33 32 oveq2d ⊢ ( 𝑧𝑂 = 𝑧 → ( 𝐴 ·s ( 𝐵 ·s 𝑧𝑂 ) ) = ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) )
34 31 33 eqeq12d ⊢ ( 𝑧𝑂 = 𝑧 → ( ( ( 𝐴 ·s 𝐵 ) ·s 𝑧𝑂 ) = ( 𝐴 ·s ( 𝐵 ·s 𝑧𝑂 ) ) ↔ ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) = ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) ) )
35 13 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝐶 ) ∪ ( R ‘ 𝐶 ) ) ( ( 𝐴 ·s 𝐵 ) ·s 𝑧𝑂 ) = ( 𝐴 ·s ( 𝐵 ·s 𝑧𝑂 ) ) )
36 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → 𝑧 ∈ 𝑅 )
37 6 36 sselid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → 𝑧 ∈ ( ( L ‘ 𝐶 ) ∪ ( R ‘ 𝐶 ) ) )
38 34 35 37 rspcdva ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) = ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) )
39 leftssno ⊢ ( L ‘ 𝐴 ) ⊆ No
40 rightssno ⊢ ( R ‘ 𝐴 ) ⊆ No
41 39 40 unssi ⊢ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ⊆ No
42 4 41 sstri ⊢ 𝑃 ⊆ No
43 42 19 sselid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → 𝑥 ∈ No )
44 2 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → 𝐵 ∈ No )
45 43 44 mulscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑥 ·s 𝐵 ) ∈ No )
46 leftssno ⊢ ( L ‘ 𝐶 ) ⊆ No
47 rightssno ⊢ ( R ‘ 𝐶 ) ⊆ No
48 46 47 unssi ⊢ ( ( L ‘ 𝐶 ) ∪ ( R ‘ 𝐶 ) ) ⊆ No
49 6 48 sstri ⊢ 𝑅 ⊆ No
50 49 36 sselid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → 𝑧 ∈ No )
51 45 50 mulscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) ∈ No )
52 1 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → 𝐴 ∈ No )
53 leftssno ⊢ ( L ‘ 𝐵 ) ⊆ No
54 rightssno ⊢ ( R ‘ 𝐵 ) ⊆ No
55 53 54 unssi ⊢ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ⊆ No
56 5 55 sstri ⊢ 𝑄 ⊆ No
57 56 28 sselid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → 𝑦 ∈ No )
58 52 57 mulscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝐴 ·s 𝑦 ) ∈ No )
59 58 50 mulscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ∈ No )
60 51 59 addscomd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) = ( ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) +s ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) ) )
61 60 oveq1d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) = ( ( ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) +s ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) )
62 43 57 mulscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑥 ·s 𝑦 ) ∈ No )
63 62 50 mulscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ∈ No )
64 59 51 63 addsubsassd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) +s ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) = ( ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) +s ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) )
65 61 64 eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) = ( ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) +s ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) )
66 65 oveq1d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) +s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) = ( ( ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) +s ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) +s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) )
67 51 63 subscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ∈ No )
68 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → 𝐶 ∈ No )
69 62 68 mulscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ∈ No )
70 59 67 69 addsassd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) +s ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) +s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) = ( ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) +s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) +s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) ) )
71 22 oveq1d ⊢ ( 𝑦𝑂 = 𝑦 → ( ( 𝐴 ·s 𝑦𝑂 ) ·s 𝑧𝑂 ) = ( ( 𝐴 ·s 𝑦 ) ·s 𝑧𝑂 ) )
72 oveq1 ⊢ ( 𝑦𝑂 = 𝑦 → ( 𝑦𝑂 ·s 𝑧𝑂 ) = ( 𝑦 ·s 𝑧𝑂 ) )
73 72 oveq2d ⊢ ( 𝑦𝑂 = 𝑦 → ( 𝐴 ·s ( 𝑦𝑂 ·s 𝑧𝑂 ) ) = ( 𝐴 ·s ( 𝑦 ·s 𝑧𝑂 ) ) )
74 71 73 eqeq12d ⊢ ( 𝑦𝑂 = 𝑦 → ( ( ( 𝐴 ·s 𝑦𝑂 ) ·s 𝑧𝑂 ) = ( 𝐴 ·s ( 𝑦𝑂 ·s 𝑧𝑂 ) ) ↔ ( ( 𝐴 ·s 𝑦 ) ·s 𝑧𝑂 ) = ( 𝐴 ·s ( 𝑦 ·s 𝑧𝑂 ) ) ) )
75 oveq2 ⊢ ( 𝑧𝑂 = 𝑧 → ( ( 𝐴 ·s 𝑦 ) ·s 𝑧𝑂 ) = ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) )
76 oveq2 ⊢ ( 𝑧𝑂 = 𝑧 → ( 𝑦 ·s 𝑧𝑂 ) = ( 𝑦 ·s 𝑧 ) )
77 76 oveq2d ⊢ ( 𝑧𝑂 = 𝑧 → ( 𝐴 ·s ( 𝑦 ·s 𝑧𝑂 ) ) = ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) )
78 75 77 eqeq12d ⊢ ( 𝑧𝑂 = 𝑧 → ( ( ( 𝐴 ·s 𝑦 ) ·s 𝑧𝑂 ) = ( 𝐴 ·s ( 𝑦 ·s 𝑧𝑂 ) ) ↔ ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) = ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) )
79 10 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝐶 ) ∪ ( R ‘ 𝐶 ) ) ( ( 𝐴 ·s 𝑦𝑂 ) ·s 𝑧𝑂 ) = ( 𝐴 ·s ( 𝑦𝑂 ·s 𝑧𝑂 ) ) )
80 74 78 79 29 37 rspc2dv ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) = ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) )
81 51 69 63 addsubsd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) = ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) +s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) )
82 14 oveq1d ⊢ ( 𝑥𝑂 = 𝑥 → ( ( 𝑥𝑂 ·s 𝐵 ) ·s 𝑧𝑂 ) = ( ( 𝑥 ·s 𝐵 ) ·s 𝑧𝑂 ) )
83 oveq1 ⊢ ( 𝑥𝑂 = 𝑥 → ( 𝑥𝑂 ·s ( 𝐵 ·s 𝑧𝑂 ) ) = ( 𝑥 ·s ( 𝐵 ·s 𝑧𝑂 ) ) )
84 82 83 eqeq12d ⊢ ( 𝑥𝑂 = 𝑥 → ( ( ( 𝑥𝑂 ·s 𝐵 ) ·s 𝑧𝑂 ) = ( 𝑥𝑂 ·s ( 𝐵 ·s 𝑧𝑂 ) ) ↔ ( ( 𝑥 ·s 𝐵 ) ·s 𝑧𝑂 ) = ( 𝑥 ·s ( 𝐵 ·s 𝑧𝑂 ) ) ) )
85 oveq2 ⊢ ( 𝑧𝑂 = 𝑧 → ( ( 𝑥 ·s 𝐵 ) ·s 𝑧𝑂 ) = ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) )
86 32 oveq2d ⊢ ( 𝑧𝑂 = 𝑧 → ( 𝑥 ·s ( 𝐵 ·s 𝑧𝑂 ) ) = ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) )
87 85 86 eqeq12d ⊢ ( 𝑧𝑂 = 𝑧 → ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧𝑂 ) = ( 𝑥 ·s ( 𝐵 ·s 𝑧𝑂 ) ) ↔ ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) = ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) )
88 9 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝐶 ) ∪ ( R ‘ 𝐶 ) ) ( ( 𝑥𝑂 ·s 𝐵 ) ·s 𝑧𝑂 ) = ( 𝑥𝑂 ·s ( 𝐵 ·s 𝑧𝑂 ) ) )
89 84 87 88 20 37 rspc2dv ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) = ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) )
90 oveq1 ⊢ ( 𝑥𝑂 = 𝑥 → ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑥 ·s 𝑦𝑂 ) )
91 90 oveq1d ⊢ ( 𝑥𝑂 = 𝑥 → ( ( 𝑥𝑂 ·s 𝑦𝑂 ) ·s 𝐶 ) = ( ( 𝑥 ·s 𝑦𝑂 ) ·s 𝐶 ) )
92 oveq1 ⊢ ( 𝑥𝑂 = 𝑥 → ( 𝑥𝑂 ·s ( 𝑦𝑂 ·s 𝐶 ) ) = ( 𝑥 ·s ( 𝑦𝑂 ·s 𝐶 ) ) )
93 91 92 eqeq12d ⊢ ( 𝑥𝑂 = 𝑥 → ( ( ( 𝑥𝑂 ·s 𝑦𝑂 ) ·s 𝐶 ) = ( 𝑥𝑂 ·s ( 𝑦𝑂 ·s 𝐶 ) ) ↔ ( ( 𝑥 ·s 𝑦𝑂 ) ·s 𝐶 ) = ( 𝑥 ·s ( 𝑦𝑂 ·s 𝐶 ) ) ) )
94 oveq2 ⊢ ( 𝑦𝑂 = 𝑦 → ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑥 ·s 𝑦 ) )
95 94 oveq1d ⊢ ( 𝑦𝑂 = 𝑦 → ( ( 𝑥 ·s 𝑦𝑂 ) ·s 𝐶 ) = ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) )
96 24 oveq2d ⊢ ( 𝑦𝑂 = 𝑦 → ( 𝑥 ·s ( 𝑦𝑂 ·s 𝐶 ) ) = ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) )
97 95 96 eqeq12d ⊢ ( 𝑦𝑂 = 𝑦 → ( ( ( 𝑥 ·s 𝑦𝑂 ) ·s 𝐶 ) = ( 𝑥 ·s ( 𝑦𝑂 ·s 𝐶 ) ) ↔ ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) = ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) ) )
98 8 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ( ( 𝑥𝑂 ·s 𝑦𝑂 ) ·s 𝐶 ) = ( 𝑥𝑂 ·s ( 𝑦𝑂 ·s 𝐶 ) ) )
99 93 97 98 20 29 rspc2dv ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) = ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) )
100 89 99 oveq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) = ( ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) ) )
101 44 50 mulscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝐵 ·s 𝑧 ) ∈ No )
102 43 101 mulscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ∈ No )
103 57 68 mulscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑦 ·s 𝐶 ) ∈ No )
104 43 103 mulscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) ∈ No )
105 102 104 addscomd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) ) = ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) )
106 100 105 eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) = ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) )
107 90 oveq1d ⊢ ( 𝑥𝑂 = 𝑥 → ( ( 𝑥𝑂 ·s 𝑦𝑂 ) ·s 𝑧𝑂 ) = ( ( 𝑥 ·s 𝑦𝑂 ) ·s 𝑧𝑂 ) )
108 oveq1 ⊢ ( 𝑥𝑂 = 𝑥 → ( 𝑥𝑂 ·s ( 𝑦𝑂 ·s 𝑧𝑂 ) ) = ( 𝑥 ·s ( 𝑦𝑂 ·s 𝑧𝑂 ) ) )
109 107 108 eqeq12d ⊢ ( 𝑥𝑂 = 𝑥 → ( ( ( 𝑥𝑂 ·s 𝑦𝑂 ) ·s 𝑧𝑂 ) = ( 𝑥𝑂 ·s ( 𝑦𝑂 ·s 𝑧𝑂 ) ) ↔ ( ( 𝑥 ·s 𝑦𝑂 ) ·s 𝑧𝑂 ) = ( 𝑥 ·s ( 𝑦𝑂 ·s 𝑧𝑂 ) ) ) )
110 94 oveq1d ⊢ ( 𝑦𝑂 = 𝑦 → ( ( 𝑥 ·s 𝑦𝑂 ) ·s 𝑧𝑂 ) = ( ( 𝑥 ·s 𝑦 ) ·s 𝑧𝑂 ) )
111 72 oveq2d ⊢ ( 𝑦𝑂 = 𝑦 → ( 𝑥 ·s ( 𝑦𝑂 ·s 𝑧𝑂 ) ) = ( 𝑥 ·s ( 𝑦 ·s 𝑧𝑂 ) ) )
112 110 111 eqeq12d ⊢ ( 𝑦𝑂 = 𝑦 → ( ( ( 𝑥 ·s 𝑦𝑂 ) ·s 𝑧𝑂 ) = ( 𝑥 ·s ( 𝑦𝑂 ·s 𝑧𝑂 ) ) ↔ ( ( 𝑥 ·s 𝑦 ) ·s 𝑧𝑂 ) = ( 𝑥 ·s ( 𝑦 ·s 𝑧𝑂 ) ) ) )
113 oveq2 ⊢ ( 𝑧𝑂 = 𝑧 → ( ( 𝑥 ·s 𝑦 ) ·s 𝑧𝑂 ) = ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) )
114 76 oveq2d ⊢ ( 𝑧𝑂 = 𝑧 → ( 𝑥 ·s ( 𝑦 ·s 𝑧𝑂 ) ) = ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) )
115 113 114 eqeq12d ⊢ ( 𝑧𝑂 = 𝑧 → ( ( ( 𝑥 ·s 𝑦 ) ·s 𝑧𝑂 ) = ( 𝑥 ·s ( 𝑦 ·s 𝑧𝑂 ) ) ↔ ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) = ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) )
116 7 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝐶 ) ∪ ( R ‘ 𝐶 ) ) ( ( 𝑥𝑂 ·s 𝑦𝑂 ) ·s 𝑧𝑂 ) = ( 𝑥𝑂 ·s ( 𝑦𝑂 ·s 𝑧𝑂 ) ) )
117 109 112 115 116 20 29 37 rspc3dv ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) = ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) )
118 106 117 oveq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) = ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) )
119 81 118 eqtr3d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) +s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) = ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) )
120 80 119 oveq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) +s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) +s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) ) = ( ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) +s ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) ) )
121 66 70 120 3eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) +s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) = ( ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) +s ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) ) )
122 38 121 oveq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) -s ( ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) +s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) ) = ( ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) -s ( ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) +s ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) ) ) )
123 52 44 mulscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝐴 ·s 𝐵 ) ∈ No )
124 123 50 mulscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) ∈ No )
125 51 59 addscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) ∈ No )
126 125 63 subscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ∈ No )
127 124 126 69 subsubs4d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) -s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) = ( ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) -s ( ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) +s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) ) )
128 52 101 mulscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) ∈ No )
129 57 50 mulscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑦 ·s 𝑧 ) ∈ No )
130 52 129 mulscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ∈ No )
131 104 102 addscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) ∈ No )
132 43 129 mulscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ∈ No )
133 131 132 subscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) ∈ No )
134 128 130 133 subsubs4d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) -s ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) ) = ( ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) -s ( ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) +s ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) ) ) )
135 122 127 134 3eqtr4d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) -s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) = ( ( ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) -s ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) ) )
136 30 135 oveq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) +s ( ( ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) -s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) ) = ( ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) +s ( ( ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) -s ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) ) ) )
137 58 68 mulscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) ∈ No )
138 124 126 subscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) -s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) ∈ No )
139 137 138 69 addsubsd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) +s ( ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) -s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) = ( ( ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) +s ( ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) -s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) ) )
140 137 138 69 addsubsassd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) +s ( ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) -s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) = ( ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) +s ( ( ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) -s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) ) )
141 139 140 eqtr3d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) +s ( ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) -s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) ) = ( ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) +s ( ( ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) -s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) ) )
142 52 103 mulscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) ∈ No )
143 142 128 130 addsubsassd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) = ( ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) +s ( ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) ) )
144 143 oveq1d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) -s ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) ) = ( ( ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) +s ( ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) ) -s ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) ) )
145 128 130 subscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) ∈ No )
146 142 145 133 addsubsassd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) +s ( ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) ) -s ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) ) = ( ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) +s ( ( ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) -s ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) ) ) )
147 144 146 eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) -s ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) ) = ( ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) +s ( ( ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) -s ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) ) ) )
148 136 141 147 3eqtr4d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) +s ( ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) -s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) ) = ( ( ( ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) -s ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) ) )
149 21 148 oveq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) +s ( ( ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) +s ( ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) -s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) ) ) = ( ( 𝑥 ·s ( 𝐵 ·s 𝐶 ) ) +s ( ( ( ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) -s ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) ) ) )
150 45 68 mulscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) ∈ No )
151 150 137 addscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) ) ∈ No )
152 151 69 subscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) ∈ No )
153 152 124 126 addsubsassd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) ) -s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) = ( ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) +s ( ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) -s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) ) )
154 150 137 69 addsubsassd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) = ( ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) +s ( ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) ) )
155 154 oveq1d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) +s ( ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) -s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) ) = ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) +s ( ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) ) +s ( ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) -s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) ) )
156 137 69 subscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) ∈ No )
157 150 156 138 addsassd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) +s ( ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) ) +s ( ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) -s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) ) = ( ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) +s ( ( ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) +s ( ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) -s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) ) ) )
158 153 155 157 3eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) ) -s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) = ( ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) +s ( ( ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) +s ( ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) -s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) ) ) )
159 44 68 mulscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝐵 ·s 𝐶 ) ∈ No )
160 43 159 mulscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑥 ·s ( 𝐵 ·s 𝐶 ) ) ∈ No )
161 142 128 addscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) ) ∈ No )
162 161 130 subscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) ∈ No )
163 160 162 133 addsubsassd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( 𝑥 ·s ( 𝐵 ·s 𝐶 ) ) +s ( ( ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) ) -s ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) ) = ( ( 𝑥 ·s ( 𝐵 ·s 𝐶 ) ) +s ( ( ( ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) -s ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) ) ) )
164 149 158 163 3eqtr4d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) ) -s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) = ( ( ( 𝑥 ·s ( 𝐵 ·s 𝐶 ) ) +s ( ( ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) ) -s ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) ) )
165 45 58 addscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) ∈ No )
166 165 62 68 subsdird ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) ·s 𝐶 ) = ( ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) ·s 𝐶 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) )
167 45 58 68 addsdird ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) ·s 𝐶 ) = ( ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) ) )
168 167 oveq1d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) ·s 𝐶 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) = ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) )
169 166 168 eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) ·s 𝐶 ) = ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) )
170 169 oveq1d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) ·s 𝐶 ) +s ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) ) = ( ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) ) )
171 165 62 50 subsdird ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) ·s 𝑧 ) = ( ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) ·s 𝑧 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) )
172 45 58 50 addsdird ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) ·s 𝑧 ) = ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) )
173 172 oveq1d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) ·s 𝑧 ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) = ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) )
174 171 173 eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) ·s 𝑧 ) = ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) )
175 170 174 oveq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) ·s 𝐶 ) +s ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) ) -s ( ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) ·s 𝑧 ) ) = ( ( ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝐶 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝐶 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) ) -s ( ( ( ( 𝑥 ·s 𝐵 ) ·s 𝑧 ) +s ( ( 𝐴 ·s 𝑦 ) ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑦 ) ·s 𝑧 ) ) ) )
176 103 101 addscld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) ∈ No )
177 52 176 129 subsdid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝐴 ·s ( ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) ) = ( ( 𝐴 ·s ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) )
178 52 103 101 addsdid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝐴 ·s ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) ) = ( ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) ) )
179 178 oveq1d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝐴 ·s ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) = ( ( ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) )
180 177 179 eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝐴 ·s ( ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) ) = ( ( ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) )
181 180 oveq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝑥 ·s ( 𝐵 ·s 𝐶 ) ) +s ( 𝐴 ·s ( ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) ) ) = ( ( 𝑥 ·s ( 𝐵 ·s 𝐶 ) ) +s ( ( ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) ) )
182 43 176 129 subsdid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑥 ·s ( ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) ) = ( ( 𝑥 ·s ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) )
183 43 103 101 addsdid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑥 ·s ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) ) = ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) )
184 183 oveq1d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝑥 ·s ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) = ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) )
185 182 184 eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑥 ·s ( ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) ) = ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) )
186 181 185 oveq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( 𝑥 ·s ( 𝐵 ·s 𝐶 ) ) +s ( 𝐴 ·s ( ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) ) ) -s ( 𝑥 ·s ( ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) ) ) = ( ( ( 𝑥 ·s ( 𝐵 ·s 𝐶 ) ) +s ( ( ( 𝐴 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝐴 ·s ( 𝑦 ·s 𝑧 ) ) ) ) -s ( ( ( 𝑥 ·s ( 𝑦 ·s 𝐶 ) ) +s ( 𝑥 ·s ( 𝐵 ·s 𝑧 ) ) ) -s ( 𝑥 ·s ( 𝑦 ·s 𝑧 ) ) ) ) )
187 164 175 186 3eqtr4d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( ( ( ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) ·s 𝐶 ) +s ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) ) -s ( ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) ·s 𝑧 ) ) = ( ( ( 𝑥 ·s ( 𝐵 ·s 𝐶 ) ) +s ( 𝐴 ·s ( ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) ) ) -s ( 𝑥 ·s ( ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) ) ) )
188 187 eqeq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑎 = ( ( ( ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) ·s 𝐶 ) +s ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) ) -s ( ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) ·s 𝑧 ) ) ↔ 𝑎 = ( ( ( 𝑥 ·s ( 𝐵 ·s 𝐶 ) ) +s ( 𝐴 ·s ( ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) ) ) -s ( 𝑥 ·s ( ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) ) ) ) )
189 188 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ) ∧ 𝑧 ∈ 𝑅 ) → ( 𝑎 = ( ( ( ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) ·s 𝐶 ) +s ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) ) -s ( ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) ·s 𝑧 ) ) ↔ 𝑎 = ( ( ( 𝑥 ·s ( 𝐵 ·s 𝐶 ) ) +s ( 𝐴 ·s ( ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) ) ) -s ( 𝑥 ·s ( ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) ) ) ) )
190 189 rexbidva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄 ) ) → ( ∃ 𝑧 ∈ 𝑅 𝑎 = ( ( ( ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) ·s 𝐶 ) +s ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) ) -s ( ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) ·s 𝑧 ) ) ↔ ∃ 𝑧 ∈ 𝑅 𝑎 = ( ( ( 𝑥 ·s ( 𝐵 ·s 𝐶 ) ) +s ( 𝐴 ·s ( ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) ) ) -s ( 𝑥 ·s ( ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) ) ) ) )
191 190 2rexbidva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑄 ∃ 𝑧 ∈ 𝑅 𝑎 = ( ( ( ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) ·s 𝐶 ) +s ( ( 𝐴 ·s 𝐵 ) ·s 𝑧 ) ) -s ( ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) ·s 𝑧 ) ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑄 ∃ 𝑧 ∈ 𝑅 𝑎 = ( ( ( 𝑥 ·s ( 𝐵 ·s 𝐶 ) ) +s ( 𝐴 ·s ( ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) ) ) -s ( 𝑥 ·s ( ( ( 𝑦 ·s 𝐶 ) +s ( 𝐵 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) ) ) ) )