Theorem mulsasslem3 28191

Description: Lemma for mulsass 28192. 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 7438	. . . . . . . . . . 11 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s 𝐵) = (𝑥 ·s 𝐵))
2	1	oveq1d 7446	. . . . . . . . . 10 ⊢ (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝐵) ·s 𝐶) = ((𝑥 ·s 𝐵) ·s 𝐶))
3		oveq1 7438	. . . . . . . . . 10 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝐵 ·s 𝐶)) = (𝑥 ·s (𝐵 ·s 𝐶)))
4	2, 3	eqeq12d 2753	. . . . . . . . 9 ⊢ (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝐵) ·s 𝐶) = (𝑥𝑂 ·s (𝐵 ·s 𝐶)) ↔ ((𝑥 ·s 𝐵) ·s 𝐶) = (𝑥 ·s (𝐵 ·s 𝐶))))
5		mulsasslem3.11	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))((𝑥𝑂 ·s 𝐵) ·s 𝐶) = (𝑥𝑂 ·s (𝐵 ·s 𝐶)))
6	5	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))((𝑥𝑂 ·s 𝐵) ·s 𝐶) = (𝑥𝑂 ·s (𝐵 ·s 𝐶)))
7		mulsasslem3.4	. . . . . . . . . 10 ⊢ 𝑃 ⊆ (( L ‘𝐴) ∪ ( R ‘𝐴))
8		simprll 779	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑥 ∈ 𝑃)
9	7, 8	sselid 3981	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑥 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
10	4, 6, 9	rspcdva 3623	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) ·s 𝐶) = (𝑥 ·s (𝐵 ·s 𝐶)))
11		oveq2 7439	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑦 → (𝐴 ·s 𝑦𝑂) = (𝐴 ·s 𝑦))
12	11	oveq1d 7446	. . . . . . . . . . . 12 ⊢ (𝑦𝑂 = 𝑦 → ((𝐴 ·s 𝑦𝑂) ·s 𝐶) = ((𝐴 ·s 𝑦) ·s 𝐶))
13		oveq1 7438	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑦 → (𝑦𝑂 ·s 𝐶) = (𝑦 ·s 𝐶))
14	13	oveq2d 7447	. . . . . . . . . . . 12 ⊢ (𝑦𝑂 = 𝑦 → (𝐴 ·s (𝑦𝑂 ·s 𝐶)) = (𝐴 ·s (𝑦 ·s 𝐶)))
15	12, 14	eqeq12d 2753	. . . . . . . . . . 11 ⊢ (𝑦𝑂 = 𝑦 → (((𝐴 ·s 𝑦𝑂) ·s 𝐶) = (𝐴 ·s (𝑦𝑂 ·s 𝐶)) ↔ ((𝐴 ·s 𝑦) ·s 𝐶) = (𝐴 ·s (𝑦 ·s 𝐶))))
16		mulsasslem3.12	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝐴 ·s 𝑦𝑂) ·s 𝐶) = (𝐴 ·s (𝑦𝑂 ·s 𝐶)))
17	16	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝐴 ·s 𝑦𝑂) ·s 𝐶) = (𝐴 ·s (𝑦𝑂 ·s 𝐶)))
18		mulsasslem3.5	. . . . . . . . . . . 12 ⊢ 𝑄 ⊆ (( L ‘𝐵) ∪ ( R ‘𝐵))
19		simprlr 780	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑦 ∈ 𝑄)
20	18, 19	sselid 3981	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑦 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵)))
21	15, 17, 20	rspcdva 3623	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝑦) ·s 𝐶) = (𝐴 ·s (𝑦 ·s 𝐶)))
22		oveq2 7439	. . . . . . . . . . . . . 14 ⊢ (𝑧𝑂 = 𝑧 → ((𝐴 ·s 𝐵) ·s 𝑧𝑂) = ((𝐴 ·s 𝐵) ·s 𝑧))
23		oveq2 7439	. . . . . . . . . . . . . . 15 ⊢ (𝑧𝑂 = 𝑧 → (𝐵 ·s 𝑧𝑂) = (𝐵 ·s 𝑧))
24	23	oveq2d 7447	. . . . . . . . . . . . . 14 ⊢ (𝑧𝑂 = 𝑧 → (𝐴 ·s (𝐵 ·s 𝑧𝑂)) = (𝐴 ·s (𝐵 ·s 𝑧)))
25	22, 24	eqeq12d 2753	. . . . . . . . . . . . 13 ⊢ (𝑧𝑂 = 𝑧 → (((𝐴 ·s 𝐵) ·s 𝑧𝑂) = (𝐴 ·s (𝐵 ·s 𝑧𝑂)) ↔ ((𝐴 ·s 𝐵) ·s 𝑧) = (𝐴 ·s (𝐵 ·s 𝑧))))
26		mulsasslem3.13	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝐵) ·s 𝑧𝑂) = (𝐴 ·s (𝐵 ·s 𝑧𝑂)))
27	26	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝐵) ·s 𝑧𝑂) = (𝐴 ·s (𝐵 ·s 𝑧𝑂)))
28		mulsasslem3.6	. . . . . . . . . . . . . 14 ⊢ 𝑅 ⊆ (( L ‘𝐶) ∪ ( R ‘𝐶))
29		simprr 773	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑧 ∈ 𝑅)
30	28, 29	sselid 3981	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑧 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶)))
31	25, 27, 30	rspcdva 3623	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝐵) ·s 𝑧) = (𝐴 ·s (𝐵 ·s 𝑧)))
32		leftssno 27919	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( L ‘𝐴) ⊆ No
33		rightssno 27920	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( R ‘𝐴) ⊆ No
34	32, 33	unssi 4191	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (( L ‘𝐴) ∪ ( R ‘𝐴)) ⊆ No
35	7, 34	sstri 3993	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑃 ⊆ No
36	35, 8	sselid 3981	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑥 ∈ No )
37		mulsasslem3.2	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ No )
38	37	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝐵 ∈ No )
39	36, 38	mulscld 28161	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s 𝐵) ∈ No )
40		leftssno 27919	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ( L ‘𝐶) ⊆ No
41		rightssno 27920	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ( R ‘𝐶) ⊆ No
42	40, 41	unssi 4191	. . . . . . . . . . . . . . . . . . . 20 ⊢ (( L ‘𝐶) ∪ ( R ‘𝐶)) ⊆ No
43	28, 42	sstri 3993	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑅 ⊆ No
44	43, 29	sselid 3981	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑧 ∈ No )
45	39, 44	mulscld 28161	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) ·s 𝑧) ∈ No )
46		mulsasslem3.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ No )
47	46	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝐴 ∈ No )
48		leftssno 27919	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( L ‘𝐵) ⊆ No
49		rightssno 27920	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( R ‘𝐵) ⊆ No
50	48, 49	unssi 4191	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (( L ‘𝐵) ∪ ( R ‘𝐵)) ⊆ No
51	18, 50	sstri 3993	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑄 ⊆ No
52	51, 19	sselid 3981	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑦 ∈ No )
53	47, 52	mulscld 28161	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s 𝑦) ∈ No )
54	53, 44	mulscld 28161	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝑦) ·s 𝑧) ∈ No )
55	45, 54	addscomd 28000	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) = (((𝐴 ·s 𝑦) ·s 𝑧) +s ((𝑥 ·s 𝐵) ·s 𝑧)))
56	55	oveq1d 7446	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = ((((𝐴 ·s 𝑦) ·s 𝑧) +s ((𝑥 ·s 𝐵) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))
57	36, 52	mulscld 28161	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s 𝑦) ∈ No )
58	57, 44	mulscld 28161	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝑦) ·s 𝑧) ∈ No )
59	54, 45, 58	addsubsassd 28111	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝐴 ·s 𝑦) ·s 𝑧) +s ((𝑥 ·s 𝐵) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = (((𝐴 ·s 𝑦) ·s 𝑧) +s (((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧))))
60	56, 59	eqtrd 2777	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = (((𝐴 ·s 𝑦) ·s 𝑧) +s (((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧))))
61	60	oveq1d 7446	. . . . . . . . . . . . 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 28093	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) ∈ No )
63		mulsasslem3.3	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ No )
64	63	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝐶 ∈ No )
65	57, 64	mulscld 28161	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝑦) ·s 𝐶) ∈ No )
66	54, 62, 65	addsassd 28039	. . . . . . . . . . . . 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 7446	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑂 = 𝑦 → ((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = ((𝐴 ·s 𝑦) ·s 𝑧𝑂))
68		oveq1 7438	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦𝑂 = 𝑦 → (𝑦𝑂 ·s 𝑧𝑂) = (𝑦 ·s 𝑧𝑂))
69	68	oveq2d 7447	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑂 = 𝑦 → (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)) = (𝐴 ·s (𝑦 ·s 𝑧𝑂)))
70	67, 69	eqeq12d 2753	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑦 → (((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)) ↔ ((𝐴 ·s 𝑦) ·s 𝑧𝑂) = (𝐴 ·s (𝑦 ·s 𝑧𝑂))))
71		oveq2 7439	. . . . . . . . . . . . . . . 16 ⊢ (𝑧𝑂 = 𝑧 → ((𝐴 ·s 𝑦) ·s 𝑧𝑂) = ((𝐴 ·s 𝑦) ·s 𝑧))
72		oveq2 7439	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧𝑂 = 𝑧 → (𝑦 ·s 𝑧𝑂) = (𝑦 ·s 𝑧))
73	72	oveq2d 7447	. . . . . . . . . . . . . . . 16 ⊢ (𝑧𝑂 = 𝑧 → (𝐴 ·s (𝑦 ·s 𝑧𝑂)) = (𝐴 ·s (𝑦 ·s 𝑧)))
74	71, 73	eqeq12d 2753	. . . . . . . . . . . . . . 15 ⊢ (𝑧𝑂 = 𝑧 → (((𝐴 ·s 𝑦) ·s 𝑧𝑂) = (𝐴 ·s (𝑦 ·s 𝑧𝑂)) ↔ ((𝐴 ·s 𝑦) ·s 𝑧) = (𝐴 ·s (𝑦 ·s 𝑧))))
75		mulsasslem3.10	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)))
76	75	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)))
77	70, 74, 76, 20, 30	rspc2dv 3637	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝑦) ·s 𝑧) = (𝐴 ·s (𝑦 ·s 𝑧)))
78	45, 65, 58	addsubsd 28112	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝑥 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = ((((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) +s ((𝑥 ·s 𝑦) ·s 𝐶)))
79	1	oveq1d 7446	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = ((𝑥 ·s 𝐵) ·s 𝑧𝑂))
80		oveq1 7438	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)) = (𝑥 ·s (𝐵 ·s 𝑧𝑂)))
81	79, 80	eqeq12d 2753	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝐵) ·s 𝑧𝑂) = (𝑥 ·s (𝐵 ·s 𝑧𝑂))))
82		oveq2 7439	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧𝑂 = 𝑧 → ((𝑥 ·s 𝐵) ·s 𝑧𝑂) = ((𝑥 ·s 𝐵) ·s 𝑧))
83	23	oveq2d 7447	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧𝑂 = 𝑧 → (𝑥 ·s (𝐵 ·s 𝑧𝑂)) = (𝑥 ·s (𝐵 ·s 𝑧)))
84	82, 83	eqeq12d 2753	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧𝑂 = 𝑧 → (((𝑥 ·s 𝐵) ·s 𝑧𝑂) = (𝑥 ·s (𝐵 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝐵) ·s 𝑧) = (𝑥 ·s (𝐵 ·s 𝑧))))
85		mulsasslem3.9	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)))
86	85	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)))
87	81, 84, 86, 9, 30	rspc2dv 3637	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) ·s 𝑧) = (𝑥 ·s (𝐵 ·s 𝑧)))
88		oveq1 7438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s 𝑦𝑂) = (𝑥 ·s 𝑦𝑂))
89	88	oveq1d 7446	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = ((𝑥 ·s 𝑦𝑂) ·s 𝐶))
90		oveq1 7438	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)) = (𝑥 ·s (𝑦𝑂 ·s 𝐶)))
91	89, 90	eqeq12d 2753	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)) ↔ ((𝑥 ·s 𝑦𝑂) ·s 𝐶) = (𝑥 ·s (𝑦𝑂 ·s 𝐶))))
92		oveq2 7439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦𝑂 = 𝑦 → (𝑥 ·s 𝑦𝑂) = (𝑥 ·s 𝑦))
93	92	oveq1d 7446	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦𝑂 = 𝑦 → ((𝑥 ·s 𝑦𝑂) ·s 𝐶) = ((𝑥 ·s 𝑦) ·s 𝐶))
94	13	oveq2d 7447	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦𝑂 = 𝑦 → (𝑥 ·s (𝑦𝑂 ·s 𝐶)) = (𝑥 ·s (𝑦 ·s 𝐶)))
95	93, 94	eqeq12d 2753	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦𝑂 = 𝑦 → (((𝑥 ·s 𝑦𝑂) ·s 𝐶) = (𝑥 ·s (𝑦𝑂 ·s 𝐶)) ↔ ((𝑥 ·s 𝑦) ·s 𝐶) = (𝑥 ·s (𝑦 ·s 𝐶))))
96		mulsasslem3.8	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)))
97	96	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)))
98	91, 95, 97, 9, 20	rspc2dv 3637	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝑦) ·s 𝐶) = (𝑥 ·s (𝑦 ·s 𝐶)))
99	87, 98	oveq12d 7449	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝑥 ·s 𝑦) ·s 𝐶)) = ((𝑥 ·s (𝐵 ·s 𝑧)) +s (𝑥 ·s (𝑦 ·s 𝐶))))
100	38, 44	mulscld 28161	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐵 ·s 𝑧) ∈ No )
101	36, 100	mulscld 28161	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (𝐵 ·s 𝑧)) ∈ No )
102	52, 64	mulscld 28161	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑦 ·s 𝐶) ∈ No )
103	36, 102	mulscld 28161	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (𝑦 ·s 𝐶)) ∈ No )
104	101, 103	addscomd 28000	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s (𝐵 ·s 𝑧)) +s (𝑥 ·s (𝑦 ·s 𝐶))) = ((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))))
105	99, 104	eqtrd 2777	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝑥 ·s 𝑦) ·s 𝐶)) = ((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))))
106	88	oveq1d 7446	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = ((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂))
107		oveq1 7438	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)) = (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂)))
108	106, 107	eqeq12d 2753	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂))))
109	92	oveq1d 7446	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦𝑂 = 𝑦 → ((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂) = ((𝑥 ·s 𝑦) ·s 𝑧𝑂))
110	68	oveq2d 7447	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦𝑂 = 𝑦 → (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂)) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))
111	109, 110	eqeq12d 2753	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦𝑂 = 𝑦 → (((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂))))
112		oveq2 7439	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧𝑂 = 𝑧 → ((𝑥 ·s 𝑦) ·s 𝑧𝑂) = ((𝑥 ·s 𝑦) ·s 𝑧))
113	72	oveq2d 7447	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧𝑂 = 𝑧 → (𝑥 ·s (𝑦 ·s 𝑧𝑂)) = (𝑥 ·s (𝑦 ·s 𝑧)))
114	112, 113	eqeq12d 2753	. . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)))
117	108, 111, 114, 116, 9, 20, 30	rspc3dv 3641	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝑦) ·s 𝑧) = (𝑥 ·s (𝑦 ·s 𝑧)))
118	105, 117	oveq12d 7449	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝑥 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
119	78, 118	eqtr3d 2779	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) +s ((𝑥 ·s 𝑦) ·s 𝐶)) = (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
120	77, 119	oveq12d 7449	. . . . . . . . . . . . 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 2781	. . . . . . . . . . . 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 7449	. . . . . . . . . . 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 28161	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s 𝐵) ∈ No )
124	123, 44	mulscld 28161	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝐵) ·s 𝑧) ∈ No )
125	45, 54	addscld 28013	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) ∈ No )
126	125, 58	subscld 28093	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) ∈ No )
127	124, 126, 65	subsubs4d 28124	. . . . . . . . . . 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 28161	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (𝐵 ·s 𝑧)) ∈ No )
129	52, 44	mulscld 28161	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑦 ·s 𝑧) ∈ No )
130	47, 129	mulscld 28161	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (𝑦 ·s 𝑧)) ∈ No )
131	103, 101	addscld 28013	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) ∈ No )
132	36, 129	mulscld 28161	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (𝑦 ·s 𝑧)) ∈ No )
133	131, 132	subscld 28093	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))) ∈ No )
134	128, 130, 133	subsubs4d 28124	. . . . . . . . . . 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 2787	. . . . . . . . . 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 7449	. . . . . . . . 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 28161	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝑦) ·s 𝐶) ∈ No )
138	124, 126	subscld 28093	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧))) ∈ No )
139	137, 138, 65	addsubsd 28112	. . . . . . . . . 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 28111	. . . . . . . . . 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 2779	. . . . . . . . 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 28161	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (𝑦 ·s 𝐶)) ∈ No )
143	142, 128, 130	addsubsassd 28111	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))) = ((𝐴 ·s (𝑦 ·s 𝐶)) +s ((𝐴 ·s (𝐵 ·s 𝑧)) -s (𝐴 ·s (𝑦 ·s 𝑧)))))
144	143	oveq1d 7446	. . . . . . . . . 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 28093	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s (𝐵 ·s 𝑧)) -s (𝐴 ·s (𝑦 ·s 𝑧))) ∈ No )
146	142, 145, 133	addsubsassd 28111	. . . . . . . . . 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 2777	. . . . . . . . 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 2787	. . . . . . . 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 7449	. . . . . . 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 28161	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) ·s 𝐶) ∈ No )
151	150, 137	addscld 28013	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) ∈ No )
152	151, 65	subscld 28093	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)) ∈ No )
153	152, 124, 126	addsubsassd 28111	. . . . . . . 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 28111	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)) = (((𝑥 ·s 𝐵) ·s 𝐶) +s (((𝐴 ·s 𝑦) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶))))
155	154	oveq1d 7446	. . . . . . . 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 28093	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s 𝑦) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶)) ∈ No )
157	150, 156, 138	addsassd 28039	. . . . . . . 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 2781	. . . . . . 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 28161	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐵 ·s 𝐶) ∈ No )
160	36, 159	mulscld 28161	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (𝐵 ·s 𝐶)) ∈ No )
161	142, 128	addscld 28013	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) ∈ No )
162	161, 130	subscld 28093	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))) ∈ No )
163	160, 162, 133	addsubsassd 28111	. . . . . . 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 2787	. . . . . 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 28013	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ∈ No )
166	165, 57, 64	subsdird 28185	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝐶) = ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶)))
167	39, 53, 64	addsdird 28183	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝐶) = (((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)))
168	167	oveq1d 7446	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶)) = ((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)))
169	166, 168	eqtrd 2777	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝐶) = ((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)))
170	169	oveq1d 7446	. . . . . . 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 28185	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝑧) = ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)))
172	39, 53, 44	addsdird 28183	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝑧) = (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)))
173	172	oveq1d 7446	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))
174	171, 173	eqtrd 2777	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝑧) = ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))
175	170, 174	oveq12d 7449	. . . . . 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 28013	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) ∈ No )
177	47, 176, 129	subsdid 28184	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))) = ((𝐴 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))))
178	47, 102, 100	addsdid 28182	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) = ((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))))
179	178	oveq1d 7446	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))) = (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))))
180	177, 179	eqtrd 2777	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))) = (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))))
181	180	oveq2d 7447	. . . . . . 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 28184	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))) = ((𝑥 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
183	36, 102, 100	addsdid 28182	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) = ((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))))
184	183	oveq1d 7446	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))) = (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
185	182, 184	eqtrd 2777	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))) = (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
186	181, 185	oveq12d 7449	. . . . . 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 2787	. . . . 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 2748	. . . 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 467	. . 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 3220	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 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∀wral 3061  ∃wrex 3070   ∪ cun 3949   ⊆ wss 3951  ‘cfv 6561  (class class class)co 7431   No csur 27684   L cleft 27884   R cright 27885   +_s cadds 27992   -_s csubs 28052   ·_s cmuls 28132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-ot 4635  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-1o 8506  df-2o 8507  df-nadd 8704  df-no 27687  df-slt 27688  df-bday 27689  df-sle 27790  df-sslt 27826  df-scut 27828  df-0s 27869  df-made 27886  df-old 27887  df-left 27889  df-right 27890  df-norec 27971  df-norec2 27982  df-adds 27993  df-negs 28053  df-subs 28054  df-muls 28133

This theorem is referenced by:  mulsass  28192