Step | Hyp | Ref
| Expression |
1 | | oveq1 7401 |
. . . 4
⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s 𝑦) = (𝑥𝑂 ·s
𝑦)) |
2 | 1 | oveq1d 7409 |
. . 3
⊢ (𝑥 = 𝑥𝑂 → ((𝑥 ·s 𝑦) ·s 𝑧) = ((𝑥𝑂 ·s
𝑦) ·s
𝑧)) |
3 | | oveq1 7401 |
. . 3
⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s (𝑦 ·s 𝑧)) = (𝑥𝑂 ·s
(𝑦 ·s
𝑧))) |
4 | 2, 3 | eqeq12d 2748 |
. 2
⊢ (𝑥 = 𝑥𝑂 → (((𝑥 ·s 𝑦) ·s 𝑧) = (𝑥 ·s (𝑦 ·s 𝑧)) ↔ ((𝑥𝑂 ·s
𝑦) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦 ·s
𝑧)))) |
5 | | oveq2 7402 |
. . . 4
⊢ (𝑦 = 𝑦𝑂 → (𝑥𝑂
·s 𝑦) =
(𝑥𝑂
·s 𝑦𝑂)) |
6 | 5 | oveq1d 7409 |
. . 3
⊢ (𝑦 = 𝑦𝑂 → ((𝑥𝑂
·s 𝑦)
·s 𝑧) =
((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧)) |
7 | | oveq1 7401 |
. . . 4
⊢ (𝑦 = 𝑦𝑂 → (𝑦 ·s 𝑧) = (𝑦𝑂 ·s
𝑧)) |
8 | 7 | oveq2d 7410 |
. . 3
⊢ (𝑦 = 𝑦𝑂 → (𝑥𝑂
·s (𝑦
·s 𝑧)) =
(𝑥𝑂
·s (𝑦𝑂 ·s
𝑧))) |
9 | 6, 8 | eqeq12d 2748 |
. 2
⊢ (𝑦 = 𝑦𝑂 → (((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
↔ ((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧) =
(𝑥𝑂
·s (𝑦𝑂 ·s
𝑧)))) |
10 | | oveq2 7402 |
. . 3
⊢ (𝑧 = 𝑧𝑂 → ((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = ((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂)) |
11 | | oveq2 7402 |
. . . 4
⊢ (𝑧 = 𝑧𝑂 → (𝑦𝑂
·s 𝑧) =
(𝑦𝑂
·s 𝑧𝑂)) |
12 | 11 | oveq2d 7410 |
. . 3
⊢ (𝑧 = 𝑧𝑂 → (𝑥𝑂
·s (𝑦𝑂 ·s
𝑧)) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂))) |
13 | 10, 12 | eqeq12d 2748 |
. 2
⊢ (𝑧 = 𝑧𝑂 → (((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
↔ ((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)))) |
14 | | oveq1 7401 |
. . . 4
⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s 𝑦𝑂) = (𝑥𝑂
·s 𝑦𝑂)) |
15 | 14 | oveq1d 7409 |
. . 3
⊢ (𝑥 = 𝑥𝑂 → ((𝑥 ·s 𝑦𝑂)
·s 𝑧𝑂) = ((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂)) |
16 | | oveq1 7401 |
. . 3
⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s (𝑦𝑂
·s 𝑧𝑂)) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂))) |
17 | 15, 16 | eqeq12d 2748 |
. 2
⊢ (𝑥 = 𝑥𝑂 → (((𝑥 ·s 𝑦𝑂)
·s 𝑧𝑂) = (𝑥 ·s (𝑦𝑂 ·s
𝑧𝑂))
↔ ((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)))) |
18 | | oveq2 7402 |
. . . 4
⊢ (𝑦 = 𝑦𝑂 → (𝑥 ·s 𝑦) = (𝑥 ·s 𝑦𝑂)) |
19 | 18 | oveq1d 7409 |
. . 3
⊢ (𝑦 = 𝑦𝑂 → ((𝑥 ·s 𝑦) ·s 𝑧𝑂) = ((𝑥 ·s 𝑦𝑂)
·s 𝑧𝑂)) |
20 | | oveq1 7401 |
. . . 4
⊢ (𝑦 = 𝑦𝑂 → (𝑦 ·s 𝑧𝑂) = (𝑦𝑂
·s 𝑧𝑂)) |
21 | 20 | oveq2d 7410 |
. . 3
⊢ (𝑦 = 𝑦𝑂 → (𝑥 ·s (𝑦 ·s 𝑧𝑂)) = (𝑥 ·s (𝑦𝑂
·s 𝑧𝑂))) |
22 | 19, 21 | eqeq12d 2748 |
. 2
⊢ (𝑦 = 𝑦𝑂 → (((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)) ↔
((𝑥 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥 ·s (𝑦𝑂 ·s
𝑧𝑂)))) |
23 | 5 | oveq1d 7409 |
. . 3
⊢ (𝑦 = 𝑦𝑂 → ((𝑥𝑂
·s 𝑦)
·s 𝑧𝑂) = ((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂)) |
24 | 20 | oveq2d 7410 |
. . 3
⊢ (𝑦 = 𝑦𝑂 → (𝑥𝑂
·s (𝑦
·s 𝑧𝑂)) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂))) |
25 | 23, 24 | eqeq12d 2748 |
. 2
⊢ (𝑦 = 𝑦𝑂 → (((𝑥𝑂
·s 𝑦)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦 ·s
𝑧𝑂))
↔ ((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)))) |
26 | | oveq2 7402 |
. . 3
⊢ (𝑧 = 𝑧𝑂 → ((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
((𝑥 ·s
𝑦𝑂)
·s 𝑧𝑂)) |
27 | 11 | oveq2d 7410 |
. . 3
⊢ (𝑧 = 𝑧𝑂 → (𝑥 ·s (𝑦𝑂
·s 𝑧)) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂))) |
28 | 26, 27 | eqeq12d 2748 |
. 2
⊢ (𝑧 = 𝑧𝑂 → (((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧))
↔ ((𝑥
·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)))) |
29 | | oveq1 7401 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝑥 ·s 𝑦) = (𝐴 ·s 𝑦)) |
30 | 29 | oveq1d 7409 |
. . 3
⊢ (𝑥 = 𝐴 → ((𝑥 ·s 𝑦) ·s 𝑧) = ((𝐴 ·s 𝑦) ·s 𝑧)) |
31 | | oveq1 7401 |
. . 3
⊢ (𝑥 = 𝐴 → (𝑥 ·s (𝑦 ·s 𝑧)) = (𝐴 ·s (𝑦 ·s 𝑧))) |
32 | 30, 31 | eqeq12d 2748 |
. 2
⊢ (𝑥 = 𝐴 → (((𝑥 ·s 𝑦) ·s 𝑧) = (𝑥 ·s (𝑦 ·s 𝑧)) ↔ ((𝐴 ·s 𝑦) ·s 𝑧) = (𝐴 ·s (𝑦 ·s 𝑧)))) |
33 | | oveq2 7402 |
. . . 4
⊢ (𝑦 = 𝐵 → (𝐴 ·s 𝑦) = (𝐴 ·s 𝐵)) |
34 | 33 | oveq1d 7409 |
. . 3
⊢ (𝑦 = 𝐵 → ((𝐴 ·s 𝑦) ·s 𝑧) = ((𝐴 ·s 𝐵) ·s 𝑧)) |
35 | | oveq1 7401 |
. . . 4
⊢ (𝑦 = 𝐵 → (𝑦 ·s 𝑧) = (𝐵 ·s 𝑧)) |
36 | 35 | oveq2d 7410 |
. . 3
⊢ (𝑦 = 𝐵 → (𝐴 ·s (𝑦 ·s 𝑧)) = (𝐴 ·s (𝐵 ·s 𝑧))) |
37 | 34, 36 | eqeq12d 2748 |
. 2
⊢ (𝑦 = 𝐵 → (((𝐴 ·s 𝑦) ·s 𝑧) = (𝐴 ·s (𝑦 ·s 𝑧)) ↔ ((𝐴 ·s 𝐵) ·s 𝑧) = (𝐴 ·s (𝐵 ·s 𝑧)))) |
38 | | oveq2 7402 |
. . 3
⊢ (𝑧 = 𝐶 → ((𝐴 ·s 𝐵) ·s 𝑧) = ((𝐴 ·s 𝐵) ·s 𝐶)) |
39 | | oveq2 7402 |
. . . 4
⊢ (𝑧 = 𝐶 → (𝐵 ·s 𝑧) = (𝐵 ·s 𝐶)) |
40 | 39 | oveq2d 7410 |
. . 3
⊢ (𝑧 = 𝐶 → (𝐴 ·s (𝐵 ·s 𝑧)) = (𝐴 ·s (𝐵 ·s 𝐶))) |
41 | 38, 40 | eqeq12d 2748 |
. 2
⊢ (𝑧 = 𝐶 → (((𝐴 ·s 𝐵) ·s 𝑧) = (𝐴 ·s (𝐵 ·s 𝑧)) ↔ ((𝐴 ·s 𝐵) ·s 𝐶) = (𝐴 ·s (𝐵 ·s 𝐶)))) |
42 | | simpl1 1191 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → 𝑥 ∈
No ) |
43 | | simpl2 1192 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → 𝑦 ∈
No ) |
44 | | simpl3 1193 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → 𝑧 ∈
No ) |
45 | | ssun1 4169 |
. . . . . . . . . 10
⊢ ( L
‘𝑥) ⊆ (( L
‘𝑥) ∪ ( R
‘𝑥)) |
46 | | ssun1 4169 |
. . . . . . . . . 10
⊢ ( L
‘𝑦) ⊆ (( L
‘𝑦) ∪ ( R
‘𝑦)) |
47 | | ssun1 4169 |
. . . . . . . . . 10
⊢ ( L
‘𝑧) ⊆ (( L
‘𝑧) ∪ ( R
‘𝑧)) |
48 | | simpr11 1257 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))∀𝑧𝑂 ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦𝑂 ·s
𝑧𝑂))) |
49 | | simpr12 1258 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))) |
50 | | simpr13 1259 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑧𝑂 ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))((𝑥𝑂
·s 𝑦)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦 ·s
𝑧𝑂))) |
51 | | simpr22 1261 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))∀𝑧𝑂 ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))((𝑥 ·s 𝑦𝑂)
·s 𝑧𝑂) = (𝑥 ·s (𝑦𝑂 ·s
𝑧𝑂))) |
52 | | simpr21 1260 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))) |
53 | | simpr23 1262 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧))) |
54 | | simpr3 1196 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → ∀𝑧𝑂 ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂))) |
55 | 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54 | mulsasslem3 27549 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → (∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿))
↔ ∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿)))))) |
56 | 55 | abbidv 2801 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿))} =
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))}) |
57 | | ssun2 4170 |
. . . . . . . . . 10
⊢ ( R
‘𝑥) ⊆ (( L
‘𝑥) ∪ ( R
‘𝑥)) |
58 | | ssun2 4170 |
. . . . . . . . . 10
⊢ ( R
‘𝑦) ⊆ (( L
‘𝑦) ∪ ( R
‘𝑦)) |
59 | 42, 43, 44, 57, 58, 47, 48, 49, 50, 51, 52, 53, 54 | mulsasslem3 27549 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → (∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿))
↔ ∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿)))))) |
60 | 59 | abbidv 2801 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿))} =
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))}) |
61 | 56, 60 | uneq12d 4161 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿))}) =
({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))})) |
62 | | ssun2 4170 |
. . . . . . . . . 10
⊢ ( R
‘𝑧) ⊆ (( L
‘𝑧) ∪ ( R
‘𝑧)) |
63 | 42, 43, 44, 45, 58, 62, 48, 49, 50, 51, 52, 53, 54 | mulsasslem3 27549 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → (∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅))
↔ ∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅)))))) |
64 | 63 | abbidv 2801 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅))} =
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))}) |
65 | 42, 43, 44, 57, 46, 62, 48, 49, 50, 51, 52, 53, 54 | mulsasslem3 27549 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → (∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅))
↔ ∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅)))))) |
66 | 65 | abbidv 2801 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅))} =
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))}) |
67 | 64, 66 | uneq12d 4161 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅))}) =
({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))})) |
68 | 61, 67 | uneq12d 4161 |
. . . . . 6
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅))}))
= (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))}))) |
69 | | un4 4166 |
. . . . . . 7
⊢ (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))})) = (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))})
∪ ({𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))})) |
70 | | uncom 4150 |
. . . . . . . 8
⊢ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))})
= ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))}) |
71 | 70 | uneq2i 4157 |
. . . . . . 7
⊢ (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))})
∪ ({𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))})) = (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))})
∪ ({𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))})) |
72 | 69, 71 | eqtri 2760 |
. . . . . 6
⊢ (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))})) = (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))})
∪ ({𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))})) |
73 | 68, 72 | eqtrdi 2788 |
. . . . 5
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅))}))
= (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))})
∪ ({𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))}))) |
74 | 42, 43, 44, 45, 46, 62, 48, 49, 50, 51, 52, 53, 54 | mulsasslem3 27549 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → (∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅))
↔ ∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅)))))) |
75 | 74 | abbidv 2801 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅))} =
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))}) |
76 | 42, 43, 44, 57, 58, 62, 48, 49, 50, 51, 52, 53, 54 | mulsasslem3 27549 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → (∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅))
↔ ∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅)))))) |
77 | 76 | abbidv 2801 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅))} =
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))}) |
78 | 75, 77 | uneq12d 4161 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅))}) =
({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))})) |
79 | 42, 43, 44, 45, 58, 47, 48, 49, 50, 51, 52, 53, 54 | mulsasslem3 27549 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → (∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿))
↔ ∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿)))))) |
80 | 79 | abbidv 2801 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿))} =
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))}) |
81 | 42, 43, 44, 57, 46, 47, 48, 49, 50, 51, 52, 53, 54 | mulsasslem3 27549 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → (∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿))
↔ ∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿)))))) |
82 | 81 | abbidv 2801 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿))} =
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))}) |
83 | 80, 82 | uneq12d 4161 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿))}) =
({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))})) |
84 | 78, 83 | uneq12d 4161 |
. . . . . 6
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿))}))
= (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))}))) |
85 | | un4 4166 |
. . . . . . 7
⊢ (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))})) = (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))})
∪ ({𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))})) |
86 | | uncom 4150 |
. . . . . . . 8
⊢ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))})
= ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))}) |
87 | 86 | uneq2i 4157 |
. . . . . . 7
⊢ (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))})
∪ ({𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))})) = (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))})
∪ ({𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))})) |
88 | 85, 87 | eqtri 2760 |
. . . . . 6
⊢ (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))})) = (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))})
∪ ({𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))})) |
89 | 84, 88 | eqtrdi 2788 |
. . . . 5
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿))}))
= (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))})
∪ ({𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))}))) |
90 | 73, 89 | oveq12d 7412 |
. . . 4
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → ((({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅))}))
|s (({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿))})))
= ((({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))})
∪ ({𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))})) |s (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))})
∪ ({𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))})))) |
91 | 42, 43, 44 | mulsasslem1 27547 |
. . . 4
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → ((𝑥 ·s 𝑦) ·s 𝑧) = ((({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅))}))
|s (({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝑦)
+s (𝑥
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝑧)
+s ((𝑥
·s 𝑦)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝑦)
+s (𝑥
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿))})))) |
92 | 42, 43, 44 | mulsasslem2 27548 |
. . . 4
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → (𝑥 ·s (𝑦 ·s 𝑧)) = ((({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))})
∪ ({𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))})) |s (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝐿
·s 𝑧𝑅)))) -s (𝑥𝐿
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝐿 ·s
𝑧𝑅))))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝑅
·s 𝑧𝐿)))) -s (𝑥𝐿
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝑅 ·s
𝑧𝐿))))})
∪ ({𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝐿
·s 𝑧)
+s (𝑦
·s 𝑧𝐿)) -s (𝑦𝐿
·s 𝑧𝐿)))) -s (𝑥𝑅
·s (((𝑦𝐿 ·s
𝑧) +s (𝑦 ·s 𝑧𝐿))
-s (𝑦𝐿 ·s
𝑧𝐿))))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 ·s
𝑧)) +s (𝑥 ·s (((𝑦𝑅
·s 𝑧)
+s (𝑦
·s 𝑧𝑅)) -s (𝑦𝑅
·s 𝑧𝑅)))) -s (𝑥𝑅
·s (((𝑦𝑅 ·s
𝑧) +s (𝑦 ·s 𝑧𝑅))
-s (𝑦𝑅 ·s
𝑧𝑅))))})))) |
93 | 90, 91, 92 | 3eqtr4d 2782 |
. . 3
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))) → ((𝑥 ·s 𝑦) ·s 𝑧) = (𝑥 ·s (𝑦 ·s 𝑧))) |
94 | 93 | ex 413 |
. 2
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
→ (((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦𝑂)
·s 𝑧𝑂) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥𝑂
·s 𝑦𝑂) ·s
𝑧) = (𝑥𝑂 ·s
(𝑦𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥𝑂 ·s
𝑦) ·s
𝑧𝑂) =
(𝑥𝑂
·s (𝑦
·s 𝑧𝑂))) ∧ (∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))((𝑥𝑂
·s 𝑦)
·s 𝑧) =
(𝑥𝑂
·s (𝑦
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦𝑂) ·s
𝑧𝑂) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 ·s 𝑦𝑂)
·s 𝑧) =
(𝑥 ·s
(𝑦𝑂
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂))) → ((𝑥 ·s 𝑦) ·s 𝑧) = (𝑥 ·s (𝑦 ·s 𝑧)))) |
95 | 4, 9, 13, 17, 22, 25, 28, 32, 37, 41, 94 | no3inds 27371 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐶 ∈ No )
→ ((𝐴
·s 𝐵)
·s 𝐶) =
(𝐴 ·s
(𝐵 ·s
𝐶))) |