Theorem mulsasslem3 27600

Description: Lemma for mulsass 27601. Demonstrate the central equality. (Contributed by Scott Fenton, 10-Mar-2025.)

Hypotheses

Ref	Expression
mulsasslem3.1	⊢ (𝜑 → 𝐴 ∈ No )
mulsasslem3.2	⊢ (𝜑 → 𝐵 ∈ No )
mulsasslem3.3	⊢ (𝜑 → 𝐶 ∈ No )
mulsasslem3.4	⊢ 𝑃 ⊆ (( L ‘𝐴) ∪ ( R ‘𝐴))
mulsasslem3.5	⊢ 𝑄 ⊆ (( L ‘𝐵) ∪ ( R ‘𝐵))
mulsasslem3.6	⊢ 𝑅 ⊆ (( L ‘𝐶) ∪ ( R ‘𝐶))
mulsasslem3.7	⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)))
mulsasslem3.8	⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)))
mulsasslem3.9	⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)))
mulsasslem3.10	⊢ (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)))
mulsasslem3.11	⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))((𝑥𝑂 ·s 𝐵) ·s 𝐶) = (𝑥𝑂 ·s (𝐵 ·s 𝐶)))
mulsasslem3.12	⊢ (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝐴 ·s 𝑦𝑂) ·s 𝐶) = (𝐴 ·s (𝑦𝑂 ·s 𝐶)))
mulsasslem3.13	⊢ (𝜑 → ∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝐵) ·s 𝑧𝑂) = (𝐴 ·s (𝐵 ·s 𝑧𝑂)))

Assertion

Ref	Expression
mulsasslem3	⊢ (𝜑 → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑄 ∃𝑧 ∈ 𝑅 𝑎 = ((((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧)) -s ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝑧)) ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑄 ∃𝑧 ∈ 𝑅 𝑎 = (((𝑥 ·s (𝐵 ·s 𝐶)) +s (𝐴 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧)))) -s (𝑥 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))))))

Distinct variable groups:   𝑥_𝑂,𝑦_𝑂,𝑧_𝑂,𝐴   𝐵,𝑥_𝑂,𝑦_𝑂,𝑧_𝑂   𝐶,𝑥_𝑂,𝑦_𝑂,𝑧_𝑂   𝑥,𝑥_𝑂,𝑦_𝑂,𝑧_𝑂   𝑦,𝑦_𝑂,𝑧_𝑂   𝑧,𝑧_𝑂,𝑦   𝑦,𝑃,𝑧   𝑧,𝑄   𝑥,𝑦,𝑧,𝜑

Allowed substitution hints:   𝜑(𝑎,𝑥_𝑂,𝑦_𝑂,𝑧_𝑂)   𝐴(𝑥,𝑦,𝑧,𝑎)   𝐵(𝑥,𝑦,𝑧,𝑎)   𝐶(𝑥,𝑦,𝑧,𝑎)   𝑃(𝑥,𝑎,𝑥_𝑂,𝑦_𝑂,𝑧_𝑂)   𝑄(𝑥,𝑦,𝑎,𝑥_𝑂,𝑦_𝑂,𝑧_𝑂)   𝑅(𝑥,𝑦,𝑧,𝑎,𝑥_𝑂,𝑦_𝑂,𝑧_𝑂)

Proof of Theorem mulsasslem3

Step	Hyp	Ref	Expression
1		oveq1 7411	. . . . . . . . . . 11 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s 𝐵) = (𝑥 ·s 𝐵))
2	1	oveq1d 7419	. . . . . . . . . 10 ⊢ (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝐵) ·s 𝐶) = ((𝑥 ·s 𝐵) ·s 𝐶))
3		oveq1 7411	. . . . . . . . . 10 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝐵 ·s 𝐶)) = (𝑥 ·s (𝐵 ·s 𝐶)))
4	2, 3	eqeq12d 2749	. . . . . . . . 9 ⊢ (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝐵) ·s 𝐶) = (𝑥𝑂 ·s (𝐵 ·s 𝐶)) ↔ ((𝑥 ·s 𝐵) ·s 𝐶) = (𝑥 ·s (𝐵 ·s 𝐶))))
5		mulsasslem3.11	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))((𝑥𝑂 ·s 𝐵) ·s 𝐶) = (𝑥𝑂 ·s (𝐵 ·s 𝐶)))
6	5	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))((𝑥𝑂 ·s 𝐵) ·s 𝐶) = (𝑥𝑂 ·s (𝐵 ·s 𝐶)))
7		mulsasslem3.4	. . . . . . . . . 10 ⊢ 𝑃 ⊆ (( L ‘𝐴) ∪ ( R ‘𝐴))
8		simprll 778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑥 ∈ 𝑃)
9	7, 8	sselid 3979	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑥 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
10	4, 6, 9	rspcdva 3613	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) ·s 𝐶) = (𝑥 ·s (𝐵 ·s 𝐶)))
11		oveq2 7412	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑦 → (𝐴 ·s 𝑦𝑂) = (𝐴 ·s 𝑦))
12	11	oveq1d 7419	. . . . . . . . . . . 12 ⊢ (𝑦𝑂 = 𝑦 → ((𝐴 ·s 𝑦𝑂) ·s 𝐶) = ((𝐴 ·s 𝑦) ·s 𝐶))
13		oveq1 7411	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑦 → (𝑦𝑂 ·s 𝐶) = (𝑦 ·s 𝐶))
14	13	oveq2d 7420	. . . . . . . . . . . 12 ⊢ (𝑦𝑂 = 𝑦 → (𝐴 ·s (𝑦𝑂 ·s 𝐶)) = (𝐴 ·s (𝑦 ·s 𝐶)))
15	12, 14	eqeq12d 2749	. . . . . . . . . . 11 ⊢ (𝑦𝑂 = 𝑦 → (((𝐴 ·s 𝑦𝑂) ·s 𝐶) = (𝐴 ·s (𝑦𝑂 ·s 𝐶)) ↔ ((𝐴 ·s 𝑦) ·s 𝐶) = (𝐴 ·s (𝑦 ·s 𝐶))))
16		mulsasslem3.12	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝐴 ·s 𝑦𝑂) ·s 𝐶) = (𝐴 ·s (𝑦𝑂 ·s 𝐶)))
17	16	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝐴 ·s 𝑦𝑂) ·s 𝐶) = (𝐴 ·s (𝑦𝑂 ·s 𝐶)))
18		mulsasslem3.5	. . . . . . . . . . . 12 ⊢ 𝑄 ⊆ (( L ‘𝐵) ∪ ( R ‘𝐵))
19		simprlr 779	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑦 ∈ 𝑄)
20	18, 19	sselid 3979	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑦 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵)))
21	15, 17, 20	rspcdva 3613	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝑦) ·s 𝐶) = (𝐴 ·s (𝑦 ·s 𝐶)))
22		oveq2 7412	. . . . . . . . . . . . . 14 ⊢ (𝑧𝑂 = 𝑧 → ((𝐴 ·s 𝐵) ·s 𝑧𝑂) = ((𝐴 ·s 𝐵) ·s 𝑧))
23		oveq2 7412	. . . . . . . . . . . . . . 15 ⊢ (𝑧𝑂 = 𝑧 → (𝐵 ·s 𝑧𝑂) = (𝐵 ·s 𝑧))
24	23	oveq2d 7420	. . . . . . . . . . . . . 14 ⊢ (𝑧𝑂 = 𝑧 → (𝐴 ·s (𝐵 ·s 𝑧𝑂)) = (𝐴 ·s (𝐵 ·s 𝑧)))
25	22, 24	eqeq12d 2749	. . . . . . . . . . . . 13 ⊢ (𝑧𝑂 = 𝑧 → (((𝐴 ·s 𝐵) ·s 𝑧𝑂) = (𝐴 ·s (𝐵 ·s 𝑧𝑂)) ↔ ((𝐴 ·s 𝐵) ·s 𝑧) = (𝐴 ·s (𝐵 ·s 𝑧))))
26		mulsasslem3.13	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝐵) ·s 𝑧𝑂) = (𝐴 ·s (𝐵 ·s 𝑧𝑂)))
27	26	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝐵) ·s 𝑧𝑂) = (𝐴 ·s (𝐵 ·s 𝑧𝑂)))
28		mulsasslem3.6	. . . . . . . . . . . . . 14 ⊢ 𝑅 ⊆ (( L ‘𝐶) ∪ ( R ‘𝐶))
29		simprr 772	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑧 ∈ 𝑅)
30	28, 29	sselid 3979	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑧 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶)))
31	25, 27, 30	rspcdva 3613	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝐵) ·s 𝑧) = (𝐴 ·s (𝐵 ·s 𝑧)))
32		leftssno 27355	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( L ‘𝐴) ⊆ No
33		rightssno 27356	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( R ‘𝐴) ⊆ No
34	32, 33	unssi 4184	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (( L ‘𝐴) ∪ ( R ‘𝐴)) ⊆ No
35	7, 34	sstri 3990	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑃 ⊆ No
36	35, 8	sselid 3979	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑥 ∈ No )
37		mulsasslem3.2	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ No )
38	37	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝐵 ∈ No )
39	36, 38	mulscld 27571	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s 𝐵) ∈ No )
40		leftssno 27355	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ( L ‘𝐶) ⊆ No
41		rightssno 27356	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ( R ‘𝐶) ⊆ No
42	40, 41	unssi 4184	. . . . . . . . . . . . . . . . . . . 20 ⊢ (( L ‘𝐶) ∪ ( R ‘𝐶)) ⊆ No
43	28, 42	sstri 3990	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑅 ⊆ No
44	43, 29	sselid 3979	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑧 ∈ No )
45	39, 44	mulscld 27571	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) ·s 𝑧) ∈ No )
46		mulsasslem3.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ No )
47	46	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝐴 ∈ No )
48		leftssno 27355	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( L ‘𝐵) ⊆ No
49		rightssno 27356	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( R ‘𝐵) ⊆ No
50	48, 49	unssi 4184	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (( L ‘𝐵) ∪ ( R ‘𝐵)) ⊆ No
51	18, 50	sstri 3990	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑄 ⊆ No
52	51, 19	sselid 3979	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑦 ∈ No )
53	47, 52	mulscld 27571	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s 𝑦) ∈ No )
54	53, 44	mulscld 27571	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝑦) ·s 𝑧) ∈ No )
55	45, 54	addscomd 27431	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) = (((𝐴 ·s 𝑦) ·s 𝑧) +s ((𝑥 ·s 𝐵) ·s 𝑧)))
56	55	oveq1d 7419	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = ((((𝐴 ·s 𝑦) ·s 𝑧) +s ((𝑥 ·s 𝐵) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))
57	36, 52	mulscld 27571	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s 𝑦) ∈ No )
58	57, 44	mulscld 27571	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝑦) ·s 𝑧) ∈ No )
59	54, 45, 58	addsubsassd 27528	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝐴 ·s 𝑦) ·s 𝑧) +s ((𝑥 ·s 𝐵) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = (((𝐴 ·s 𝑦) ·s 𝑧) +s (((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧))))
60	56, 59	eqtrd 2773	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = (((𝐴 ·s 𝑦) ·s 𝑧) +s (((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧))))
61	60	oveq1d 7419	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) +s ((𝑥 ·s 𝑦) ·s 𝐶)) = ((((𝐴 ·s 𝑦) ·s 𝑧) +s (((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧))) +s ((𝑥 ·s 𝑦) ·s 𝐶)))
62	45, 58	subscld 27515	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) ∈ No )
63		mulsasslem3.3	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ No )
64	63	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝐶 ∈ No )
65	57, 64	mulscld 27571	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝑦) ·s 𝐶) ∈ No )
66	54, 62, 65	addsassd 27469	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝐴 ·s 𝑦) ·s 𝑧) +s (((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧))) +s ((𝑥 ·s 𝑦) ·s 𝐶)) = (((𝐴 ·s 𝑦) ·s 𝑧) +s ((((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) +s ((𝑥 ·s 𝑦) ·s 𝐶))))
67	11	oveq1d 7419	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑂 = 𝑦 → ((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = ((𝐴 ·s 𝑦) ·s 𝑧𝑂))
68		oveq1 7411	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦𝑂 = 𝑦 → (𝑦𝑂 ·s 𝑧𝑂) = (𝑦 ·s 𝑧𝑂))
69	68	oveq2d 7420	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑂 = 𝑦 → (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)) = (𝐴 ·s (𝑦 ·s 𝑧𝑂)))
70	67, 69	eqeq12d 2749	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑦 → (((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)) ↔ ((𝐴 ·s 𝑦) ·s 𝑧𝑂) = (𝐴 ·s (𝑦 ·s 𝑧𝑂))))
71		oveq2 7412	. . . . . . . . . . . . . . . 16 ⊢ (𝑧𝑂 = 𝑧 → ((𝐴 ·s 𝑦) ·s 𝑧𝑂) = ((𝐴 ·s 𝑦) ·s 𝑧))
72		oveq2 7412	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧𝑂 = 𝑧 → (𝑦 ·s 𝑧𝑂) = (𝑦 ·s 𝑧))
73	72	oveq2d 7420	. . . . . . . . . . . . . . . 16 ⊢ (𝑧𝑂 = 𝑧 → (𝐴 ·s (𝑦 ·s 𝑧𝑂)) = (𝐴 ·s (𝑦 ·s 𝑧)))
74	71, 73	eqeq12d 2749	. . . . . . . . . . . . . . 15 ⊢ (𝑧𝑂 = 𝑧 → (((𝐴 ·s 𝑦) ·s 𝑧𝑂) = (𝐴 ·s (𝑦 ·s 𝑧𝑂)) ↔ ((𝐴 ·s 𝑦) ·s 𝑧) = (𝐴 ·s (𝑦 ·s 𝑧))))
75		mulsasslem3.10	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)))
76	75	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)))
77	70, 74, 76, 20, 30	rspc2dv 3625	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝑦) ·s 𝑧) = (𝐴 ·s (𝑦 ·s 𝑧)))
78	45, 65, 58	addsubsd 27529	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝑥 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = ((((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) +s ((𝑥 ·s 𝑦) ·s 𝐶)))
79	1	oveq1d 7419	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = ((𝑥 ·s 𝐵) ·s 𝑧𝑂))
80		oveq1 7411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)) = (𝑥 ·s (𝐵 ·s 𝑧𝑂)))
81	79, 80	eqeq12d 2749	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝐵) ·s 𝑧𝑂) = (𝑥 ·s (𝐵 ·s 𝑧𝑂))))
82		oveq2 7412	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧𝑂 = 𝑧 → ((𝑥 ·s 𝐵) ·s 𝑧𝑂) = ((𝑥 ·s 𝐵) ·s 𝑧))
83	23	oveq2d 7420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧𝑂 = 𝑧 → (𝑥 ·s (𝐵 ·s 𝑧𝑂)) = (𝑥 ·s (𝐵 ·s 𝑧)))
84	82, 83	eqeq12d 2749	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧𝑂 = 𝑧 → (((𝑥 ·s 𝐵) ·s 𝑧𝑂) = (𝑥 ·s (𝐵 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝐵) ·s 𝑧) = (𝑥 ·s (𝐵 ·s 𝑧))))
85		mulsasslem3.9	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)))
86	85	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)))
87	81, 84, 86, 9, 30	rspc2dv 3625	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) ·s 𝑧) = (𝑥 ·s (𝐵 ·s 𝑧)))
88		oveq1 7411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s 𝑦𝑂) = (𝑥 ·s 𝑦𝑂))
89	88	oveq1d 7419	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = ((𝑥 ·s 𝑦𝑂) ·s 𝐶))
90		oveq1 7411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)) = (𝑥 ·s (𝑦𝑂 ·s 𝐶)))
91	89, 90	eqeq12d 2749	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)) ↔ ((𝑥 ·s 𝑦𝑂) ·s 𝐶) = (𝑥 ·s (𝑦𝑂 ·s 𝐶))))
92		oveq2 7412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦𝑂 = 𝑦 → (𝑥 ·s 𝑦𝑂) = (𝑥 ·s 𝑦))
93	92	oveq1d 7419	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦𝑂 = 𝑦 → ((𝑥 ·s 𝑦𝑂) ·s 𝐶) = ((𝑥 ·s 𝑦) ·s 𝐶))
94	13	oveq2d 7420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦𝑂 = 𝑦 → (𝑥 ·s (𝑦𝑂 ·s 𝐶)) = (𝑥 ·s (𝑦 ·s 𝐶)))
95	93, 94	eqeq12d 2749	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦𝑂 = 𝑦 → (((𝑥 ·s 𝑦𝑂) ·s 𝐶) = (𝑥 ·s (𝑦𝑂 ·s 𝐶)) ↔ ((𝑥 ·s 𝑦) ·s 𝐶) = (𝑥 ·s (𝑦 ·s 𝐶))))
96		mulsasslem3.8	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)))
97	96	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)))
98	91, 95, 97, 9, 20	rspc2dv 3625	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝑦) ·s 𝐶) = (𝑥 ·s (𝑦 ·s 𝐶)))
99	87, 98	oveq12d 7422	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝑥 ·s 𝑦) ·s 𝐶)) = ((𝑥 ·s (𝐵 ·s 𝑧)) +s (𝑥 ·s (𝑦 ·s 𝐶))))
100	38, 44	mulscld 27571	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐵 ·s 𝑧) ∈ No )
101	36, 100	mulscld 27571	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (𝐵 ·s 𝑧)) ∈ No )
102	52, 64	mulscld 27571	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑦 ·s 𝐶) ∈ No )
103	36, 102	mulscld 27571	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (𝑦 ·s 𝐶)) ∈ No )
104	101, 103	addscomd 27431	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s (𝐵 ·s 𝑧)) +s (𝑥 ·s (𝑦 ·s 𝐶))) = ((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))))
105	99, 104	eqtrd 2773	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝑥 ·s 𝑦) ·s 𝐶)) = ((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))))
106	88	oveq1d 7419	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = ((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂))
107		oveq1 7411	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)) = (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂)))
108	106, 107	eqeq12d 2749	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂))))
109	92	oveq1d 7419	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦𝑂 = 𝑦 → ((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂) = ((𝑥 ·s 𝑦) ·s 𝑧𝑂))
110	68	oveq2d 7420	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦𝑂 = 𝑦 → (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂)) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))
111	109, 110	eqeq12d 2749	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦𝑂 = 𝑦 → (((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂))))
112		oveq2 7412	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧𝑂 = 𝑧 → ((𝑥 ·s 𝑦) ·s 𝑧𝑂) = ((𝑥 ·s 𝑦) ·s 𝑧))
113	72	oveq2d 7420	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧𝑂 = 𝑧 → (𝑥 ·s (𝑦 ·s 𝑧𝑂)) = (𝑥 ·s (𝑦 ·s 𝑧)))
114	112, 113	eqeq12d 2749	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧𝑂 = 𝑧 → (((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝑦) ·s 𝑧) = (𝑥 ·s (𝑦 ·s 𝑧))))
115		mulsasslem3.7	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)))
116	115	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)))
117	108, 111, 114, 116, 9, 20, 30	rspc3dv 3628	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝑦) ·s 𝑧) = (𝑥 ·s (𝑦 ·s 𝑧)))
118	105, 117	oveq12d 7422	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝑥 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
119	78, 118	eqtr3d 2775	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) +s ((𝑥 ·s 𝑦) ·s 𝐶)) = (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
120	77, 119	oveq12d 7422	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s 𝑦) ·s 𝑧) +s ((((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) +s ((𝑥 ·s 𝑦) ·s 𝐶))) = ((𝐴 ·s (𝑦 ·s 𝑧)) +s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧)))))
121	61, 66, 120	3eqtrd 2777	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) +s ((𝑥 ·s 𝑦) ·s 𝐶)) = ((𝐴 ·s (𝑦 ·s 𝑧)) +s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧)))))
122	31, 121	oveq12d 7422	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s 𝐵) ·s 𝑧) -s (((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) +s ((𝑥 ·s 𝑦) ·s 𝐶))) = ((𝐴 ·s (𝐵 ·s 𝑧)) -s ((𝐴 ·s (𝑦 ·s 𝑧)) +s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))))
123	47, 38	mulscld 27571	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s 𝐵) ∈ No )
124	123, 44	mulscld 27571	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝐵) ·s 𝑧) ∈ No )
125	45, 54	addscld 27444	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) ∈ No )
126	125, 58	subscld 27515	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) ∈ No )
127	124, 126, 65	subsubs4d 27540	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧))) -s ((𝑥 ·s 𝑦) ·s 𝐶)) = (((𝐴 ·s 𝐵) ·s 𝑧) -s (((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) +s ((𝑥 ·s 𝑦) ·s 𝐶))))
128	47, 100	mulscld 27571	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (𝐵 ·s 𝑧)) ∈ No )
129	52, 44	mulscld 27571	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑦 ·s 𝑧) ∈ No )
130	47, 129	mulscld 27571	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (𝑦 ·s 𝑧)) ∈ No )
131	103, 101	addscld 27444	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) ∈ No )
132	36, 129	mulscld 27571	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (𝑦 ·s 𝑧)) ∈ No )
133	131, 132	subscld 27515	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))) ∈ No )
134	128, 130, 133	subsubs4d 27540	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s (𝐵 ·s 𝑧)) -s (𝐴 ·s (𝑦 ·s 𝑧))) -s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧)))) = ((𝐴 ·s (𝐵 ·s 𝑧)) -s ((𝐴 ·s (𝑦 ·s 𝑧)) +s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))))
135	122, 127, 134	3eqtr4d 2783	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧))) -s ((𝑥 ·s 𝑦) ·s 𝐶)) = (((𝐴 ·s (𝐵 ·s 𝑧)) -s (𝐴 ·s (𝑦 ·s 𝑧))) -s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧)))))
136	21, 135	oveq12d 7422	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s 𝑦) ·s 𝐶) +s ((((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧))) -s ((𝑥 ·s 𝑦) ·s 𝐶))) = ((𝐴 ·s (𝑦 ·s 𝐶)) +s (((𝐴 ·s (𝐵 ·s 𝑧)) -s (𝐴 ·s (𝑦 ·s 𝑧))) -s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))))
137	53, 64	mulscld 27571	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝑦) ·s 𝐶) ∈ No )
138	124, 126	subscld 27515	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧))) ∈ No )
139	137, 138, 65	addsubsd 27529	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝐴 ·s 𝑦) ·s 𝐶) +s (((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))) -s ((𝑥 ·s 𝑦) ·s 𝐶)) = ((((𝐴 ·s 𝑦) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶)) +s (((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))))
140	137, 138, 65	addsubsassd 27528	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝐴 ·s 𝑦) ·s 𝐶) +s (((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))) -s ((𝑥 ·s 𝑦) ·s 𝐶)) = (((𝐴 ·s 𝑦) ·s 𝐶) +s ((((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧))) -s ((𝑥 ·s 𝑦) ·s 𝐶))))
141	139, 140	eqtr3d 2775	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝐴 ·s 𝑦) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶)) +s (((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))) = (((𝐴 ·s 𝑦) ·s 𝐶) +s ((((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧))) -s ((𝑥 ·s 𝑦) ·s 𝐶))))
142	47, 102	mulscld 27571	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (𝑦 ·s 𝐶)) ∈ No )
143	142, 128, 130	addsubsassd 27528	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))) = ((𝐴 ·s (𝑦 ·s 𝐶)) +s ((𝐴 ·s (𝐵 ·s 𝑧)) -s (𝐴 ·s (𝑦 ·s 𝑧)))))
144	143	oveq1d 7419	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))) -s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧)))) = (((𝐴 ·s (𝑦 ·s 𝐶)) +s ((𝐴 ·s (𝐵 ·s 𝑧)) -s (𝐴 ·s (𝑦 ·s 𝑧)))) -s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧)))))
145	128, 130	subscld 27515	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s (𝐵 ·s 𝑧)) -s (𝐴 ·s (𝑦 ·s 𝑧))) ∈ No )
146	142, 145, 133	addsubsassd 27528	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s (𝑦 ·s 𝐶)) +s ((𝐴 ·s (𝐵 ·s 𝑧)) -s (𝐴 ·s (𝑦 ·s 𝑧)))) -s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧)))) = ((𝐴 ·s (𝑦 ·s 𝐶)) +s (((𝐴 ·s (𝐵 ·s 𝑧)) -s (𝐴 ·s (𝑦 ·s 𝑧))) -s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))))
147	144, 146	eqtrd 2773	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))) -s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧)))) = ((𝐴 ·s (𝑦 ·s 𝐶)) +s (((𝐴 ·s (𝐵 ·s 𝑧)) -s (𝐴 ·s (𝑦 ·s 𝑧))) -s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))))
148	136, 141, 147	3eqtr4d 2783	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝐴 ·s 𝑦) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶)) +s (((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))) = ((((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))) -s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧)))))
149	10, 148	oveq12d 7422	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝐶) +s ((((𝐴 ·s 𝑦) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶)) +s (((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧))))) = ((𝑥 ·s (𝐵 ·s 𝐶)) +s ((((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))) -s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))))
150	39, 64	mulscld 27571	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) ·s 𝐶) ∈ No )
151	150, 137	addscld 27444	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) ∈ No )
152	151, 65	subscld 27515	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)) ∈ No )
153	152, 124, 126	addsubsassd 27528	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)) +s ((𝐴 ·s 𝐵) ·s 𝑧)) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧))) = (((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)) +s (((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))))
154	150, 137, 65	addsubsassd 27528	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)) = (((𝑥 ·s 𝐵) ·s 𝐶) +s (((𝐴 ·s 𝑦) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶))))
155	154	oveq1d 7419	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)) +s (((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))) = ((((𝑥 ·s 𝐵) ·s 𝐶) +s (((𝐴 ·s 𝑦) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶))) +s (((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))))
156	137, 65	subscld 27515	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s 𝑦) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶)) ∈ No )
157	150, 156, 138	addsassd 27469	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝐶) +s (((𝐴 ·s 𝑦) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶))) +s (((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))) = (((𝑥 ·s 𝐵) ·s 𝐶) +s ((((𝐴 ·s 𝑦) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶)) +s (((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧))))))
158	153, 155, 157	3eqtrd 2777	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)) +s ((𝐴 ·s 𝐵) ·s 𝑧)) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧))) = (((𝑥 ·s 𝐵) ·s 𝐶) +s ((((𝐴 ·s 𝑦) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶)) +s (((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧))))))
159	38, 64	mulscld 27571	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐵 ·s 𝐶) ∈ No )
160	36, 159	mulscld 27571	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (𝐵 ·s 𝐶)) ∈ No )
161	142, 128	addscld 27444	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) ∈ No )
162	161, 130	subscld 27515	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))) ∈ No )
163	160, 162, 133	addsubsassd 27528	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s (𝐵 ·s 𝐶)) +s (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧)))) -s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧)))) = ((𝑥 ·s (𝐵 ·s 𝐶)) +s ((((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))) -s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))))
164	149, 158, 163	3eqtr4d 2783	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)) +s ((𝐴 ·s 𝐵) ·s 𝑧)) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧))) = (((𝑥 ·s (𝐵 ·s 𝐶)) +s (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧)))) -s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧)))))
165	39, 53	addscld 27444	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ∈ No )
166	165, 57, 64	subsdird 27594	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝐶) = ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶)))
167	39, 53, 64	addsdird 27592	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝐶) = (((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)))
168	167	oveq1d 7419	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶)) = ((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)))
169	166, 168	eqtrd 2773	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝐶) = ((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)))
170	169	oveq1d 7419	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧)) = (((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)) +s ((𝐴 ·s 𝐵) ·s 𝑧)))
171	165, 57, 44	subsdird 27594	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝑧) = ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)))
172	39, 53, 44	addsdird 27592	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝑧) = (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)))
173	172	oveq1d 7419	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))
174	171, 173	eqtrd 2773	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝑧) = ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))
175	170, 174	oveq12d 7422	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧)) -s ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝑧)) = ((((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)) +s ((𝐴 ·s 𝐵) ·s 𝑧)) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧))))
176	102, 100	addscld 27444	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) ∈ No )
177	47, 176, 129	subsdid 27593	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))) = ((𝐴 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))))
178	47, 102, 100	addsdid 27591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) = ((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))))
179	178	oveq1d 7419	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))) = (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))))
180	177, 179	eqtrd 2773	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))) = (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))))
181	180	oveq2d 7420	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s (𝐵 ·s 𝐶)) +s (𝐴 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧)))) = ((𝑥 ·s (𝐵 ·s 𝐶)) +s (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧)))))
182	36, 176, 129	subsdid 27593	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))) = ((𝑥 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
183	36, 102, 100	addsdid 27591	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) = ((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))))
184	183	oveq1d 7419	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))) = (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
185	182, 184	eqtrd 2773	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))) = (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
186	181, 185	oveq12d 7422	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s (𝐵 ·s 𝐶)) +s (𝐴 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧)))) -s (𝑥 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧)))) = (((𝑥 ·s (𝐵 ·s 𝐶)) +s (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧)))) -s (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧)))))
187	164, 175, 186	3eqtr4d 2783	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧)) -s ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝑧)) = (((𝑥 ·s (𝐵 ·s 𝐶)) +s (𝐴 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧)))) -s (𝑥 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧)))))
188	187	eqeq2d 2744	. . . 4 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑎 = ((((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧)) -s ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝑧)) ↔ 𝑎 = (((𝑥 ·s (𝐵 ·s 𝐶)) +s (𝐴 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧)))) -s (𝑥 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))))))
189	188	anassrs 469	. . 3 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄)) ∧ 𝑧 ∈ 𝑅) → (𝑎 = ((((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧)) -s ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝑧)) ↔ 𝑎 = (((𝑥 ·s (𝐵 ·s 𝐶)) +s (𝐴 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧)))) -s (𝑥 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))))))
190	189	rexbidva 3177	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄)) → (∃𝑧 ∈ 𝑅 𝑎 = ((((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧)) -s ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝑧)) ↔ ∃𝑧 ∈ 𝑅 𝑎 = (((𝑥 ·s (𝐵 ·s 𝐶)) +s (𝐴 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧)))) -s (𝑥 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))))))
191	190	2rexbidva 3218	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑄 ∃𝑧 ∈ 𝑅 𝑎 = ((((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧)) -s ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝑧)) ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑄 ∃𝑧 ∈ 𝑅 𝑎 = (((𝑥 ·s (𝐵 ·s 𝐶)) +s (𝐴 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧)))) -s (𝑥 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∀wral 3062  ∃wrex 3071   ∪ cun 3945   ⊆ wss 3947  ‘cfv 6540  (class class class)co 7404   No csur 27123   L cleft 27320   R cright 27321   +_s cadds 27423   -_s csubs 27475   ·_s cmuls 27542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-ot 4636  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-1st 7970  df-2nd 7971  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-1o 8461  df-2o 8462  df-nadd 8661  df-no 27126  df-slt 27127  df-bday 27128  df-sle 27228  df-sslt 27263  df-scut 27265  df-0s 27305  df-made 27322  df-old 27323  df-left 27325  df-right 27326  df-norec 27402  df-norec2 27413  df-adds 27424  df-negs 27476  df-subs 27477  df-muls 27543

This theorem is referenced by:  mulsass  27601