Theorem mulsasslem3 28431

Description: Lemma for mulsass 28432. 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 7421	. . . . . . . . . . 11 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s 𝐵) = (𝑥 ·s 𝐵))
2	1	oveq1d 7429	. . . . . . . . . 10 ⊢ (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝐵) ·s 𝐶) = ((𝑥 ·s 𝐵) ·s 𝐶))
3		oveq1 7421	. . . . . . . . . 10 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝐵 ·s 𝐶)) = (𝑥 ·s (𝐵 ·s 𝐶)))
4	2, 3	eqeq12d 2776	. . . . . . . . 9 ⊢ (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝐵) ·s 𝐶) = (𝑥𝑂 ·s (𝐵 ·s 𝐶)) ↔ ((𝑥 ·s 𝐵) ·s 𝐶) = (𝑥 ·s (𝐵 ·s 𝐶))))
5		mulsasslem3.11	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))((𝑥𝑂 ·s 𝐵) ·s 𝐶) = (𝑥𝑂 ·s (𝐵 ·s 𝐶)))
6	5	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))((𝑥𝑂 ·s 𝐵) ·s 𝐶) = (𝑥𝑂 ·s (𝐵 ·s 𝐶)))
7		mulsasslem3.4	. . . . . . . . . 10 ⊢ 𝑃 ⊆ (( L ‘𝐴) ∪ ( R ‘𝐴))
8		simprll 791	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑥 ∈ 𝑃)
9	7, 8	sselid 3929	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑥 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
10	4, 6, 9	rspcdva 3577	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) ·s 𝐶) = (𝑥 ·s (𝐵 ·s 𝐶)))
11		oveq2 7422	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑦 → (𝐴 ·s 𝑦𝑂) = (𝐴 ·s 𝑦))
12	11	oveq1d 7429	. . . . . . . . . . . 12 ⊢ (𝑦𝑂 = 𝑦 → ((𝐴 ·s 𝑦𝑂) ·s 𝐶) = ((𝐴 ·s 𝑦) ·s 𝐶))
13		oveq1 7421	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑦 → (𝑦𝑂 ·s 𝐶) = (𝑦 ·s 𝐶))
14	13	oveq2d 7430	. . . . . . . . . . . 12 ⊢ (𝑦𝑂 = 𝑦 → (𝐴 ·s (𝑦𝑂 ·s 𝐶)) = (𝐴 ·s (𝑦 ·s 𝐶)))
15	12, 14	eqeq12d 2776	. . . . . . . . . . 11 ⊢ (𝑦𝑂 = 𝑦 → (((𝐴 ·s 𝑦𝑂) ·s 𝐶) = (𝐴 ·s (𝑦𝑂 ·s 𝐶)) ↔ ((𝐴 ·s 𝑦) ·s 𝐶) = (𝐴 ·s (𝑦 ·s 𝐶))))
16		mulsasslem3.12	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝐴 ·s 𝑦𝑂) ·s 𝐶) = (𝐴 ·s (𝑦𝑂 ·s 𝐶)))
17	16	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝐴 ·s 𝑦𝑂) ·s 𝐶) = (𝐴 ·s (𝑦𝑂 ·s 𝐶)))
18		mulsasslem3.5	. . . . . . . . . . . 12 ⊢ 𝑄 ⊆ (( L ‘𝐵) ∪ ( R ‘𝐵))
19		simprlr 792	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑦 ∈ 𝑄)
20	18, 19	sselid 3929	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑦 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵)))
21	15, 17, 20	rspcdva 3577	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝑦) ·s 𝐶) = (𝐴 ·s (𝑦 ·s 𝐶)))
22		oveq2 7422	. . . . . . . . . . . . . 14 ⊢ (𝑧𝑂 = 𝑧 → ((𝐴 ·s 𝐵) ·s 𝑧𝑂) = ((𝐴 ·s 𝐵) ·s 𝑧))
23		oveq2 7422	. . . . . . . . . . . . . . 15 ⊢ (𝑧𝑂 = 𝑧 → (𝐵 ·s 𝑧𝑂) = (𝐵 ·s 𝑧))
24	23	oveq2d 7430	. . . . . . . . . . . . . 14 ⊢ (𝑧𝑂 = 𝑧 → (𝐴 ·s (𝐵 ·s 𝑧𝑂)) = (𝐴 ·s (𝐵 ·s 𝑧)))
25	22, 24	eqeq12d 2776	. . . . . . . . . . . . 13 ⊢ (𝑧𝑂 = 𝑧 → (((𝐴 ·s 𝐵) ·s 𝑧𝑂) = (𝐴 ·s (𝐵 ·s 𝑧𝑂)) ↔ ((𝐴 ·s 𝐵) ·s 𝑧) = (𝐴 ·s (𝐵 ·s 𝑧))))
26		mulsasslem3.13	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝐵) ·s 𝑧𝑂) = (𝐴 ·s (𝐵 ·s 𝑧𝑂)))
27	26	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝐵) ·s 𝑧𝑂) = (𝐴 ·s (𝐵 ·s 𝑧𝑂)))
28		mulsasslem3.6	. . . . . . . . . . . . . 14 ⊢ 𝑅 ⊆ (( L ‘𝐶) ∪ ( R ‘𝐶))
29		simprr 785	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑧 ∈ 𝑅)
30	28, 29	sselid 3929	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑧 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶)))
31	25, 27, 30	rspcdva 3577	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝐵) ·s 𝑧) = (𝐴 ·s (𝐵 ·s 𝑧)))
32		leftssno 28139	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( L ‘𝐴) ⊆ No
33		rightssno 28140	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( R ‘𝐴) ⊆ No
34	32, 33	unssi 4137	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (( L ‘𝐴) ∪ ( R ‘𝐴)) ⊆ No
35	7, 34	sstri 3940	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑃 ⊆ No
36	35, 8	sselid 3929	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑥 ∈ No )
37		mulsasslem3.2	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ No )
38	37	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝐵 ∈ No )
39	36, 38	mulscld 28401	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s 𝐵) ∈ No )
40		leftssno 28139	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ( L ‘𝐶) ⊆ No
41		rightssno 28140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ( R ‘𝐶) ⊆ No
42	40, 41	unssi 4137	. . . . . . . . . . . . . . . . . . . 20 ⊢ (( L ‘𝐶) ∪ ( R ‘𝐶)) ⊆ No
43	28, 42	sstri 3940	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑅 ⊆ No
44	43, 29	sselid 3929	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑧 ∈ No )
45	39, 44	mulscld 28401	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) ·s 𝑧) ∈ No )
46		mulsasslem3.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ No )
47	46	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝐴 ∈ No )
48		leftssno 28139	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( L ‘𝐵) ⊆ No
49		rightssno 28140	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( R ‘𝐵) ⊆ No
50	48, 49	unssi 4137	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (( L ‘𝐵) ∪ ( R ‘𝐵)) ⊆ No
51	18, 50	sstri 3940	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑄 ⊆ No
52	51, 19	sselid 3929	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑦 ∈ No )
53	47, 52	mulscld 28401	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s 𝑦) ∈ No )
54	53, 44	mulscld 28401	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝑦) ·s 𝑧) ∈ No )
55	45, 54	addscomd 28233	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) = (((𝐴 ·s 𝑦) ·s 𝑧) +s ((𝑥 ·s 𝐵) ·s 𝑧)))
56	55	oveq1d 7429	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = ((((𝐴 ·s 𝑦) ·s 𝑧) +s ((𝑥 ·s 𝐵) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))
57	36, 52	mulscld 28401	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s 𝑦) ∈ No )
58	57, 44	mulscld 28401	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝑦) ·s 𝑧) ∈ No )
59	54, 45, 58	addsubsassd 28347	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝐴 ·s 𝑦) ·s 𝑧) +s ((𝑥 ·s 𝐵) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = (((𝐴 ·s 𝑦) ·s 𝑧) +s (((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧))))
60	56, 59	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = (((𝐴 ·s 𝑦) ·s 𝑧) +s (((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧))))
61	60	oveq1d 7429	. . . . . . . . . . . . 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 28329	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) ∈ No )
63		mulsasslem3.3	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ No )
64	63	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝐶 ∈ No )
65	57, 64	mulscld 28401	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝑦) ·s 𝐶) ∈ No )
66	54, 62, 65	addsassd 28272	. . . . . . . . . . . . 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 7429	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑂 = 𝑦 → ((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = ((𝐴 ·s 𝑦) ·s 𝑧𝑂))
68		oveq1 7421	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦𝑂 = 𝑦 → (𝑦𝑂 ·s 𝑧𝑂) = (𝑦 ·s 𝑧𝑂))
69	68	oveq2d 7430	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑂 = 𝑦 → (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)) = (𝐴 ·s (𝑦 ·s 𝑧𝑂)))
70	67, 69	eqeq12d 2776	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑦 → (((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)) ↔ ((𝐴 ·s 𝑦) ·s 𝑧𝑂) = (𝐴 ·s (𝑦 ·s 𝑧𝑂))))
71		oveq2 7422	. . . . . . . . . . . . . . . 16 ⊢ (𝑧𝑂 = 𝑧 → ((𝐴 ·s 𝑦) ·s 𝑧𝑂) = ((𝐴 ·s 𝑦) ·s 𝑧))
72		oveq2 7422	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧𝑂 = 𝑧 → (𝑦 ·s 𝑧𝑂) = (𝑦 ·s 𝑧))
73	72	oveq2d 7430	. . . . . . . . . . . . . . . 16 ⊢ (𝑧𝑂 = 𝑧 → (𝐴 ·s (𝑦 ·s 𝑧𝑂)) = (𝐴 ·s (𝑦 ·s 𝑧)))
74	71, 73	eqeq12d 2776	. . . . . . . . . . . . . . 15 ⊢ (𝑧𝑂 = 𝑧 → (((𝐴 ·s 𝑦) ·s 𝑧𝑂) = (𝐴 ·s (𝑦 ·s 𝑧𝑂)) ↔ ((𝐴 ·s 𝑦) ·s 𝑧) = (𝐴 ·s (𝑦 ·s 𝑧))))
75		mulsasslem3.10	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)))
76	75	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)))
77	70, 74, 76, 20, 30	rspc2dv 3591	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝑦) ·s 𝑧) = (𝐴 ·s (𝑦 ·s 𝑧)))
78	45, 65, 58	addsubsd 28348	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝑥 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = ((((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) +s ((𝑥 ·s 𝑦) ·s 𝐶)))
79	1	oveq1d 7429	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = ((𝑥 ·s 𝐵) ·s 𝑧𝑂))
80		oveq1 7421	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)) = (𝑥 ·s (𝐵 ·s 𝑧𝑂)))
81	79, 80	eqeq12d 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝐵) ·s 𝑧𝑂) = (𝑥 ·s (𝐵 ·s 𝑧𝑂))))
82		oveq2 7422	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧𝑂 = 𝑧 → ((𝑥 ·s 𝐵) ·s 𝑧𝑂) = ((𝑥 ·s 𝐵) ·s 𝑧))
83	23	oveq2d 7430	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧𝑂 = 𝑧 → (𝑥 ·s (𝐵 ·s 𝑧𝑂)) = (𝑥 ·s (𝐵 ·s 𝑧)))
84	82, 83	eqeq12d 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧𝑂 = 𝑧 → (((𝑥 ·s 𝐵) ·s 𝑧𝑂) = (𝑥 ·s (𝐵 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝐵) ·s 𝑧) = (𝑥 ·s (𝐵 ·s 𝑧))))
85		mulsasslem3.9	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)))
86	85	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)))
87	81, 84, 86, 9, 30	rspc2dv 3591	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) ·s 𝑧) = (𝑥 ·s (𝐵 ·s 𝑧)))
88		oveq1 7421	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s 𝑦𝑂) = (𝑥 ·s 𝑦𝑂))
89	88	oveq1d 7429	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = ((𝑥 ·s 𝑦𝑂) ·s 𝐶))
90		oveq1 7421	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)) = (𝑥 ·s (𝑦𝑂 ·s 𝐶)))
91	89, 90	eqeq12d 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)) ↔ ((𝑥 ·s 𝑦𝑂) ·s 𝐶) = (𝑥 ·s (𝑦𝑂 ·s 𝐶))))
92		oveq2 7422	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦𝑂 = 𝑦 → (𝑥 ·s 𝑦𝑂) = (𝑥 ·s 𝑦))
93	92	oveq1d 7429	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦𝑂 = 𝑦 → ((𝑥 ·s 𝑦𝑂) ·s 𝐶) = ((𝑥 ·s 𝑦) ·s 𝐶))
94	13	oveq2d 7430	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦𝑂 = 𝑦 → (𝑥 ·s (𝑦𝑂 ·s 𝐶)) = (𝑥 ·s (𝑦 ·s 𝐶)))
95	93, 94	eqeq12d 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦𝑂 = 𝑦 → (((𝑥 ·s 𝑦𝑂) ·s 𝐶) = (𝑥 ·s (𝑦𝑂 ·s 𝐶)) ↔ ((𝑥 ·s 𝑦) ·s 𝐶) = (𝑥 ·s (𝑦 ·s 𝐶))))
96		mulsasslem3.8	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)))
97	96	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)))
98	91, 95, 97, 9, 20	rspc2dv 3591	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝑦) ·s 𝐶) = (𝑥 ·s (𝑦 ·s 𝐶)))
99	87, 98	oveq12d 7432	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝑥 ·s 𝑦) ·s 𝐶)) = ((𝑥 ·s (𝐵 ·s 𝑧)) +s (𝑥 ·s (𝑦 ·s 𝐶))))
100	38, 44	mulscld 28401	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐵 ·s 𝑧) ∈ No )
101	36, 100	mulscld 28401	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (𝐵 ·s 𝑧)) ∈ No )
102	52, 64	mulscld 28401	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑦 ·s 𝐶) ∈ No )
103	36, 102	mulscld 28401	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (𝑦 ·s 𝐶)) ∈ No )
104	101, 103	addscomd 28233	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s (𝐵 ·s 𝑧)) +s (𝑥 ·s (𝑦 ·s 𝐶))) = ((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))))
105	99, 104	eqtrd 2795	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝑥 ·s 𝑦) ·s 𝐶)) = ((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))))
106	88	oveq1d 7429	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = ((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂))
107		oveq1 7421	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)) = (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂)))
108	106, 107	eqeq12d 2776	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂))))
109	92	oveq1d 7429	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦𝑂 = 𝑦 → ((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂) = ((𝑥 ·s 𝑦) ·s 𝑧𝑂))
110	68	oveq2d 7430	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦𝑂 = 𝑦 → (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂)) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))
111	109, 110	eqeq12d 2776	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦𝑂 = 𝑦 → (((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂))))
112		oveq2 7422	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧𝑂 = 𝑧 → ((𝑥 ·s 𝑦) ·s 𝑧𝑂) = ((𝑥 ·s 𝑦) ·s 𝑧))
113	72	oveq2d 7430	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧𝑂 = 𝑧 → (𝑥 ·s (𝑦 ·s 𝑧𝑂)) = (𝑥 ·s (𝑦 ·s 𝑧)))
114	112, 113	eqeq12d 2776	. . . . . . . . . . . . . . . . 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 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)))
117	108, 111, 114, 116, 9, 20, 30	rspc3dv 3595	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝑦) ·s 𝑧) = (𝑥 ·s (𝑦 ·s 𝑧)))
118	105, 117	oveq12d 7432	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝑥 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
119	78, 118	eqtr3d 2797	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) +s ((𝑥 ·s 𝑦) ·s 𝐶)) = (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
120	77, 119	oveq12d 7432	. . . . . . . . . . . . 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 2799	. . . . . . . . . . . 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 7432	. . . . . . . . . . 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 28401	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s 𝐵) ∈ No )
124	123, 44	mulscld 28401	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝐵) ·s 𝑧) ∈ No )
125	45, 54	addscld 28246	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) ∈ No )
126	125, 58	subscld 28329	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)) ∈ No )
127	124, 126, 65	subsubs4d 28360	. . . . . . . . . . 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 28401	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (𝐵 ·s 𝑧)) ∈ No )
129	52, 44	mulscld 28401	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑦 ·s 𝑧) ∈ No )
130	47, 129	mulscld 28401	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (𝑦 ·s 𝑧)) ∈ No )
131	103, 101	addscld 28246	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) ∈ No )
132	36, 129	mulscld 28401	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (𝑦 ·s 𝑧)) ∈ No )
133	131, 132	subscld 28329	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))) ∈ No )
134	128, 130, 133	subsubs4d 28360	. . . . . . . . . . 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 2805	. . . . . . . . . 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 7432	. . . . . . . . 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 28401	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝑦) ·s 𝐶) ∈ No )
138	124, 126	subscld 28329	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s 𝐵) ·s 𝑧) -s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧))) ∈ No )
139	137, 138, 65	addsubsd 28348	. . . . . . . . . 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 28347	. . . . . . . . . 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 2797	. . . . . . . . 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 28401	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (𝑦 ·s 𝐶)) ∈ No )
143	142, 128, 130	addsubsassd 28347	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))) = ((𝐴 ·s (𝑦 ·s 𝐶)) +s ((𝐴 ·s (𝐵 ·s 𝑧)) -s (𝐴 ·s (𝑦 ·s 𝑧)))))
144	143	oveq1d 7429	. . . . . . . . . 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 28329	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s (𝐵 ·s 𝑧)) -s (𝐴 ·s (𝑦 ·s 𝑧))) ∈ No )
146	142, 145, 133	addsubsassd 28347	. . . . . . . . . 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 2795	. . . . . . . . 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 2805	. . . . . . . 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 7432	. . . . . . 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 28401	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) ·s 𝐶) ∈ No )
151	150, 137	addscld 28246	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) ∈ No )
152	151, 65	subscld 28329	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)) ∈ No )
153	152, 124, 126	addsubsassd 28347	. . . . . . . 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 28347	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)) = (((𝑥 ·s 𝐵) ·s 𝐶) +s (((𝐴 ·s 𝑦) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶))))
155	154	oveq1d 7429	. . . . . . . 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 28329	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s 𝑦) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶)) ∈ No )
157	150, 156, 138	addsassd 28272	. . . . . . . 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 2799	. . . . . . 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 28401	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐵 ·s 𝐶) ∈ No )
160	36, 159	mulscld 28401	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (𝐵 ·s 𝐶)) ∈ No )
161	142, 128	addscld 28246	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) ∈ No )
162	161, 130	subscld 28329	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))) ∈ No )
163	160, 162, 133	addsubsassd 28347	. . . . . . 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 2805	. . . . . 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 28246	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ∈ No )
166	165, 57, 64	subsdird 28425	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝐶) = ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶)))
167	39, 53, 64	addsdird 28423	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝐶) = (((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)))
168	167	oveq1d 7429	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝐶) -s ((𝑥 ·s 𝑦) ·s 𝐶)) = ((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)))
169	166, 168	eqtrd 2795	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝐶) = ((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) -s ((𝑥 ·s 𝑦) ·s 𝐶)))
170	169	oveq1d 7429	. . . . . . 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 28425	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝑧) = ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)))
172	39, 53, 44	addsdird 28423	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝑧) = (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)))
173	172	oveq1d 7429	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝑧) -s ((𝑥 ·s 𝑦) ·s 𝑧)) = ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))
174	171, 173	eqtrd 2795	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝑧) = ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) -s ((𝑥 ·s 𝑦) ·s 𝑧)))
175	170, 174	oveq12d 7432	. . . . . 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 28246	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) ∈ No )
177	47, 176, 129	subsdid 28424	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))) = ((𝐴 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))))
178	47, 102, 100	addsdid 28422	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) = ((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))))
179	178	oveq1d 7429	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))) = (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))))
180	177, 179	eqtrd 2795	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))) = (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) -s (𝐴 ·s (𝑦 ·s 𝑧))))
181	180	oveq2d 7430	. . . . . . 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 28424	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))) = ((𝑥 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
183	36, 102, 100	addsdid 28422	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) = ((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))))
184	183	oveq1d 7429	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))) = (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
185	182, 184	eqtrd 2795	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))) = (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) -s (𝑥 ·s (𝑦 ·s 𝑧))))
186	181, 185	oveq12d 7432	. . . . . 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 2805	. . . . 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 2771	. . . 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 473	. . 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 3184	. 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 3225	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 𝑧))))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3076  ∃wrex 3086   ∪ cun 3897   ⊆ wss 3899  ‘cfv 6533  (class class class)co 7414   No csur 27877   L cleft 28091   R cright 28092   +_s cadds 28225   -_s csubs 28286   ·_s cmuls 28372

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-ot 4593  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-1st 7987  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-1o 8456  df-2o 8457  df-nadd 8655  df-no 27880  df-lts 27881  df-bday 27882  df-les 27982  df-slts 28024  df-cuts 28026  df-0s 28073  df-made 28093  df-old 28094  df-left 28096  df-right 28097  df-norec 28204  df-norec2 28215  df-adds 28226  df-negs 28287  df-subs 28288  df-muls 28373

This theorem is used by:  mulsass  28432