Proof of Theorem addsdilem4
| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . . . 6
⊢ (𝑥𝑂 = 𝑋 → (𝑥𝑂 ·s
(𝐵 +s 𝐶)) = (𝑋 ·s (𝐵 +s 𝐶))) |
| 2 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥𝑂 = 𝑋 → (𝑥𝑂 ·s
𝐵) = (𝑋 ·s 𝐵)) |
| 3 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥𝑂 = 𝑋 → (𝑥𝑂 ·s
𝐶) = (𝑋 ·s 𝐶)) |
| 4 | 2, 3 | oveq12d 7449 |
. . . . . 6
⊢ (𝑥𝑂 = 𝑋 → ((𝑥𝑂 ·s
𝐵) +s (𝑥𝑂
·s 𝐶)) =
((𝑋 ·s
𝐵) +s (𝑋 ·s 𝐶))) |
| 5 | 1, 4 | eqeq12d 2753 |
. . . . 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 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))(𝑥𝑂 ·s
(𝐵 +s 𝐶)) = ((𝑥𝑂 ·s
𝐵) +s (𝑥𝑂
·s 𝐶))) |
| 8 | | addsdilem4.7 |
. . . . . 6
⊢ (𝜓 → 𝑋 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))) |
| 9 | 8 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))) |
| 10 | 5, 7, 9 | rspcdva 3623 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝑋 ·s (𝐵 +s 𝐶)) = ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶))) |
| 11 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑧𝑂 = 𝑍 → (𝐵 +s 𝑧𝑂) = (𝐵 +s 𝑍)) |
| 12 | 11 | oveq2d 7447 |
. . . . . 6
⊢ (𝑧𝑂 = 𝑍 → (𝐴 ·s (𝐵 +s 𝑧𝑂)) = (𝐴 ·s (𝐵 +s 𝑍))) |
| 13 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑧𝑂 = 𝑍 → (𝐴 ·s 𝑧𝑂) = (𝐴 ·s 𝑍)) |
| 14 | 13 | oveq2d 7447 |
. . . . . 6
⊢ (𝑧𝑂 = 𝑍 → ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑧𝑂)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍))) |
| 15 | 12, 14 | eqeq12d 2753 |
. . . . 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 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))(𝐴 ·s (𝐵 +s 𝑧𝑂)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑧𝑂))) |
| 18 | | addsdilem4.8 |
. . . . . 6
⊢ (𝜓 → 𝑍 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))) |
| 19 | 18 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝑍 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))) |
| 20 | 15, 17, 19 | rspcdva 3623 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝐴 ·s (𝐵 +s 𝑍)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍))) |
| 21 | 10, 20 | oveq12d 7449 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((𝑋 ·s (𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑍))) = (((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍)))) |
| 22 | | oveq1 7438 |
. . . . 5
⊢ (𝑥𝑂 = 𝑋 → (𝑥𝑂 ·s
(𝐵 +s 𝑧𝑂)) = (𝑋 ·s (𝐵 +s 𝑧𝑂))) |
| 23 | | oveq1 7438 |
. . . . . 6
⊢ (𝑥𝑂 = 𝑋 → (𝑥𝑂 ·s
𝑧𝑂) =
(𝑋 ·s
𝑧𝑂)) |
| 24 | 2, 23 | oveq12d 7449 |
. . . . 5
⊢ (𝑥𝑂 = 𝑋 → ((𝑥𝑂 ·s
𝐵) +s (𝑥𝑂
·s 𝑧𝑂)) = ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝑧𝑂))) |
| 25 | 22, 24 | eqeq12d 2753 |
. . . 4
⊢ (𝑥𝑂 = 𝑋 → ((𝑥𝑂 ·s
(𝐵 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝐵)
+s (𝑥𝑂 ·s
𝑧𝑂))
↔ (𝑋
·s (𝐵
+s 𝑧𝑂)) = ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝑧𝑂)))) |
| 26 | 11 | oveq2d 7447 |
. . . . 5
⊢ (𝑧𝑂 = 𝑍 → (𝑋 ·s (𝐵 +s 𝑧𝑂)) = (𝑋 ·s (𝐵 +s 𝑍))) |
| 27 | | oveq2 7439 |
. . . . . 6
⊢ (𝑧𝑂 = 𝑍 → (𝑋 ·s 𝑧𝑂) = (𝑋 ·s 𝑍)) |
| 28 | 27 | oveq2d 7447 |
. . . . 5
⊢ (𝑧𝑂 = 𝑍 → ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝑧𝑂)) = ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝑍))) |
| 29 | 26, 28 | eqeq12d 2753 |
. . . 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 480 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))(𝑥𝑂 ·s
(𝐵 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝐵)
+s (𝑥𝑂 ·s
𝑧𝑂))) |
| 32 | 25, 29, 31, 9, 19 | rspc2dv 3637 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (𝑋 ·s (𝐵 +s 𝑍)) = ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝑍))) |
| 33 | 21, 32 | oveq12d 7449 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (((𝑋 ·s (𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑍))) -s (𝑋 ·s (𝐵 +s 𝑍))) = ((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍))) -s ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝑍)))) |
| 34 | | leftssno 27919 |
. . . . . . . . 9
⊢ ( L
‘𝐴) ⊆ No |
| 35 | | rightssno 27920 |
. . . . . . . . 9
⊢ ( R
‘𝐴) ⊆ No |
| 36 | 34, 35 | unssi 4191 |
. . . . . . . 8
⊢ (( L
‘𝐴) ∪ ( R
‘𝐴)) ⊆ No |
| 37 | 36, 8 | sselid 3981 |
. . . . . . 7
⊢ (𝜓 → 𝑋 ∈ No
) |
| 38 | 37 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ No
) |
| 39 | | addsdilem4.2 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ No
) |
| 40 | 39 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝐵 ∈ No
) |
| 41 | 38, 40 | mulscld 28161 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (𝑋 ·s 𝐵) ∈ No
) |
| 42 | | addsdilem4.3 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ No
) |
| 43 | 42 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ No
) |
| 44 | 38, 43 | mulscld 28161 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (𝑋 ·s 𝐶) ∈ No
) |
| 45 | 41, 44 | addscld 28013 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) ∈ No
) |
| 46 | | addsdilem4.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ No
) |
| 47 | 46, 39 | mulscld 28161 |
. . . . . 6
⊢ (𝜑 → (𝐴 ·s 𝐵) ∈ No
) |
| 48 | 47 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (𝐴 ·s 𝐵) ∈ No
) |
| 49 | 46 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ No
) |
| 50 | | leftssno 27919 |
. . . . . . . . 9
⊢ ( L
‘𝐶) ⊆ No |
| 51 | | rightssno 27920 |
. . . . . . . . 9
⊢ ( R
‘𝐶) ⊆ No |
| 52 | 50, 51 | unssi 4191 |
. . . . . . . 8
⊢ (( L
‘𝐶) ∪ ( R
‘𝐶)) ⊆ No |
| 53 | 52, 18 | sselid 3981 |
. . . . . . 7
⊢ (𝜓 → 𝑍 ∈ No
) |
| 54 | 53 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝑍 ∈ No
) |
| 55 | 49, 54 | mulscld 28161 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (𝐴 ·s 𝑍) ∈ No
) |
| 56 | 48, 55 | addscld 28013 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍)) ∈ No
) |
| 57 | 45, 56 | addscld 28013 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍))) ∈ No
) |
| 58 | 38, 54 | mulscld 28161 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (𝑋 ·s 𝑍) ∈ No
) |
| 59 | 57, 41, 58 | subsubs4d 28124 |
. 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 28112 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍))) -s (𝑋 ·s 𝐵)) = ((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) -s (𝑋 ·s 𝐵)) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍)))) |
| 61 | 41, 44 | addscomd 28000 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) = ((𝑋 ·s 𝐶) +s (𝑋 ·s 𝐵))) |
| 62 | 61 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) -s (𝑋 ·s 𝐵)) = (((𝑋 ·s 𝐶) +s (𝑋 ·s 𝐵)) -s (𝑋 ·s 𝐵))) |
| 63 | | pncans 28102 |
. . . . . . . 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 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → (((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) -s (𝑋 ·s 𝐵)) = (𝑋 ·s 𝐶)) |
| 66 | 65 | oveq1d 7446 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) -s (𝑋 ·s 𝐵)) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍))) = ((𝑋 ·s 𝐶) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍)))) |
| 67 | 44, 48, 55 | adds12d 28041 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ((𝑋 ·s 𝐶) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍))) = ((𝐴 ·s 𝐵) +s ((𝑋 ·s 𝐶) +s (𝐴 ·s 𝑍)))) |
| 68 | 60, 66, 67 | 3eqtrd 2781 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍))) -s (𝑋 ·s 𝐵)) = ((𝐴 ·s 𝐵) +s ((𝑋 ·s 𝐶) +s (𝐴 ·s 𝑍)))) |
| 69 | 68 | oveq1d 7446 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍))) -s (𝑋 ·s 𝐵)) -s (𝑋 ·s 𝑍)) = (((𝐴 ·s 𝐵) +s ((𝑋 ·s 𝐶) +s (𝐴 ·s 𝑍))) -s (𝑋 ·s 𝑍))) |
| 70 | 44, 55 | addscld 28013 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ((𝑋 ·s 𝐶) +s (𝐴 ·s 𝑍)) ∈ No
) |
| 71 | 48, 70, 58 | addsubsassd 28111 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (((𝐴 ·s 𝐵) +s ((𝑋 ·s 𝐶) +s (𝐴 ·s 𝑍))) -s (𝑋 ·s 𝑍)) = ((𝐴 ·s 𝐵) +s (((𝑋 ·s 𝐶) +s (𝐴 ·s 𝑍)) -s (𝑋 ·s 𝑍)))) |
| 72 | 69, 71 | eqtrd 2777 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (((((𝑋 ·s 𝐵) +s (𝑋 ·s 𝐶)) +s ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑍))) -s (𝑋 ·s 𝐵)) -s (𝑋 ·s 𝑍)) = ((𝐴 ·s 𝐵) +s (((𝑋 ·s 𝐶) +s (𝐴 ·s 𝑍)) -s (𝑋 ·s 𝑍)))) |
| 73 | 33, 59, 72 | 3eqtr2d 2783 |
1
⊢ ((𝜑 ∧ 𝜓) → (((𝑋 ·s (𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑍))) -s (𝑋 ·s (𝐵 +s 𝑍))) = ((𝐴 ·s 𝐵) +s (((𝑋 ·s 𝐶) +s (𝐴 ·s 𝑍)) -s (𝑋 ·s 𝑍)))) |