Metamath Proof Explorer

Theorem mulscom

Description: Surreal multiplication commutes. Part of theorem 7 of Conway p. 19. (Contributed by Scott Fenton, 6-Mar-2025)

Ref Expression
Assertion mulscom ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ·s 𝐵 ) = ( 𝐵 ·s 𝐴 ) )

Proof

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 leftssno ⊢ ( L ‘ 𝑥 ) ⊆ No
35 34 20 sselid ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑝 ∈ ( L ‘ 𝑥 ) ∧ 𝑞 ∈ ( L ‘ 𝑦 ) ) ) → 𝑝 ∈ No )
36 33 35 mulscld ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑝 ∈ ( L ‘ 𝑥 ) ∧ 𝑞 ∈ ( L ‘ 𝑦 ) ) ) → ( 𝑦 ·s 𝑝 ) ∈ No )
37 leftssno ⊢ ( L ‘ 𝑦 ) ⊆ No
38 37 28 sselid ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑝 ∈ ( L ‘ 𝑥 ) ∧ 𝑞 ∈ ( L ‘ 𝑦 ) ) ) → 𝑞 ∈ No )
39 simplll ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑝 ∈ ( L ‘ 𝑥 ) ∧ 𝑞 ∈ ( L ‘ 𝑦 ) ) ) → 𝑥 ∈ No )
40 38 39 mulscld ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑝 ∈ ( L ‘ 𝑥 ) ∧ 𝑞 ∈ ( L ‘ 𝑦 ) ) ) → ( 𝑞 ·s 𝑥 ) ∈ No )
41 36 40 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 𝑝 ) ) )
42 32 41 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 𝑝 ) ) )
43 oveq1 ⊢ ( 𝑥𝑂 = 𝑝 → ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑝 ·s 𝑦𝑂 ) )
44 oveq2 ⊢ ( 𝑥𝑂 = 𝑝 → ( 𝑦𝑂 ·s 𝑥𝑂 ) = ( 𝑦𝑂 ·s 𝑝 ) )
45 43 44 eqeq12d ⊢ ( 𝑥𝑂 = 𝑝 → ( ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ↔ ( 𝑝 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑝 ) ) )
46 oveq2 ⊢ ( 𝑦𝑂 = 𝑞 → ( 𝑝 ·s 𝑦𝑂 ) = ( 𝑝 ·s 𝑞 ) )
47 oveq1 ⊢ ( 𝑦𝑂 = 𝑞 → ( 𝑦𝑂 ·s 𝑝 ) = ( 𝑞 ·s 𝑝 ) )
48 46 47 eqeq12d ⊢ ( 𝑦𝑂 = 𝑞 → ( ( 𝑝 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑝 ) ↔ ( 𝑝 ·s 𝑞 ) = ( 𝑞 ·s 𝑝 ) ) )
49 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 𝑥𝑂 ) )
50 45 48 49 22 30 rspc2dv ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑝 ∈ ( L ‘ 𝑥 ) ∧ 𝑞 ∈ ( L ‘ 𝑦 ) ) ) → ( 𝑝 ·s 𝑞 ) = ( 𝑞 ·s 𝑝 ) )
51 42 50 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 𝑝 ) ) )
52 51 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 𝑝 ) ) ) )
53 52 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 𝑝 ) ) ) )
54 rexcom ⊢ ( ∃ 𝑝 ∈ ( L ‘ 𝑥 ) ∃ 𝑞 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑞 ·s 𝑥 ) +s ( 𝑦 ·s 𝑝 ) ) -s ( 𝑞 ·s 𝑝 ) ) ↔ ∃ 𝑞 ∈ ( L ‘ 𝑦 ) ∃ 𝑝 ∈ ( L ‘ 𝑥 ) 𝑎 = ( ( ( 𝑞 ·s 𝑥 ) +s ( 𝑦 ·s 𝑝 ) ) -s ( 𝑞 ·s 𝑝 ) ) )
55 53 54 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 𝑝 ) ) ) )
56 55 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 𝑝 ) ) } )
57 oveq1 ⊢ ( 𝑥𝑂 = 𝑟 → ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑟 ·s 𝑦 ) )
58 oveq2 ⊢ ( 𝑥𝑂 = 𝑟 → ( 𝑦 ·s 𝑥𝑂 ) = ( 𝑦 ·s 𝑟 ) )
59 57 58 eqeq12d ⊢ ( 𝑥𝑂 = 𝑟 → ( ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ↔ ( 𝑟 ·s 𝑦 ) = ( 𝑦 ·s 𝑟 ) ) )
60 simplr2 ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑟 ∈ ( R ‘ 𝑥 ) ∧ 𝑠 ∈ ( R ‘ 𝑦 ) ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) )
61 simprl ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑟 ∈ ( R ‘ 𝑥 ) ∧ 𝑠 ∈ ( R ‘ 𝑦 ) ) ) → 𝑟 ∈ ( R ‘ 𝑥 ) )
62 elun2 ⊢ ( 𝑟 ∈ ( R ‘ 𝑥 ) → 𝑟 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
63 61 62 syl ⊢ ( ( ( ( 𝑥 ∈ 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 ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑟 ∈ ( R ‘ 𝑥 ) ∧ 𝑠 ∈ ( R ‘ 𝑦 ) ) ) → ( 𝑟 ·s 𝑦 ) = ( 𝑦 ·s 𝑟 ) )
65 oveq2 ⊢ ( 𝑦𝑂 = 𝑠 → ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑥 ·s 𝑠 ) )
66 oveq1 ⊢ ( 𝑦𝑂 = 𝑠 → ( 𝑦𝑂 ·s 𝑥 ) = ( 𝑠 ·s 𝑥 ) )
67 65 66 eqeq12d ⊢ ( 𝑦𝑂 = 𝑠 → ( ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ↔ ( 𝑥 ·s 𝑠 ) = ( 𝑠 ·s 𝑥 ) ) )
68 simplr3 ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑟 ∈ ( R ‘ 𝑥 ) ∧ 𝑠 ∈ ( R ‘ 𝑦 ) ) ) → ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) )
69 simprr ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑟 ∈ ( R ‘ 𝑥 ) ∧ 𝑠 ∈ ( R ‘ 𝑦 ) ) ) → 𝑠 ∈ ( R ‘ 𝑦 ) )
70 elun2 ⊢ ( 𝑠 ∈ ( R ‘ 𝑦 ) → 𝑠 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
71 69 70 syl ⊢ ( ( ( ( 𝑥 ∈ 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 ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑟 ∈ ( R ‘ 𝑥 ) ∧ 𝑠 ∈ ( R ‘ 𝑦 ) ) ) → ( 𝑥 ·s 𝑠 ) = ( 𝑠 ·s 𝑥 ) )
73 64 72 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 𝑥 ) ) )
74 simpllr ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑟 ∈ ( R ‘ 𝑥 ) ∧ 𝑠 ∈ ( R ‘ 𝑦 ) ) ) → 𝑦 ∈ No )
75 rightssno ⊢ ( R ‘ 𝑥 ) ⊆ No
76 75 61 sselid ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑟 ∈ ( R ‘ 𝑥 ) ∧ 𝑠 ∈ ( R ‘ 𝑦 ) ) ) → 𝑟 ∈ No )
77 74 76 mulscld ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑟 ∈ ( R ‘ 𝑥 ) ∧ 𝑠 ∈ ( R ‘ 𝑦 ) ) ) → ( 𝑦 ·s 𝑟 ) ∈ No )
78 rightssno ⊢ ( R ‘ 𝑦 ) ⊆ No
79 78 69 sselid ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑟 ∈ ( R ‘ 𝑥 ) ∧ 𝑠 ∈ ( R ‘ 𝑦 ) ) ) → 𝑠 ∈ No )
80 simplll ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑟 ∈ ( R ‘ 𝑥 ) ∧ 𝑠 ∈ ( R ‘ 𝑦 ) ) ) → 𝑥 ∈ No )
81 79 80 mulscld ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑟 ∈ ( R ‘ 𝑥 ) ∧ 𝑠 ∈ ( R ‘ 𝑦 ) ) ) → ( 𝑠 ·s 𝑥 ) ∈ No )
82 77 81 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 𝑟 ) ) )
83 73 82 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 𝑟 ) ) )
84 oveq1 ⊢ ( 𝑥𝑂 = 𝑟 → ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑟 ·s 𝑦𝑂 ) )
85 oveq2 ⊢ ( 𝑥𝑂 = 𝑟 → ( 𝑦𝑂 ·s 𝑥𝑂 ) = ( 𝑦𝑂 ·s 𝑟 ) )
86 84 85 eqeq12d ⊢ ( 𝑥𝑂 = 𝑟 → ( ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ↔ ( 𝑟 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑟 ) ) )
87 oveq2 ⊢ ( 𝑦𝑂 = 𝑠 → ( 𝑟 ·s 𝑦𝑂 ) = ( 𝑟 ·s 𝑠 ) )
88 oveq1 ⊢ ( 𝑦𝑂 = 𝑠 → ( 𝑦𝑂 ·s 𝑟 ) = ( 𝑠 ·s 𝑟 ) )
89 87 88 eqeq12d ⊢ ( 𝑦𝑂 = 𝑠 → ( ( 𝑟 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑟 ) ↔ ( 𝑟 ·s 𝑠 ) = ( 𝑠 ·s 𝑟 ) ) )
90 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 𝑥𝑂 ) )
91 86 89 90 63 71 rspc2dv ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑟 ∈ ( R ‘ 𝑥 ) ∧ 𝑠 ∈ ( R ‘ 𝑦 ) ) ) → ( 𝑟 ·s 𝑠 ) = ( 𝑠 ·s 𝑟 ) )
92 83 91 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 𝑟 ) ) )
93 92 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 𝑟 ) ) ) )
94 93 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 𝑟 ) ) ) )
95 rexcom ⊢ ( ∃ 𝑟 ∈ ( R ‘ 𝑥 ) ∃ 𝑠 ∈ ( R ‘ 𝑦 ) 𝑏 = ( ( ( 𝑠 ·s 𝑥 ) +s ( 𝑦 ·s 𝑟 ) ) -s ( 𝑠 ·s 𝑟 ) ) ↔ ∃ 𝑠 ∈ ( R ‘ 𝑦 ) ∃ 𝑟 ∈ ( R ‘ 𝑥 ) 𝑏 = ( ( ( 𝑠 ·s 𝑥 ) +s ( 𝑦 ·s 𝑟 ) ) -s ( 𝑠 ·s 𝑟 ) ) )
96 94 95 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 𝑟 ) ) ) )
97 96 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 𝑟 ) ) } )
98 56 97 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 𝑟 ) ) } ) )
99 oveq1 ⊢ ( 𝑥𝑂 = 𝑡 → ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑡 ·s 𝑦 ) )
100 oveq2 ⊢ ( 𝑥𝑂 = 𝑡 → ( 𝑦 ·s 𝑥𝑂 ) = ( 𝑦 ·s 𝑡 ) )
101 99 100 eqeq12d ⊢ ( 𝑥𝑂 = 𝑡 → ( ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ↔ ( 𝑡 ·s 𝑦 ) = ( 𝑦 ·s 𝑡 ) ) )
102 simplr2 ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝑥 ) ∧ 𝑢 ∈ ( R ‘ 𝑦 ) ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) )
103 simprl ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝑥 ) ∧ 𝑢 ∈ ( R ‘ 𝑦 ) ) ) → 𝑡 ∈ ( L ‘ 𝑥 ) )
104 elun1 ⊢ ( 𝑡 ∈ ( L ‘ 𝑥 ) → 𝑡 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
105 103 104 syl ⊢ ( ( ( ( 𝑥 ∈ 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 ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝑥 ) ∧ 𝑢 ∈ ( R ‘ 𝑦 ) ) ) → ( 𝑡 ·s 𝑦 ) = ( 𝑦 ·s 𝑡 ) )
107 oveq2 ⊢ ( 𝑦𝑂 = 𝑢 → ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑥 ·s 𝑢 ) )
108 oveq1 ⊢ ( 𝑦𝑂 = 𝑢 → ( 𝑦𝑂 ·s 𝑥 ) = ( 𝑢 ·s 𝑥 ) )
109 107 108 eqeq12d ⊢ ( 𝑦𝑂 = 𝑢 → ( ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ↔ ( 𝑥 ·s 𝑢 ) = ( 𝑢 ·s 𝑥 ) ) )
110 simplr3 ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝑥 ) ∧ 𝑢 ∈ ( R ‘ 𝑦 ) ) ) → ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) )
111 simprr ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝑥 ) ∧ 𝑢 ∈ ( R ‘ 𝑦 ) ) ) → 𝑢 ∈ ( R ‘ 𝑦 ) )
112 elun2 ⊢ ( 𝑢 ∈ ( R ‘ 𝑦 ) → 𝑢 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
113 111 112 syl ⊢ ( ( ( ( 𝑥 ∈ 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 ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝑥 ) ∧ 𝑢 ∈ ( R ‘ 𝑦 ) ) ) → ( 𝑥 ·s 𝑢 ) = ( 𝑢 ·s 𝑥 ) )
115 106 114 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 𝑥 ) ) )
116 simpllr ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝑥 ) ∧ 𝑢 ∈ ( R ‘ 𝑦 ) ) ) → 𝑦 ∈ No )
117 34 103 sselid ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝑥 ) ∧ 𝑢 ∈ ( R ‘ 𝑦 ) ) ) → 𝑡 ∈ No )
118 116 117 mulscld ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝑥 ) ∧ 𝑢 ∈ ( R ‘ 𝑦 ) ) ) → ( 𝑦 ·s 𝑡 ) ∈ No )
119 78 111 sselid ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝑥 ) ∧ 𝑢 ∈ ( R ‘ 𝑦 ) ) ) → 𝑢 ∈ No )
120 simplll ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝑥 ) ∧ 𝑢 ∈ ( R ‘ 𝑦 ) ) ) → 𝑥 ∈ No )
121 119 120 mulscld ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝑥 ) ∧ 𝑢 ∈ ( R ‘ 𝑦 ) ) ) → ( 𝑢 ·s 𝑥 ) ∈ No )
122 118 121 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 𝑡 ) ) )
123 115 122 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 𝑡 ) ) )
124 oveq1 ⊢ ( 𝑥𝑂 = 𝑡 → ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑡 ·s 𝑦𝑂 ) )
125 oveq2 ⊢ ( 𝑥𝑂 = 𝑡 → ( 𝑦𝑂 ·s 𝑥𝑂 ) = ( 𝑦𝑂 ·s 𝑡 ) )
126 124 125 eqeq12d ⊢ ( 𝑥𝑂 = 𝑡 → ( ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ↔ ( 𝑡 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑡 ) ) )
127 oveq2 ⊢ ( 𝑦𝑂 = 𝑢 → ( 𝑡 ·s 𝑦𝑂 ) = ( 𝑡 ·s 𝑢 ) )
128 oveq1 ⊢ ( 𝑦𝑂 = 𝑢 → ( 𝑦𝑂 ·s 𝑡 ) = ( 𝑢 ·s 𝑡 ) )
129 127 128 eqeq12d ⊢ ( 𝑦𝑂 = 𝑢 → ( ( 𝑡 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑡 ) ↔ ( 𝑡 ·s 𝑢 ) = ( 𝑢 ·s 𝑡 ) ) )
130 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 𝑥𝑂 ) )
131 126 129 130 105 113 rspc2dv ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝑥 ) ∧ 𝑢 ∈ ( R ‘ 𝑦 ) ) ) → ( 𝑡 ·s 𝑢 ) = ( 𝑢 ·s 𝑡 ) )
132 123 131 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 𝑡 ) ) )
133 132 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 𝑡 ) ) ) )
134 133 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 𝑡 ) ) ) )
135 rexcom ⊢ ( ∃ 𝑡 ∈ ( L ‘ 𝑥 ) ∃ 𝑢 ∈ ( R ‘ 𝑦 ) 𝑐 = ( ( ( 𝑢 ·s 𝑥 ) +s ( 𝑦 ·s 𝑡 ) ) -s ( 𝑢 ·s 𝑡 ) ) ↔ ∃ 𝑢 ∈ ( R ‘ 𝑦 ) ∃ 𝑡 ∈ ( L ‘ 𝑥 ) 𝑐 = ( ( ( 𝑢 ·s 𝑥 ) +s ( 𝑦 ·s 𝑡 ) ) -s ( 𝑢 ·s 𝑡 ) ) )
136 134 135 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 𝑡 ) ) ) )
137 136 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 𝑡 ) ) } )
138 oveq1 ⊢ ( 𝑥𝑂 = 𝑣 → ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑣 ·s 𝑦 ) )
139 oveq2 ⊢ ( 𝑥𝑂 = 𝑣 → ( 𝑦 ·s 𝑥𝑂 ) = ( 𝑦 ·s 𝑣 ) )
140 138 139 eqeq12d ⊢ ( 𝑥𝑂 = 𝑣 → ( ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ↔ ( 𝑣 ·s 𝑦 ) = ( 𝑦 ·s 𝑣 ) ) )
141 simplr2 ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝑥 ) ∧ 𝑤 ∈ ( L ‘ 𝑦 ) ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) )
142 simprl ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝑥 ) ∧ 𝑤 ∈ ( L ‘ 𝑦 ) ) ) → 𝑣 ∈ ( R ‘ 𝑥 ) )
143 elun2 ⊢ ( 𝑣 ∈ ( R ‘ 𝑥 ) → 𝑣 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
144 142 143 syl ⊢ ( ( ( ( 𝑥 ∈ 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 ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝑥 ) ∧ 𝑤 ∈ ( L ‘ 𝑦 ) ) ) → ( 𝑣 ·s 𝑦 ) = ( 𝑦 ·s 𝑣 ) )
146 oveq2 ⊢ ( 𝑦𝑂 = 𝑤 → ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑥 ·s 𝑤 ) )
147 oveq1 ⊢ ( 𝑦𝑂 = 𝑤 → ( 𝑦𝑂 ·s 𝑥 ) = ( 𝑤 ·s 𝑥 ) )
148 146 147 eqeq12d ⊢ ( 𝑦𝑂 = 𝑤 → ( ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ↔ ( 𝑥 ·s 𝑤 ) = ( 𝑤 ·s 𝑥 ) ) )
149 simplr3 ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝑥 ) ∧ 𝑤 ∈ ( L ‘ 𝑦 ) ) ) → ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) )
150 simprr ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝑥 ) ∧ 𝑤 ∈ ( L ‘ 𝑦 ) ) ) → 𝑤 ∈ ( L ‘ 𝑦 ) )
151 elun1 ⊢ ( 𝑤 ∈ ( L ‘ 𝑦 ) → 𝑤 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
152 150 151 syl ⊢ ( ( ( ( 𝑥 ∈ 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 ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝑥 ) ∧ 𝑤 ∈ ( L ‘ 𝑦 ) ) ) → ( 𝑥 ·s 𝑤 ) = ( 𝑤 ·s 𝑥 ) )
154 145 153 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 𝑥 ) ) )
155 simpllr ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝑥 ) ∧ 𝑤 ∈ ( L ‘ 𝑦 ) ) ) → 𝑦 ∈ No )
156 75 142 sselid ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝑥 ) ∧ 𝑤 ∈ ( L ‘ 𝑦 ) ) ) → 𝑣 ∈ No )
157 155 156 mulscld ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝑥 ) ∧ 𝑤 ∈ ( L ‘ 𝑦 ) ) ) → ( 𝑦 ·s 𝑣 ) ∈ No )
158 37 150 sselid ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝑥 ) ∧ 𝑤 ∈ ( L ‘ 𝑦 ) ) ) → 𝑤 ∈ No )
159 simplll ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝑥 ) ∧ 𝑤 ∈ ( L ‘ 𝑦 ) ) ) → 𝑥 ∈ No )
160 158 159 mulscld ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝑥 ) ∧ 𝑤 ∈ ( L ‘ 𝑦 ) ) ) → ( 𝑤 ·s 𝑥 ) ∈ No )
161 157 160 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 𝑣 ) ) )
162 154 161 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 𝑣 ) ) )
163 oveq1 ⊢ ( 𝑥𝑂 = 𝑣 → ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑣 ·s 𝑦𝑂 ) )
164 oveq2 ⊢ ( 𝑥𝑂 = 𝑣 → ( 𝑦𝑂 ·s 𝑥𝑂 ) = ( 𝑦𝑂 ·s 𝑣 ) )
165 163 164 eqeq12d ⊢ ( 𝑥𝑂 = 𝑣 → ( ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ↔ ( 𝑣 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑣 ) ) )
166 oveq2 ⊢ ( 𝑦𝑂 = 𝑤 → ( 𝑣 ·s 𝑦𝑂 ) = ( 𝑣 ·s 𝑤 ) )
167 oveq1 ⊢ ( 𝑦𝑂 = 𝑤 → ( 𝑦𝑂 ·s 𝑣 ) = ( 𝑤 ·s 𝑣 ) )
168 166 167 eqeq12d ⊢ ( 𝑦𝑂 = 𝑤 → ( ( 𝑣 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑣 ) ↔ ( 𝑣 ·s 𝑤 ) = ( 𝑤 ·s 𝑣 ) ) )
169 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 𝑥𝑂 ) )
170 165 168 169 144 152 rspc2dv ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝑥 ) ∧ 𝑤 ∈ ( L ‘ 𝑦 ) ) ) → ( 𝑣 ·s 𝑤 ) = ( 𝑤 ·s 𝑣 ) )
171 162 170 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 𝑣 ) ) )
172 171 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 𝑣 ) ) ) )
173 172 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 𝑣 ) ) ) )
174 rexcom ⊢ ( ∃ 𝑣 ∈ ( R ‘ 𝑥 ) ∃ 𝑤 ∈ ( L ‘ 𝑦 ) 𝑑 = ( ( ( 𝑤 ·s 𝑥 ) +s ( 𝑦 ·s 𝑣 ) ) -s ( 𝑤 ·s 𝑣 ) ) ↔ ∃ 𝑤 ∈ ( L ‘ 𝑦 ) ∃ 𝑣 ∈ ( R ‘ 𝑥 ) 𝑑 = ( ( ( 𝑤 ·s 𝑥 ) +s ( 𝑦 ·s 𝑣 ) ) -s ( 𝑤 ·s 𝑣 ) ) )
175 173 174 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 𝑣 ) ) ) )
176 175 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 𝑣 ) ) } )
177 137 176 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 𝑣 ) ) } ) )
178 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 𝑡 ) ) } )
179 177 178 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 𝑡 ) ) } ) )
180 98 179 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 𝑡 ) ) } ) ) )
181 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 𝑤 ) ) } ) ) )
182 181 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 𝑤 ) ) } ) ) )
183 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 𝑡 ) ) } ) ) )
184 183 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 𝑡 ) ) } ) ) )
185 184 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 𝑡 ) ) } ) ) )
186 180 182 185 3eqtr4d ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥𝑂 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑦 ·s 𝑥𝑂 ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑦𝑂 ·s 𝑥 ) ) ) → ( 𝑥 ·s 𝑦 ) = ( 𝑦 ·s 𝑥 ) )
187 186 ex ⊢ ( ( 𝑥 ∈ 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 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ·s 𝐵 ) = ( 𝐵 ·s 𝐴 ) )