Theorem mulscom 28166

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

Assertion

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

Proof of Theorem mulscom

Dummy variables 𝑥 𝑦 𝑥_𝑂 𝑦_𝑂 𝑎 𝑏 𝑐 𝑑 𝑝 𝑞 𝑟 𝑠 𝑡 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  {cab 2713  ∀wral 3060  ∃wrex 3069   ∪ cun 3948  ‘cfv 6560  (class class class)co 7432   No csur 27685   |s cscut 27828   L cleft 27885   R cright 27886   +_s cadds 27993   -_s csubs 28053   ·_s cmuls 28133

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-ot 4634  df-uni 4907  df-int 4946  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-se 5637  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-1st 8015  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-1o 8507  df-2o 8508  df-nadd 8705  df-no 27688  df-slt 27689  df-bday 27690  df-sle 27791  df-sslt 27827  df-scut 27829  df-0s 27870  df-made 27887  df-old 27888  df-left 27890  df-right 27891  df-norec 27972  df-norec2 27983  df-adds 27994  df-negs 28054  df-subs 28055  df-muls 28134

This theorem is referenced by:  mulscomd  28167  muls02  28168  mulslid  28169