Step | Hyp | Ref
| Expression |
1 | | oveq1 7401 |
. . 3
⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s 𝑦) = (𝑥𝑂 ·s
𝑦)) |
2 | | oveq2 7402 |
. . 3
⊢ (𝑥 = 𝑥𝑂 → (𝑦 ·s 𝑥) = (𝑦 ·s 𝑥𝑂)) |
3 | 1, 2 | eqeq12d 2748 |
. 2
⊢ (𝑥 = 𝑥𝑂 → ((𝑥 ·s 𝑦) = (𝑦 ·s 𝑥) ↔ (𝑥𝑂 ·s
𝑦) = (𝑦 ·s 𝑥𝑂))) |
4 | | oveq2 7402 |
. . 3
⊢ (𝑦 = 𝑦𝑂 → (𝑥𝑂
·s 𝑦) =
(𝑥𝑂
·s 𝑦𝑂)) |
5 | | oveq1 7401 |
. . 3
⊢ (𝑦 = 𝑦𝑂 → (𝑦 ·s 𝑥𝑂) = (𝑦𝑂
·s 𝑥𝑂)) |
6 | 4, 5 | eqeq12d 2748 |
. 2
⊢ (𝑦 = 𝑦𝑂 → ((𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
↔ (𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂))) |
7 | | oveq1 7401 |
. . 3
⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s 𝑦𝑂) = (𝑥𝑂
·s 𝑦𝑂)) |
8 | | oveq2 7402 |
. . 3
⊢ (𝑥 = 𝑥𝑂 → (𝑦𝑂
·s 𝑥) =
(𝑦𝑂
·s 𝑥𝑂)) |
9 | 7, 8 | eqeq12d 2748 |
. 2
⊢ (𝑥 = 𝑥𝑂 → ((𝑥 ·s 𝑦𝑂) = (𝑦𝑂
·s 𝑥)
↔ (𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂))) |
10 | | oveq1 7401 |
. . 3
⊢ (𝑥 = 𝐴 → (𝑥 ·s 𝑦) = (𝐴 ·s 𝑦)) |
11 | | oveq2 7402 |
. . 3
⊢ (𝑥 = 𝐴 → (𝑦 ·s 𝑥) = (𝑦 ·s 𝐴)) |
12 | 10, 11 | eqeq12d 2748 |
. 2
⊢ (𝑥 = 𝐴 → ((𝑥 ·s 𝑦) = (𝑦 ·s 𝑥) ↔ (𝐴 ·s 𝑦) = (𝑦 ·s 𝐴))) |
13 | | oveq2 7402 |
. . 3
⊢ (𝑦 = 𝐵 → (𝐴 ·s 𝑦) = (𝐴 ·s 𝐵)) |
14 | | oveq1 7401 |
. . 3
⊢ (𝑦 = 𝐵 → (𝑦 ·s 𝐴) = (𝐵 ·s 𝐴)) |
15 | 13, 14 | eqeq12d 2748 |
. 2
⊢ (𝑦 = 𝐵 → ((𝐴 ·s 𝑦) = (𝑦 ·s 𝐴) ↔ (𝐴 ·s 𝐵) = (𝐵 ·s 𝐴))) |
16 | | oveq1 7401 |
. . . . . . . . . . . . . . 15
⊢ (𝑥𝑂 = 𝑝 → (𝑥𝑂 ·s
𝑦) = (𝑝 ·s 𝑦)) |
17 | | oveq2 7402 |
. . . . . . . . . . . . . . 15
⊢ (𝑥𝑂 = 𝑝 → (𝑦 ·s 𝑥𝑂) = (𝑦 ·s 𝑝)) |
18 | 16, 17 | eqeq12d 2748 |
. . . . . . . . . . . . . 14
⊢ (𝑥𝑂 = 𝑝 → ((𝑥𝑂 ·s
𝑦) = (𝑦 ·s 𝑥𝑂) ↔ (𝑝 ·s 𝑦) = (𝑦 ·s 𝑝))) |
19 | | simplr2 1216 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
𝑦) = (𝑦 ·s 𝑥𝑂)) |
20 | | simprl 769 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → 𝑝 ∈ ( L ‘𝑥)) |
21 | | elun1 4173 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ ( L ‘𝑥) → 𝑝 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → 𝑝 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) |
23 | 18, 19, 22 | rspcdva 3611 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → (𝑝 ·s 𝑦) = (𝑦 ·s 𝑝)) |
24 | | oveq2 7402 |
. . . . . . . . . . . . . . 15
⊢ (𝑦𝑂 = 𝑞 → (𝑥 ·s 𝑦𝑂) = (𝑥 ·s 𝑞)) |
25 | | oveq1 7401 |
. . . . . . . . . . . . . . 15
⊢ (𝑦𝑂 = 𝑞 → (𝑦𝑂 ·s
𝑥) = (𝑞 ·s 𝑥)) |
26 | 24, 25 | eqeq12d 2748 |
. . . . . . . . . . . . . 14
⊢ (𝑦𝑂 = 𝑞 → ((𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥) ↔ (𝑥 ·s 𝑞) = (𝑞 ·s 𝑥))) |
27 | | simplr3 1217 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥)) |
28 | | simprr 771 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → 𝑞 ∈ ( L ‘𝑦)) |
29 | | elun1 4173 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 ∈ ( L ‘𝑦) → 𝑞 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → 𝑞 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))) |
31 | 26, 27, 30 | rspcdva 3611 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → (𝑥 ·s 𝑞) = (𝑞 ·s 𝑥)) |
32 | 23, 31 | oveq12d 7412 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → ((𝑝 ·s 𝑦) +s (𝑥 ·s 𝑞)) = ((𝑦 ·s 𝑝) +s (𝑞 ·s 𝑥))) |
33 | | simpllr 774 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → 𝑦 ∈ No
) |
34 | | leftssno 27304 |
. . . . . . . . . . . . . . 15
⊢ ( L
‘𝑥) ⊆ No |
35 | 34, 20 | sselid 3977 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → 𝑝 ∈ No
) |
36 | 33, 35 | mulscld 27520 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → (𝑦 ·s 𝑝) ∈ No
) |
37 | | leftssno 27304 |
. . . . . . . . . . . . . . 15
⊢ ( L
‘𝑦) ⊆ No |
38 | 37, 28 | sselid 3977 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → 𝑞 ∈ No
) |
39 | | simplll 773 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → 𝑥 ∈ No
) |
40 | 38, 39 | mulscld 27520 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → (𝑞 ·s 𝑥) ∈ No
) |
41 | 36, 40 | addscomd 27380 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → ((𝑦 ·s 𝑝) +s (𝑞 ·s 𝑥)) = ((𝑞 ·s 𝑥) +s (𝑦 ·s 𝑝))) |
42 | 32, 41 | eqtrd 2772 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → ((𝑝 ·s 𝑦) +s (𝑥 ·s 𝑞)) = ((𝑞 ·s 𝑥) +s (𝑦 ·s 𝑝))) |
43 | | oveq1 7401 |
. . . . . . . . . . . . 13
⊢ (𝑥𝑂 = 𝑝 → (𝑥𝑂 ·s
𝑦𝑂) =
(𝑝 ·s
𝑦𝑂)) |
44 | | oveq2 7402 |
. . . . . . . . . . . . 13
⊢ (𝑥𝑂 = 𝑝 → (𝑦𝑂 ·s
𝑥𝑂) =
(𝑦𝑂
·s 𝑝)) |
45 | 43, 44 | eqeq12d 2748 |
. . . . . . . . . . . 12
⊢ (𝑥𝑂 = 𝑝 → ((𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ↔ (𝑝 ·s 𝑦𝑂) = (𝑦𝑂
·s 𝑝))) |
46 | | oveq2 7402 |
. . . . . . . . . . . . 13
⊢ (𝑦𝑂 = 𝑞 → (𝑝 ·s 𝑦𝑂) = (𝑝 ·s 𝑞)) |
47 | | oveq1 7401 |
. . . . . . . . . . . . 13
⊢ (𝑦𝑂 = 𝑞 → (𝑦𝑂 ·s
𝑝) = (𝑞 ·s 𝑝)) |
48 | 46, 47 | eqeq12d 2748 |
. . . . . . . . . . . 12
⊢ (𝑦𝑂 = 𝑞 → ((𝑝 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑝) ↔ (𝑝 ·s 𝑞) = (𝑞 ·s 𝑝))) |
49 | | simplr1 1215 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂)) |
50 | 45, 48, 49, 22, 30 | rspc2dv 3623 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → (𝑝 ·s 𝑞) = (𝑞 ·s 𝑝)) |
51 | 42, 50 | oveq12d 7412 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → (((𝑝 ·s 𝑦) +s (𝑥 ·s 𝑞)) -s (𝑝 ·s 𝑞)) = (((𝑞 ·s 𝑥) +s (𝑦 ·s 𝑝)) -s (𝑞 ·s 𝑝))) |
52 | 51 | eqeq2d 2743 |
. . . . . . . . 9
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → (𝑎 = (((𝑝 ·s 𝑦) +s (𝑥 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ 𝑎 = (((𝑞 ·s 𝑥) +s (𝑦 ·s 𝑝)) -s (𝑞 ·s 𝑝)))) |
53 | 52 | 2rexbidva 3217 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) → (∃𝑝 ∈ ( L ‘𝑥)∃𝑞 ∈ ( L ‘𝑦)𝑎 = (((𝑝 ·s 𝑦) +s (𝑥 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ ∃𝑝 ∈ ( L ‘𝑥)∃𝑞 ∈ ( L ‘𝑦)𝑎 = (((𝑞 ·s 𝑥) +s (𝑦 ·s 𝑝)) -s (𝑞 ·s 𝑝)))) |
54 | | rexcom 3287 |
. . . . . . . 8
⊢
(∃𝑝 ∈ ( L
‘𝑥)∃𝑞 ∈ ( L ‘𝑦)𝑎 = (((𝑞 ·s 𝑥) +s (𝑦 ·s 𝑝)) -s (𝑞 ·s 𝑝)) ↔ ∃𝑞 ∈ ( L ‘𝑦)∃𝑝 ∈ ( L ‘𝑥)𝑎 = (((𝑞 ·s 𝑥) +s (𝑦 ·s 𝑝)) -s (𝑞 ·s 𝑝))) |
55 | 53, 54 | bitrdi 286 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) → (∃𝑝 ∈ ( L ‘𝑥)∃𝑞 ∈ ( L ‘𝑦)𝑎 = (((𝑝 ·s 𝑦) +s (𝑥 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ ∃𝑞 ∈ ( L ‘𝑦)∃𝑝 ∈ ( L ‘𝑥)𝑎 = (((𝑞 ·s 𝑥) +s (𝑦 ·s 𝑝)) -s (𝑞 ·s 𝑝)))) |
56 | 55 | abbidv 2801 |
. . . . . 6
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) → {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝑥)∃𝑞 ∈ ( L ‘𝑦)𝑎 = (((𝑝 ·s 𝑦) +s (𝑥 ·s 𝑞)) -s (𝑝 ·s 𝑞))} = {𝑎 ∣ ∃𝑞 ∈ ( L ‘𝑦)∃𝑝 ∈ ( L ‘𝑥)𝑎 = (((𝑞 ·s 𝑥) +s (𝑦 ·s 𝑝)) -s (𝑞 ·s 𝑝))}) |
57 | | oveq1 7401 |
. . . . . . . . . . . . . . 15
⊢ (𝑥𝑂 = 𝑟 → (𝑥𝑂 ·s
𝑦) = (𝑟 ·s 𝑦)) |
58 | | oveq2 7402 |
. . . . . . . . . . . . . . 15
⊢ (𝑥𝑂 = 𝑟 → (𝑦 ·s 𝑥𝑂) = (𝑦 ·s 𝑟)) |
59 | 57, 58 | eqeq12d 2748 |
. . . . . . . . . . . . . 14
⊢ (𝑥𝑂 = 𝑟 → ((𝑥𝑂 ·s
𝑦) = (𝑦 ·s 𝑥𝑂) ↔ (𝑟 ·s 𝑦) = (𝑦 ·s 𝑟))) |
60 | | simplr2 1216 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
𝑦) = (𝑦 ·s 𝑥𝑂)) |
61 | | simprl 769 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → 𝑟 ∈ ( R ‘𝑥)) |
62 | | elun2 4174 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 ∈ ( R ‘𝑥) → 𝑟 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → 𝑟 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) |
64 | 59, 60, 63 | rspcdva 3611 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → (𝑟 ·s 𝑦) = (𝑦 ·s 𝑟)) |
65 | | oveq2 7402 |
. . . . . . . . . . . . . . 15
⊢ (𝑦𝑂 = 𝑠 → (𝑥 ·s 𝑦𝑂) = (𝑥 ·s 𝑠)) |
66 | | oveq1 7401 |
. . . . . . . . . . . . . . 15
⊢ (𝑦𝑂 = 𝑠 → (𝑦𝑂 ·s
𝑥) = (𝑠 ·s 𝑥)) |
67 | 65, 66 | eqeq12d 2748 |
. . . . . . . . . . . . . 14
⊢ (𝑦𝑂 = 𝑠 → ((𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥) ↔ (𝑥 ·s 𝑠) = (𝑠 ·s 𝑥))) |
68 | | simplr3 1217 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥)) |
69 | | simprr 771 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → 𝑠 ∈ ( R ‘𝑦)) |
70 | | elun2 4174 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ ( R ‘𝑦) → 𝑠 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))) |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → 𝑠 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))) |
72 | 67, 68, 71 | rspcdva 3611 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → (𝑥 ·s 𝑠) = (𝑠 ·s 𝑥)) |
73 | 64, 72 | oveq12d 7412 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → ((𝑟 ·s 𝑦) +s (𝑥 ·s 𝑠)) = ((𝑦 ·s 𝑟) +s (𝑠 ·s 𝑥))) |
74 | | simpllr 774 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → 𝑦 ∈ No
) |
75 | | rightssno 27305 |
. . . . . . . . . . . . . . 15
⊢ ( R
‘𝑥) ⊆ No |
76 | 75, 61 | sselid 3977 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → 𝑟 ∈ No
) |
77 | 74, 76 | mulscld 27520 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → (𝑦 ·s 𝑟) ∈ No
) |
78 | | rightssno 27305 |
. . . . . . . . . . . . . . 15
⊢ ( R
‘𝑦) ⊆ No |
79 | 78, 69 | sselid 3977 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → 𝑠 ∈ No
) |
80 | | simplll 773 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → 𝑥 ∈ No
) |
81 | 79, 80 | mulscld 27520 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → (𝑠 ·s 𝑥) ∈ No
) |
82 | 77, 81 | addscomd 27380 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → ((𝑦 ·s 𝑟) +s (𝑠 ·s 𝑥)) = ((𝑠 ·s 𝑥) +s (𝑦 ·s 𝑟))) |
83 | 73, 82 | eqtrd 2772 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → ((𝑟 ·s 𝑦) +s (𝑥 ·s 𝑠)) = ((𝑠 ·s 𝑥) +s (𝑦 ·s 𝑟))) |
84 | | oveq1 7401 |
. . . . . . . . . . . . 13
⊢ (𝑥𝑂 = 𝑟 → (𝑥𝑂 ·s
𝑦𝑂) =
(𝑟 ·s
𝑦𝑂)) |
85 | | oveq2 7402 |
. . . . . . . . . . . . 13
⊢ (𝑥𝑂 = 𝑟 → (𝑦𝑂 ·s
𝑥𝑂) =
(𝑦𝑂
·s 𝑟)) |
86 | 84, 85 | eqeq12d 2748 |
. . . . . . . . . . . 12
⊢ (𝑥𝑂 = 𝑟 → ((𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ↔ (𝑟 ·s 𝑦𝑂) = (𝑦𝑂
·s 𝑟))) |
87 | | oveq2 7402 |
. . . . . . . . . . . . 13
⊢ (𝑦𝑂 = 𝑠 → (𝑟 ·s 𝑦𝑂) = (𝑟 ·s 𝑠)) |
88 | | oveq1 7401 |
. . . . . . . . . . . . 13
⊢ (𝑦𝑂 = 𝑠 → (𝑦𝑂 ·s
𝑟) = (𝑠 ·s 𝑟)) |
89 | 87, 88 | eqeq12d 2748 |
. . . . . . . . . . . 12
⊢ (𝑦𝑂 = 𝑠 → ((𝑟 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑟) ↔ (𝑟 ·s 𝑠) = (𝑠 ·s 𝑟))) |
90 | | simplr1 1215 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂)) |
91 | 86, 89, 90, 63, 71 | rspc2dv 3623 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → (𝑟 ·s 𝑠) = (𝑠 ·s 𝑟)) |
92 | 83, 91 | oveq12d 7412 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → (((𝑟 ·s 𝑦) +s (𝑥 ·s 𝑠)) -s (𝑟 ·s 𝑠)) = (((𝑠 ·s 𝑥) +s (𝑦 ·s 𝑟)) -s (𝑠 ·s 𝑟))) |
93 | 92 | eqeq2d 2743 |
. . . . . . . . 9
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → (𝑏 = (((𝑟 ·s 𝑦) +s (𝑥 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ 𝑏 = (((𝑠 ·s 𝑥) +s (𝑦 ·s 𝑟)) -s (𝑠 ·s 𝑟)))) |
94 | 93 | 2rexbidva 3217 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) → (∃𝑟 ∈ ( R ‘𝑥)∃𝑠 ∈ ( R ‘𝑦)𝑏 = (((𝑟 ·s 𝑦) +s (𝑥 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ ∃𝑟 ∈ ( R ‘𝑥)∃𝑠 ∈ ( R ‘𝑦)𝑏 = (((𝑠 ·s 𝑥) +s (𝑦 ·s 𝑟)) -s (𝑠 ·s 𝑟)))) |
95 | | rexcom 3287 |
. . . . . . . 8
⊢
(∃𝑟 ∈ ( R
‘𝑥)∃𝑠 ∈ ( R ‘𝑦)𝑏 = (((𝑠 ·s 𝑥) +s (𝑦 ·s 𝑟)) -s (𝑠 ·s 𝑟)) ↔ ∃𝑠 ∈ ( R ‘𝑦)∃𝑟 ∈ ( R ‘𝑥)𝑏 = (((𝑠 ·s 𝑥) +s (𝑦 ·s 𝑟)) -s (𝑠 ·s 𝑟))) |
96 | 94, 95 | bitrdi 286 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) → (∃𝑟 ∈ ( R ‘𝑥)∃𝑠 ∈ ( R ‘𝑦)𝑏 = (((𝑟 ·s 𝑦) +s (𝑥 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ ∃𝑠 ∈ ( R ‘𝑦)∃𝑟 ∈ ( R ‘𝑥)𝑏 = (((𝑠 ·s 𝑥) +s (𝑦 ·s 𝑟)) -s (𝑠 ·s 𝑟)))) |
97 | 96 | abbidv 2801 |
. . . . . 6
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) → {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝑥)∃𝑠 ∈ ( R ‘𝑦)𝑏 = (((𝑟 ·s 𝑦) +s (𝑥 ·s 𝑠)) -s (𝑟 ·s 𝑠))} = {𝑏 ∣ ∃𝑠 ∈ ( R ‘𝑦)∃𝑟 ∈ ( R ‘𝑥)𝑏 = (((𝑠 ·s 𝑥) +s (𝑦 ·s 𝑟)) -s (𝑠 ·s 𝑟))}) |
98 | 56, 97 | uneq12d 4161 |
. . . . 5
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) → ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝑥)∃𝑞 ∈ ( L ‘𝑦)𝑎 = (((𝑝 ·s 𝑦) +s (𝑥 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝑥)∃𝑠 ∈ ( R ‘𝑦)𝑏 = (((𝑟 ·s 𝑦) +s (𝑥 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) = ({𝑎 ∣ ∃𝑞 ∈ ( L ‘𝑦)∃𝑝 ∈ ( L ‘𝑥)𝑎 = (((𝑞 ·s 𝑥) +s (𝑦 ·s 𝑝)) -s (𝑞 ·s 𝑝))} ∪ {𝑏 ∣ ∃𝑠 ∈ ( R ‘𝑦)∃𝑟 ∈ ( R ‘𝑥)𝑏 = (((𝑠 ·s 𝑥) +s (𝑦 ·s 𝑟)) -s (𝑠 ·s 𝑟))})) |
99 | | oveq1 7401 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥𝑂 = 𝑡 → (𝑥𝑂 ·s
𝑦) = (𝑡 ·s 𝑦)) |
100 | | oveq2 7402 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥𝑂 = 𝑡 → (𝑦 ·s 𝑥𝑂) = (𝑦 ·s 𝑡)) |
101 | 99, 100 | eqeq12d 2748 |
. . . . . . . . . . . . . . 15
⊢ (𝑥𝑂 = 𝑡 → ((𝑥𝑂 ·s
𝑦) = (𝑦 ·s 𝑥𝑂) ↔ (𝑡 ·s 𝑦) = (𝑦 ·s 𝑡))) |
102 | | simplr2 1216 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
𝑦) = (𝑦 ·s 𝑥𝑂)) |
103 | | simprl 769 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → 𝑡 ∈ ( L ‘𝑥)) |
104 | | elun1 4173 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ ( L ‘𝑥) → 𝑡 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → 𝑡 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) |
106 | 101, 102,
105 | rspcdva 3611 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → (𝑡 ·s 𝑦) = (𝑦 ·s 𝑡)) |
107 | | oveq2 7402 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦𝑂 = 𝑢 → (𝑥 ·s 𝑦𝑂) = (𝑥 ·s 𝑢)) |
108 | | oveq1 7401 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦𝑂 = 𝑢 → (𝑦𝑂 ·s
𝑥) = (𝑢 ·s 𝑥)) |
109 | 107, 108 | eqeq12d 2748 |
. . . . . . . . . . . . . . 15
⊢ (𝑦𝑂 = 𝑢 → ((𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥) ↔ (𝑥 ·s 𝑢) = (𝑢 ·s 𝑥))) |
110 | | simplr3 1217 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥)) |
111 | | simprr 771 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → 𝑢 ∈ ( R ‘𝑦)) |
112 | | elun2 4174 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ( R ‘𝑦) → 𝑢 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))) |
113 | 111, 112 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → 𝑢 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))) |
114 | 109, 110,
113 | rspcdva 3611 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → (𝑥 ·s 𝑢) = (𝑢 ·s 𝑥)) |
115 | 106, 114 | oveq12d 7412 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → ((𝑡 ·s 𝑦) +s (𝑥 ·s 𝑢)) = ((𝑦 ·s 𝑡) +s (𝑢 ·s 𝑥))) |
116 | | simpllr 774 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → 𝑦 ∈ No
) |
117 | 34, 103 | sselid 3977 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → 𝑡 ∈ No
) |
118 | 116, 117 | mulscld 27520 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → (𝑦 ·s 𝑡) ∈ No
) |
119 | 78, 111 | sselid 3977 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → 𝑢 ∈ No
) |
120 | | simplll 773 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → 𝑥 ∈ No
) |
121 | 119, 120 | mulscld 27520 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → (𝑢 ·s 𝑥) ∈ No
) |
122 | 118, 121 | addscomd 27380 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → ((𝑦 ·s 𝑡) +s (𝑢 ·s 𝑥)) = ((𝑢 ·s 𝑥) +s (𝑦 ·s 𝑡))) |
123 | 115, 122 | eqtrd 2772 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → ((𝑡 ·s 𝑦) +s (𝑥 ·s 𝑢)) = ((𝑢 ·s 𝑥) +s (𝑦 ·s 𝑡))) |
124 | | oveq1 7401 |
. . . . . . . . . . . . . 14
⊢ (𝑥𝑂 = 𝑡 → (𝑥𝑂 ·s
𝑦𝑂) =
(𝑡 ·s
𝑦𝑂)) |
125 | | oveq2 7402 |
. . . . . . . . . . . . . 14
⊢ (𝑥𝑂 = 𝑡 → (𝑦𝑂 ·s
𝑥𝑂) =
(𝑦𝑂
·s 𝑡)) |
126 | 124, 125 | eqeq12d 2748 |
. . . . . . . . . . . . 13
⊢ (𝑥𝑂 = 𝑡 → ((𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ↔ (𝑡 ·s 𝑦𝑂) = (𝑦𝑂
·s 𝑡))) |
127 | | oveq2 7402 |
. . . . . . . . . . . . . 14
⊢ (𝑦𝑂 = 𝑢 → (𝑡 ·s 𝑦𝑂) = (𝑡 ·s 𝑢)) |
128 | | oveq1 7401 |
. . . . . . . . . . . . . 14
⊢ (𝑦𝑂 = 𝑢 → (𝑦𝑂 ·s
𝑡) = (𝑢 ·s 𝑡)) |
129 | 127, 128 | eqeq12d 2748 |
. . . . . . . . . . . . 13
⊢ (𝑦𝑂 = 𝑢 → ((𝑡 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑡) ↔ (𝑡 ·s 𝑢) = (𝑢 ·s 𝑡))) |
130 | | simplr1 1215 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂)) |
131 | 126, 129,
130, 105, 113 | rspc2dv 3623 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → (𝑡 ·s 𝑢) = (𝑢 ·s 𝑡)) |
132 | 123, 131 | oveq12d 7412 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → (((𝑡 ·s 𝑦) +s (𝑥 ·s 𝑢)) -s (𝑡 ·s 𝑢)) = (((𝑢 ·s 𝑥) +s (𝑦 ·s 𝑡)) -s (𝑢 ·s 𝑡))) |
133 | 132 | eqeq2d 2743 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → (𝑐 = (((𝑡 ·s 𝑦) +s (𝑥 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ 𝑐 = (((𝑢 ·s 𝑥) +s (𝑦 ·s 𝑡)) -s (𝑢 ·s 𝑡)))) |
134 | 133 | 2rexbidva 3217 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) → (∃𝑡 ∈ ( L ‘𝑥)∃𝑢 ∈ ( R ‘𝑦)𝑐 = (((𝑡 ·s 𝑦) +s (𝑥 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ ∃𝑡 ∈ ( L ‘𝑥)∃𝑢 ∈ ( R ‘𝑦)𝑐 = (((𝑢 ·s 𝑥) +s (𝑦 ·s 𝑡)) -s (𝑢 ·s 𝑡)))) |
135 | | rexcom 3287 |
. . . . . . . . 9
⊢
(∃𝑡 ∈ ( L
‘𝑥)∃𝑢 ∈ ( R ‘𝑦)𝑐 = (((𝑢 ·s 𝑥) +s (𝑦 ·s 𝑡)) -s (𝑢 ·s 𝑡)) ↔ ∃𝑢 ∈ ( R ‘𝑦)∃𝑡 ∈ ( L ‘𝑥)𝑐 = (((𝑢 ·s 𝑥) +s (𝑦 ·s 𝑡)) -s (𝑢 ·s 𝑡))) |
136 | 134, 135 | bitrdi 286 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) → (∃𝑡 ∈ ( L ‘𝑥)∃𝑢 ∈ ( R ‘𝑦)𝑐 = (((𝑡 ·s 𝑦) +s (𝑥 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ ∃𝑢 ∈ ( R ‘𝑦)∃𝑡 ∈ ( L ‘𝑥)𝑐 = (((𝑢 ·s 𝑥) +s (𝑦 ·s 𝑡)) -s (𝑢 ·s 𝑡)))) |
137 | 136 | abbidv 2801 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) → {𝑐 ∣ ∃𝑡 ∈ ( L ‘𝑥)∃𝑢 ∈ ( R ‘𝑦)𝑐 = (((𝑡 ·s 𝑦) +s (𝑥 ·s 𝑢)) -s (𝑡 ·s 𝑢))} = {𝑐 ∣ ∃𝑢 ∈ ( R ‘𝑦)∃𝑡 ∈ ( L ‘𝑥)𝑐 = (((𝑢 ·s 𝑥) +s (𝑦 ·s 𝑡)) -s (𝑢 ·s 𝑡))}) |
138 | | oveq1 7401 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥𝑂 = 𝑣 → (𝑥𝑂 ·s
𝑦) = (𝑣 ·s 𝑦)) |
139 | | oveq2 7402 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥𝑂 = 𝑣 → (𝑦 ·s 𝑥𝑂) = (𝑦 ·s 𝑣)) |
140 | 138, 139 | eqeq12d 2748 |
. . . . . . . . . . . . . . 15
⊢ (𝑥𝑂 = 𝑣 → ((𝑥𝑂 ·s
𝑦) = (𝑦 ·s 𝑥𝑂) ↔ (𝑣 ·s 𝑦) = (𝑦 ·s 𝑣))) |
141 | | simplr2 1216 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
𝑦) = (𝑦 ·s 𝑥𝑂)) |
142 | | simprl 769 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → 𝑣 ∈ ( R ‘𝑥)) |
143 | | elun2 4174 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ ( R ‘𝑥) → 𝑣 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) |
144 | 142, 143 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → 𝑣 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) |
145 | 140, 141,
144 | rspcdva 3611 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → (𝑣 ·s 𝑦) = (𝑦 ·s 𝑣)) |
146 | | oveq2 7402 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦𝑂 = 𝑤 → (𝑥 ·s 𝑦𝑂) = (𝑥 ·s 𝑤)) |
147 | | oveq1 7401 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦𝑂 = 𝑤 → (𝑦𝑂 ·s
𝑥) = (𝑤 ·s 𝑥)) |
148 | 146, 147 | eqeq12d 2748 |
. . . . . . . . . . . . . . 15
⊢ (𝑦𝑂 = 𝑤 → ((𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥) ↔ (𝑥 ·s 𝑤) = (𝑤 ·s 𝑥))) |
149 | | simplr3 1217 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥)) |
150 | | simprr 771 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → 𝑤 ∈ ( L ‘𝑦)) |
151 | | elun1 4173 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ( L ‘𝑦) → 𝑤 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))) |
152 | 150, 151 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → 𝑤 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))) |
153 | 148, 149,
152 | rspcdva 3611 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → (𝑥 ·s 𝑤) = (𝑤 ·s 𝑥)) |
154 | 145, 153 | oveq12d 7412 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → ((𝑣 ·s 𝑦) +s (𝑥 ·s 𝑤)) = ((𝑦 ·s 𝑣) +s (𝑤 ·s 𝑥))) |
155 | | simpllr 774 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → 𝑦 ∈ No
) |
156 | 75, 142 | sselid 3977 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → 𝑣 ∈ No
) |
157 | 155, 156 | mulscld 27520 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → (𝑦 ·s 𝑣) ∈ No
) |
158 | 37, 150 | sselid 3977 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → 𝑤 ∈ No
) |
159 | | simplll 773 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → 𝑥 ∈ No
) |
160 | 158, 159 | mulscld 27520 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → (𝑤 ·s 𝑥) ∈ No
) |
161 | 157, 160 | addscomd 27380 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → ((𝑦 ·s 𝑣) +s (𝑤 ·s 𝑥)) = ((𝑤 ·s 𝑥) +s (𝑦 ·s 𝑣))) |
162 | 154, 161 | eqtrd 2772 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → ((𝑣 ·s 𝑦) +s (𝑥 ·s 𝑤)) = ((𝑤 ·s 𝑥) +s (𝑦 ·s 𝑣))) |
163 | | oveq1 7401 |
. . . . . . . . . . . . . 14
⊢ (𝑥𝑂 = 𝑣 → (𝑥𝑂 ·s
𝑦𝑂) =
(𝑣 ·s
𝑦𝑂)) |
164 | | oveq2 7402 |
. . . . . . . . . . . . . 14
⊢ (𝑥𝑂 = 𝑣 → (𝑦𝑂 ·s
𝑥𝑂) =
(𝑦𝑂
·s 𝑣)) |
165 | 163, 164 | eqeq12d 2748 |
. . . . . . . . . . . . 13
⊢ (𝑥𝑂 = 𝑣 → ((𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ↔ (𝑣 ·s 𝑦𝑂) = (𝑦𝑂
·s 𝑣))) |
166 | | oveq2 7402 |
. . . . . . . . . . . . . 14
⊢ (𝑦𝑂 = 𝑤 → (𝑣 ·s 𝑦𝑂) = (𝑣 ·s 𝑤)) |
167 | | oveq1 7401 |
. . . . . . . . . . . . . 14
⊢ (𝑦𝑂 = 𝑤 → (𝑦𝑂 ·s
𝑣) = (𝑤 ·s 𝑣)) |
168 | 166, 167 | eqeq12d 2748 |
. . . . . . . . . . . . 13
⊢ (𝑦𝑂 = 𝑤 → ((𝑣 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑣) ↔ (𝑣 ·s 𝑤) = (𝑤 ·s 𝑣))) |
169 | | simplr1 1215 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂)) |
170 | 165, 168,
169, 144, 152 | rspc2dv 3623 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → (𝑣 ·s 𝑤) = (𝑤 ·s 𝑣)) |
171 | 162, 170 | oveq12d 7412 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → (((𝑣 ·s 𝑦) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤)) = (((𝑤 ·s 𝑥) +s (𝑦 ·s 𝑣)) -s (𝑤 ·s 𝑣))) |
172 | 171 | eqeq2d 2743 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → (𝑑 = (((𝑣 ·s 𝑦) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ 𝑑 = (((𝑤 ·s 𝑥) +s (𝑦 ·s 𝑣)) -s (𝑤 ·s 𝑣)))) |
173 | 172 | 2rexbidva 3217 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) → (∃𝑣 ∈ ( R ‘𝑥)∃𝑤 ∈ ( L ‘𝑦)𝑑 = (((𝑣 ·s 𝑦) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ ∃𝑣 ∈ ( R ‘𝑥)∃𝑤 ∈ ( L ‘𝑦)𝑑 = (((𝑤 ·s 𝑥) +s (𝑦 ·s 𝑣)) -s (𝑤 ·s 𝑣)))) |
174 | | rexcom 3287 |
. . . . . . . . 9
⊢
(∃𝑣 ∈ ( R
‘𝑥)∃𝑤 ∈ ( L ‘𝑦)𝑑 = (((𝑤 ·s 𝑥) +s (𝑦 ·s 𝑣)) -s (𝑤 ·s 𝑣)) ↔ ∃𝑤 ∈ ( L ‘𝑦)∃𝑣 ∈ ( R ‘𝑥)𝑑 = (((𝑤 ·s 𝑥) +s (𝑦 ·s 𝑣)) -s (𝑤 ·s 𝑣))) |
175 | 173, 174 | bitrdi 286 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) → (∃𝑣 ∈ ( R ‘𝑥)∃𝑤 ∈ ( L ‘𝑦)𝑑 = (((𝑣 ·s 𝑦) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ ∃𝑤 ∈ ( L ‘𝑦)∃𝑣 ∈ ( R ‘𝑥)𝑑 = (((𝑤 ·s 𝑥) +s (𝑦 ·s 𝑣)) -s (𝑤 ·s 𝑣)))) |
176 | 175 | abbidv 2801 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) → {𝑑 ∣ ∃𝑣 ∈ ( R ‘𝑥)∃𝑤 ∈ ( L ‘𝑦)𝑑 = (((𝑣 ·s 𝑦) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤))} = {𝑑 ∣ ∃𝑤 ∈ ( L ‘𝑦)∃𝑣 ∈ ( R ‘𝑥)𝑑 = (((𝑤 ·s 𝑥) +s (𝑦 ·s 𝑣)) -s (𝑤 ·s 𝑣))}) |
177 | 137, 176 | uneq12d 4161 |
. . . . . 6
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) → ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝑥)∃𝑢 ∈ ( R ‘𝑦)𝑐 = (((𝑡 ·s 𝑦) +s (𝑥 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ ( R ‘𝑥)∃𝑤 ∈ ( L ‘𝑦)𝑑 = (((𝑣 ·s 𝑦) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤))}) = ({𝑐 ∣ ∃𝑢 ∈ ( R ‘𝑦)∃𝑡 ∈ ( L ‘𝑥)𝑐 = (((𝑢 ·s 𝑥) +s (𝑦 ·s 𝑡)) -s (𝑢 ·s 𝑡))} ∪ {𝑑 ∣ ∃𝑤 ∈ ( L ‘𝑦)∃𝑣 ∈ ( R ‘𝑥)𝑑 = (((𝑤 ·s 𝑥) +s (𝑦 ·s 𝑣)) -s (𝑤 ·s 𝑣))})) |
178 | | uncom 4150 |
. . . . . 6
⊢ ({𝑐 ∣ ∃𝑢 ∈ ( R ‘𝑦)∃𝑡 ∈ ( L ‘𝑥)𝑐 = (((𝑢 ·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 𝑡))}) |
179 | 177, 178 | eqtrdi 2788 |
. . . . 5
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) → ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝑥)∃𝑢 ∈ ( R ‘𝑦)𝑐 = (((𝑡 ·s 𝑦) +s (𝑥 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ ( R ‘𝑥)∃𝑤 ∈ ( L ‘𝑦)𝑑 = (((𝑣 ·s 𝑦) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤))}) = ({𝑑 ∣ ∃𝑤 ∈ ( L ‘𝑦)∃𝑣 ∈ ( R ‘𝑥)𝑑 = (((𝑤 ·s 𝑥) +s (𝑦 ·s 𝑣)) -s (𝑤 ·s 𝑣))} ∪ {𝑐 ∣ ∃𝑢 ∈ ( R ‘𝑦)∃𝑡 ∈ ( L ‘𝑥)𝑐 = (((𝑢 ·s 𝑥) +s (𝑦 ·s 𝑡)) -s (𝑢 ·s 𝑡))})) |
180 | 98, 179 | oveq12d 7412 |
. . . 4
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) → (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝑥)∃𝑞 ∈ ( L ‘𝑦)𝑎 = (((𝑝 ·s 𝑦) +s (𝑥 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝑥)∃𝑠 ∈ ( R ‘𝑦)𝑏 = (((𝑟 ·s 𝑦) +s (𝑥 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) |s ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝑥)∃𝑢 ∈ ( R ‘𝑦)𝑐 = (((𝑡 ·s 𝑦) +s (𝑥 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ ( R ‘𝑥)∃𝑤 ∈ ( L ‘𝑦)𝑑 = (((𝑣 ·s 𝑦) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤))})) = (({𝑎 ∣ ∃𝑞 ∈ ( L ‘𝑦)∃𝑝 ∈ ( L ‘𝑥)𝑎 = (((𝑞 ·s 𝑥) +s (𝑦 ·s 𝑝)) -s (𝑞 ·s 𝑝))} ∪ {𝑏 ∣ ∃𝑠 ∈ ( R ‘𝑦)∃𝑟 ∈ ( R ‘𝑥)𝑏 = (((𝑠 ·s 𝑥) +s (𝑦 ·s 𝑟)) -s (𝑠 ·s 𝑟))}) |s ({𝑑 ∣ ∃𝑤 ∈ ( L ‘𝑦)∃𝑣 ∈ ( R ‘𝑥)𝑑 = (((𝑤 ·s 𝑥) +s (𝑦 ·s 𝑣)) -s (𝑤 ·s 𝑣))} ∪ {𝑐 ∣ ∃𝑢 ∈ ( R ‘𝑦)∃𝑡 ∈ ( L ‘𝑥)𝑐 = (((𝑢 ·s 𝑥) +s (𝑦 ·s 𝑡)) -s (𝑢 ·s 𝑡))}))) |
181 | | mulsval 27494 |
. . . . 5
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ) → (𝑥 ·s 𝑦) = (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝑥)∃𝑞 ∈ ( L ‘𝑦)𝑎 = (((𝑝 ·s 𝑦) +s (𝑥 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝑥)∃𝑠 ∈ ( R ‘𝑦)𝑏 = (((𝑟 ·s 𝑦) +s (𝑥 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) |s ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝑥)∃𝑢 ∈ ( R ‘𝑦)𝑐 = (((𝑡 ·s 𝑦) +s (𝑥 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ ( R ‘𝑥)∃𝑤 ∈ ( L ‘𝑦)𝑑 = (((𝑣 ·s 𝑦) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))) |
182 | 181 | adantr 481 |
. . . 4
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) → (𝑥 ·s 𝑦) = (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝑥)∃𝑞 ∈ ( L ‘𝑦)𝑎 = (((𝑝 ·s 𝑦) +s (𝑥 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝑥)∃𝑠 ∈ ( R ‘𝑦)𝑏 = (((𝑟 ·s 𝑦) +s (𝑥 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) |s ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝑥)∃𝑢 ∈ ( R ‘𝑦)𝑐 = (((𝑡 ·s 𝑦) +s (𝑥 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ ( R ‘𝑥)∃𝑤 ∈ ( L ‘𝑦)𝑑 = (((𝑣 ·s 𝑦) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))) |
183 | | mulsval 27494 |
. . . . . 6
⊢ ((𝑦 ∈
No ∧ 𝑥 ∈
No ) → (𝑦 ·s 𝑥) = (({𝑎 ∣ ∃𝑞 ∈ ( L ‘𝑦)∃𝑝 ∈ ( L ‘𝑥)𝑎 = (((𝑞 ·s 𝑥) +s (𝑦 ·s 𝑝)) -s (𝑞 ·s 𝑝))} ∪ {𝑏 ∣ ∃𝑠 ∈ ( R ‘𝑦)∃𝑟 ∈ ( R ‘𝑥)𝑏 = (((𝑠 ·s 𝑥) +s (𝑦 ·s 𝑟)) -s (𝑠 ·s 𝑟))}) |s ({𝑑 ∣ ∃𝑤 ∈ ( L ‘𝑦)∃𝑣 ∈ ( R ‘𝑥)𝑑 = (((𝑤 ·s 𝑥) +s (𝑦 ·s 𝑣)) -s (𝑤 ·s 𝑣))} ∪ {𝑐 ∣ ∃𝑢 ∈ ( R ‘𝑦)∃𝑡 ∈ ( L ‘𝑥)𝑐 = (((𝑢 ·s 𝑥) +s (𝑦 ·s 𝑡)) -s (𝑢 ·s 𝑡))}))) |
184 | 183 | ancoms 459 |
. . . . 5
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ) → (𝑦 ·s 𝑥) = (({𝑎 ∣ ∃𝑞 ∈ ( L ‘𝑦)∃𝑝 ∈ ( L ‘𝑥)𝑎 = (((𝑞 ·s 𝑥) +s (𝑦 ·s 𝑝)) -s (𝑞 ·s 𝑝))} ∪ {𝑏 ∣ ∃𝑠 ∈ ( R ‘𝑦)∃𝑟 ∈ ( R ‘𝑥)𝑏 = (((𝑠 ·s 𝑥) +s (𝑦 ·s 𝑟)) -s (𝑠 ·s 𝑟))}) |s ({𝑑 ∣ ∃𝑤 ∈ ( L ‘𝑦)∃𝑣 ∈ ( R ‘𝑥)𝑑 = (((𝑤 ·s 𝑥) +s (𝑦 ·s 𝑣)) -s (𝑤 ·s 𝑣))} ∪ {𝑐 ∣ ∃𝑢 ∈ ( R ‘𝑦)∃𝑡 ∈ ( L ‘𝑥)𝑐 = (((𝑢 ·s 𝑥) +s (𝑦 ·s 𝑡)) -s (𝑢 ·s 𝑡))}))) |
185 | 184 | adantr 481 |
. . . 4
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) → (𝑦 ·s 𝑥) = (({𝑎 ∣ ∃𝑞 ∈ ( L ‘𝑦)∃𝑝 ∈ ( L ‘𝑥)𝑎 = (((𝑞 ·s 𝑥) +s (𝑦 ·s 𝑝)) -s (𝑞 ·s 𝑝))} ∪ {𝑏 ∣ ∃𝑠 ∈ ( R ‘𝑦)∃𝑟 ∈ ( R ‘𝑥)𝑏 = (((𝑠 ·s 𝑥) +s (𝑦 ·s 𝑟)) -s (𝑠 ·s 𝑟))}) |s ({𝑑 ∣ ∃𝑤 ∈ ( L ‘𝑦)∃𝑣 ∈ ( R ‘𝑥)𝑑 = (((𝑤 ·s 𝑥) +s (𝑦 ·s 𝑣)) -s (𝑤 ·s 𝑣))} ∪ {𝑐 ∣ ∃𝑢 ∈ ( R ‘𝑦)∃𝑡 ∈ ( L ‘𝑥)𝑐 = (((𝑢 ·s 𝑥) +s (𝑦 ·s 𝑡)) -s (𝑢 ·s 𝑡))}))) |
186 | 180, 182,
185 | 3eqtr4d 2782 |
. . 3
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥))) → (𝑥 ·s 𝑦) = (𝑦 ·s 𝑥)) |
187 | 186 | ex 413 |
. 2
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ) → ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
𝑦𝑂) =
(𝑦𝑂
·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 𝑦) =
(𝑦 ·s
𝑥𝑂)
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s
𝑥)) → (𝑥 ·s 𝑦) = (𝑦 ·s 𝑥))) |
188 | 3, 6, 9, 12, 15, 187 | no2inds 27368 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 ·s 𝐵) = (𝐵 ·s 𝐴)) |