Proof of Theorem addsdilem3
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 | | addsdilem3.4 |
. . . . . 6
⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))(𝑥𝑂 ·s
(𝐵 +s 𝐶)) = ((𝑥𝑂 ·s
𝐵) +s (𝑥𝑂
·s 𝐶))) |
7 | 6 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))(𝑥𝑂 ·s
(𝐵 +s 𝐶)) = ((𝑥𝑂 ·s
𝐵) +s (𝑥𝑂
·s 𝐶))) |
8 | | addsdilem3.7 |
. . . . . 6
⊢ (𝜓 → 𝑋 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))) |
9 | 8 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))) |
10 | 5, 7, 9 | rspcdva 3611 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝑋 ·s (𝐵 +s 𝐶)) = ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶))) |
11 | | oveq1 7401 |
. . . . . . 7
⊢ (𝑦𝑂 = 𝑌 → (𝑦𝑂 +s 𝐶) = (𝑌 +s 𝐶)) |
12 | 11 | oveq2d 7410 |
. . . . . 6
⊢ (𝑦𝑂 = 𝑌 → (𝐴 ·s (𝑦𝑂 +s 𝐶)) = (𝐴 ·s (𝑌 +s 𝐶))) |
13 | | oveq2 7402 |
. . . . . . 7
⊢ (𝑦𝑂 = 𝑌 → (𝐴 ·s 𝑦𝑂) = (𝐴 ·s 𝑌)) |
14 | 13 | oveq1d 7409 |
. . . . . 6
⊢ (𝑦𝑂 = 𝑌 → ((𝐴 ·s 𝑦𝑂) +s (𝐴 ·s 𝐶)) = ((𝐴 ·s 𝑌) +s (𝐴 ·s 𝐶))) |
15 | 12, 14 | eqeq12d 2748 |
. . . . 5
⊢ (𝑦𝑂 = 𝑌 → ((𝐴 ·s (𝑦𝑂 +s 𝐶)) = ((𝐴 ·s 𝑦𝑂) +s (𝐴 ·s 𝐶)) ↔ (𝐴 ·s (𝑌 +s 𝐶)) = ((𝐴 ·s 𝑌) +s (𝐴 ·s 𝐶)))) |
16 | | addsdilem3.5 |
. . . . . 6
⊢ (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))(𝐴 ·s (𝑦𝑂 +s 𝐶)) = ((𝐴 ·s 𝑦𝑂) +s (𝐴 ·s 𝐶))) |
17 | 16 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))(𝐴 ·s (𝑦𝑂 +s 𝐶)) = ((𝐴 ·s 𝑦𝑂) +s (𝐴 ·s 𝐶))) |
18 | | addsdilem3.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 | 23, 3 | 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 | oveq1d 7409 |
. . . . 5
⊢ (𝑦𝑂 = 𝑌 → ((𝑋 ·s 𝑦𝑂) +s (𝑋 ·s 𝐶)) = ((𝑋 ·s 𝑌) +s (𝑋 ·s 𝐶))) |
29 | 26, 28 | eqeq12d 2748 |
. . . 4
⊢ (𝑦𝑂 = 𝑌 → ((𝑋 ·s (𝑦𝑂 +s 𝐶)) = ((𝑋 ·s 𝑦𝑂) +s (𝑋 ·s 𝐶)) ↔ (𝑋 ·s (𝑌 +s 𝐶)) = ((𝑋 ·s 𝑌) +s (𝑋 ·s 𝐶)))) |
30 | | addsdilem3.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 |
. . . . . . . . . . 11
⊢ ( L
‘𝐴) ⊆ No |
35 | | rightssno 27305 |
. . . . . . . . . . 11
⊢ ( R
‘𝐴) ⊆ No |
36 | 34, 35 | unssi 4182 |
. . . . . . . . . 10
⊢ (( L
‘𝐴) ∪ ( R
‘𝐴)) ⊆ No |
37 | 36, 8 | sselid 3977 |
. . . . . . . . 9
⊢ (𝜓 → 𝑋 ∈ No
) |
38 | 37 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ No
) |
39 | | addsdilem3.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ No
) |
40 | 39 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → 𝐵 ∈ No
) |
41 | 38, 40 | mulscld 27520 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (𝑋 ·s 𝐵) ∈ No
) |
42 | | addsdilem3.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ No
) |
43 | 42 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ No
) |
44 | 38, 43 | mulscld 27520 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (𝑋 ·s 𝐶) ∈ No
) |
45 | | pncans 27469 |
. . . . . . 7
⊢ (((𝑋 ·s 𝐵) ∈
No ∧ (𝑋
·s 𝐶)
∈ No ) → (((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) -s (𝑋 ·s 𝐶)) = (𝑋 ·s 𝐵)) |
46 | 41, 44, 45 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → (((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) -s (𝑋 ·s 𝐶)) = (𝑋 ·s 𝐵)) |
47 | 46 | oveq1d 7409 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) -s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝑌) +s (𝐴 ·s 𝐶))) = ((𝑋 ·s 𝐵) +s ((𝐴 ·s 𝑌) +s (𝐴 ·s 𝐶)))) |
48 | 41, 44 | addscld 27393 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) ∈ No
) |
49 | | addsdilem3.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ No
) |
50 | 49 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ No
) |
51 | | leftssno 27304 |
. . . . . . . . . . 11
⊢ ( L
‘𝐵) ⊆ No |
52 | | rightssno 27305 |
. . . . . . . . . . 11
⊢ ( R
‘𝐵) ⊆ No |
53 | 51, 52 | unssi 4182 |
. . . . . . . . . 10
⊢ (( L
‘𝐵) ∪ ( R
‘𝐵)) ⊆ No |
54 | 53, 18 | sselid 3977 |
. . . . . . . . 9
⊢ (𝜓 → 𝑌 ∈ No
) |
55 | 54 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ No
) |
56 | 50, 55 | mulscld 27520 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (𝐴 ·s 𝑌) ∈ No
) |
57 | 49, 42 | mulscld 27520 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ·s 𝐶) ∈ No
) |
58 | 57 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (𝐴 ·s 𝐶) ∈ No
) |
59 | 56, 58 | addscld 27393 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → ((𝐴 ·s 𝑌) +s (𝐴 ·s 𝐶)) ∈ No
) |
60 | 48, 59, 44 | addsubsd 27478 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝑌) +s (𝐴 ·s 𝐶))) -s (𝑋 ·s 𝐶)) = ((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) -s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝑌) +s (𝐴 ·s 𝐶)))) |
61 | 41, 56, 58 | addsassd 27418 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (((𝑋 ·s 𝐵) +s (𝐴 ·s 𝑌)) +s (𝐴 ·s 𝐶)) = ((𝑋 ·s 𝐵) +s ((𝐴 ·s 𝑌) +s (𝐴 ·s 𝐶)))) |
62 | 47, 60, 61 | 3eqtr4d 2782 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝑌) +s (𝐴 ·s 𝐶))) -s (𝑋 ·s 𝐶)) = (((𝑋 ·s 𝐵) +s (𝐴 ·s 𝑌)) +s (𝐴 ·s 𝐶))) |
63 | 62 | oveq1d 7409 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝑌) +s (𝐴 ·s 𝐶))) -s (𝑋 ·s 𝐶)) -s (𝑋 ·s 𝑌)) = ((((𝑋 ·s 𝐵) +s (𝐴 ·s 𝑌)) +s (𝐴 ·s 𝐶)) -s (𝑋 ·s 𝑌))) |
64 | 48, 59 | addscld 27393 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝑌) +s (𝐴 ·s 𝐶))) ∈ No
) |
65 | 37, 54 | mulscld 27520 |
. . . . . 6
⊢ (𝜓 → (𝑋 ·s 𝑌) ∈ No
) |
66 | 65 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (𝑋 ·s 𝑌) ∈ No
) |
67 | 64, 44, 66 | subsubs4d 27489 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝑌) +s (𝐴 ·s 𝐶))) -s (𝑋 ·s 𝐶)) -s (𝑋 ·s 𝑌)) = ((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝑌) +s (𝐴 ·s 𝐶))) -s ((𝑋 ·s 𝐶) +s (𝑋 ·s 𝑌)))) |
68 | 44, 66 | addscomd 27380 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ((𝑋 ·s 𝐶) +s (𝑋 ·s 𝑌)) = ((𝑋 ·s 𝑌) +s (𝑋 ·s 𝐶))) |
69 | 68 | oveq2d 7410 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ((((𝑋 ·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 2772 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝑌) +s (𝐴 ·s 𝐶))) -s (𝑋 ·s 𝐶)) -s (𝑋 ·s 𝑌)) = ((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝑌) +s (𝐴 ·s 𝐶))) -s ((𝑋 ·s 𝑌) +s (𝑋 ·s 𝐶)))) |
71 | 41, 56 | addscld 27393 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ((𝑋 ·s 𝐵) +s (𝐴 ·s 𝑌)) ∈ No
) |
72 | 71, 58, 66 | addsubsd 27478 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((((𝑋 ·s 𝐵) +s (𝐴 ·s 𝑌)) +s (𝐴 ·s 𝐶)) -s (𝑋 ·s 𝑌)) = ((((𝑋 ·s 𝐵) +s (𝐴 ·s 𝑌)) -s (𝑋 ·s 𝑌)) +s (𝐴 ·s 𝐶))) |
73 | 63, 70, 72 | 3eqtr3d 2780 |
. 2
⊢ ((𝜑 ∧ 𝜓) → ((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝑌) +s (𝐴 ·s 𝐶))) -s ((𝑋 ·s 𝑌) +s (𝑋 ·s 𝐶))) = ((((𝑋 ·s 𝐵) +s (𝐴 ·s 𝑌)) -s (𝑋 ·s 𝑌)) +s (𝐴 ·s 𝐶))) |
74 | 33, 73 | eqtrd 2772 |
1
⊢ ((𝜑 ∧ 𝜓) → (((𝑋 ·s (𝐵 +s 𝐶)) +s (𝐴 ·s (𝑌 +s 𝐶))) -s (𝑋 ·s (𝑌 +s 𝐶))) = ((((𝑋 ·s 𝐵) +s (𝐴 ·s 𝑌)) -s (𝑋 ·s 𝑌)) +s (𝐴 ·s 𝐶))) |