Theorem mulsasslem3 28358

Description: Lemma for mulsass 28359. 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 7417	. . . . . . . . . . 11 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s 𝐵) = (𝑥 ·s 𝐵))
2	1	oveq1d 7425	. . . . . . . . . 10 ⊢ (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝐵) ·s 𝐶) = ((𝑥 ·s 𝐵) ·s 𝐶))
3		oveq1 7417	. . . . . . . . . 10 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝐵 ·s 𝐶)) = (𝑥 ·s (𝐵 ·s 𝐶)))
4	2, 3	eqeq12d 2779	. . . . . . . . 9 ⊢ (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝐵) ·s 𝐶) = (𝑥𝑂 ·s (𝐵 ·s 𝐶)) ↔ ((𝑥 ·s 𝐵) ·s 𝐶) = (𝑥 ·s (𝐵 ·s 𝐶))))
5		mulsasslem3.11	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))((𝑥𝑂 ·s 𝐵) ·s 𝐶) = (𝑥𝑂 ·s (𝐵 ·s 𝐶)))
6	5	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))((𝑥𝑂 ·s 𝐵) ·s 𝐶) = (𝑥𝑂 ·s (𝐵 ·s 𝐶)))
7		mulsasslem3.4	. . . . . . . . . 10 ⊢ 𝑃 ⊆ (( L ‘𝐴) ∪ ( R ‘𝐴))
8		simprll 790	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑥 ∈ 𝑃)
9	7, 8	sselid 3935	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑥 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
10	4, 6, 9	rspcdva 3582	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) ·s 𝐶) = (𝑥 ·s (𝐵 ·s 𝐶)))
11		oveq2 7418	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑦 → (𝐴 ·s 𝑦𝑂) = (𝐴 ·s 𝑦))
12	11	oveq1d 7425	. . . . . . . . . . . 12 ⊢ (𝑦𝑂 = 𝑦 → ((𝐴 ·s 𝑦𝑂) ·s 𝐶) = ((𝐴 ·s 𝑦) ·s 𝐶))
13		oveq1 7417	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑦 → (𝑦𝑂 ·s 𝐶) = (𝑦 ·s 𝐶))
14	13	oveq2d 7426	. . . . . . . . . . . 12 ⊢ (𝑦𝑂 = 𝑦 → (𝐴 ·s (𝑦𝑂 ·s 𝐶)) = (𝐴 ·s (𝑦 ·s 𝐶)))
15	12, 14	eqeq12d 2779	. . . . . . . . . . 11 ⊢ (𝑦𝑂 = 𝑦 → (((𝐴 ·s 𝑦𝑂) ·s 𝐶) = (𝐴 ·s (𝑦𝑂 ·s 𝐶)) ↔ ((𝐴 ·s 𝑦) ·s 𝐶) = (𝐴 ·s (𝑦 ·s 𝐶))))
16		mulsasslem3.12	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝐴 ·s 𝑦𝑂) ·s 𝐶) = (𝐴 ·s (𝑦𝑂 ·s 𝐶)))
17	16	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝐴 ·s 𝑦𝑂) ·s 𝐶) = (𝐴 ·s (𝑦𝑂 ·s 𝐶)))
18		mulsasslem3.5	. . . . . . . . . . . 12 ⊢ 𝑄 ⊆ (( L ‘𝐵) ∪ ( R ‘𝐵))
19		simprlr 791	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑦 ∈ 𝑄)
20	18, 19	sselid 3935	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑦 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵)))
21	15, 17, 20	rspcdva 3582	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝑦) ·s 𝐶) = (𝐴 ·s (𝑦 ·s 𝐶)))
22		oveq2 7418	. . . . . . . . . . . . . 14 ⊢ (𝑧𝑂 = 𝑧 → ((𝐴 ·s 𝐵) ·s 𝑧𝑂) = ((𝐴 ·s 𝐵) ·s 𝑧))
23		oveq2 7418	. . . . . . . . . . . . . . 15 ⊢ (𝑧𝑂 = 𝑧 → (𝐵 ·s 𝑧𝑂) = (𝐵 ·s 𝑧))
24	23	oveq2d 7426	. . . . . . . . . . . . . 14 ⊢ (𝑧𝑂 = 𝑧 → (𝐴 ·s (𝐵 ·s 𝑧𝑂)) = (𝐴 ·s (𝐵 ·s 𝑧)))
25	22, 24	eqeq12d 2779	. . . . . . . . . . . . 13 ⊢ (𝑧𝑂 = 𝑧 → (((𝐴 ·s 𝐵) ·s 𝑧𝑂) = (𝐴 ·s (𝐵 ·s 𝑧𝑂)) ↔ ((𝐴 ·s 𝐵) ·s 𝑧) = (𝐴 ·s (𝐵 ·s 𝑧))))
26		mulsasslem3.13	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝐵) ·s 𝑧𝑂) = (𝐴 ·s (𝐵 ·s 𝑧𝑂)))
27	26	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝐵) ·s 𝑧𝑂) = (𝐴 ·s (𝐵 ·s 𝑧𝑂)))
28		mulsasslem3.6	. . . . . . . . . . . . . 14 ⊢ 𝑅 ⊆ (( L ‘𝐶) ∪ ( R ‘𝐶))
29		simprr 784	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑧 ∈ 𝑅)
30	28, 29	sselid 3935	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑧 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶)))
31	25, 27, 30	rspcdva 3582	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝐵) ·s 𝑧) = (𝐴 ·s (𝐵 ·s 𝑧)))
32		leftssno 28066	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( L ‘𝐴) ⊆ No
33		rightssno 28067	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( R ‘𝐴) ⊆ No
34	32, 33	unssi 4144	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (( L ‘𝐴) ∪ ( R ‘𝐴)) ⊆ No
35	7, 34	sstri 3946	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑃 ⊆ No
36	35, 8	sselid 3935	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑥 ∈ No )
37		mulsasslem3.2	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ No )
38	37	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝐵 ∈ No )
39	36, 38	mulscld 28328	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s 𝐵) ∈ No )
40		leftssno 28066	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ( L ‘𝐶) ⊆ No
41		rightssno 28067	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ( R ‘𝐶) ⊆ No
42	40, 41	unssi 4144	. . . . . . . . . . . . . . . . . . . 20 ⊢ (( L ‘𝐶) ∪ ( R ‘𝐶)) ⊆ No
43	28, 42	sstri 3946	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑅 ⊆ No
44	43, 29	sselid 3935	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑧 ∈ No )
45	39, 44	mulscld 28328	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) ·s 𝑧) ∈ No )
46		mulsasslem3.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ No )
47	46	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝐴 ∈ No )
48		leftssno 28066	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( L ‘𝐵) ⊆ No
49		rightssno 28067	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( R ‘𝐵) ⊆ No
50	48, 49	unssi 4144	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (( L ‘𝐵) ∪ ( R ‘𝐵)) ⊆ No
51	18, 50	sstri 3946	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑄 ⊆ No
52	51, 19	sselid 3935	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑦 ∈ No )
53	47, 52	mulscld 28328	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s 𝑦) ∈ No )
54	53, 44	mulscld 28328	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝑦) ·s 𝑧) ∈ No )
55	45, 54	addscomd 28160	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) = (((𝐴 ·s 𝑦) ·s 𝑧) +s ((𝑥 ·s 𝐵) ·s 𝑧)))
56	55	oveq1d 7425	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = ((((𝐴 ·s 𝑦) ·s 𝑧) +s ((𝑥 ·s 𝐵) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))
57	36, 52	mulscld 28328	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s 𝑦) ∈ No )
58	57, 44	mulscld 28328	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝑦) ·s 𝑧) ∈ No )
59	54, 45, 58	addsubsassd 28274	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝐴 ·s 𝑦) ·s 𝑧) +s ((𝑥 ·s 𝐵) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = (((𝐴 ·s 𝑦) ·s 𝑧) +s (((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧))))
60	56, 59	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = (((𝐴 ·s 𝑦) ·s 𝑧) +s (((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧))))
61	60	oveq1d 7425	. . . . . . . . . . . . 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 28256	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) ∈ No )
63		mulsasslem3.3	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ No )
64	63	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝐶 ∈ No )
65	57, 64	mulscld 28328	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝑦) ·s 𝐶) ∈ No )
66	54, 62, 65	addsassd 28199	. . . . . . . . . . . . 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 7425	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑂 = 𝑦 → ((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = ((𝐴 ·s 𝑦) ·s 𝑧𝑂))
68		oveq1 7417	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦𝑂 = 𝑦 → (𝑦𝑂 ·s 𝑧𝑂) = (𝑦 ·s 𝑧𝑂))
69	68	oveq2d 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑂 = 𝑦 → (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)) = (𝐴 ·s (𝑦 ·s 𝑧𝑂)))
70	67, 69	eqeq12d 2779	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑦 → (((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)) ↔ ((𝐴 ·s 𝑦) ·s 𝑧𝑂) = (𝐴 ·s (𝑦 ·s 𝑧𝑂))))
71		oveq2 7418	. . . . . . . . . . . . . . . 16 ⊢ (𝑧𝑂 = 𝑧 → ((𝐴 ·s 𝑦) ·s 𝑧𝑂) = ((𝐴 ·s 𝑦) ·s 𝑧))
72		oveq2 7418	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧𝑂 = 𝑧 → (𝑦 ·s 𝑧𝑂) = (𝑦 ·s 𝑧))
73	72	oveq2d 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝑧𝑂 = 𝑧 → (𝐴 ·s (𝑦 ·s 𝑧𝑂)) = (𝐴 ·s (𝑦 ·s 𝑧)))
74	71, 73	eqeq12d 2779	. . . . . . . . . . . . . . 15 ⊢ (𝑧𝑂 = 𝑧 → (((𝐴 ·s 𝑦) ·s 𝑧𝑂) = (𝐴 ·s (𝑦 ·s 𝑧𝑂)) ↔ ((𝐴 ·s 𝑦) ·s 𝑧) = (𝐴 ·s (𝑦 ·s 𝑧))))
75		mulsasslem3.10	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)))
76	75	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)))
77	70, 74, 76, 20, 30	rspc2dv 3596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝑦) ·s 𝑧) = (𝐴 ·s (𝑦 ·s 𝑧)))
78	45, 65, 58	addsubsd 28275	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝑥 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = ((((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) +s ((𝑥 ·s 𝑦) ·s 𝐶)))
79	1	oveq1d 7425	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = ((𝑥 ·s 𝐵) ·s 𝑧𝑂))
80		oveq1 7417	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)) = (𝑥 ·s (𝐵 ·s 𝑧𝑂)))
81	79, 80	eqeq12d 2779	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝐵) ·s 𝑧𝑂) = (𝑥 ·s (𝐵 ·s 𝑧𝑂))))
82		oveq2 7418	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧𝑂 = 𝑧 → ((𝑥 ·s 𝐵) ·s 𝑧𝑂) = ((𝑥 ·s 𝐵) ·s 𝑧))
83	23	oveq2d 7426	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧𝑂 = 𝑧 → (𝑥 ·s (𝐵 ·s 𝑧𝑂)) = (𝑥 ·s (𝐵 ·s 𝑧)))
84	82, 83	eqeq12d 2779	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧𝑂 = 𝑧 → (((𝑥 ·s 𝐵) ·s 𝑧𝑂) = (𝑥 ·s (𝐵 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝐵) ·s 𝑧) = (𝑥 ·s (𝐵 ·s 𝑧))))
85		mulsasslem3.9	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)))
86	85	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)))
87	81, 84, 86, 9, 30	rspc2dv 3596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) ·s 𝑧) = (𝑥 ·s (𝐵 ·s 𝑧)))
88		oveq1 7417	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s 𝑦𝑂) = (𝑥 ·s 𝑦𝑂))
89	88	oveq1d 7425	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = ((𝑥 ·s 𝑦𝑂) ·s 𝐶))
90		oveq1 7417	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)) = (𝑥 ·s (𝑦𝑂 ·s 𝐶)))
91	89, 90	eqeq12d 2779	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)) ↔ ((𝑥 ·s 𝑦𝑂) ·s 𝐶) = (𝑥 ·s (𝑦𝑂 ·s 𝐶))))
92		oveq2 7418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦𝑂 = 𝑦 → (𝑥 ·s 𝑦𝑂) = (𝑥 ·s 𝑦))
93	92	oveq1d 7425	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦𝑂 = 𝑦 → ((𝑥 ·s 𝑦𝑂) ·s 𝐶) = ((𝑥 ·s 𝑦) ·s 𝐶))
94	13	oveq2d 7426	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦𝑂 = 𝑦 → (𝑥 ·s (𝑦𝑂 ·s 𝐶)) = (𝑥 ·s (𝑦 ·s 𝐶)))
95	93, 94	eqeq12d 2779	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦𝑂 = 𝑦 → (((𝑥 ·s 𝑦𝑂) ·s 𝐶) = (𝑥 ·s (𝑦𝑂 ·s 𝐶)) ↔ ((𝑥 ·s 𝑦) ·s 𝐶) = (𝑥 ·s (𝑦 ·s 𝐶))))
96		mulsasslem3.8	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)))
97	96	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)))
98	91, 95, 97, 9, 20	rspc2dv 3596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝑦) ·s 𝐶) = (𝑥 ·s (𝑦 ·s 𝐶)))
99	87, 98	oveq12d 7428	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝑥 ·s 𝑦) ·s 𝐶)) = ((𝑥 ·s (𝐵 ·s 𝑧)) +s (𝑥 ·s (𝑦 ·s 𝐶))))
100	38, 44	mulscld 28328	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐵 ·s 𝑧) ∈ No )
101	36, 100	mulscld 28328	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (𝐵 ·s 𝑧)) ∈ No )
102	52, 64	mulscld 28328	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑦 ·s 𝐶) ∈ No )
103	36, 102	mulscld 28328	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (𝑦 ·s 𝐶)) ∈ No )
104	101, 103	addscomd 28160	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s (𝐵 ·s 𝑧)) +s (𝑥 ·s (𝑦 ·s 𝐶))) = ((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))))
105	99, 104	eqtrd 2798	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝑥 ·s 𝑦) ·s 𝐶)) = ((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))))
106	88	oveq1d 7425	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = ((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂))
107		oveq1 7417	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)) = (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂)))
108	106, 107	eqeq12d 2779	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂))))
109	92	oveq1d 7425	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦𝑂 = 𝑦 → ((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂) = ((𝑥 ·s 𝑦) ·s 𝑧𝑂))
110	68	oveq2d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦𝑂 = 𝑦 → (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂)) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))
111	109, 110	eqeq12d 2779	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦𝑂 = 𝑦 → (((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂))))
112		oveq2 7418	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧𝑂 = 𝑧 → ((𝑥 ·s 𝑦) ·s 𝑧𝑂) = ((𝑥 ·s 𝑦) ·s 𝑧))
113	72	oveq2d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧𝑂 = 𝑧 → (𝑥 ·s (𝑦 ·s 𝑧𝑂)) = (𝑥 ·s (𝑦 ·s 𝑧)))
114	112, 113	eqeq12d 2779	. . . . . . . . . . . . . . . . 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 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)))
117	108, 111, 114, 116, 9, 20, 30	rspc3dv 3600	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝑦) ·s 𝑧) = (𝑥 ·s (𝑦 ·s 𝑧)))
118	105, 117	oveq12d 7428	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝑥 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
119	78, 118	eqtr3d 2800	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) +s ((𝑥 ·s 𝑦) ·s 𝐶)) = (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
120	77, 119	oveq12d 7428	. . . . . . . . . . . . 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 2802	. . . . . . . . . . . 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 7428	. . . . . . . . . . 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 28328	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s 𝐵) ∈ No )
124	123, 44	mulscld 28328	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝐵) ·s 𝑧) ∈ No )
125	45, 54	addscld 28173	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) ∈ No )
126	125, 58	subscld 28256	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) ∈ No )
127	124, 126, 65	subsubs4d 28287	. . . . . . . . . . 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 28328	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (𝐵 ·s 𝑧)) ∈ No )
129	52, 44	mulscld 28328	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑦 ·s 𝑧) ∈ No )
130	47, 129	mulscld 28328	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (𝑦 ·s 𝑧)) ∈ No )
131	103, 101	addscld 28173	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) ∈ No )
132	36, 129	mulscld 28328	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (𝑦 ·s 𝑧)) ∈ No )
133	131, 132	subscld 28256	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))) ∈ No )
134	128, 130, 133	subsubs4d 28287	. . . . . . . . . . 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 2808	. . . . . . . . . 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 7428	. . . . . . . . 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 28328	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝑦) ·s 𝐶) ∈ No )
138	124, 126	subscld 28256	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧))) ∈ No )
139	137, 138, 65	addsubsd 28275	. . . . . . . . . 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 28274	. . . . . . . . . 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 2800	. . . . . . . . 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 28328	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (𝑦 ·s 𝐶)) ∈ No )
143	142, 128, 130	addsubsassd 28274	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))) = ((𝐴 ·s (𝑦 ·s 𝐶)) +s ((𝐴 ·s (𝐵 ·s 𝑧)) -s (𝐴 ·s (𝑦 ·s 𝑧)))))
144	143	oveq1d 7425	. . . . . . . . . 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 28256	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s (𝐵 ·s 𝑧)) -s (𝐴 ·s (𝑦 ·s 𝑧))) ∈ No )
146	142, 145, 133	addsubsassd 28274	. . . . . . . . . 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 2798	. . . . . . . . 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 2808	. . . . . . . 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 7428	. . . . . . 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 28328	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) ·s 𝐶) ∈ No )
151	150, 137	addscld 28173	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) ∈ No )
152	151, 65	subscld 28256	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)) ∈ No )
153	152, 124, 126	addsubsassd 28274	. . . . . . . 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 28274	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)) = (((𝑥 ·s 𝐵) ·s 𝐶) +s (((𝐴 ·s 𝑦) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶))))
155	154	oveq1d 7425	. . . . . . . 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 28256	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s 𝑦) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶)) ∈ No )
157	150, 156, 138	addsassd 28199	. . . . . . . 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 2802	. . . . . . 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 28328	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐵 ·s 𝐶) ∈ No )
160	36, 159	mulscld 28328	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (𝐵 ·s 𝐶)) ∈ No )
161	142, 128	addscld 28173	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) ∈ No )
162	161, 130	subscld 28256	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))) ∈ No )
163	160, 162, 133	addsubsassd 28274	. . . . . . 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 2808	. . . . . 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 28173	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ∈ No )
166	165, 57, 64	subsdird 28352	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝐶) = ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶)))
167	39, 53, 64	addsdird 28350	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝐶) = (((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)))
168	167	oveq1d 7425	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶)) = ((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)))
169	166, 168	eqtrd 2798	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝐶) = ((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)))
170	169	oveq1d 7425	. . . . . . 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 28352	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝑧) = ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)))
172	39, 53, 44	addsdird 28350	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝑧) = (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)))
173	172	oveq1d 7425	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))
174	171, 173	eqtrd 2798	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝑧) = ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))
175	170, 174	oveq12d 7428	. . . . . 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 28173	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) ∈ No )
177	47, 176, 129	subsdid 28351	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))) = ((𝐴 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))))
178	47, 102, 100	addsdid 28349	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) = ((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))))
179	178	oveq1d 7425	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))) = (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))))
180	177, 179	eqtrd 2798	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))) = (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))))
181	180	oveq2d 7426	. . . . . . 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 28351	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))) = ((𝑥 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
183	36, 102, 100	addsdid 28349	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) = ((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))))
184	183	oveq1d 7425	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))) = (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
185	182, 184	eqtrd 2798	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))) = (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
186	181, 185	oveq12d 7428	. . . . . 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 2808	. . . . 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 2774	. . . 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 472	. . 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 3187	. 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 3228	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 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∀wral 3079  ∃wrex 3089   ∪ cun 3903   ⊆ wss 3905  ‘cfv 6536  (class class class)co 7410   No csur 27804   L cleft 28018   R cright 28019   +_s cadds 28152   -_s csubs 28213   ·_s cmuls 28299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  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 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-tp 4594  df-op 4596  df-ot 4598  df-uni 4873  df-int 4913  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-se 5615  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-1st 7982  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-1o 8449  df-2o 8450  df-nadd 8648  df-no 27807  df-lts 27808  df-bday 27809  df-les 27909  df-slts 27951  df-cuts 27953  df-0s 28000  df-made 28020  df-old 28021  df-left 28023  df-right 28024  df-norec 28131  df-norec2 28142  df-adds 28153  df-negs 28214  df-subs 28215  df-muls 28300

This theorem is referenced by:  mulsass  28359