Theorem mulscom 28537

Description: Surreal multiplication is commutative. 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 7434	. . 3 ⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s 𝑦) = (𝑥𝑂 ·s 𝑦))
2		oveq2 7435	. . 3 ⊢ (𝑥 = 𝑥𝑂 → (𝑦 ·s 𝑥) = (𝑦 ·s 𝑥𝑂))
3	1, 2	eqeq12d 2779	. 2 ⊢ (𝑥 = 𝑥𝑂 → ((𝑥 ·s 𝑦) = (𝑦 ·s 𝑥) ↔ (𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂)))
4		oveq2 7435	. . 3 ⊢ (𝑦 = 𝑦𝑂 → (𝑥𝑂 ·s 𝑦) = (𝑥𝑂 ·s 𝑦𝑂))
5		oveq1 7434	. . 3 ⊢ (𝑦 = 𝑦𝑂 → (𝑦 ·s 𝑥𝑂) = (𝑦𝑂 ·s 𝑥𝑂))
6	4, 5	eqeq12d 2779	. 2 ⊢ (𝑦 = 𝑦𝑂 → ((𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ↔ (𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂)))
7		oveq1 7434	. . 3 ⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s 𝑦𝑂) = (𝑥𝑂 ·s 𝑦𝑂))
8		oveq2 7435	. . 3 ⊢ (𝑥 = 𝑥𝑂 → (𝑦𝑂 ·s 𝑥) = (𝑦𝑂 ·s 𝑥𝑂))
9	7, 8	eqeq12d 2779	. 2 ⊢ (𝑥 = 𝑥𝑂 → ((𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥) ↔ (𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂)))
10		oveq1 7434	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ·s 𝑦) = (𝐴 ·s 𝑦))
11		oveq2 7435	. . 3 ⊢ (𝑥 = 𝐴 → (𝑦 ·s 𝑥) = (𝑦 ·s 𝐴))
12	10, 11	eqeq12d 2779	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ·s 𝑦) = (𝑦 ·s 𝑥) ↔ (𝐴 ·s 𝑦) = (𝑦 ·s 𝐴)))
13		oveq2 7435	. . 3 ⊢ (𝑦 = 𝐵 → (𝐴 ·s 𝑦) = (𝐴 ·s 𝐵))
14		oveq1 7434	. . 3 ⊢ (𝑦 = 𝐵 → (𝑦 ·s 𝐴) = (𝐵 ·s 𝐴))
15	13, 14	eqeq12d 2779	. 2 ⊢ (𝑦 = 𝐵 → ((𝐴 ·s 𝑦) = (𝑦 ·s 𝐴) ↔ (𝐴 ·s 𝐵) = (𝐵 ·s 𝐴)))
16		oveq1 7434	. . . . . . . . . . . . . . 15 ⊢ (𝑥𝑂 = 𝑝 → (𝑥𝑂 ·s 𝑦) = (𝑝 ·s 𝑦))
17		oveq2 7435	. . . . . . . . . . . . . . 15 ⊢ (𝑥𝑂 = 𝑝 → (𝑦 ·s 𝑥𝑂) = (𝑦 ·s 𝑝))
18	16, 17	eqeq12d 2779	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑂 = 𝑝 → ((𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ↔ (𝑝 ·s 𝑦) = (𝑦 ·s 𝑝)))
19		simplr2 1235	. . . . . . . . . . . . . 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 783	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑝 ∈ (L‘𝑥) ∧ 𝑞 ∈ (L‘𝑦))) → 𝑝 ∈ (L‘𝑥))
21		elun1 4182	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ (L‘𝑥) → 𝑝 ∈ ((L‘𝑥) ∪ (R‘𝑥)))
22	20, 21	syl 18	. . . . . . . . . . . . . 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 3580	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑝 ∈ (L‘𝑥) ∧ 𝑞 ∈ (L‘𝑦))) → (𝑝 ·s 𝑦) = (𝑦 ·s 𝑝))
24		oveq2 7435	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑞 → (𝑥 ·s 𝑦𝑂) = (𝑥 ·s 𝑞))
25		oveq1 7434	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑞 → (𝑦𝑂 ·s 𝑥) = (𝑞 ·s 𝑥))
26	24, 25	eqeq12d 2779	. . . . . . . . . . . . . 14 ⊢ (𝑦𝑂 = 𝑞 → ((𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥) ↔ (𝑥 ·s 𝑞) = (𝑞 ·s 𝑥)))
27		simplr3 1236	. . . . . . . . . . . . . 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 785	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑝 ∈ (L‘𝑥) ∧ 𝑞 ∈ (L‘𝑦))) → 𝑞 ∈ (L‘𝑦))
29		elun1 4182	. . . . . . . . . . . . . . 15 ⊢ (𝑞 ∈ (L‘𝑦) → 𝑞 ∈ ((L‘𝑦) ∪ (R‘𝑦)))
30	28, 29	syl 18	. . . . . . . . . . . . . 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 3580	. . . . . . . . . . . . 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 7445	. . . . . . . . . . . 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 788	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑝 ∈ (L‘𝑥) ∧ 𝑞 ∈ (L‘𝑦))) → 𝑦 ∈ No)
34	20	leftnod 28278	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑝 ∈ (L‘𝑥) ∧ 𝑞 ∈ (L‘𝑦))) → 𝑝 ∈ No)
35	33, 34	mulscld 28533	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑝 ∈ (L‘𝑥) ∧ 𝑞 ∈ (L‘𝑦))) → (𝑦 ·s 𝑝) ∈ No)
36	28	leftnod 28278	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑝 ∈ (L‘𝑥) ∧ 𝑞 ∈ (L‘𝑦))) → 𝑞 ∈ No)
37		simplll 787	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑝 ∈ (L‘𝑥) ∧ 𝑞 ∈ (L‘𝑦))) → 𝑥 ∈ No)
38	36, 37	mulscld 28533	. . . . . . . . . . . . 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 28365	. . . . . . . . . . . 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 2798	. . . . . . . . . . 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 7434	. . . . . . . . . . . . 13 ⊢ (𝑥𝑂 = 𝑝 → (𝑥𝑂 ·s 𝑦𝑂) = (𝑝 ·s 𝑦𝑂))
42		oveq2 7435	. . . . . . . . . . . . 13 ⊢ (𝑥𝑂 = 𝑝 → (𝑦𝑂 ·s 𝑥𝑂) = (𝑦𝑂 ·s 𝑝))
43	41, 42	eqeq12d 2779	. . . . . . . . . . . 12 ⊢ (𝑥𝑂 = 𝑝 → ((𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ↔ (𝑝 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑝)))
44		oveq2 7435	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑞 → (𝑝 ·s 𝑦𝑂) = (𝑝 ·s 𝑞))
45		oveq1 7434	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑞 → (𝑦𝑂 ·s 𝑝) = (𝑞 ·s 𝑝))
46	44, 45	eqeq12d 2779	. . . . . . . . . . . 12 ⊢ (𝑦𝑂 = 𝑞 → ((𝑝 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑝) ↔ (𝑝 ·s 𝑞) = (𝑞 ·s 𝑝)))
47		simplr1 1234	. . . . . . . . . . . 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 3593	. . . . . . . . . . 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 7445	. . . . . . . . . 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 2774	. . . . . . . . 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 3228	. . . . . . . 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 3294	. . . . . . . 8 ⊢ (∃𝑝 ∈ (L‘𝑥)∃𝑞 ∈ (L‘𝑦)𝑎 = (((𝑞 ·s 𝑥) +s (𝑦 ·s 𝑝)) −s (𝑞 ·s 𝑝)) ↔ ∃𝑞 ∈ (L‘𝑦)∃𝑝 ∈ (L‘𝑥)𝑎 = (((𝑞 ·s 𝑥) +s (𝑦 ·s 𝑝)) −s (𝑞 ·s 𝑝)))
53	51, 52	bitrdi 290	. . . . . . 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 2829	. . . . . 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 7434	. . . . . . . . . . . . . . 15 ⊢ (𝑥𝑂 = 𝑟 → (𝑥𝑂 ·s 𝑦) = (𝑟 ·s 𝑦))
56		oveq2 7435	. . . . . . . . . . . . . . 15 ⊢ (𝑥𝑂 = 𝑟 → (𝑦 ·s 𝑥𝑂) = (𝑦 ·s 𝑟))
57	55, 56	eqeq12d 2779	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑂 = 𝑟 → ((𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ↔ (𝑟 ·s 𝑦) = (𝑦 ·s 𝑟)))
58		simplr2 1235	. . . . . . . . . . . . . 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 783	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑟 ∈ (R‘𝑥) ∧ 𝑠 ∈ (R‘𝑦))) → 𝑟 ∈ (R‘𝑥))
60		elun2 4183	. . . . . . . . . . . . . . 15 ⊢ (𝑟 ∈ (R‘𝑥) → 𝑟 ∈ ((L‘𝑥) ∪ (R‘𝑥)))
61	59, 60	syl 18	. . . . . . . . . . . . . 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 3580	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑟 ∈ (R‘𝑥) ∧ 𝑠 ∈ (R‘𝑦))) → (𝑟 ·s 𝑦) = (𝑦 ·s 𝑟))
63		oveq2 7435	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑠 → (𝑥 ·s 𝑦𝑂) = (𝑥 ·s 𝑠))
64		oveq1 7434	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑠 → (𝑦𝑂 ·s 𝑥) = (𝑠 ·s 𝑥))
65	63, 64	eqeq12d 2779	. . . . . . . . . . . . . 14 ⊢ (𝑦𝑂 = 𝑠 → ((𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥) ↔ (𝑥 ·s 𝑠) = (𝑠 ·s 𝑥)))
66		simplr3 1236	. . . . . . . . . . . . . 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 785	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑟 ∈ (R‘𝑥) ∧ 𝑠 ∈ (R‘𝑦))) → 𝑠 ∈ (R‘𝑦))
68		elun2 4183	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ (R‘𝑦) → 𝑠 ∈ ((L‘𝑦) ∪ (R‘𝑦)))
69	67, 68	syl 18	. . . . . . . . . . . . . 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 3580	. . . . . . . . . . . . 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 7445	. . . . . . . . . . . 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 788	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑟 ∈ (R‘𝑥) ∧ 𝑠 ∈ (R‘𝑦))) → 𝑦 ∈ No)
73	59	rightnod 28280	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑟 ∈ (R‘𝑥) ∧ 𝑠 ∈ (R‘𝑦))) → 𝑟 ∈ No)
74	72, 73	mulscld 28533	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑟 ∈ (R‘𝑥) ∧ 𝑠 ∈ (R‘𝑦))) → (𝑦 ·s 𝑟) ∈ No)
75	67	rightnod 28280	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑟 ∈ (R‘𝑥) ∧ 𝑠 ∈ (R‘𝑦))) → 𝑠 ∈ No)
76		simplll 787	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑟 ∈ (R‘𝑥) ∧ 𝑠 ∈ (R‘𝑦))) → 𝑥 ∈ No)
77	75, 76	mulscld 28533	. . . . . . . . . . . . 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 28365	. . . . . . . . . . . 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 2798	. . . . . . . . . . 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 7434	. . . . . . . . . . . . 13 ⊢ (𝑥𝑂 = 𝑟 → (𝑥𝑂 ·s 𝑦𝑂) = (𝑟 ·s 𝑦𝑂))
81		oveq2 7435	. . . . . . . . . . . . 13 ⊢ (𝑥𝑂 = 𝑟 → (𝑦𝑂 ·s 𝑥𝑂) = (𝑦𝑂 ·s 𝑟))
82	80, 81	eqeq12d 2779	. . . . . . . . . . . 12 ⊢ (𝑥𝑂 = 𝑟 → ((𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ↔ (𝑟 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑟)))
83		oveq2 7435	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑠 → (𝑟 ·s 𝑦𝑂) = (𝑟 ·s 𝑠))
84		oveq1 7434	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑠 → (𝑦𝑂 ·s 𝑟) = (𝑠 ·s 𝑟))
85	83, 84	eqeq12d 2779	. . . . . . . . . . . 12 ⊢ (𝑦𝑂 = 𝑠 → ((𝑟 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑟) ↔ (𝑟 ·s 𝑠) = (𝑠 ·s 𝑟)))
86		simplr1 1234	. . . . . . . . . . . 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 3593	. . . . . . . . . . 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 7445	. . . . . . . . . 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 2774	. . . . . . . . 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 3228	. . . . . . . 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 3294	. . . . . . . 8 ⊢ (∃𝑟 ∈ (R‘𝑥)∃𝑠 ∈ (R‘𝑦)𝑏 = (((𝑠 ·s 𝑥) +s (𝑦 ·s 𝑟)) −s (𝑠 ·s 𝑟)) ↔ ∃𝑠 ∈ (R‘𝑦)∃𝑟 ∈ (R‘𝑥)𝑏 = (((𝑠 ·s 𝑥) +s (𝑦 ·s 𝑟)) −s (𝑠 ·s 𝑟)))
92	90, 91	bitrdi 290	. . . . . . 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 2829	. . . . . 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 4170	. . . . 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 7434	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝑂 = 𝑡 → (𝑥𝑂 ·s 𝑦) = (𝑡 ·s 𝑦))
96		oveq2 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝑂 = 𝑡 → (𝑦 ·s 𝑥𝑂) = (𝑦 ·s 𝑡))
97	95, 96	eqeq12d 2779	. . . . . . . . . . . . . . 15 ⊢ (𝑥𝑂 = 𝑡 → ((𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ↔ (𝑡 ·s 𝑦) = (𝑦 ·s 𝑡)))
98		simplr2 1235	. . . . . . . . . . . . . . 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 783	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑡 ∈ (L‘𝑥) ∧ 𝑢 ∈ (R‘𝑦))) → 𝑡 ∈ (L‘𝑥))
100		elun1 4182	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (L‘𝑥) → 𝑡 ∈ ((L‘𝑥) ∪ (R‘𝑥)))
101	99, 100	syl 18	. . . . . . . . . . . . . . 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 3580	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑡 ∈ (L‘𝑥) ∧ 𝑢 ∈ (R‘𝑦))) → (𝑡 ·s 𝑦) = (𝑦 ·s 𝑡))
103		oveq2 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑂 = 𝑢 → (𝑥 ·s 𝑦𝑂) = (𝑥 ·s 𝑢))
104		oveq1 7434	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑂 = 𝑢 → (𝑦𝑂 ·s 𝑥) = (𝑢 ·s 𝑥))
105	103, 104	eqeq12d 2779	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑢 → ((𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥) ↔ (𝑥 ·s 𝑢) = (𝑢 ·s 𝑥)))
106		simplr3 1236	. . . . . . . . . . . . . . 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 785	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑡 ∈ (L‘𝑥) ∧ 𝑢 ∈ (R‘𝑦))) → 𝑢 ∈ (R‘𝑦))
108		elun2 4183	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ (R‘𝑦) → 𝑢 ∈ ((L‘𝑦) ∪ (R‘𝑦)))
109	107, 108	syl 18	. . . . . . . . . . . . . . 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 3580	. . . . . . . . . . . . . 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 7445	. . . . . . . . . . . . 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 788	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑡 ∈ (L‘𝑥) ∧ 𝑢 ∈ (R‘𝑦))) → 𝑦 ∈ No)
113	99	leftnod 28278	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑡 ∈ (L‘𝑥) ∧ 𝑢 ∈ (R‘𝑦))) → 𝑡 ∈ No)
114	112, 113	mulscld 28533	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑡 ∈ (L‘𝑥) ∧ 𝑢 ∈ (R‘𝑦))) → (𝑦 ·s 𝑡) ∈ No)
115	107	rightnod 28280	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑡 ∈ (L‘𝑥) ∧ 𝑢 ∈ (R‘𝑦))) → 𝑢 ∈ No)
116		simplll 787	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑡 ∈ (L‘𝑥) ∧ 𝑢 ∈ (R‘𝑦))) → 𝑥 ∈ No)
117	115, 116	mulscld 28533	. . . . . . . . . . . . . 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 28365	. . . . . . . . . . . . 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 2798	. . . . . . . . . . . 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 7434	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑂 = 𝑡 → (𝑥𝑂 ·s 𝑦𝑂) = (𝑡 ·s 𝑦𝑂))
121		oveq2 7435	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑂 = 𝑡 → (𝑦𝑂 ·s 𝑥𝑂) = (𝑦𝑂 ·s 𝑡))
122	120, 121	eqeq12d 2779	. . . . . . . . . . . . 13 ⊢ (𝑥𝑂 = 𝑡 → ((𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ↔ (𝑡 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑡)))
123		oveq2 7435	. . . . . . . . . . . . . 14 ⊢ (𝑦𝑂 = 𝑢 → (𝑡 ·s 𝑦𝑂) = (𝑡 ·s 𝑢))
124		oveq1 7434	. . . . . . . . . . . . . 14 ⊢ (𝑦𝑂 = 𝑢 → (𝑦𝑂 ·s 𝑡) = (𝑢 ·s 𝑡))
125	123, 124	eqeq12d 2779	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑢 → ((𝑡 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑡) ↔ (𝑡 ·s 𝑢) = (𝑢 ·s 𝑡)))
126		simplr1 1234	. . . . . . . . . . . . 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 3593	. . . . . . . . . . . 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 7445	. . . . . . . . . . 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 2774	. . . . . . . . . 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 3228	. . . . . . . . 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 3294	. . . . . . . . 9 ⊢ (∃𝑡 ∈ (L‘𝑥)∃𝑢 ∈ (R‘𝑦)𝑐 = (((𝑢 ·s 𝑥) +s (𝑦 ·s 𝑡)) −s (𝑢 ·s 𝑡)) ↔ ∃𝑢 ∈ (R‘𝑦)∃𝑡 ∈ (L‘𝑥)𝑐 = (((𝑢 ·s 𝑥) +s (𝑦 ·s 𝑡)) −s (𝑢 ·s 𝑡)))
132	130, 131	bitrdi 290	. . . . . . . 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 2829	. . . . . . 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 7434	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝑂 = 𝑣 → (𝑥𝑂 ·s 𝑦) = (𝑣 ·s 𝑦))
135		oveq2 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝑂 = 𝑣 → (𝑦 ·s 𝑥𝑂) = (𝑦 ·s 𝑣))
136	134, 135	eqeq12d 2779	. . . . . . . . . . . . . . 15 ⊢ (𝑥𝑂 = 𝑣 → ((𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ↔ (𝑣 ·s 𝑦) = (𝑦 ·s 𝑣)))
137		simplr2 1235	. . . . . . . . . . . . . . 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 783	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑣 ∈ (R‘𝑥) ∧ 𝑤 ∈ (L‘𝑦))) → 𝑣 ∈ (R‘𝑥))
139		elun2 4183	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ (R‘𝑥) → 𝑣 ∈ ((L‘𝑥) ∪ (R‘𝑥)))
140	138, 139	syl 18	. . . . . . . . . . . . . . 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 3580	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑣 ∈ (R‘𝑥) ∧ 𝑤 ∈ (L‘𝑦))) → (𝑣 ·s 𝑦) = (𝑦 ·s 𝑣))
142		oveq2 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑂 = 𝑤 → (𝑥 ·s 𝑦𝑂) = (𝑥 ·s 𝑤))
143		oveq1 7434	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑂 = 𝑤 → (𝑦𝑂 ·s 𝑥) = (𝑤 ·s 𝑥))
144	142, 143	eqeq12d 2779	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑤 → ((𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥) ↔ (𝑥 ·s 𝑤) = (𝑤 ·s 𝑥)))
145		simplr3 1236	. . . . . . . . . . . . . . 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 785	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑣 ∈ (R‘𝑥) ∧ 𝑤 ∈ (L‘𝑦))) → 𝑤 ∈ (L‘𝑦))
147		elun1 4182	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ (L‘𝑦) → 𝑤 ∈ ((L‘𝑦) ∪ (R‘𝑦)))
148	146, 147	syl 18	. . . . . . . . . . . . . . 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 3580	. . . . . . . . . . . . . 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 7445	. . . . . . . . . . . . 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 788	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑣 ∈ (R‘𝑥) ∧ 𝑤 ∈ (L‘𝑦))) → 𝑦 ∈ No)
152	138	rightnod 28280	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑣 ∈ (R‘𝑥) ∧ 𝑤 ∈ (L‘𝑦))) → 𝑣 ∈ No)
153	151, 152	mulscld 28533	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑣 ∈ (R‘𝑥) ∧ 𝑤 ∈ (L‘𝑦))) → (𝑦 ·s 𝑣) ∈ No)
154	146	leftnod 28278	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑣 ∈ (R‘𝑥) ∧ 𝑤 ∈ (L‘𝑦))) → 𝑤 ∈ No)
155		simplll 787	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) ∧ (𝑣 ∈ (R‘𝑥) ∧ 𝑤 ∈ (L‘𝑦))) → 𝑥 ∈ No)
156	154, 155	mulscld 28533	. . . . . . . . . . . . . 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 28365	. . . . . . . . . . . . 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 2798	. . . . . . . . . . . 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 7434	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑂 = 𝑣 → (𝑥𝑂 ·s 𝑦𝑂) = (𝑣 ·s 𝑦𝑂))
160		oveq2 7435	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑂 = 𝑣 → (𝑦𝑂 ·s 𝑥𝑂) = (𝑦𝑂 ·s 𝑣))
161	159, 160	eqeq12d 2779	. . . . . . . . . . . . 13 ⊢ (𝑥𝑂 = 𝑣 → ((𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ↔ (𝑣 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑣)))
162		oveq2 7435	. . . . . . . . . . . . . 14 ⊢ (𝑦𝑂 = 𝑤 → (𝑣 ·s 𝑦𝑂) = (𝑣 ·s 𝑤))
163		oveq1 7434	. . . . . . . . . . . . . 14 ⊢ (𝑦𝑂 = 𝑤 → (𝑦𝑂 ·s 𝑣) = (𝑤 ·s 𝑣))
164	162, 163	eqeq12d 2779	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑤 → ((𝑣 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑣) ↔ (𝑣 ·s 𝑤) = (𝑤 ·s 𝑣)))
165		simplr1 1234	. . . . . . . . . . . . 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 3593	. . . . . . . . . . . 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 7445	. . . . . . . . . . 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 2774	. . . . . . . . . 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 3228	. . . . . . . . 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 3294	. . . . . . . . 9 ⊢ (∃𝑣 ∈ (R‘𝑥)∃𝑤 ∈ (L‘𝑦)𝑑 = (((𝑤 ·s 𝑥) +s (𝑦 ·s 𝑣)) −s (𝑤 ·s 𝑣)) ↔ ∃𝑤 ∈ (L‘𝑦)∃𝑣 ∈ (R‘𝑥)𝑑 = (((𝑤 ·s 𝑥) +s (𝑦 ·s 𝑣)) −s (𝑤 ·s 𝑣)))
171	169, 170	bitrdi 290	. . . . . . . 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 2829	. . . . . . 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 4170	. . . . . 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 4159	. . . . . 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 2814	. . . . 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 7445	. . . 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 28507	. . . . 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 486	. . . 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 28507	. . . . . 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 464	. . . . 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 486	. . . 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 2808	. . 3 ⊢ (((𝑥 ∈ No ∧ 𝑦 ∈ No) ∧ (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥𝑂 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 𝑦) = (𝑦 ·s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ ((L‘𝑦) ∪ (R‘𝑦))(𝑥 ·s 𝑦𝑂) = (𝑦𝑂 ·s 𝑥))) → (𝑥 ·s 𝑦) = (𝑦 ·s 𝑥))
183	182	ex 418	. 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 28353	1 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (𝐴 ·s 𝐵) = (𝐵 ·s 𝐴))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2146  {cab 2741  ∀wral 3079  ∃wrex 3089   ∪ cun 4151  ‘cfv 6546  (class class class)co 7427  Nocsur 28009   |s ccuts 28157  Lcleft 28223  Rcright 28224   +_s cadds 28357   −_s csubs 28418   ·_s cmuls 28504

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-rep 5234  ax-sep 5251  ax-nul 5262  ax-pow 5330  ax-pr 5394  ax-un 7758

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-pss 4016  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4838  df-ot 4861  df-uni 4870  df-int 4910  df-iun 4955  df-br 5106  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5549  df-eprel 5554  df-po 5562  df-so 5563  df-fr 5607  df-se 5608  df-we 5609  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6310  df-ord 6371  df-on 6372  df-suc 6374  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-riota 7384  df-ov 7430  df-oprab 7431  df-mpo 7432  df-1st 8008  df-2nd 8009  df-frecs 8310  df-wrecs 8341  df-recs 8390  df-1o 8487  df-2o 8488  df-nadd 8686  df-no 28012  df-lts 28013  df-bday 28014  df-les 28114  df-slts 28156  df-cuts 28158  df-0s 28205  df-made 28225  df-old 28226  df-left 28228  df-right 28229  df-norec 28336  df-norec2 28347  df-adds 28358  df-negs 28419  df-subs 28420  df-muls 28505

This theorem is used by:  mulscomd  28538  muls02  28539  mulslid  28540