Metamath Proof Explorer

Theorem addsdilem3

Description: Lemma for addsdi . Show one of the equalities involved in the final expression. (Contributed by Scott Fenton, 9-Mar-2025)

Ref Expression
Hypotheses addsdilem3.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
addsdilem3.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
addsdilem3.3 ⊢ ( 𝜑 → 𝐶 ∈ No )
addsdilem3.4 ⊢ ( 𝜑 → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 𝑥𝑂 ·s ( 𝐵 +s 𝐶 ) ) = ( ( 𝑥𝑂 ·s 𝐵 ) +s ( 𝑥𝑂 ·s 𝐶 ) ) )
addsdilem3.5 ⊢ ( 𝜑 → ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ( 𝐴 ·s ( 𝑦𝑂 +s 𝐶 ) ) = ( ( 𝐴 ·s 𝑦𝑂 ) +s ( 𝐴 ·s 𝐶 ) ) )
addsdilem3.6 ⊢ ( 𝜑 → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝐶 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝐶 ) ) )
addsdilem3.7 ⊢ ( 𝜓 → 𝑋 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
addsdilem3.8 ⊢ ( 𝜓 → 𝑌 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) )
Assertion addsdilem3 ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝑋 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑌 +s 𝐶 ) ) ) -s ( 𝑋 ·s ( 𝑌 +s 𝐶 ) ) ) = ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝐴 ·s 𝑌 ) ) -s ( 𝑋 ·s 𝑌 ) ) +s ( 𝐴 ·s 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 addsdilem3.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
2 addsdilem3.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
3 addsdilem3.3 ⊢ ( 𝜑 → 𝐶 ∈ No )
4 addsdilem3.4 ⊢ ( 𝜑 → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 𝑥𝑂 ·s ( 𝐵 +s 𝐶 ) ) = ( ( 𝑥𝑂 ·s 𝐵 ) +s ( 𝑥𝑂 ·s 𝐶 ) ) )
5 addsdilem3.5 ⊢ ( 𝜑 → ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ( 𝐴 ·s ( 𝑦𝑂 +s 𝐶 ) ) = ( ( 𝐴 ·s 𝑦𝑂 ) +s ( 𝐴 ·s 𝐶 ) ) )
6 addsdilem3.6 ⊢ ( 𝜑 → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝐶 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝐶 ) ) )
7 addsdilem3.7 ⊢ ( 𝜓 → 𝑋 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
8 addsdilem3.8 ⊢ ( 𝜓 → 𝑌 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) )
9 oveq1 ⊢ ( 𝑥𝑂 = 𝑋 → ( 𝑥𝑂 ·s ( 𝐵 +s 𝐶 ) ) = ( 𝑋 ·s ( 𝐵 +s 𝐶 ) ) )
10 oveq1 ⊢ ( 𝑥𝑂 = 𝑋 → ( 𝑥𝑂 ·s 𝐵 ) = ( 𝑋 ·s 𝐵 ) )
11 oveq1 ⊢ ( 𝑥𝑂 = 𝑋 → ( 𝑥𝑂 ·s 𝐶 ) = ( 𝑋 ·s 𝐶 ) )
12 10 11 oveq12d ⊢ ( 𝑥𝑂 = 𝑋 → ( ( 𝑥𝑂 ·s 𝐵 ) +s ( 𝑥𝑂 ·s 𝐶 ) ) = ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) )
13 9 12 eqeq12d ⊢ ( 𝑥𝑂 = 𝑋 → ( ( 𝑥𝑂 ·s ( 𝐵 +s 𝐶 ) ) = ( ( 𝑥𝑂 ·s 𝐵 ) +s ( 𝑥𝑂 ·s 𝐶 ) ) ↔ ( 𝑋 ·s ( 𝐵 +s 𝐶 ) ) = ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) ) )
14 4 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 𝑥𝑂 ·s ( 𝐵 +s 𝐶 ) ) = ( ( 𝑥𝑂 ·s 𝐵 ) +s ( 𝑥𝑂 ·s 𝐶 ) ) )
15 7 adantl ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑋 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
16 13 14 15 rspcdva ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑋 ·s ( 𝐵 +s 𝐶 ) ) = ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) )
17 oveq1 ⊢ ( 𝑦𝑂 = 𝑌 → ( 𝑦𝑂 +s 𝐶 ) = ( 𝑌 +s 𝐶 ) )
18 17 oveq2d ⊢ ( 𝑦𝑂 = 𝑌 → ( 𝐴 ·s ( 𝑦𝑂 +s 𝐶 ) ) = ( 𝐴 ·s ( 𝑌 +s 𝐶 ) ) )
19 oveq2 ⊢ ( 𝑦𝑂 = 𝑌 → ( 𝐴 ·s 𝑦𝑂 ) = ( 𝐴 ·s 𝑌 ) )
20 19 oveq1d ⊢ ( 𝑦𝑂 = 𝑌 → ( ( 𝐴 ·s 𝑦𝑂 ) +s ( 𝐴 ·s 𝐶 ) ) = ( ( 𝐴 ·s 𝑌 ) +s ( 𝐴 ·s 𝐶 ) ) )
21 18 20 eqeq12d ⊢ ( 𝑦𝑂 = 𝑌 → ( ( 𝐴 ·s ( 𝑦𝑂 +s 𝐶 ) ) = ( ( 𝐴 ·s 𝑦𝑂 ) +s ( 𝐴 ·s 𝐶 ) ) ↔ ( 𝐴 ·s ( 𝑌 +s 𝐶 ) ) = ( ( 𝐴 ·s 𝑌 ) +s ( 𝐴 ·s 𝐶 ) ) ) )
22 5 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ( 𝐴 ·s ( 𝑦𝑂 +s 𝐶 ) ) = ( ( 𝐴 ·s 𝑦𝑂 ) +s ( 𝐴 ·s 𝐶 ) ) )
23 8 adantl ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑌 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) )
24 21 22 23 rspcdva ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐴 ·s ( 𝑌 +s 𝐶 ) ) = ( ( 𝐴 ·s 𝑌 ) +s ( 𝐴 ·s 𝐶 ) ) )
25 16 24 oveq12d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑋 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑌 +s 𝐶 ) ) ) = ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝑌 ) +s ( 𝐴 ·s 𝐶 ) ) ) )
26 oveq1 ⊢ ( 𝑥𝑂 = 𝑋 → ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝐶 ) ) = ( 𝑋 ·s ( 𝑦𝑂 +s 𝐶 ) ) )
27 oveq1 ⊢ ( 𝑥𝑂 = 𝑋 → ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑋 ·s 𝑦𝑂 ) )
28 27 11 oveq12d ⊢ ( 𝑥𝑂 = 𝑋 → ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝐶 ) ) = ( ( 𝑋 ·s 𝑦𝑂 ) +s ( 𝑋 ·s 𝐶 ) ) )
29 26 28 eqeq12d ⊢ ( 𝑥𝑂 = 𝑋 → ( ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝐶 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝐶 ) ) ↔ ( 𝑋 ·s ( 𝑦𝑂 +s 𝐶 ) ) = ( ( 𝑋 ·s 𝑦𝑂 ) +s ( 𝑋 ·s 𝐶 ) ) ) )
30 17 oveq2d ⊢ ( 𝑦𝑂 = 𝑌 → ( 𝑋 ·s ( 𝑦𝑂 +s 𝐶 ) ) = ( 𝑋 ·s ( 𝑌 +s 𝐶 ) ) )
31 oveq2 ⊢ ( 𝑦𝑂 = 𝑌 → ( 𝑋 ·s 𝑦𝑂 ) = ( 𝑋 ·s 𝑌 ) )
32 31 oveq1d ⊢ ( 𝑦𝑂 = 𝑌 → ( ( 𝑋 ·s 𝑦𝑂 ) +s ( 𝑋 ·s 𝐶 ) ) = ( ( 𝑋 ·s 𝑌 ) +s ( 𝑋 ·s 𝐶 ) ) )
33 30 32 eqeq12d ⊢ ( 𝑦𝑂 = 𝑌 → ( ( 𝑋 ·s ( 𝑦𝑂 +s 𝐶 ) ) = ( ( 𝑋 ·s 𝑦𝑂 ) +s ( 𝑋 ·s 𝐶 ) ) ↔ ( 𝑋 ·s ( 𝑌 +s 𝐶 ) ) = ( ( 𝑋 ·s 𝑌 ) +s ( 𝑋 ·s 𝐶 ) ) ) )
34 6 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝐶 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝐶 ) ) )
35 29 33 34 15 23 rspc2dv ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑋 ·s ( 𝑌 +s 𝐶 ) ) = ( ( 𝑋 ·s 𝑌 ) +s ( 𝑋 ·s 𝐶 ) ) )
36 25 35 oveq12d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝑋 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑌 +s 𝐶 ) ) ) -s ( 𝑋 ·s ( 𝑌 +s 𝐶 ) ) ) = ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝑌 ) +s ( 𝐴 ·s 𝐶 ) ) ) -s ( ( 𝑋 ·s 𝑌 ) +s ( 𝑋 ·s 𝐶 ) ) ) )
37 leftssno ⊢ ( L ‘ 𝐴 ) ⊆ No
38 rightssno ⊢ ( R ‘ 𝐴 ) ⊆ No
39 37 38 unssi ⊢ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ⊆ No
40 39 7 sselid ⊢ ( 𝜓 → 𝑋 ∈ No )
41 40 adantl ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑋 ∈ No )
42 2 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐵 ∈ No )
43 41 42 mulscld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑋 ·s 𝐵 ) ∈ No )
44 3 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 ∈ No )
45 41 44 mulscld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑋 ·s 𝐶 ) ∈ No )
46 pncans ⊢ ( ( ( 𝑋 ·s 𝐵 ) ∈ No ∧ ( 𝑋 ·s 𝐶 ) ∈ No ) → ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) -s ( 𝑋 ·s 𝐶 ) ) = ( 𝑋 ·s 𝐵 ) )
47 43 45 46 syl2anc ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) -s ( 𝑋 ·s 𝐶 ) ) = ( 𝑋 ·s 𝐵 ) )
48 47 oveq1d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) -s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝑌 ) +s ( 𝐴 ·s 𝐶 ) ) ) = ( ( 𝑋 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑌 ) +s ( 𝐴 ·s 𝐶 ) ) ) )
49 43 45 addscld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) ∈ No )
50 1 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐴 ∈ No )
51 leftssno ⊢ ( L ‘ 𝐵 ) ⊆ No
52 rightssno ⊢ ( R ‘ 𝐵 ) ⊆ No
53 51 52 unssi ⊢ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ⊆ No
54 53 8 sselid ⊢ ( 𝜓 → 𝑌 ∈ No )
55 54 adantl ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑌 ∈ No )
56 50 55 mulscld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐴 ·s 𝑌 ) ∈ No )
57 1 3 mulscld ⊢ ( 𝜑 → ( 𝐴 ·s 𝐶 ) ∈ No )
58 57 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐴 ·s 𝐶 ) ∈ No )
59 56 58 addscld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐴 ·s 𝑌 ) +s ( 𝐴 ·s 𝐶 ) ) ∈ No )
60 49 59 45 addsubsd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝑌 ) +s ( 𝐴 ·s 𝐶 ) ) ) -s ( 𝑋 ·s 𝐶 ) ) = ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) -s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝑌 ) +s ( 𝐴 ·s 𝐶 ) ) ) )
61 43 56 58 addsassd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝐴 ·s 𝑌 ) ) +s ( 𝐴 ·s 𝐶 ) ) = ( ( 𝑋 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑌 ) +s ( 𝐴 ·s 𝐶 ) ) ) )
62 48 60 61 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝑌 ) +s ( 𝐴 ·s 𝐶 ) ) ) -s ( 𝑋 ·s 𝐶 ) ) = ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝐴 ·s 𝑌 ) ) +s ( 𝐴 ·s 𝐶 ) ) )
63 62 oveq1d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝑌 ) +s ( 𝐴 ·s 𝐶 ) ) ) -s ( 𝑋 ·s 𝐶 ) ) -s ( 𝑋 ·s 𝑌 ) ) = ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝐴 ·s 𝑌 ) ) +s ( 𝐴 ·s 𝐶 ) ) -s ( 𝑋 ·s 𝑌 ) ) )
64 49 59 addscld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝑌 ) +s ( 𝐴 ·s 𝐶 ) ) ) ∈ No )
65 40 54 mulscld ⊢ ( 𝜓 → ( 𝑋 ·s 𝑌 ) ∈ No )
66 65 adantl ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑋 ·s 𝑌 ) ∈ No )
67 64 45 66 subsubs4d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝑌 ) +s ( 𝐴 ·s 𝐶 ) ) ) -s ( 𝑋 ·s 𝐶 ) ) -s ( 𝑋 ·s 𝑌 ) ) = ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝑌 ) +s ( 𝐴 ·s 𝐶 ) ) ) -s ( ( 𝑋 ·s 𝐶 ) +s ( 𝑋 ·s 𝑌 ) ) ) )
68 45 66 addscomd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑋 ·s 𝐶 ) +s ( 𝑋 ·s 𝑌 ) ) = ( ( 𝑋 ·s 𝑌 ) +s ( 𝑋 ·s 𝐶 ) ) )
69 68 oveq2d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝑌 ) +s ( 𝐴 ·s 𝐶 ) ) ) -s ( ( 𝑋 ·s 𝐶 ) +s ( 𝑋 ·s 𝑌 ) ) ) = ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝑌 ) +s ( 𝐴 ·s 𝐶 ) ) ) -s ( ( 𝑋 ·s 𝑌 ) +s ( 𝑋 ·s 𝐶 ) ) ) )
70 67 69 eqtrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝑌 ) +s ( 𝐴 ·s 𝐶 ) ) ) -s ( 𝑋 ·s 𝐶 ) ) -s ( 𝑋 ·s 𝑌 ) ) = ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝑌 ) +s ( 𝐴 ·s 𝐶 ) ) ) -s ( ( 𝑋 ·s 𝑌 ) +s ( 𝑋 ·s 𝐶 ) ) ) )
71 43 56 addscld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑋 ·s 𝐵 ) +s ( 𝐴 ·s 𝑌 ) ) ∈ No )
72 71 58 66 addsubsd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝐴 ·s 𝑌 ) ) +s ( 𝐴 ·s 𝐶 ) ) -s ( 𝑋 ·s 𝑌 ) ) = ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝐴 ·s 𝑌 ) ) -s ( 𝑋 ·s 𝑌 ) ) +s ( 𝐴 ·s 𝐶 ) ) )
73 63 70 72 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝑌 ) +s ( 𝐴 ·s 𝐶 ) ) ) -s ( ( 𝑋 ·s 𝑌 ) +s ( 𝑋 ·s 𝐶 ) ) ) = ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝐴 ·s 𝑌 ) ) -s ( 𝑋 ·s 𝑌 ) ) +s ( 𝐴 ·s 𝐶 ) ) )
74 36 73 eqtrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝑋 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑌 +s 𝐶 ) ) ) -s ( 𝑋 ·s ( 𝑌 +s 𝐶 ) ) ) = ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝐴 ·s 𝑌 ) ) -s ( 𝑋 ·s 𝑌 ) ) +s ( 𝐴 ·s 𝐶 ) ) )