Step | Hyp | Ref
| Expression |
1 | | oveq1 7401 |
. . 3
⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s (𝑦 +s 𝑧)) = (𝑥𝑂 ·s
(𝑦 +s 𝑧))) |
2 | | oveq1 7401 |
. . . 4
⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s 𝑦) = (𝑥𝑂 ·s
𝑦)) |
3 | | oveq1 7401 |
. . . 4
⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s 𝑧) = (𝑥𝑂 ·s
𝑧)) |
4 | 2, 3 | oveq12d 7412 |
. . 3
⊢ (𝑥 = 𝑥𝑂 → ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))) |
5 | 1, 4 | eqeq12d 2748 |
. 2
⊢ (𝑥 = 𝑥𝑂 → ((𝑥 ·s (𝑦 +s 𝑧)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧)) ↔ (𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧)))) |
6 | | oveq1 7401 |
. . . 4
⊢ (𝑦 = 𝑦𝑂 → (𝑦 +s 𝑧) = (𝑦𝑂 +s 𝑧)) |
7 | 6 | oveq2d 7410 |
. . 3
⊢ (𝑦 = 𝑦𝑂 → (𝑥𝑂
·s (𝑦
+s 𝑧)) = (𝑥𝑂
·s (𝑦𝑂 +s 𝑧))) |
8 | | oveq2 7402 |
. . . 4
⊢ (𝑦 = 𝑦𝑂 → (𝑥𝑂
·s 𝑦) =
(𝑥𝑂
·s 𝑦𝑂)) |
9 | 8 | oveq1d 7409 |
. . 3
⊢ (𝑦 = 𝑦𝑂 → ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧))) |
10 | 7, 9 | eqeq12d 2748 |
. 2
⊢ (𝑦 = 𝑦𝑂 → ((𝑥𝑂
·s (𝑦
+s 𝑧)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧)) ↔ (𝑥𝑂
·s (𝑦𝑂 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧)))) |
11 | | oveq2 7402 |
. . . 4
⊢ (𝑧 = 𝑧𝑂 → (𝑦𝑂
+s 𝑧) = (𝑦𝑂
+s 𝑧𝑂)) |
12 | 11 | oveq2d 7410 |
. . 3
⊢ (𝑧 = 𝑧𝑂 → (𝑥𝑂
·s (𝑦𝑂 +s 𝑧)) = (𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂))) |
13 | | oveq2 7402 |
. . . 4
⊢ (𝑧 = 𝑧𝑂 → (𝑥𝑂
·s 𝑧) =
(𝑥𝑂
·s 𝑧𝑂)) |
14 | 13 | oveq2d 7410 |
. . 3
⊢ (𝑧 = 𝑧𝑂 → ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧)) =
((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧𝑂))) |
15 | 12, 14 | eqeq12d 2748 |
. 2
⊢ (𝑧 = 𝑧𝑂 → ((𝑥𝑂
·s (𝑦𝑂 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧)) ↔ (𝑥𝑂
·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧𝑂)))) |
16 | | oveq1 7401 |
. . 3
⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s (𝑦𝑂
+s 𝑧𝑂)) = (𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂))) |
17 | | oveq1 7401 |
. . . 4
⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s 𝑦𝑂) = (𝑥𝑂
·s 𝑦𝑂)) |
18 | | oveq1 7401 |
. . . 4
⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s 𝑧𝑂) = (𝑥𝑂
·s 𝑧𝑂)) |
19 | 17, 18 | oveq12d 7412 |
. . 3
⊢ (𝑥 = 𝑥𝑂 → ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))) |
20 | 16, 19 | eqeq12d 2748 |
. 2
⊢ (𝑥 = 𝑥𝑂 → ((𝑥 ·s (𝑦𝑂
+s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂) +s (𝑥 ·s 𝑧𝑂)) ↔
(𝑥𝑂
·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧𝑂)))) |
21 | | oveq1 7401 |
. . . 4
⊢ (𝑦 = 𝑦𝑂 → (𝑦 +s 𝑧𝑂) = (𝑦𝑂
+s 𝑧𝑂)) |
22 | 21 | oveq2d 7410 |
. . 3
⊢ (𝑦 = 𝑦𝑂 → (𝑥 ·s (𝑦 +s 𝑧𝑂)) = (𝑥 ·s (𝑦𝑂
+s 𝑧𝑂))) |
23 | | oveq2 7402 |
. . . 4
⊢ (𝑦 = 𝑦𝑂 → (𝑥 ·s 𝑦) = (𝑥 ·s 𝑦𝑂)) |
24 | 23 | oveq1d 7409 |
. . 3
⊢ (𝑦 = 𝑦𝑂 → ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂))) |
25 | 22, 24 | eqeq12d 2748 |
. 2
⊢ (𝑦 = 𝑦𝑂 → ((𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)) ↔
(𝑥 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂) +s (𝑥 ·s 𝑧𝑂)))) |
26 | 21 | oveq2d 7410 |
. . 3
⊢ (𝑦 = 𝑦𝑂 → (𝑥𝑂
·s (𝑦
+s 𝑧𝑂)) = (𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂))) |
27 | 8 | oveq1d 7409 |
. . 3
⊢ (𝑦 = 𝑦𝑂 → ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)) =
((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧𝑂))) |
28 | 26, 27 | eqeq12d 2748 |
. 2
⊢ (𝑦 = 𝑦𝑂 → ((𝑥𝑂
·s (𝑦
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧𝑂)) ↔ (𝑥𝑂
·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧𝑂)))) |
29 | 11 | oveq2d 7410 |
. . 3
⊢ (𝑧 = 𝑧𝑂 → (𝑥 ·s (𝑦𝑂
+s 𝑧)) = (𝑥 ·s (𝑦𝑂
+s 𝑧𝑂))) |
30 | | oveq2 7402 |
. . . 4
⊢ (𝑧 = 𝑧𝑂 → (𝑥 ·s 𝑧) = (𝑥 ·s 𝑧𝑂)) |
31 | 30 | oveq2d 7410 |
. . 3
⊢ (𝑧 = 𝑧𝑂 → ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)) =
((𝑥 ·s
𝑦𝑂)
+s (𝑥
·s 𝑧𝑂))) |
32 | 29, 31 | eqeq12d 2748 |
. 2
⊢ (𝑧 = 𝑧𝑂 → ((𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧))
↔ (𝑥
·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)))) |
33 | | oveq1 7401 |
. . 3
⊢ (𝑥 = 𝐴 → (𝑥 ·s (𝑦 +s 𝑧)) = (𝐴 ·s (𝑦 +s 𝑧))) |
34 | | oveq1 7401 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝑥 ·s 𝑦) = (𝐴 ·s 𝑦)) |
35 | | oveq1 7401 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝑥 ·s 𝑧) = (𝐴 ·s 𝑧)) |
36 | 34, 35 | oveq12d 7412 |
. . 3
⊢ (𝑥 = 𝐴 → ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧)) = ((𝐴 ·s 𝑦) +s (𝐴 ·s 𝑧))) |
37 | 33, 36 | eqeq12d 2748 |
. 2
⊢ (𝑥 = 𝐴 → ((𝑥 ·s (𝑦 +s 𝑧)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧)) ↔ (𝐴 ·s (𝑦 +s 𝑧)) = ((𝐴 ·s 𝑦) +s (𝐴 ·s 𝑧)))) |
38 | | oveq1 7401 |
. . . 4
⊢ (𝑦 = 𝐵 → (𝑦 +s 𝑧) = (𝐵 +s 𝑧)) |
39 | 38 | oveq2d 7410 |
. . 3
⊢ (𝑦 = 𝐵 → (𝐴 ·s (𝑦 +s 𝑧)) = (𝐴 ·s (𝐵 +s 𝑧))) |
40 | | oveq2 7402 |
. . . 4
⊢ (𝑦 = 𝐵 → (𝐴 ·s 𝑦) = (𝐴 ·s 𝐵)) |
41 | 40 | oveq1d 7409 |
. . 3
⊢ (𝑦 = 𝐵 → ((𝐴 ·s 𝑦) +s (𝐴 ·s 𝑧)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑧))) |
42 | 39, 41 | eqeq12d 2748 |
. 2
⊢ (𝑦 = 𝐵 → ((𝐴 ·s (𝑦 +s 𝑧)) = ((𝐴 ·s 𝑦) +s (𝐴 ·s 𝑧)) ↔ (𝐴 ·s (𝐵 +s 𝑧)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑧)))) |
43 | | oveq2 7402 |
. . . 4
⊢ (𝑧 = 𝐶 → (𝐵 +s 𝑧) = (𝐵 +s 𝐶)) |
44 | 43 | oveq2d 7410 |
. . 3
⊢ (𝑧 = 𝐶 → (𝐴 ·s (𝐵 +s 𝑧)) = (𝐴 ·s (𝐵 +s 𝐶))) |
45 | | oveq2 7402 |
. . . 4
⊢ (𝑧 = 𝐶 → (𝐴 ·s 𝑧) = (𝐴 ·s 𝐶)) |
46 | 45 | oveq2d 7410 |
. . 3
⊢ (𝑧 = 𝐶 → ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑧)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝐶))) |
47 | 44, 46 | eqeq12d 2748 |
. 2
⊢ (𝑧 = 𝐶 → ((𝐴 ·s (𝐵 +s 𝑧)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑧)) ↔ (𝐴 ·s (𝐵 +s 𝐶)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝐶)))) |
48 | | simpl1 1191 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → 𝑥 ∈
No ) |
49 | | simpl2 1192 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → 𝑦 ∈
No ) |
50 | | simpl3 1193 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → 𝑧 ∈
No ) |
51 | | simpr21 1260 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s (𝑦
+s 𝑧)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧))) |
52 | | simpr23 1262 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧))) |
53 | | simpr12 1258 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥𝑂
·s (𝑦𝑂 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧))) |
54 | | elun1 4173 |
. . . . . . . . . . . . 13
⊢ (𝑥𝐿 ∈ ( L
‘𝑥) → 𝑥𝐿 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) |
55 | 54 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑦𝐿 ∈ ( L
‘𝑦)) → 𝑥𝐿 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) |
56 | | elun1 4173 |
. . . . . . . . . . . . 13
⊢ (𝑦𝐿 ∈ ( L
‘𝑦) → 𝑦𝐿 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))) |
57 | 56 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑦𝐿 ∈ ( L
‘𝑦)) → 𝑦𝐿 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))) |
58 | 48, 49, 50, 51, 52, 53, 55, 57 | addsdilem3 27537 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑦𝐿 ∈ ( L
‘𝑦))) → (((𝑥𝐿
·s (𝑦
+s 𝑧))
+s (𝑥
·s (𝑦𝐿 +s 𝑧))) -s (𝑥𝐿
·s (𝑦𝐿 +s 𝑧))) = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))) |
59 | 58 | eqeq2d 2743 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑦𝐿 ∈ ( L
‘𝑦))) → (𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝐿
+s 𝑧))) ↔
𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧)))) |
60 | 59 | 2rexbidva 3217 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝐿
+s 𝑧))) ↔
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧)))) |
61 | 60 | abbidv 2801 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝐿
+s 𝑧)))} =
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}) |
62 | | simpr3 1196 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → ∀𝑧𝑂 ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂))) |
63 | | simpr13 1259 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑧𝑂 ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))(𝑥𝑂
·s (𝑦
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧𝑂))) |
64 | 54 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑧𝐿 ∈ ( L
‘𝑧)) → 𝑥𝐿 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) |
65 | | elun1 4173 |
. . . . . . . . . . . . 13
⊢ (𝑧𝐿 ∈ ( L
‘𝑧) → 𝑧𝐿 ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))) |
66 | 65 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑧𝐿 ∈ ( L
‘𝑧)) → 𝑧𝐿 ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))) |
67 | 48, 49, 50, 51, 62, 63, 64, 66 | addsdilem4 27538 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑧𝐿 ∈ ( L
‘𝑧))) → (((𝑥𝐿
·s (𝑦
+s 𝑧))
+s (𝑥
·s (𝑦
+s 𝑧𝐿))) -s (𝑥𝐿
·s (𝑦
+s 𝑧𝐿))) = ((𝑥 ·s 𝑦) +s (((𝑥𝐿
·s 𝑧)
+s (𝑥
·s 𝑧𝐿)) -s (𝑥𝐿
·s 𝑧𝐿)))) |
68 | 67 | eqeq2d 2743 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑧𝐿 ∈ ( L
‘𝑧))) → (𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝐿))) ↔
𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝐿 ·s
𝑧𝐿))))) |
69 | 68 | 2rexbidva 3217 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝐿))) ↔
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝐿 ·s
𝑧𝐿))))) |
70 | 69 | abbidv 2801 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝐿)))} =
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝐿 ·s
𝑧𝐿)))}) |
71 | 61, 70 | uneq12d 4161 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝐿
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝐿)))}) =
({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝐿 ·s
𝑧𝐿)))})) |
72 | | elun2 4174 |
. . . . . . . . . . . . 13
⊢ (𝑥𝑅 ∈ ( R
‘𝑥) → 𝑥𝑅 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) |
73 | 72 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑦𝑅 ∈ ( R
‘𝑦)) → 𝑥𝑅 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) |
74 | | elun2 4174 |
. . . . . . . . . . . . 13
⊢ (𝑦𝑅 ∈ ( R
‘𝑦) → 𝑦𝑅 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))) |
75 | 74 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑦𝑅 ∈ ( R
‘𝑦)) → 𝑦𝑅 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))) |
76 | 48, 49, 50, 51, 52, 53, 73, 75 | addsdilem3 27537 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑦𝑅 ∈ ( R
‘𝑦))) → (((𝑥𝑅
·s (𝑦
+s 𝑧))
+s (𝑥
·s (𝑦𝑅 +s 𝑧))) -s (𝑥𝑅
·s (𝑦𝑅 +s 𝑧))) = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))) |
77 | 76 | eqeq2d 2743 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑦𝑅 ∈ ( R
‘𝑦))) → (𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝑅
+s 𝑧))) ↔
𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧)))) |
78 | 77 | 2rexbidva 3217 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝑅
+s 𝑧))) ↔
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧)))) |
79 | 78 | abbidv 2801 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝑅
+s 𝑧)))} =
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}) |
80 | 72 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑧𝑅 ∈ ( R
‘𝑧)) → 𝑥𝑅 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) |
81 | | elun2 4174 |
. . . . . . . . . . . . 13
⊢ (𝑧𝑅 ∈ ( R
‘𝑧) → 𝑧𝑅 ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))) |
82 | 81 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑧𝑅 ∈ ( R
‘𝑧)) → 𝑧𝑅 ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))) |
83 | 48, 49, 50, 51, 62, 63, 80, 82 | addsdilem4 27538 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑧𝑅 ∈ ( R
‘𝑧))) → (((𝑥𝑅
·s (𝑦
+s 𝑧))
+s (𝑥
·s (𝑦
+s 𝑧𝑅))) -s (𝑥𝑅
·s (𝑦
+s 𝑧𝑅))) = ((𝑥 ·s 𝑦) +s (((𝑥𝑅
·s 𝑧)
+s (𝑥
·s 𝑧𝑅)) -s (𝑥𝑅
·s 𝑧𝑅)))) |
84 | 83 | eqeq2d 2743 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑧𝑅 ∈ ( R
‘𝑧))) → (𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝑅))) ↔
𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝑅 ·s
𝑧𝑅))))) |
85 | 84 | 2rexbidva 3217 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝑅))) ↔
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝑅 ·s
𝑧𝑅))))) |
86 | 85 | abbidv 2801 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝑅)))} =
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝑅 ·s
𝑧𝑅)))}) |
87 | 79, 86 | uneq12d 4161 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝑅
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝑅)))}) =
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝑅 ·s
𝑧𝑅)))})) |
88 | 71, 87 | uneq12d 4161 |
. . . . . 6
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝐿
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝐿)))}) ∪
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝑅
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝑅)))})) =
(({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝐿 ·s
𝑧𝐿)))})
∪ ({𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝑅 ·s
𝑧𝑅)))}))) |
89 | | un4 4166 |
. . . . . 6
⊢ (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝐿 ·s
𝑧𝐿)))})
∪ ({𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝑅 ·s
𝑧𝑅)))}))
= (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝐿 ·s
𝑧𝐿)))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝑅 ·s
𝑧𝑅)))})) |
90 | 88, 89 | eqtrdi 2788 |
. . . . 5
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝐿
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝐿)))}) ∪
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝑅
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝑅)))})) =
(({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝐿 ·s
𝑧𝐿)))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝑅 ·s
𝑧𝑅)))}))) |
91 | 54 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑦𝑅 ∈ ( R
‘𝑦)) → 𝑥𝐿 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) |
92 | 74 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑦𝑅 ∈ ( R
‘𝑦)) → 𝑦𝑅 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))) |
93 | 48, 49, 50, 51, 52, 53, 91, 92 | addsdilem3 27537 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑦𝑅 ∈ ( R
‘𝑦))) → (((𝑥𝐿
·s (𝑦
+s 𝑧))
+s (𝑥
·s (𝑦𝑅 +s 𝑧))) -s (𝑥𝐿
·s (𝑦𝑅 +s 𝑧))) = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))) |
94 | 93 | eqeq2d 2743 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑦𝑅 ∈ ( R
‘𝑦))) → (𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝑅
+s 𝑧))) ↔
𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧)))) |
95 | 94 | 2rexbidva 3217 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝑅
+s 𝑧))) ↔
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧)))) |
96 | 95 | abbidv 2801 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝑅
+s 𝑧)))} =
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}) |
97 | 54 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑧𝑅 ∈ ( R
‘𝑧)) → 𝑥𝐿 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) |
98 | 81 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑧𝑅 ∈ ( R
‘𝑧)) → 𝑧𝑅 ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))) |
99 | 48, 49, 50, 51, 62, 63, 97, 98 | addsdilem4 27538 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑧𝑅 ∈ ( R
‘𝑧))) → (((𝑥𝐿
·s (𝑦
+s 𝑧))
+s (𝑥
·s (𝑦
+s 𝑧𝑅))) -s (𝑥𝐿
·s (𝑦
+s 𝑧𝑅))) = ((𝑥 ·s 𝑦) +s (((𝑥𝐿
·s 𝑧)
+s (𝑥
·s 𝑧𝑅)) -s (𝑥𝐿
·s 𝑧𝑅)))) |
100 | 99 | eqeq2d 2743 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑧𝑅 ∈ ( R
‘𝑧))) → (𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝑅))) ↔
𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝐿 ·s
𝑧𝑅))))) |
101 | 100 | 2rexbidva 3217 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝑅))) ↔
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝐿 ·s
𝑧𝑅))))) |
102 | 101 | abbidv 2801 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝑅)))} =
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝐿 ·s
𝑧𝑅)))}) |
103 | 96, 102 | uneq12d 4161 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝑅
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝑅)))}) =
({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝐿 ·s
𝑧𝑅)))})) |
104 | 72 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑦𝐿 ∈ ( L
‘𝑦)) → 𝑥𝑅 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) |
105 | 56 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑦𝐿 ∈ ( L
‘𝑦)) → 𝑦𝐿 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))) |
106 | 48, 49, 50, 51, 52, 53, 104, 105 | addsdilem3 27537 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑦𝐿 ∈ ( L
‘𝑦))) → (((𝑥𝑅
·s (𝑦
+s 𝑧))
+s (𝑥
·s (𝑦𝐿 +s 𝑧))) -s (𝑥𝑅
·s (𝑦𝐿 +s 𝑧))) = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))) |
107 | 106 | eqeq2d 2743 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑦𝐿 ∈ ( L
‘𝑦))) → (𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝐿
+s 𝑧))) ↔
𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧)))) |
108 | 107 | 2rexbidva 3217 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝐿
+s 𝑧))) ↔
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧)))) |
109 | 108 | abbidv 2801 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝐿
+s 𝑧)))} =
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}) |
110 | 72 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑧𝐿 ∈ ( L
‘𝑧)) → 𝑥𝑅 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) |
111 | 65 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑧𝐿 ∈ ( L
‘𝑧)) → 𝑧𝐿 ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))) |
112 | 48, 49, 50, 51, 62, 63, 110, 111 | addsdilem4 27538 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑧𝐿 ∈ ( L
‘𝑧))) → (((𝑥𝑅
·s (𝑦
+s 𝑧))
+s (𝑥
·s (𝑦
+s 𝑧𝐿))) -s (𝑥𝑅
·s (𝑦
+s 𝑧𝐿))) = ((𝑥 ·s 𝑦) +s (((𝑥𝑅
·s 𝑧)
+s (𝑥
·s 𝑧𝐿)) -s (𝑥𝑅
·s 𝑧𝐿)))) |
113 | 112 | eqeq2d 2743 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑧𝐿 ∈ ( L
‘𝑧))) → (𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝐿))) ↔
𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝑅 ·s
𝑧𝐿))))) |
114 | 113 | 2rexbidva 3217 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝐿))) ↔
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝑅 ·s
𝑧𝐿))))) |
115 | 114 | abbidv 2801 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝐿)))} =
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝑅 ·s
𝑧𝐿)))}) |
116 | 109, 115 | uneq12d 4161 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝐿
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝐿)))}) =
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝑅 ·s
𝑧𝐿)))})) |
117 | 103, 116 | uneq12d 4161 |
. . . . . 6
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝑅
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝑅)))}) ∪
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝐿
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝐿)))})) =
(({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝐿 ·s
𝑧𝑅)))})
∪ ({𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝑅 ·s
𝑧𝐿)))}))) |
118 | | un4 4166 |
. . . . . 6
⊢ (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝐿 ·s
𝑧𝑅)))})
∪ ({𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝑅 ·s
𝑧𝐿)))}))
= (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝐿 ·s
𝑧𝑅)))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝑅 ·s
𝑧𝐿)))})) |
119 | 117, 118 | eqtrdi 2788 |
. . . . 5
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝑅
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝑅)))}) ∪
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝐿
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝐿)))})) =
(({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝐿 ·s
𝑧𝑅)))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝑅 ·s
𝑧𝐿)))}))) |
120 | 90, 119 | oveq12d 7412 |
. . . 4
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → ((({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝐿
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝐿)))}) ∪
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝑅
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝑅)))})) |s
(({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝑅
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝑅)))}) ∪
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝐿
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝐿)))}))) =
((({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝐿 ·s
𝑧𝐿)))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝑅 ·s
𝑧𝑅)))}))
|s (({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝐿 ·s
𝑧𝑅)))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝑅 ·s
𝑧𝐿)))})))) |
121 | 48, 49, 50 | addsdilem1 27535 |
. . . 4
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (𝑥 ·s (𝑦 +s 𝑧)) = ((({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝐿
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝐿)))}) ∪
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝑅
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝑅)))})) |s
(({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝑅
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝑅)))}) ∪
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝐿
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝐿)))})))) |
122 | 48, 49, 50 | addsdilem2 27536 |
. . . 4
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧)) = ((({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝐿 ·s
𝑧𝐿)))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝑅 ·s
𝑧𝑅)))}))
|s (({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝐿 ·s
𝑧𝑅)))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝑅 ·s
𝑧𝐿)))})))) |
123 | 120, 121,
122 | 3eqtr4d 2782 |
. . 3
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (𝑥 ·s (𝑦 +s 𝑧)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧))) |
124 | 123 | ex 413 |
. 2
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
→ (((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂))) → (𝑥 ·s (𝑦 +s 𝑧)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧)))) |
125 | 5, 10, 15, 20, 25, 28, 32, 37, 42, 47, 124 | no3inds 27371 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐶 ∈ No )
→ (𝐴
·s (𝐵
+s 𝐶)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝐶))) |