Theorem mulscom 28078

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 7353	. . 3 ⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s 𝑦) = (𝑥𝑂 ·s 𝑦))
2		oveq2 7354	. . 3 ⊢ (𝑥 = 𝑥𝑂 → (𝑦 ·s 𝑥) = (𝑦 ·s 𝑥𝑂))
3	1, 2	eqeq12d 2747	. 2 ⊢ (𝑥 = 𝑥𝑂 → ((𝑥 ·s 𝑦) = (𝑦 ·s 𝑥) ↔ (𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂)))
4		oveq2 7354	. . 3 ⊢ (𝑦 = 𝑦𝑂 → (𝑥𝑂 ·s 𝑦) = (𝑥𝑂 ·s 𝑦𝑂))
5		oveq1 7353	. . 3 ⊢ (𝑦 = 𝑦𝑂 → (𝑦 ·s 𝑥𝑂) = (𝑦𝑂 ·s 𝑥𝑂))
6	4, 5	eqeq12d 2747	. 2 ⊢ (𝑦 = 𝑦𝑂 → ((𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ↔ (𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂)))
7		oveq1 7353	. . 3 ⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s 𝑦𝑂) = (𝑥𝑂 ·s 𝑦𝑂))
8		oveq2 7354	. . 3 ⊢ (𝑥 = 𝑥𝑂 → (𝑦𝑂 ·s 𝑥) = (𝑦𝑂 ·s 𝑥𝑂))
9	7, 8	eqeq12d 2747	. 2 ⊢ (𝑥 = 𝑥𝑂 → ((𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥) ↔ (𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂)))
10		oveq1 7353	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ·s 𝑦) = (𝐴 ·s 𝑦))
11		oveq2 7354	. . 3 ⊢ (𝑥 = 𝐴 → (𝑦 ·s 𝑥) = (𝑦 ·s 𝐴))
12	10, 11	eqeq12d 2747	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ·s 𝑦) = (𝑦 ·s 𝑥) ↔ (𝐴 ·s 𝑦) = (𝑦 ·s 𝐴)))
13		oveq2 7354	. . 3 ⊢ (𝑦 = 𝐵 → (𝐴 ·s 𝑦) = (𝐴 ·s 𝐵))
14		oveq1 7353	. . 3 ⊢ (𝑦 = 𝐵 → (𝑦 ·s 𝐴) = (𝐵 ·s 𝐴))
15	13, 14	eqeq12d 2747	. 2 ⊢ (𝑦 = 𝐵 → ((𝐴 ·s 𝑦) = (𝑦 ·s 𝐴) ↔ (𝐴 ·s 𝐵) = (𝐵 ·s 𝐴)))
16		oveq1 7353	. . . . . . . . . . . . . . 15 ⊢ (𝑥𝑂 = 𝑝 → (𝑥𝑂 ·s 𝑦) = (𝑝 ·s 𝑦))
17		oveq2 7354	. . . . . . . . . . . . . . 15 ⊢ (𝑥𝑂 = 𝑝 → (𝑦 ·s 𝑥𝑂) = (𝑦 ·s 𝑝))
18	16, 17	eqeq12d 2747	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑂 = 𝑝 → ((𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ↔ (𝑝 ·s 𝑦) = (𝑦 ·s 𝑝)))
19		simplr2 1217	. . . . . . . . . . . . . 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 4129	. . . . . . . . . . . . . . 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 3573	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → (𝑝 ·s 𝑦) = (𝑦 ·s 𝑝))
24		oveq2 7354	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑞 → (𝑥 ·s 𝑦𝑂) = (𝑥 ·s 𝑞))
25		oveq1 7353	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑞 → (𝑦𝑂 ·s 𝑥) = (𝑞 ·s 𝑥))
26	24, 25	eqeq12d 2747	. . . . . . . . . . . . . 14 ⊢ (𝑦𝑂 = 𝑞 → ((𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥) ↔ (𝑥 ·s 𝑞) = (𝑞 ·s 𝑥)))
27		simplr3 1218	. . . . . . . . . . . . . 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 4129	. . . . . . . . . . . . . . 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 3573	. . . . . . . . . . . . 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 7364	. . . . . . . . . . . 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 27826	. . . . . . . . . . . . . . 15 ⊢ ( L ‘𝑥) ⊆ No
35	34, 20	sselid 3927	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → 𝑝 ∈ No )
36	33, 35	mulscld 28074	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → (𝑦 ·s 𝑝) ∈ No )
37		leftssno 27826	. . . . . . . . . . . . . . 15 ⊢ ( L ‘𝑦) ⊆ No
38	37, 28	sselid 3927	. . . . . . . . . . . . . 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 28074	. . . . . . . . . . . . 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 27910	. . . . . . . . . . . 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 2766	. . . . . . . . . . 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 7353	. . . . . . . . . . . . 13 ⊢ (𝑥𝑂 = 𝑝 → (𝑥𝑂 ·s 𝑦𝑂) = (𝑝 ·s 𝑦𝑂))
44		oveq2 7354	. . . . . . . . . . . . 13 ⊢ (𝑥𝑂 = 𝑝 → (𝑦𝑂 ·s 𝑥𝑂) = (𝑦𝑂 ·s 𝑝))
45	43, 44	eqeq12d 2747	. . . . . . . . . . . 12 ⊢ (𝑥𝑂 = 𝑝 → ((𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ↔ (𝑝 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑝)))
46		oveq2 7354	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑞 → (𝑝 ·s 𝑦𝑂) = (𝑝 ·s 𝑞))
47		oveq1 7353	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑞 → (𝑦𝑂 ·s 𝑝) = (𝑞 ·s 𝑝))
48	46, 47	eqeq12d 2747	. . . . . . . . . . . 12 ⊢ (𝑦𝑂 = 𝑞 → ((𝑝 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑝) ↔ (𝑝 ·s 𝑞) = (𝑞 ·s 𝑝)))
49		simplr1 1216	. . . . . . . . . . . 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 3587	. . . . . . . . . . 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 7364	. . . . . . . . . 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 2742	. . . . . . . . 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 3195	. . . . . . . 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 3261	. . . . . . . 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 2797	. . . . . 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 7353	. . . . . . . . . . . . . . 15 ⊢ (𝑥𝑂 = 𝑟 → (𝑥𝑂 ·s 𝑦) = (𝑟 ·s 𝑦))
58		oveq2 7354	. . . . . . . . . . . . . . 15 ⊢ (𝑥𝑂 = 𝑟 → (𝑦 ·s 𝑥𝑂) = (𝑦 ·s 𝑟))
59	57, 58	eqeq12d 2747	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑂 = 𝑟 → ((𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ↔ (𝑟 ·s 𝑦) = (𝑦 ·s 𝑟)))
60		simplr2 1217	. . . . . . . . . . . . . 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 4130	. . . . . . . . . . . . . . 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 3573	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → (𝑟 ·s 𝑦) = (𝑦 ·s 𝑟))
65		oveq2 7354	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑠 → (𝑥 ·s 𝑦𝑂) = (𝑥 ·s 𝑠))
66		oveq1 7353	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑠 → (𝑦𝑂 ·s 𝑥) = (𝑠 ·s 𝑥))
67	65, 66	eqeq12d 2747	. . . . . . . . . . . . . 14 ⊢ (𝑦𝑂 = 𝑠 → ((𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥) ↔ (𝑥 ·s 𝑠) = (𝑠 ·s 𝑥)))
68		simplr3 1218	. . . . . . . . . . . . . 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 4130	. . . . . . . . . . . . . . 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 3573	. . . . . . . . . . . . 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 7364	. . . . . . . . . . . 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 27827	. . . . . . . . . . . . . . 15 ⊢ ( R ‘𝑥) ⊆ No
76	75, 61	sselid 3927	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → 𝑟 ∈ No )
77	74, 76	mulscld 28074	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → (𝑦 ·s 𝑟) ∈ No )
78		rightssno 27827	. . . . . . . . . . . . . . 15 ⊢ ( R ‘𝑦) ⊆ No
79	78, 69	sselid 3927	. . . . . . . . . . . . . 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 28074	. . . . . . . . . . . . 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 27910	. . . . . . . . . . . 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 2766	. . . . . . . . . . 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 7353	. . . . . . . . . . . . 13 ⊢ (𝑥𝑂 = 𝑟 → (𝑥𝑂 ·s 𝑦𝑂) = (𝑟 ·s 𝑦𝑂))
85		oveq2 7354	. . . . . . . . . . . . 13 ⊢ (𝑥𝑂 = 𝑟 → (𝑦𝑂 ·s 𝑥𝑂) = (𝑦𝑂 ·s 𝑟))
86	84, 85	eqeq12d 2747	. . . . . . . . . . . 12 ⊢ (𝑥𝑂 = 𝑟 → ((𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ↔ (𝑟 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑟)))
87		oveq2 7354	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑠 → (𝑟 ·s 𝑦𝑂) = (𝑟 ·s 𝑠))
88		oveq1 7353	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑠 → (𝑦𝑂 ·s 𝑟) = (𝑠 ·s 𝑟))
89	87, 88	eqeq12d 2747	. . . . . . . . . . . 12 ⊢ (𝑦𝑂 = 𝑠 → ((𝑟 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑟) ↔ (𝑟 ·s 𝑠) = (𝑠 ·s 𝑟)))
90		simplr1 1216	. . . . . . . . . . . 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 3587	. . . . . . . . . . 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 7364	. . . . . . . . . 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 2742	. . . . . . . . 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 3195	. . . . . . . 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 3261	. . . . . . . 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 2797	. . . . . 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 4116	. . . . 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 7353	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝑂 = 𝑡 → (𝑥𝑂 ·s 𝑦) = (𝑡 ·s 𝑦))
100		oveq2 7354	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝑂 = 𝑡 → (𝑦 ·s 𝑥𝑂) = (𝑦 ·s 𝑡))
101	99, 100	eqeq12d 2747	. . . . . . . . . . . . . . 15 ⊢ (𝑥𝑂 = 𝑡 → ((𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ↔ (𝑡 ·s 𝑦) = (𝑦 ·s 𝑡)))
102		simplr2 1217	. . . . . . . . . . . . . . 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 4129	. . . . . . . . . . . . . . . 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 3573	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → (𝑡 ·s 𝑦) = (𝑦 ·s 𝑡))
107		oveq2 7354	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑂 = 𝑢 → (𝑥 ·s 𝑦𝑂) = (𝑥 ·s 𝑢))
108		oveq1 7353	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑂 = 𝑢 → (𝑦𝑂 ·s 𝑥) = (𝑢 ·s 𝑥))
109	107, 108	eqeq12d 2747	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑢 → ((𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥) ↔ (𝑥 ·s 𝑢) = (𝑢 ·s 𝑥)))
110		simplr3 1218	. . . . . . . . . . . . . . 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 4130	. . . . . . . . . . . . . . . 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 3573	. . . . . . . . . . . . . 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 7364	. . . . . . . . . . . . 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 3927	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → 𝑡 ∈ No )
118	116, 117	mulscld 28074	. . . . . . . . . . . . . 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 3927	. . . . . . . . . . . . . . 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 28074	. . . . . . . . . . . . . 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 27910	. . . . . . . . . . . . 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 2766	. . . . . . . . . . . 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 7353	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑂 = 𝑡 → (𝑥𝑂 ·s 𝑦𝑂) = (𝑡 ·s 𝑦𝑂))
125		oveq2 7354	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑂 = 𝑡 → (𝑦𝑂 ·s 𝑥𝑂) = (𝑦𝑂 ·s 𝑡))
126	124, 125	eqeq12d 2747	. . . . . . . . . . . . 13 ⊢ (𝑥𝑂 = 𝑡 → ((𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ↔ (𝑡 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑡)))
127		oveq2 7354	. . . . . . . . . . . . . 14 ⊢ (𝑦𝑂 = 𝑢 → (𝑡 ·s 𝑦𝑂) = (𝑡 ·s 𝑢))
128		oveq1 7353	. . . . . . . . . . . . . 14 ⊢ (𝑦𝑂 = 𝑢 → (𝑦𝑂 ·s 𝑡) = (𝑢 ·s 𝑡))
129	127, 128	eqeq12d 2747	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑢 → ((𝑡 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑡) ↔ (𝑡 ·s 𝑢) = (𝑢 ·s 𝑡)))
130		simplr1 1216	. . . . . . . . . . . . 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 3587	. . . . . . . . . . . 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 7364	. . . . . . . . . . 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 2742	. . . . . . . . . 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 3195	. . . . . . . . 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 3261	. . . . . . . . 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 2797	. . . . . . 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 7353	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝑂 = 𝑣 → (𝑥𝑂 ·s 𝑦) = (𝑣 ·s 𝑦))
139		oveq2 7354	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝑂 = 𝑣 → (𝑦 ·s 𝑥𝑂) = (𝑦 ·s 𝑣))
140	138, 139	eqeq12d 2747	. . . . . . . . . . . . . . 15 ⊢ (𝑥𝑂 = 𝑣 → ((𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ↔ (𝑣 ·s 𝑦) = (𝑦 ·s 𝑣)))
141		simplr2 1217	. . . . . . . . . . . . . . 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 4130	. . . . . . . . . . . . . . . 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 3573	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → (𝑣 ·s 𝑦) = (𝑦 ·s 𝑣))
146		oveq2 7354	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑂 = 𝑤 → (𝑥 ·s 𝑦𝑂) = (𝑥 ·s 𝑤))
147		oveq1 7353	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑂 = 𝑤 → (𝑦𝑂 ·s 𝑥) = (𝑤 ·s 𝑥))
148	146, 147	eqeq12d 2747	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑤 → ((𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥) ↔ (𝑥 ·s 𝑤) = (𝑤 ·s 𝑥)))
149		simplr3 1218	. . . . . . . . . . . . . . 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 4129	. . . . . . . . . . . . . . . 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 3573	. . . . . . . . . . . . . 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 7364	. . . . . . . . . . . . 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 3927	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → 𝑣 ∈ No )
157	155, 156	mulscld 28074	. . . . . . . . . . . . . 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 3927	. . . . . . . . . . . . . . 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 28074	. . . . . . . . . . . . . 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 27910	. . . . . . . . . . . . 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 2766	. . . . . . . . . . . 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 7353	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑂 = 𝑣 → (𝑥𝑂 ·s 𝑦𝑂) = (𝑣 ·s 𝑦𝑂))
164		oveq2 7354	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑂 = 𝑣 → (𝑦𝑂 ·s 𝑥𝑂) = (𝑦𝑂 ·s 𝑣))
165	163, 164	eqeq12d 2747	. . . . . . . . . . . . 13 ⊢ (𝑥𝑂 = 𝑣 → ((𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ↔ (𝑣 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑣)))
166		oveq2 7354	. . . . . . . . . . . . . 14 ⊢ (𝑦𝑂 = 𝑤 → (𝑣 ·s 𝑦𝑂) = (𝑣 ·s 𝑤))
167		oveq1 7353	. . . . . . . . . . . . . 14 ⊢ (𝑦𝑂 = 𝑤 → (𝑦𝑂 ·s 𝑣) = (𝑤 ·s 𝑣))
168	166, 167	eqeq12d 2747	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑤 → ((𝑣 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑣) ↔ (𝑣 ·s 𝑤) = (𝑤 ·s 𝑣)))
169		simplr1 1216	. . . . . . . . . . . . 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 3587	. . . . . . . . . . . 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 7364	. . . . . . . . . . 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 2742	. . . . . . . . . 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 3195	. . . . . . . . 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 3261	. . . . . . . . 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 2797	. . . . . . 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 4116	. . . . . 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 4105	. . . . . 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 2782	. . . . 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 7364	. . . 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 28048	. . . . 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 28048	. . . . . 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 2776	. . 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 27898	1 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ·s 𝐵) = (𝐵 ·s 𝐴))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111  {cab 2709  ∀wral 3047  ∃wrex 3056   ∪ cun 3895  ‘cfv 6481  (class class class)co 7346   No csur 27578   |s cscut 27722   L cleft 27786   R cright 27787   +_s cadds 27902   -_s csubs 27962   ·_s cmuls 28045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5215  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-tp 4578  df-op 4580  df-ot 4582  df-uni 4857  df-int 4896  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-se 5568  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6248  df-ord 6309  df-on 6310  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-1st 7921  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-1o 8385  df-2o 8386  df-nadd 8581  df-no 27581  df-slt 27582  df-bday 27583  df-sle 27684  df-sslt 27721  df-scut 27723  df-0s 27768  df-made 27788  df-old 27789  df-left 27791  df-right 27792  df-norec 27881  df-norec2 27892  df-adds 27903  df-negs 27963  df-subs 27964  df-muls 28046

This theorem is referenced by:  mulscomd  28079  muls02  28080  mulslid  28081