Step | Hyp | Ref
| Expression |
1 | | oveq1 7358 |
. . . 4
⊢ (𝑥 = 𝑥O → (𝑥 +s 𝑦) = (𝑥O +s 𝑦)) |
2 | 1 | oveq1d 7366 |
. . 3
⊢ (𝑥 = 𝑥O → ((𝑥 +s 𝑦) +s 𝑧) = ((𝑥O +s 𝑦) +s 𝑧)) |
3 | | oveq1 7358 |
. . 3
⊢ (𝑥 = 𝑥O → (𝑥 +s (𝑦 +s 𝑧)) = (𝑥O +s (𝑦 +s 𝑧))) |
4 | 2, 3 | eqeq12d 2753 |
. 2
⊢ (𝑥 = 𝑥O → (((𝑥 +s 𝑦) +s 𝑧) = (𝑥 +s (𝑦 +s 𝑧)) ↔ ((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)))) |
5 | | oveq2 7359 |
. . . 4
⊢ (𝑦 = 𝑦O → (𝑥O +s 𝑦) = (𝑥O +s 𝑦O)) |
6 | 5 | oveq1d 7366 |
. . 3
⊢ (𝑦 = 𝑦O → ((𝑥O +s 𝑦) +s 𝑧) = ((𝑥O +s 𝑦O) +s 𝑧)) |
7 | | oveq1 7358 |
. . . 4
⊢ (𝑦 = 𝑦O → (𝑦 +s 𝑧) = (𝑦O +s 𝑧)) |
8 | 7 | oveq2d 7367 |
. . 3
⊢ (𝑦 = 𝑦O → (𝑥O +s (𝑦 +s 𝑧)) = (𝑥O +s (𝑦O +s 𝑧))) |
9 | 6, 8 | eqeq12d 2753 |
. 2
⊢ (𝑦 = 𝑦O → (((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ↔ ((𝑥O +s 𝑦O) +s 𝑧) = (𝑥O +s (𝑦O +s 𝑧)))) |
10 | | oveq2 7359 |
. . 3
⊢ (𝑧 = 𝑧O → ((𝑥O +s 𝑦O) +s 𝑧) = ((𝑥O +s 𝑦O) +s 𝑧O)) |
11 | | oveq2 7359 |
. . . 4
⊢ (𝑧 = 𝑧O → (𝑦O +s 𝑧) = (𝑦O +s 𝑧O)) |
12 | 11 | oveq2d 7367 |
. . 3
⊢ (𝑧 = 𝑧O → (𝑥O +s (𝑦O +s 𝑧)) = (𝑥O +s (𝑦O +s 𝑧O))) |
13 | 10, 12 | eqeq12d 2753 |
. 2
⊢ (𝑧 = 𝑧O → (((𝑥O +s 𝑦O) +s 𝑧) = (𝑥O +s (𝑦O +s 𝑧)) ↔ ((𝑥O +s 𝑦O) +s 𝑧O) = (𝑥O +s (𝑦O +s 𝑧O)))) |
14 | | oveq1 7358 |
. . . 4
⊢ (𝑥 = 𝑥O → (𝑥 +s 𝑦O) = (𝑥O +s 𝑦O)) |
15 | 14 | oveq1d 7366 |
. . 3
⊢ (𝑥 = 𝑥O → ((𝑥 +s 𝑦O) +s 𝑧O) = ((𝑥O +s 𝑦O) +s 𝑧O)) |
16 | | oveq1 7358 |
. . 3
⊢ (𝑥 = 𝑥O → (𝑥 +s (𝑦O +s 𝑧O)) = (𝑥O +s (𝑦O +s 𝑧O))) |
17 | 15, 16 | eqeq12d 2753 |
. 2
⊢ (𝑥 = 𝑥O → (((𝑥 +s 𝑦O) +s 𝑧O) = (𝑥 +s (𝑦O +s 𝑧O)) ↔ ((𝑥O +s 𝑦O) +s 𝑧O) = (𝑥O +s (𝑦O +s 𝑧O)))) |
18 | | oveq2 7359 |
. . . 4
⊢ (𝑦 = 𝑦O → (𝑥 +s 𝑦) = (𝑥 +s 𝑦O)) |
19 | 18 | oveq1d 7366 |
. . 3
⊢ (𝑦 = 𝑦O → ((𝑥 +s 𝑦) +s 𝑧O) = ((𝑥 +s 𝑦O) +s 𝑧O)) |
20 | | oveq1 7358 |
. . . 4
⊢ (𝑦 = 𝑦O → (𝑦 +s 𝑧O) = (𝑦O +s 𝑧O)) |
21 | 20 | oveq2d 7367 |
. . 3
⊢ (𝑦 = 𝑦O → (𝑥 +s (𝑦 +s 𝑧O)) = (𝑥 +s (𝑦O +s 𝑧O))) |
22 | 19, 21 | eqeq12d 2753 |
. 2
⊢ (𝑦 = 𝑦O → (((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)) ↔ ((𝑥 +s 𝑦O) +s 𝑧O) = (𝑥 +s (𝑦O +s 𝑧O)))) |
23 | 5 | oveq1d 7366 |
. . 3
⊢ (𝑦 = 𝑦O → ((𝑥O +s 𝑦) +s 𝑧O) = ((𝑥O +s 𝑦O) +s 𝑧O)) |
24 | 20 | oveq2d 7367 |
. . 3
⊢ (𝑦 = 𝑦O → (𝑥O +s (𝑦 +s 𝑧O)) = (𝑥O +s (𝑦O +s 𝑧O))) |
25 | 23, 24 | eqeq12d 2753 |
. 2
⊢ (𝑦 = 𝑦O → (((𝑥O +s 𝑦) +s 𝑧O) = (𝑥O +s (𝑦 +s 𝑧O)) ↔ ((𝑥O +s 𝑦O) +s 𝑧O) = (𝑥O +s (𝑦O +s 𝑧O)))) |
26 | | oveq2 7359 |
. . 3
⊢ (𝑧 = 𝑧O → ((𝑥 +s 𝑦O) +s 𝑧) = ((𝑥 +s 𝑦O) +s 𝑧O)) |
27 | 11 | oveq2d 7367 |
. . 3
⊢ (𝑧 = 𝑧O → (𝑥 +s (𝑦O +s 𝑧)) = (𝑥 +s (𝑦O +s 𝑧O))) |
28 | 26, 27 | eqeq12d 2753 |
. 2
⊢ (𝑧 = 𝑧O → (((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ↔ ((𝑥 +s 𝑦O) +s 𝑧O) = (𝑥 +s (𝑦O +s 𝑧O)))) |
29 | | oveq1 7358 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝑥 +s 𝑦) = (𝐴 +s 𝑦)) |
30 | 29 | oveq1d 7366 |
. . 3
⊢ (𝑥 = 𝐴 → ((𝑥 +s 𝑦) +s 𝑧) = ((𝐴 +s 𝑦) +s 𝑧)) |
31 | | oveq1 7358 |
. . 3
⊢ (𝑥 = 𝐴 → (𝑥 +s (𝑦 +s 𝑧)) = (𝐴 +s (𝑦 +s 𝑧))) |
32 | 30, 31 | eqeq12d 2753 |
. 2
⊢ (𝑥 = 𝐴 → (((𝑥 +s 𝑦) +s 𝑧) = (𝑥 +s (𝑦 +s 𝑧)) ↔ ((𝐴 +s 𝑦) +s 𝑧) = (𝐴 +s (𝑦 +s 𝑧)))) |
33 | | oveq2 7359 |
. . . 4
⊢ (𝑦 = 𝐵 → (𝐴 +s 𝑦) = (𝐴 +s 𝐵)) |
34 | 33 | oveq1d 7366 |
. . 3
⊢ (𝑦 = 𝐵 → ((𝐴 +s 𝑦) +s 𝑧) = ((𝐴 +s 𝐵) +s 𝑧)) |
35 | | oveq1 7358 |
. . . 4
⊢ (𝑦 = 𝐵 → (𝑦 +s 𝑧) = (𝐵 +s 𝑧)) |
36 | 35 | oveq2d 7367 |
. . 3
⊢ (𝑦 = 𝐵 → (𝐴 +s (𝑦 +s 𝑧)) = (𝐴 +s (𝐵 +s 𝑧))) |
37 | 34, 36 | eqeq12d 2753 |
. 2
⊢ (𝑦 = 𝐵 → (((𝐴 +s 𝑦) +s 𝑧) = (𝐴 +s (𝑦 +s 𝑧)) ↔ ((𝐴 +s 𝐵) +s 𝑧) = (𝐴 +s (𝐵 +s 𝑧)))) |
38 | | oveq2 7359 |
. . 3
⊢ (𝑧 = 𝐶 → ((𝐴 +s 𝐵) +s 𝑧) = ((𝐴 +s 𝐵) +s 𝐶)) |
39 | | oveq2 7359 |
. . . 4
⊢ (𝑧 = 𝐶 → (𝐵 +s 𝑧) = (𝐵 +s 𝐶)) |
40 | 39 | oveq2d 7367 |
. . 3
⊢ (𝑧 = 𝐶 → (𝐴 +s (𝐵 +s 𝑧)) = (𝐴 +s (𝐵 +s 𝐶))) |
41 | 38, 40 | eqeq12d 2753 |
. 2
⊢ (𝑧 = 𝐶 → (((𝐴 +s 𝐵) +s 𝑧) = (𝐴 +s (𝐵 +s 𝑧)) ↔ ((𝐴 +s 𝐵) +s 𝐶) = (𝐴 +s (𝐵 +s 𝐶)))) |
42 | | simp21 1206 |
. . . 4
⊢
(((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥O +s 𝑦O) +s 𝑧O) = (𝑥O +s (𝑦O +s 𝑧O)) ∧ ∀𝑥O ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦O ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥O +s 𝑦O) +s 𝑧) = (𝑥O +s (𝑦O +s 𝑧)) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥O +s 𝑦) +s 𝑧O) = (𝑥O +s (𝑦 +s 𝑧O))) ∧ (∀𝑥O ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦O) +s 𝑧O) = (𝑥 +s (𝑦O +s 𝑧O)) ∧ ∀𝑦O ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧))) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O))) → ∀𝑥O ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧))) |
43 | | simp23 1208 |
. . . 4
⊢
(((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥O +s 𝑦O) +s 𝑧O) = (𝑥O +s (𝑦O +s 𝑧O)) ∧ ∀𝑥O ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦O ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥O +s 𝑦O) +s 𝑧) = (𝑥O +s (𝑦O +s 𝑧)) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥O +s 𝑦) +s 𝑧O) = (𝑥O +s (𝑦 +s 𝑧O))) ∧ (∀𝑥O ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦O) +s 𝑧O) = (𝑥 +s (𝑦O +s 𝑧O)) ∧ ∀𝑦O ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧))) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O))) → ∀𝑦O ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧))) |
44 | | simp3 1138 |
. . . 4
⊢
(((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥O +s 𝑦O) +s 𝑧O) = (𝑥O +s (𝑦O +s 𝑧O)) ∧ ∀𝑥O ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦O ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥O +s 𝑦O) +s 𝑧) = (𝑥O +s (𝑦O +s 𝑧)) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥O +s 𝑦) +s 𝑧O) = (𝑥O +s (𝑦 +s 𝑧O))) ∧ (∀𝑥O ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦O) +s 𝑧O) = (𝑥 +s (𝑦O +s 𝑧O)) ∧ ∀𝑦O ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧))) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O))) → ∀𝑧O ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O))) |
45 | 42, 43, 44 | 3jca 1128 |
. . 3
⊢
(((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥O +s 𝑦O) +s 𝑧O) = (𝑥O +s (𝑦O +s 𝑧O)) ∧ ∀𝑥O ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦O ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥O +s 𝑦O) +s 𝑧) = (𝑥O +s (𝑦O +s 𝑧)) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥O +s 𝑦) +s 𝑧O) = (𝑥O +s (𝑦 +s 𝑧O))) ∧ (∀𝑥O ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦O) +s 𝑧O) = (𝑥 +s (𝑦O +s 𝑧O)) ∧ ∀𝑦O ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧))) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O))) → (∀𝑥O ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) |
46 | | oveq1 7358 |
. . . . . . . . . . . . . 14
⊢ (𝑥O = 𝑥L → (𝑥O +s 𝑦) = (𝑥L +s 𝑦)) |
47 | 46 | oveq1d 7366 |
. . . . . . . . . . . . 13
⊢ (𝑥O = 𝑥L → ((𝑥O +s 𝑦) +s 𝑧) = ((𝑥L +s 𝑦) +s 𝑧)) |
48 | | oveq1 7358 |
. . . . . . . . . . . . 13
⊢ (𝑥O = 𝑥L → (𝑥O +s (𝑦 +s 𝑧)) = (𝑥L +s (𝑦 +s 𝑧))) |
49 | 47, 48 | eqeq12d 2753 |
. . . . . . . . . . . 12
⊢ (𝑥O = 𝑥L → (((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ↔ ((𝑥L +s 𝑦) +s 𝑧) = (𝑥L +s (𝑦 +s 𝑧)))) |
50 | | simplr1 1215 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑥L ∈ ( L ‘𝑥)) → ∀𝑥O ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧))) |
51 | | elun1 4134 |
. . . . . . . . . . . . 13
⊢ (𝑥L ∈ ( L
‘𝑥) → 𝑥L ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) |
52 | 51 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑥L ∈ ( L ‘𝑥)) → 𝑥L ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) |
53 | 49, 50, 52 | rspcdva 3580 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑥L ∈ ( L ‘𝑥)) → ((𝑥L +s 𝑦) +s 𝑧) = (𝑥L +s (𝑦 +s 𝑧))) |
54 | 53 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑥L ∈ ( L ‘𝑥)) → (𝑎 = ((𝑥L +s 𝑦) +s 𝑧) ↔ 𝑎 = (𝑥L +s (𝑦 +s 𝑧)))) |
55 | 54 | rexbidva 3171 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → (∃𝑥L ∈ ( L
‘𝑥)𝑎 = ((𝑥L +s 𝑦) +s 𝑧) ↔ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s (𝑦 +s 𝑧)))) |
56 | 55 | abbidv 2806 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → {𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = ((𝑥L +s 𝑦) +s 𝑧)} = {𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s (𝑦 +s 𝑧))}) |
57 | | oveq2 7359 |
. . . . . . . . . . . . . 14
⊢ (𝑦O = 𝑦L → (𝑥 +s 𝑦O) = (𝑥 +s 𝑦L)) |
58 | 57 | oveq1d 7366 |
. . . . . . . . . . . . 13
⊢ (𝑦O = 𝑦L → ((𝑥 +s 𝑦O) +s 𝑧) = ((𝑥 +s 𝑦L) +s 𝑧)) |
59 | | oveq1 7358 |
. . . . . . . . . . . . . 14
⊢ (𝑦O = 𝑦L → (𝑦O +s 𝑧) = (𝑦L +s 𝑧)) |
60 | 59 | oveq2d 7367 |
. . . . . . . . . . . . 13
⊢ (𝑦O = 𝑦L → (𝑥 +s (𝑦O +s 𝑧)) = (𝑥 +s (𝑦L +s 𝑧))) |
61 | 58, 60 | eqeq12d 2753 |
. . . . . . . . . . . 12
⊢ (𝑦O = 𝑦L → (((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ↔ ((𝑥 +s 𝑦L) +s 𝑧) = (𝑥 +s (𝑦L +s 𝑧)))) |
62 | | simplr2 1216 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑦L ∈ ( L ‘𝑦)) → ∀𝑦O ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧))) |
63 | | elun1 4134 |
. . . . . . . . . . . . 13
⊢ (𝑦L ∈ ( L
‘𝑦) → 𝑦L ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))) |
64 | 63 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑦L ∈ ( L ‘𝑦)) → 𝑦L ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))) |
65 | 61, 62, 64 | rspcdva 3580 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑦L ∈ ( L ‘𝑦)) → ((𝑥 +s 𝑦L) +s 𝑧) = (𝑥 +s (𝑦L +s 𝑧))) |
66 | 65 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑦L ∈ ( L ‘𝑦)) → (𝑏 = ((𝑥 +s 𝑦L) +s 𝑧) ↔ 𝑏 = (𝑥 +s (𝑦L +s 𝑧)))) |
67 | 66 | rexbidva 3171 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → (∃𝑦L ∈ ( L
‘𝑦)𝑏 = ((𝑥 +s 𝑦L) +s 𝑧) ↔ ∃𝑦L ∈ ( L ‘𝑦)𝑏 = (𝑥 +s (𝑦L +s 𝑧)))) |
68 | 67 | abbidv 2806 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → {𝑏 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑏 = ((𝑥 +s 𝑦L) +s 𝑧)} = {𝑏 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑏 = (𝑥 +s (𝑦L +s 𝑧))}) |
69 | 56, 68 | uneq12d 4122 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = ((𝑥L +s 𝑦) +s 𝑧)} ∪ {𝑏 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑏 = ((𝑥 +s 𝑦L) +s 𝑧)}) = ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s (𝑦 +s 𝑧))} ∪ {𝑏 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑏 = (𝑥 +s (𝑦L +s 𝑧))})) |
70 | | oveq2 7359 |
. . . . . . . . . . . 12
⊢ (𝑧O = 𝑧L → ((𝑥 +s 𝑦) +s 𝑧O) = ((𝑥 +s 𝑦) +s 𝑧L)) |
71 | | oveq2 7359 |
. . . . . . . . . . . . 13
⊢ (𝑧O = 𝑧L → (𝑦 +s 𝑧O) = (𝑦 +s 𝑧L)) |
72 | 71 | oveq2d 7367 |
. . . . . . . . . . . 12
⊢ (𝑧O = 𝑧L → (𝑥 +s (𝑦 +s 𝑧O)) = (𝑥 +s (𝑦 +s 𝑧L))) |
73 | 70, 72 | eqeq12d 2753 |
. . . . . . . . . . 11
⊢ (𝑧O = 𝑧L → (((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)) ↔ ((𝑥 +s 𝑦) +s 𝑧L) = (𝑥 +s (𝑦 +s 𝑧L)))) |
74 | | simplr3 1217 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑧L ∈ ( L ‘𝑧)) → ∀𝑧O ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O))) |
75 | | elun1 4134 |
. . . . . . . . . . . 12
⊢ (𝑧L ∈ ( L
‘𝑧) → 𝑧L ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))) |
76 | 75 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑧L ∈ ( L ‘𝑧)) → 𝑧L ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))) |
77 | 73, 74, 76 | rspcdva 3580 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑧L ∈ ( L ‘𝑧)) → ((𝑥 +s 𝑦) +s 𝑧L) = (𝑥 +s (𝑦 +s 𝑧L))) |
78 | 77 | eqeq2d 2748 |
. . . . . . . . 9
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑧L ∈ ( L ‘𝑧)) → (𝑐 = ((𝑥 +s 𝑦) +s 𝑧L) ↔ 𝑐 = (𝑥 +s (𝑦 +s 𝑧L)))) |
79 | 78 | rexbidva 3171 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → (∃𝑧L ∈ ( L
‘𝑧)𝑐 = ((𝑥 +s 𝑦) +s 𝑧L) ↔ ∃𝑧L ∈ ( L
‘𝑧)𝑐 = (𝑥 +s (𝑦 +s 𝑧L)))) |
80 | 79 | abbidv 2806 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → {𝑐 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑐 = ((𝑥 +s 𝑦) +s 𝑧L)} = {𝑐 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑐 = (𝑥 +s (𝑦 +s 𝑧L))}) |
81 | 69, 80 | uneq12d 4122 |
. . . . . 6
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → (({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = ((𝑥L +s 𝑦) +s 𝑧)} ∪ {𝑏 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑏 = ((𝑥 +s 𝑦L) +s 𝑧)}) ∪ {𝑐 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑐 = ((𝑥 +s 𝑦) +s 𝑧L)}) = (({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s (𝑦 +s 𝑧))} ∪ {𝑏 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑏 = (𝑥 +s (𝑦L +s 𝑧))}) ∪ {𝑐 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑐 = (𝑥 +s (𝑦 +s 𝑧L))})) |
82 | | oveq1 7358 |
. . . . . . . . . . . . . 14
⊢ (𝑥O = 𝑥R → (𝑥O +s 𝑦) = (𝑥R +s 𝑦)) |
83 | 82 | oveq1d 7366 |
. . . . . . . . . . . . 13
⊢ (𝑥O = 𝑥R → ((𝑥O +s 𝑦) +s 𝑧) = ((𝑥R +s 𝑦) +s 𝑧)) |
84 | | oveq1 7358 |
. . . . . . . . . . . . 13
⊢ (𝑥O = 𝑥R → (𝑥O +s (𝑦 +s 𝑧)) = (𝑥R +s (𝑦 +s 𝑧))) |
85 | 83, 84 | eqeq12d 2753 |
. . . . . . . . . . . 12
⊢ (𝑥O = 𝑥R → (((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ↔ ((𝑥R +s 𝑦) +s 𝑧) = (𝑥R +s (𝑦 +s 𝑧)))) |
86 | | simplr1 1215 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑥R ∈ ( R ‘𝑥)) → ∀𝑥O ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧))) |
87 | | elun2 4135 |
. . . . . . . . . . . . 13
⊢ (𝑥R ∈ ( R
‘𝑥) → 𝑥R ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) |
88 | 87 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑥R ∈ ( R ‘𝑥)) → 𝑥R ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) |
89 | 85, 86, 88 | rspcdva 3580 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑥R ∈ ( R ‘𝑥)) → ((𝑥R +s 𝑦) +s 𝑧) = (𝑥R +s (𝑦 +s 𝑧))) |
90 | 89 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑥R ∈ ( R ‘𝑥)) → (𝑑 = ((𝑥R +s 𝑦) +s 𝑧) ↔ 𝑑 = (𝑥R +s (𝑦 +s 𝑧)))) |
91 | 90 | rexbidva 3171 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → (∃𝑥R ∈ ( R
‘𝑥)𝑑 = ((𝑥R +s 𝑦) +s 𝑧) ↔ ∃𝑥R ∈ ( R ‘𝑥)𝑑 = (𝑥R +s (𝑦 +s 𝑧)))) |
92 | 91 | abbidv 2806 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → {𝑑 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑑 = ((𝑥R +s 𝑦) +s 𝑧)} = {𝑑 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑑 = (𝑥R +s (𝑦 +s 𝑧))}) |
93 | | oveq2 7359 |
. . . . . . . . . . . . . 14
⊢ (𝑦O = 𝑦R → (𝑥 +s 𝑦O) = (𝑥 +s 𝑦R)) |
94 | 93 | oveq1d 7366 |
. . . . . . . . . . . . 13
⊢ (𝑦O = 𝑦R → ((𝑥 +s 𝑦O) +s 𝑧) = ((𝑥 +s 𝑦R) +s 𝑧)) |
95 | | oveq1 7358 |
. . . . . . . . . . . . . 14
⊢ (𝑦O = 𝑦R → (𝑦O +s 𝑧) = (𝑦R +s 𝑧)) |
96 | 95 | oveq2d 7367 |
. . . . . . . . . . . . 13
⊢ (𝑦O = 𝑦R → (𝑥 +s (𝑦O +s 𝑧)) = (𝑥 +s (𝑦R +s 𝑧))) |
97 | 94, 96 | eqeq12d 2753 |
. . . . . . . . . . . 12
⊢ (𝑦O = 𝑦R → (((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ↔ ((𝑥 +s 𝑦R) +s 𝑧) = (𝑥 +s (𝑦R +s 𝑧)))) |
98 | | simplr2 1216 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑦R ∈ ( R ‘𝑦)) → ∀𝑦O ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧))) |
99 | | elun2 4135 |
. . . . . . . . . . . . 13
⊢ (𝑦R ∈ ( R
‘𝑦) → 𝑦R ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))) |
100 | 99 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑦R ∈ ( R ‘𝑦)) → 𝑦R ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))) |
101 | 97, 98, 100 | rspcdva 3580 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑦R ∈ ( R ‘𝑦)) → ((𝑥 +s 𝑦R) +s 𝑧) = (𝑥 +s (𝑦R +s 𝑧))) |
102 | 101 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑦R ∈ ( R ‘𝑦)) → (𝑒 = ((𝑥 +s 𝑦R) +s 𝑧) ↔ 𝑒 = (𝑥 +s (𝑦R +s 𝑧)))) |
103 | 102 | rexbidva 3171 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → (∃𝑦R ∈ ( R
‘𝑦)𝑒 = ((𝑥 +s 𝑦R) +s 𝑧) ↔ ∃𝑦R ∈ ( R ‘𝑦)𝑒 = (𝑥 +s (𝑦R +s 𝑧)))) |
104 | 103 | abbidv 2806 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → {𝑒 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑒 = ((𝑥 +s 𝑦R) +s 𝑧)} = {𝑒 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑒 = (𝑥 +s (𝑦R +s 𝑧))}) |
105 | 92, 104 | uneq12d 4122 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → ({𝑑 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑑 = ((𝑥R +s 𝑦) +s 𝑧)} ∪ {𝑒 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑒 = ((𝑥 +s 𝑦R) +s 𝑧)}) = ({𝑑 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑑 = (𝑥R +s (𝑦 +s 𝑧))} ∪ {𝑒 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑒 = (𝑥 +s (𝑦R +s 𝑧))})) |
106 | | oveq2 7359 |
. . . . . . . . . . . 12
⊢ (𝑧O = 𝑧R → ((𝑥 +s 𝑦) +s 𝑧O) = ((𝑥 +s 𝑦) +s 𝑧R)) |
107 | | oveq2 7359 |
. . . . . . . . . . . . 13
⊢ (𝑧O = 𝑧R → (𝑦 +s 𝑧O) = (𝑦 +s 𝑧R)) |
108 | 107 | oveq2d 7367 |
. . . . . . . . . . . 12
⊢ (𝑧O = 𝑧R → (𝑥 +s (𝑦 +s 𝑧O)) = (𝑥 +s (𝑦 +s 𝑧R))) |
109 | 106, 108 | eqeq12d 2753 |
. . . . . . . . . . 11
⊢ (𝑧O = 𝑧R → (((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)) ↔ ((𝑥 +s 𝑦) +s 𝑧R) = (𝑥 +s (𝑦 +s 𝑧R)))) |
110 | | simplr3 1217 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑧R ∈ ( R ‘𝑧)) → ∀𝑧O ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O))) |
111 | | elun2 4135 |
. . . . . . . . . . . 12
⊢ (𝑧R ∈ ( R
‘𝑧) → 𝑧R ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))) |
112 | 111 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑧R ∈ ( R ‘𝑧)) → 𝑧R ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))) |
113 | 109, 110,
112 | rspcdva 3580 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑧R ∈ ( R ‘𝑧)) → ((𝑥 +s 𝑦) +s 𝑧R) = (𝑥 +s (𝑦 +s 𝑧R))) |
114 | 113 | eqeq2d 2748 |
. . . . . . . . 9
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑧R ∈ ( R ‘𝑧)) → (𝑓 = ((𝑥 +s 𝑦) +s 𝑧R) ↔ 𝑓 = (𝑥 +s (𝑦 +s 𝑧R)))) |
115 | 114 | rexbidva 3171 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → (∃𝑧R ∈ ( R
‘𝑧)𝑓 = ((𝑥 +s 𝑦) +s 𝑧R) ↔ ∃𝑧R ∈ ( R
‘𝑧)𝑓 = (𝑥 +s (𝑦 +s 𝑧R)))) |
116 | 115 | abbidv 2806 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → {𝑓 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑓 = ((𝑥 +s 𝑦) +s 𝑧R)} = {𝑓 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑓 = (𝑥 +s (𝑦 +s 𝑧R))}) |
117 | 105, 116 | uneq12d 4122 |
. . . . . 6
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → (({𝑑 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑑 = ((𝑥R +s 𝑦) +s 𝑧)} ∪ {𝑒 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑒 = ((𝑥 +s 𝑦R) +s 𝑧)}) ∪ {𝑓 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑓 = ((𝑥 +s 𝑦) +s 𝑧R)}) = (({𝑑 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑑 = (𝑥R +s (𝑦 +s 𝑧))} ∪ {𝑒 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑒 = (𝑥 +s (𝑦R +s 𝑧))}) ∪ {𝑓 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑓 = (𝑥 +s (𝑦 +s 𝑧R))})) |
118 | 81, 117 | oveq12d 7369 |
. . . . 5
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → ((({𝑎 ∣ ∃𝑥L ∈ ( L
‘𝑥)𝑎 = ((𝑥L +s 𝑦) +s 𝑧)} ∪ {𝑏 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑏 = ((𝑥 +s 𝑦L) +s 𝑧)}) ∪ {𝑐 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑐 = ((𝑥 +s 𝑦) +s 𝑧L)}) |s (({𝑑 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑑 = ((𝑥R +s 𝑦) +s 𝑧)} ∪ {𝑒 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑒 = ((𝑥 +s 𝑦R) +s 𝑧)}) ∪ {𝑓 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑓 = ((𝑥 +s 𝑦) +s 𝑧R)})) = ((({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s (𝑦 +s 𝑧))} ∪ {𝑏 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑏 = (𝑥 +s (𝑦L +s 𝑧))}) ∪ {𝑐 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑐 = (𝑥 +s (𝑦 +s 𝑧L))}) |s (({𝑑 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑑 = (𝑥R +s (𝑦 +s 𝑧))} ∪ {𝑒 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑒 = (𝑥 +s (𝑦R +s 𝑧))}) ∪ {𝑓 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑓 = (𝑥 +s (𝑦 +s 𝑧R))}))) |
119 | | simpl1 1191 |
. . . . . 6
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → 𝑥 ∈ No
) |
120 | | simpl2 1192 |
. . . . . 6
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → 𝑦 ∈ No
) |
121 | | simpl3 1193 |
. . . . . 6
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → 𝑧 ∈ No
) |
122 | 119, 120,
121 | addsasslem1 34301 |
. . . . 5
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → ((𝑥 +s 𝑦) +s 𝑧) = ((({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = ((𝑥L +s 𝑦) +s 𝑧)} ∪ {𝑏 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑏 = ((𝑥 +s 𝑦L) +s 𝑧)}) ∪ {𝑐 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑐 = ((𝑥 +s 𝑦) +s 𝑧L)}) |s (({𝑑 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑑 = ((𝑥R +s 𝑦) +s 𝑧)} ∪ {𝑒 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑒 = ((𝑥 +s 𝑦R) +s 𝑧)}) ∪ {𝑓 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑓 = ((𝑥 +s 𝑦) +s 𝑧R)}))) |
123 | 119, 120,
121 | addsasslem2 34302 |
. . . . 5
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → (𝑥 +s (𝑦 +s 𝑧)) = ((({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s (𝑦 +s 𝑧))} ∪ {𝑏 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑏 = (𝑥 +s (𝑦L +s 𝑧))}) ∪ {𝑐 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑐 = (𝑥 +s (𝑦 +s 𝑧L))}) |s (({𝑑 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑑 = (𝑥R +s (𝑦 +s 𝑧))} ∪ {𝑒 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑒 = (𝑥 +s (𝑦R +s 𝑧))}) ∪ {𝑓 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑓 = (𝑥 +s (𝑦 +s 𝑧R))}))) |
124 | 118, 122,
123 | 3eqtr4d 2787 |
. . . 4
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → ((𝑥 +s 𝑦) +s 𝑧) = (𝑥 +s (𝑦 +s 𝑧))) |
125 | 124 | ex 413 |
. . 3
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
→ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O))) → ((𝑥 +s 𝑦) +s 𝑧) = (𝑥 +s (𝑦 +s 𝑧)))) |
126 | 45, 125 | syl5 34 |
. 2
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
→ (((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥O +s 𝑦O) +s 𝑧O) = (𝑥O +s (𝑦O +s 𝑧O)) ∧ ∀𝑥O ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦O ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥O +s 𝑦O) +s 𝑧) = (𝑥O +s (𝑦O +s 𝑧)) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥O +s 𝑦) +s 𝑧O) = (𝑥O +s (𝑦 +s 𝑧O))) ∧ (∀𝑥O ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦O) +s 𝑧O) = (𝑥 +s (𝑦O +s 𝑧O)) ∧ ∀𝑦O ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧))) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O))) → ((𝑥 +s 𝑦) +s 𝑧) = (𝑥 +s (𝑦 +s 𝑧)))) |
127 | 4, 9, 13, 17, 22, 25, 28, 32, 37, 41, 126 | no3inds 34266 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐶 ∈ No )
→ ((𝐴 +s 𝐵) +s 𝐶) = (𝐴 +s (𝐵 +s 𝐶))) |