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