Theorem mulscom 28149

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  {cab 2717  ∀wral 3053  ∃wrex 3063   ∪ cun 3881  ‘cfv 6485  (class class class)co 7356   No csur 27621   |s ccuts 27769   L cleft 27835   R cright 27836   +_s cadds 27969   -_s csubs 28030   ·_s cmuls 28116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-ot 4564  df-uni 4839  df-int 4878  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-se 5572  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-1o 8395  df-2o 8396  df-nadd 8592  df-no 27624  df-lts 27625  df-bday 27626  df-les 27727  df-slts 27768  df-cuts 27770  df-0s 27817  df-made 27837  df-old 27838  df-left 27840  df-right 27841  df-norec 27948  df-norec2 27959  df-adds 27970  df-negs 28031  df-subs 28032  df-muls 28117

This theorem is referenced by:  mulscomd  28150  muls02  28151  mulslid  28152