Proof of Theorem addsdilem4
Step | Hyp | Ref
| Expression |
1 | | oveq1 7401 |
. . . . . 6
⊢ (𝑥𝑂 = 𝑋 → (𝑥𝑂 ·s
(𝐵 +s 𝐶)) = (𝑋 ·s (𝐵 +s 𝐶))) |
2 | | oveq1 7401 |
. . . . . . 7
⊢ (𝑥𝑂 = 𝑋 → (𝑥𝑂 ·s
𝐵) = (𝑋 ·s 𝐵)) |
3 | | oveq1 7401 |
. . . . . . 7
⊢ (𝑥𝑂 = 𝑋 → (𝑥𝑂 ·s
𝐶) = (𝑋 ·s 𝐶)) |
4 | 2, 3 | oveq12d 7412 |
. . . . . 6
⊢ (𝑥𝑂 = 𝑋 → ((𝑥𝑂 ·s
𝐵) +s (𝑥𝑂
·s 𝐶)) =
((𝑋 ·s
𝐵) +s (𝑋 ·s 𝐶))) |
5 | 1, 4 | eqeq12d 2748 |
. . . . 5
⊢ (𝑥𝑂 = 𝑋 → ((𝑥𝑂 ·s
(𝐵 +s 𝐶)) = ((𝑥𝑂 ·s
𝐵) +s (𝑥𝑂
·s 𝐶))
↔ (𝑋
·s (𝐵
+s 𝐶)) = ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)))) |
6 | | addsdilem4.4 |
. . . . . 6
⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))(𝑥𝑂 ·s
(𝐵 +s 𝐶)) = ((𝑥𝑂 ·s
𝐵) +s (𝑥𝑂
·s 𝐶))) |
7 | 6 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))(𝑥𝑂 ·s
(𝐵 +s 𝐶)) = ((𝑥𝑂 ·s
𝐵) +s (𝑥𝑂
·s 𝐶))) |
8 | | addsdilem4.7 |
. . . . . 6
⊢ (𝜓 → 𝑋 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))) |
9 | 8 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))) |
10 | 5, 7, 9 | rspcdva 3611 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝑋 ·s (𝐵 +s 𝐶)) = ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶))) |
11 | | oveq2 7402 |
. . . . . . 7
⊢ (𝑧𝑂 = 𝑍 → (𝐵 +s 𝑧𝑂) = (𝐵 +s 𝑍)) |
12 | 11 | oveq2d 7410 |
. . . . . 6
⊢ (𝑧𝑂 = 𝑍 → (𝐴 ·s (𝐵 +s 𝑧𝑂)) = (𝐴 ·s (𝐵 +s 𝑍))) |
13 | | oveq2 7402 |
. . . . . . 7
⊢ (𝑧𝑂 = 𝑍 → (𝐴 ·s 𝑧𝑂) = (𝐴 ·s 𝑍)) |
14 | 13 | oveq2d 7410 |
. . . . . 6
⊢ (𝑧𝑂 = 𝑍 → ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑧𝑂)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍))) |
15 | 12, 14 | eqeq12d 2748 |
. . . . 5
⊢ (𝑧𝑂 = 𝑍 → ((𝐴 ·s (𝐵 +s 𝑧𝑂)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑧𝑂)) ↔ (𝐴 ·s (𝐵 +s 𝑍)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍)))) |
16 | | addsdilem4.5 |
. . . . . 6
⊢ (𝜑 → ∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))(𝐴 ·s (𝐵 +s 𝑧𝑂)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑧𝑂))) |
17 | 16 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))(𝐴 ·s (𝐵 +s 𝑧𝑂)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑧𝑂))) |
18 | | addsdilem4.8 |
. . . . . 6
⊢ (𝜓 → 𝑍 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))) |
19 | 18 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝑍 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))) |
20 | 15, 17, 19 | rspcdva 3611 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝐴 ·s (𝐵 +s 𝑍)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍))) |
21 | 10, 20 | oveq12d 7412 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((𝑋 ·s (𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑍))) = (((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍)))) |
22 | | oveq1 7401 |
. . . . 5
⊢ (𝑥𝑂 = 𝑋 → (𝑥𝑂 ·s
(𝐵 +s 𝑧𝑂)) = (𝑋 ·s (𝐵 +s 𝑧𝑂))) |
23 | | oveq1 7401 |
. . . . . 6
⊢ (𝑥𝑂 = 𝑋 → (𝑥𝑂 ·s
𝑧𝑂) =
(𝑋 ·s
𝑧𝑂)) |
24 | 2, 23 | oveq12d 7412 |
. . . . 5
⊢ (𝑥𝑂 = 𝑋 → ((𝑥𝑂 ·s
𝐵) +s (𝑥𝑂
·s 𝑧𝑂)) = ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝑧𝑂))) |
25 | 22, 24 | eqeq12d 2748 |
. . . 4
⊢ (𝑥𝑂 = 𝑋 → ((𝑥𝑂 ·s
(𝐵 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝐵)
+s (𝑥𝑂 ·s
𝑧𝑂))
↔ (𝑋
·s (𝐵
+s 𝑧𝑂)) = ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝑧𝑂)))) |
26 | 11 | oveq2d 7410 |
. . . . 5
⊢ (𝑧𝑂 = 𝑍 → (𝑋 ·s (𝐵 +s 𝑧𝑂)) = (𝑋 ·s (𝐵 +s 𝑍))) |
27 | | oveq2 7402 |
. . . . . 6
⊢ (𝑧𝑂 = 𝑍 → (𝑋 ·s 𝑧𝑂) = (𝑋 ·s 𝑍)) |
28 | 27 | oveq2d 7410 |
. . . . 5
⊢ (𝑧𝑂 = 𝑍 → ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝑧𝑂)) = ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝑍))) |
29 | 26, 28 | eqeq12d 2748 |
. . . 4
⊢ (𝑧𝑂 = 𝑍 → ((𝑋 ·s (𝐵 +s 𝑧𝑂)) = ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝑧𝑂)) ↔ (𝑋 ·s (𝐵 +s 𝑍)) = ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝑍)))) |
30 | | addsdilem4.6 |
. . . . 5
⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))(𝑥𝑂 ·s
(𝐵 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝐵)
+s (𝑥𝑂 ·s
𝑧𝑂))) |
31 | 30 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))(𝑥𝑂 ·s
(𝐵 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝐵)
+s (𝑥𝑂 ·s
𝑧𝑂))) |
32 | 25, 29, 31, 9, 19 | rspc2dv 3623 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (𝑋 ·s (𝐵 +s 𝑍)) = ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝑍))) |
33 | 21, 32 | oveq12d 7412 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (((𝑋 ·s (𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑍))) -s (𝑋 ·s (𝐵 +s 𝑍))) = ((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍))) -s ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝑍)))) |
34 | | leftssno 27304 |
. . . . . . . . 9
⊢ ( L
‘𝐴) ⊆ No |
35 | | rightssno 27305 |
. . . . . . . . 9
⊢ ( R
‘𝐴) ⊆ No |
36 | 34, 35 | unssi 4182 |
. . . . . . . 8
⊢ (( L
‘𝐴) ∪ ( R
‘𝐴)) ⊆ No |
37 | 36, 8 | sselid 3977 |
. . . . . . 7
⊢ (𝜓 → 𝑋 ∈ No
) |
38 | 37 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ No
) |
39 | | addsdilem4.2 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ No
) |
40 | 39 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝐵 ∈ No
) |
41 | 38, 40 | mulscld 27520 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (𝑋 ·s 𝐵) ∈ No
) |
42 | | addsdilem4.3 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ No
) |
43 | 42 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ No
) |
44 | 38, 43 | mulscld 27520 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (𝑋 ·s 𝐶) ∈ No
) |
45 | 41, 44 | addscld 27393 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) ∈ No
) |
46 | | addsdilem4.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ No
) |
47 | 46, 39 | mulscld 27520 |
. . . . . 6
⊢ (𝜑 → (𝐴 ·s 𝐵) ∈ No
) |
48 | 47 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (𝐴 ·s 𝐵) ∈ No
) |
49 | 46 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ No
) |
50 | | leftssno 27304 |
. . . . . . . . 9
⊢ ( L
‘𝐶) ⊆ No |
51 | | rightssno 27305 |
. . . . . . . . 9
⊢ ( R
‘𝐶) ⊆ No |
52 | 50, 51 | unssi 4182 |
. . . . . . . 8
⊢ (( L
‘𝐶) ∪ ( R
‘𝐶)) ⊆ No |
53 | 52, 18 | sselid 3977 |
. . . . . . 7
⊢ (𝜓 → 𝑍 ∈ No
) |
54 | 53 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝑍 ∈ No
) |
55 | 49, 54 | mulscld 27520 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (𝐴 ·s 𝑍) ∈ No
) |
56 | 48, 55 | addscld 27393 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍)) ∈ No
) |
57 | 45, 56 | addscld 27393 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍))) ∈ No
) |
58 | 38, 54 | mulscld 27520 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (𝑋 ·s 𝑍) ∈ No
) |
59 | 57, 41, 58 | subsubs4d 27489 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍))) -s (𝑋 ·s 𝐵)) -s (𝑋 ·s 𝑍)) = ((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍))) -s ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝑍)))) |
60 | 45, 56, 41 | addsubsd 27478 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍))) -s (𝑋 ·s 𝐵)) = ((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) -s (𝑋 ·s 𝐵)) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍)))) |
61 | 41, 44 | addscomd 27380 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) = ((𝑋 ·s 𝐶) +s (𝑋 ·s 𝐵))) |
62 | 61 | oveq1d 7409 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) -s (𝑋 ·s 𝐵)) = (((𝑋 ·s 𝐶) +s (𝑋 ·s 𝐵)) -s (𝑋 ·s 𝐵))) |
63 | | pncans 27469 |
. . . . . . . 8
⊢ (((𝑋 ·s 𝐶) ∈
No ∧ (𝑋
·s 𝐵)
∈ No ) → (((𝑋 ·s 𝐶) +s (𝑋 ·s 𝐵)) -s (𝑋 ·s 𝐵)) = (𝑋 ·s 𝐶)) |
64 | 44, 41, 63 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (((𝑋 ·s 𝐶) +s (𝑋 ·s 𝐵)) -s (𝑋 ·s 𝐵)) = (𝑋 ·s 𝐶)) |
65 | 62, 64 | eqtrd 2772 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → (((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) -s (𝑋 ·s 𝐵)) = (𝑋 ·s 𝐶)) |
66 | 65 | oveq1d 7409 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) -s (𝑋 ·s 𝐵)) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍))) = ((𝑋 ·s 𝐶) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍)))) |
67 | 44, 48, 55 | adds12d 27420 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ((𝑋 ·s 𝐶) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍))) = ((𝐴 ·s 𝐵) +s ((𝑋 ·s 𝐶) +s (𝐴 ·s 𝑍)))) |
68 | 60, 66, 67 | 3eqtrd 2776 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍))) -s (𝑋 ·s 𝐵)) = ((𝐴 ·s 𝐵) +s ((𝑋 ·s 𝐶) +s (𝐴 ·s 𝑍)))) |
69 | 68 | oveq1d 7409 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍))) -s (𝑋 ·s 𝐵)) -s (𝑋 ·s 𝑍)) = (((𝐴 ·s 𝐵) +s ((𝑋 ·s 𝐶) +s (𝐴 ·s 𝑍))) -s (𝑋 ·s 𝑍))) |
70 | 44, 55 | addscld 27393 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ((𝑋 ·s 𝐶) +s (𝐴 ·s 𝑍)) ∈ No
) |
71 | 48, 70, 58 | addsubsassd 27477 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (((𝐴 ·s 𝐵) +s ((𝑋 ·s 𝐶) +s (𝐴 ·s 𝑍))) -s (𝑋 ·s 𝑍)) = ((𝐴 ·s 𝐵) +s (((𝑋 ·s 𝐶) +s (𝐴 ·s 𝑍)) -s (𝑋 ·s 𝑍)))) |
72 | 69, 71 | eqtrd 2772 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍))) -s (𝑋 ·s 𝐵)) -s (𝑋 ·s 𝑍)) = ((𝐴 ·s 𝐵) +s (((𝑋 ·s 𝐶) +s (𝐴 ·s 𝑍)) -s (𝑋 ·s 𝑍)))) |
73 | 33, 59, 72 | 3eqtr2d 2778 |
1
⊢ ((𝜑 ∧ 𝜓) → (((𝑋 ·s (𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑍))) -s (𝑋 ·s (𝐵 +s 𝑍))) = ((𝐴 ·s 𝐵) +s (((𝑋 ·s 𝐶) +s (𝐴 ·s 𝑍)) -s (𝑋 ·s 𝑍)))) |