Theorem mulscom 27943

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 7408	. . 3 ⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s 𝑦) = (𝑥𝑂 ·s 𝑦))
2		oveq2 7409	. . 3 ⊢ (𝑥 = 𝑥𝑂 → (𝑦 ·s 𝑥) = (𝑦 ·s 𝑥𝑂))
3	1, 2	eqeq12d 2740	. 2 ⊢ (𝑥 = 𝑥𝑂 → ((𝑥 ·s 𝑦) = (𝑦 ·s 𝑥) ↔ (𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂)))
4		oveq2 7409	. . 3 ⊢ (𝑦 = 𝑦𝑂 → (𝑥𝑂 ·s 𝑦) = (𝑥𝑂 ·s 𝑦𝑂))
5		oveq1 7408	. . 3 ⊢ (𝑦 = 𝑦𝑂 → (𝑦 ·s 𝑥𝑂) = (𝑦𝑂 ·s 𝑥𝑂))
6	4, 5	eqeq12d 2740	. 2 ⊢ (𝑦 = 𝑦𝑂 → ((𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ↔ (𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂)))
7		oveq1 7408	. . 3 ⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s 𝑦𝑂) = (𝑥𝑂 ·s 𝑦𝑂))
8		oveq2 7409	. . 3 ⊢ (𝑥 = 𝑥𝑂 → (𝑦𝑂 ·s 𝑥) = (𝑦𝑂 ·s 𝑥𝑂))
9	7, 8	eqeq12d 2740	. 2 ⊢ (𝑥 = 𝑥𝑂 → ((𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥) ↔ (𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂)))
10		oveq1 7408	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ·s 𝑦) = (𝐴 ·s 𝑦))
11		oveq2 7409	. . 3 ⊢ (𝑥 = 𝐴 → (𝑦 ·s 𝑥) = (𝑦 ·s 𝐴))
12	10, 11	eqeq12d 2740	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ·s 𝑦) = (𝑦 ·s 𝑥) ↔ (𝐴 ·s 𝑦) = (𝑦 ·s 𝐴)))
13		oveq2 7409	. . 3 ⊢ (𝑦 = 𝐵 → (𝐴 ·s 𝑦) = (𝐴 ·s 𝐵))
14		oveq1 7408	. . 3 ⊢ (𝑦 = 𝐵 → (𝑦 ·s 𝐴) = (𝐵 ·s 𝐴))
15	13, 14	eqeq12d 2740	. 2 ⊢ (𝑦 = 𝐵 → ((𝐴 ·s 𝑦) = (𝑦 ·s 𝐴) ↔ (𝐴 ·s 𝐵) = (𝐵 ·s 𝐴)))
16		oveq1 7408	. . . . . . . . . . . . . . 15 ⊢ (𝑥𝑂 = 𝑝 → (𝑥𝑂 ·s 𝑦) = (𝑝 ·s 𝑦))
17		oveq2 7409	. . . . . . . . . . . . . . 15 ⊢ (𝑥𝑂 = 𝑝 → (𝑦 ·s 𝑥𝑂) = (𝑦 ·s 𝑝))
18	16, 17	eqeq12d 2740	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑂 = 𝑝 → ((𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ↔ (𝑝 ·s 𝑦) = (𝑦 ·s 𝑝)))
19		simplr2 1213	. . . . . . . . . . . . . 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 768	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → 𝑝 ∈ ( L ‘𝑥))
21		elun1 4168	. . . . . . . . . . . . . . 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 3605	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → (𝑝 ·s 𝑦) = (𝑦 ·s 𝑝))
24		oveq2 7409	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑞 → (𝑥 ·s 𝑦𝑂) = (𝑥 ·s 𝑞))
25		oveq1 7408	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑞 → (𝑦𝑂 ·s 𝑥) = (𝑞 ·s 𝑥))
26	24, 25	eqeq12d 2740	. . . . . . . . . . . . . 14 ⊢ (𝑦𝑂 = 𝑞 → ((𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥) ↔ (𝑥 ·s 𝑞) = (𝑞 ·s 𝑥)))
27		simplr3 1214	. . . . . . . . . . . . . 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 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → 𝑞 ∈ ( L ‘𝑦))
29		elun1 4168	. . . . . . . . . . . . . . 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 3605	. . . . . . . . . . . . 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 7419	. . . . . . . . . . . 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 773	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → 𝑦 ∈ No )
34		leftssno 27711	. . . . . . . . . . . . . . 15 ⊢ ( L ‘𝑥) ⊆ No
35	34, 20	sselid 3972	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → 𝑝 ∈ No )
36	33, 35	mulscld 27939	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → (𝑦 ·s 𝑝) ∈ No )
37		leftssno 27711	. . . . . . . . . . . . . . 15 ⊢ ( L ‘𝑦) ⊆ No
38	37, 28	sselid 3972	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → 𝑞 ∈ No )
39		simplll 772	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑝 ∈ ( L ‘𝑥) ∧ 𝑞 ∈ ( L ‘𝑦))) → 𝑥 ∈ No )
40	38, 39	mulscld 27939	. . . . . . . . . . . . 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 27788	. . . . . . . . . . . 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 2764	. . . . . . . . . . 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 7408	. . . . . . . . . . . . 13 ⊢ (𝑥𝑂 = 𝑝 → (𝑥𝑂 ·s 𝑦𝑂) = (𝑝 ·s 𝑦𝑂))
44		oveq2 7409	. . . . . . . . . . . . 13 ⊢ (𝑥𝑂 = 𝑝 → (𝑦𝑂 ·s 𝑥𝑂) = (𝑦𝑂 ·s 𝑝))
45	43, 44	eqeq12d 2740	. . . . . . . . . . . 12 ⊢ (𝑥𝑂 = 𝑝 → ((𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ↔ (𝑝 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑝)))
46		oveq2 7409	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑞 → (𝑝 ·s 𝑦𝑂) = (𝑝 ·s 𝑞))
47		oveq1 7408	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑞 → (𝑦𝑂 ·s 𝑝) = (𝑞 ·s 𝑝))
48	46, 47	eqeq12d 2740	. . . . . . . . . . . 12 ⊢ (𝑦𝑂 = 𝑞 → ((𝑝 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑝) ↔ (𝑝 ·s 𝑞) = (𝑞 ·s 𝑝)))
49		simplr1 1212	. . . . . . . . . . . 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 3618	. . . . . . . . . . 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 7419	. . . . . . . . . 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 2735	. . . . . . . . 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 3209	. . . . . . . 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 3279	. . . . . . . 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 2793	. . . . . 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 7408	. . . . . . . . . . . . . . 15 ⊢ (𝑥𝑂 = 𝑟 → (𝑥𝑂 ·s 𝑦) = (𝑟 ·s 𝑦))
58		oveq2 7409	. . . . . . . . . . . . . . 15 ⊢ (𝑥𝑂 = 𝑟 → (𝑦 ·s 𝑥𝑂) = (𝑦 ·s 𝑟))
59	57, 58	eqeq12d 2740	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑂 = 𝑟 → ((𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ↔ (𝑟 ·s 𝑦) = (𝑦 ·s 𝑟)))
60		simplr2 1213	. . . . . . . . . . . . . 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 768	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → 𝑟 ∈ ( R ‘𝑥))
62		elun2 4169	. . . . . . . . . . . . . . 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 3605	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → (𝑟 ·s 𝑦) = (𝑦 ·s 𝑟))
65		oveq2 7409	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑠 → (𝑥 ·s 𝑦𝑂) = (𝑥 ·s 𝑠))
66		oveq1 7408	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑠 → (𝑦𝑂 ·s 𝑥) = (𝑠 ·s 𝑥))
67	65, 66	eqeq12d 2740	. . . . . . . . . . . . . 14 ⊢ (𝑦𝑂 = 𝑠 → ((𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥) ↔ (𝑥 ·s 𝑠) = (𝑠 ·s 𝑥)))
68		simplr3 1214	. . . . . . . . . . . . . 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 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → 𝑠 ∈ ( R ‘𝑦))
70		elun2 4169	. . . . . . . . . . . . . . 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 3605	. . . . . . . . . . . . 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 7419	. . . . . . . . . . . 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 773	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → 𝑦 ∈ No )
75		rightssno 27712	. . . . . . . . . . . . . . 15 ⊢ ( R ‘𝑥) ⊆ No
76	75, 61	sselid 3972	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → 𝑟 ∈ No )
77	74, 76	mulscld 27939	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → (𝑦 ·s 𝑟) ∈ No )
78		rightssno 27712	. . . . . . . . . . . . . . 15 ⊢ ( R ‘𝑦) ⊆ No
79	78, 69	sselid 3972	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → 𝑠 ∈ No )
80		simplll 772	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑟 ∈ ( R ‘𝑥) ∧ 𝑠 ∈ ( R ‘𝑦))) → 𝑥 ∈ No )
81	79, 80	mulscld 27939	. . . . . . . . . . . . 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 27788	. . . . . . . . . . . 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 2764	. . . . . . . . . . 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 7408	. . . . . . . . . . . . 13 ⊢ (𝑥𝑂 = 𝑟 → (𝑥𝑂 ·s 𝑦𝑂) = (𝑟 ·s 𝑦𝑂))
85		oveq2 7409	. . . . . . . . . . . . 13 ⊢ (𝑥𝑂 = 𝑟 → (𝑦𝑂 ·s 𝑥𝑂) = (𝑦𝑂 ·s 𝑟))
86	84, 85	eqeq12d 2740	. . . . . . . . . . . 12 ⊢ (𝑥𝑂 = 𝑟 → ((𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ↔ (𝑟 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑟)))
87		oveq2 7409	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑠 → (𝑟 ·s 𝑦𝑂) = (𝑟 ·s 𝑠))
88		oveq1 7408	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑠 → (𝑦𝑂 ·s 𝑟) = (𝑠 ·s 𝑟))
89	87, 88	eqeq12d 2740	. . . . . . . . . . . 12 ⊢ (𝑦𝑂 = 𝑠 → ((𝑟 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑟) ↔ (𝑟 ·s 𝑠) = (𝑠 ·s 𝑟)))
90		simplr1 1212	. . . . . . . . . . . 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 3618	. . . . . . . . . . 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 7419	. . . . . . . . . 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 2735	. . . . . . . . 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 3209	. . . . . . . 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 3279	. . . . . . . 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 2793	. . . . . 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 4156	. . . . 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 7408	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝑂 = 𝑡 → (𝑥𝑂 ·s 𝑦) = (𝑡 ·s 𝑦))
100		oveq2 7409	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝑂 = 𝑡 → (𝑦 ·s 𝑥𝑂) = (𝑦 ·s 𝑡))
101	99, 100	eqeq12d 2740	. . . . . . . . . . . . . . 15 ⊢ (𝑥𝑂 = 𝑡 → ((𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ↔ (𝑡 ·s 𝑦) = (𝑦 ·s 𝑡)))
102		simplr2 1213	. . . . . . . . . . . . . . 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 768	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → 𝑡 ∈ ( L ‘𝑥))
104		elun1 4168	. . . . . . . . . . . . . . . 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 3605	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → (𝑡 ·s 𝑦) = (𝑦 ·s 𝑡))
107		oveq2 7409	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑂 = 𝑢 → (𝑥 ·s 𝑦𝑂) = (𝑥 ·s 𝑢))
108		oveq1 7408	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑂 = 𝑢 → (𝑦𝑂 ·s 𝑥) = (𝑢 ·s 𝑥))
109	107, 108	eqeq12d 2740	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑢 → ((𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥) ↔ (𝑥 ·s 𝑢) = (𝑢 ·s 𝑥)))
110		simplr3 1214	. . . . . . . . . . . . . . 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 770	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → 𝑢 ∈ ( R ‘𝑦))
112		elun2 4169	. . . . . . . . . . . . . . . 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 3605	. . . . . . . . . . . . . 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 7419	. . . . . . . . . . . . 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 773	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → 𝑦 ∈ No )
117	34, 103	sselid 3972	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → 𝑡 ∈ No )
118	116, 117	mulscld 27939	. . . . . . . . . . . . . 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 3972	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → 𝑢 ∈ No )
120		simplll 772	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑡 ∈ ( L ‘𝑥) ∧ 𝑢 ∈ ( R ‘𝑦))) → 𝑥 ∈ No )
121	119, 120	mulscld 27939	. . . . . . . . . . . . . 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 27788	. . . . . . . . . . . . 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 2764	. . . . . . . . . . . 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 7408	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑂 = 𝑡 → (𝑥𝑂 ·s 𝑦𝑂) = (𝑡 ·s 𝑦𝑂))
125		oveq2 7409	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑂 = 𝑡 → (𝑦𝑂 ·s 𝑥𝑂) = (𝑦𝑂 ·s 𝑡))
126	124, 125	eqeq12d 2740	. . . . . . . . . . . . 13 ⊢ (𝑥𝑂 = 𝑡 → ((𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ↔ (𝑡 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑡)))
127		oveq2 7409	. . . . . . . . . . . . . 14 ⊢ (𝑦𝑂 = 𝑢 → (𝑡 ·s 𝑦𝑂) = (𝑡 ·s 𝑢))
128		oveq1 7408	. . . . . . . . . . . . . 14 ⊢ (𝑦𝑂 = 𝑢 → (𝑦𝑂 ·s 𝑡) = (𝑢 ·s 𝑡))
129	127, 128	eqeq12d 2740	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑢 → ((𝑡 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑡) ↔ (𝑡 ·s 𝑢) = (𝑢 ·s 𝑡)))
130		simplr1 1212	. . . . . . . . . . . . 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 3618	. . . . . . . . . . . 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 7419	. . . . . . . . . . 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 2735	. . . . . . . . . 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 3209	. . . . . . . . 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 3279	. . . . . . . . 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 2793	. . . . . . 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 7408	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝑂 = 𝑣 → (𝑥𝑂 ·s 𝑦) = (𝑣 ·s 𝑦))
139		oveq2 7409	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝑂 = 𝑣 → (𝑦 ·s 𝑥𝑂) = (𝑦 ·s 𝑣))
140	138, 139	eqeq12d 2740	. . . . . . . . . . . . . . 15 ⊢ (𝑥𝑂 = 𝑣 → ((𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ↔ (𝑣 ·s 𝑦) = (𝑦 ·s 𝑣)))
141		simplr2 1213	. . . . . . . . . . . . . . 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 768	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → 𝑣 ∈ ( R ‘𝑥))
143		elun2 4169	. . . . . . . . . . . . . . . 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 3605	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → (𝑣 ·s 𝑦) = (𝑦 ·s 𝑣))
146		oveq2 7409	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑂 = 𝑤 → (𝑥 ·s 𝑦𝑂) = (𝑥 ·s 𝑤))
147		oveq1 7408	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑂 = 𝑤 → (𝑦𝑂 ·s 𝑥) = (𝑤 ·s 𝑥))
148	146, 147	eqeq12d 2740	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑤 → ((𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥) ↔ (𝑥 ·s 𝑤) = (𝑤 ·s 𝑥)))
149		simplr3 1214	. . . . . . . . . . . . . . 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 770	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → 𝑤 ∈ ( L ‘𝑦))
151		elun1 4168	. . . . . . . . . . . . . . . 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 3605	. . . . . . . . . . . . . 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 7419	. . . . . . . . . . . . 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 773	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → 𝑦 ∈ No )
156	75, 142	sselid 3972	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → 𝑣 ∈ No )
157	155, 156	mulscld 27939	. . . . . . . . . . . . . 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 3972	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → 𝑤 ∈ No )
159		simplll 772	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑣 ∈ ( R ‘𝑥) ∧ 𝑤 ∈ ( L ‘𝑦))) → 𝑥 ∈ No )
160	158, 159	mulscld 27939	. . . . . . . . . . . . . 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 27788	. . . . . . . . . . . . 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 2764	. . . . . . . . . . . 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 7408	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑂 = 𝑣 → (𝑥𝑂 ·s 𝑦𝑂) = (𝑣 ·s 𝑦𝑂))
164		oveq2 7409	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑂 = 𝑣 → (𝑦𝑂 ·s 𝑥𝑂) = (𝑦𝑂 ·s 𝑣))
165	163, 164	eqeq12d 2740	. . . . . . . . . . . . 13 ⊢ (𝑥𝑂 = 𝑣 → ((𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ↔ (𝑣 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑣)))
166		oveq2 7409	. . . . . . . . . . . . . 14 ⊢ (𝑦𝑂 = 𝑤 → (𝑣 ·s 𝑦𝑂) = (𝑣 ·s 𝑤))
167		oveq1 7408	. . . . . . . . . . . . . 14 ⊢ (𝑦𝑂 = 𝑤 → (𝑦𝑂 ·s 𝑣) = (𝑤 ·s 𝑣))
168	166, 167	eqeq12d 2740	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑤 → ((𝑣 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑣) ↔ (𝑣 ·s 𝑤) = (𝑤 ·s 𝑣)))
169		simplr1 1212	. . . . . . . . . . . . 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 3618	. . . . . . . . . . . 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 7419	. . . . . . . . . . 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 2735	. . . . . . . . . 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 3209	. . . . . . . . 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 3279	. . . . . . . . 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 2793	. . . . . . 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 4156	. . . . . 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 4145	. . . . . 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 2780	. . . . 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 7419	. . . 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 27913	. . . . 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 27913	. . . . . 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 2774	. . 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 27776	1 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ·s 𝐵) = (𝐵 ·s 𝐴))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  {cab 2701  ∀wral 3053  ∃wrex 3062   ∪ cun 3938  ‘cfv 6533  (class class class)co 7401   No csur 27477   |s cscut 27619   L cleft 27676   R cright 27677   +_s cadds 27780   -_s csubs 27837   ·_s cmuls 27910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-ot 4629  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-1o 8461  df-2o 8462  df-nadd 8660  df-no 27480  df-slt 27481  df-bday 27482  df-sle 27582  df-sslt 27618  df-scut 27620  df-0s 27661  df-made 27678  df-old 27679  df-left 27681  df-right 27682  df-norec 27759  df-norec2 27770  df-adds 27781  df-negs 27838  df-subs 27839  df-muls 27911

This theorem is referenced by:  mulscomd  27944  muls02  27945  mulslid  27946