Theorem mulsasslem3 28563

Description: Lemma for mulsass 28564. 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 7434	. . . . . . . . . . 11 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s 𝐵) = (𝑥 ·s 𝐵))
2	1	oveq1d 7442	. . . . . . . . . 10 ⊢ (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝐵) ·s 𝐶) = ((𝑥 ·s 𝐵) ·s 𝐶))
3		oveq1 7434	. . . . . . . . . 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 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑥𝑂 ∈ ((L‘𝐴) ∪ (R‘𝐴))((𝑥𝑂 ·s 𝐵) ·s 𝐶) = (𝑥𝑂 ·s (𝐵 ·s 𝐶)))
7		mulsasslem3.4	. . . . . . . . . 10 ⊢ 𝑃 ⊆ ((L‘𝐴) ∪ (R‘𝐴))
8		simprll 791	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑥 ∈ 𝑃)
9	7, 8	sselid 3910	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑥 ∈ ((L‘𝐴) ∪ (R‘𝐴)))
10	4, 6, 9	rspcdva 3580	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) ·s 𝐶) = (𝑥 ·s (𝐵 ·s 𝐶)))
11		oveq2 7435	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑦 → (𝐴 ·s 𝑦𝑂) = (𝐴 ·s 𝑦))
12	11	oveq1d 7442	. . . . . . . . . . . 12 ⊢ (𝑦𝑂 = 𝑦 → ((𝐴 ·s 𝑦𝑂) ·s 𝐶) = ((𝐴 ·s 𝑦) ·s 𝐶))
13		oveq1 7434	. . . . . . . . . . . . 13 ⊢ (𝑦𝑂 = 𝑦 → (𝑦𝑂 ·s 𝐶) = (𝑦 ·s 𝐶))
14	13	oveq2d 7443	. . . . . . . . . . . 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 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑦𝑂 ∈ ((L‘𝐵) ∪ (R‘𝐵))((𝐴 ·s 𝑦𝑂) ·s 𝐶) = (𝐴 ·s (𝑦𝑂 ·s 𝐶)))
18		mulsasslem3.5	. . . . . . . . . . . 12 ⊢ 𝑄 ⊆ ((L‘𝐵) ∪ (R‘𝐵))
19		simprlr 792	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑦 ∈ 𝑄)
20	18, 19	sselid 3910	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑦 ∈ ((L‘𝐵) ∪ (R‘𝐵)))
21	15, 17, 20	rspcdva 3580	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝑦) ·s 𝐶) = (𝐴 ·s (𝑦 ·s 𝐶)))
22		oveq2 7435	. . . . . . . . . . . . . 14 ⊢ (𝑧𝑂 = 𝑧 → ((𝐴 ·s 𝐵) ·s 𝑧𝑂) = ((𝐴 ·s 𝐵) ·s 𝑧))
23		oveq2 7435	. . . . . . . . . . . . . . 15 ⊢ (𝑧𝑂 = 𝑧 → (𝐵 ·s 𝑧𝑂) = (𝐵 ·s 𝑧))
24	23	oveq2d 7443	. . . . . . . . . . . . . 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 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑧𝑂 ∈ ((L‘𝐶) ∪ (R‘𝐶))((𝐴 ·s 𝐵) ·s 𝑧𝑂) = (𝐴 ·s (𝐵 ·s 𝑧𝑂)))
28		mulsasslem3.6	. . . . . . . . . . . . . 14 ⊢ 𝑅 ⊆ ((L‘𝐶) ∪ (R‘𝐶))
29		simprr 785	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑧 ∈ 𝑅)
30	28, 29	sselid 3910	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑧 ∈ ((L‘𝐶) ∪ (R‘𝐶)))
31	25, 27, 30	rspcdva 3580	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝐵) ·s 𝑧) = (𝐴 ·s (𝐵 ·s 𝑧)))
32		leftssno 28271	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (L‘𝐴) ⊆ No
33		rightssno 28272	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (R‘𝐴) ⊆ No
34	32, 33	unssi 4191	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((L‘𝐴) ∪ (R‘𝐴)) ⊆ No
35	7, 34	sstri 3921	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑃 ⊆ No
36	35, 8	sselid 3910	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑥 ∈ No)
37		mulsasslem3.2	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ No)
38	37	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝐵 ∈ No)
39	36, 38	mulscld 28533	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s 𝐵) ∈ No)
40		leftssno 28271	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (L‘𝐶) ⊆ No
41		rightssno 28272	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (R‘𝐶) ⊆ No
42	40, 41	unssi 4191	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((L‘𝐶) ∪ (R‘𝐶)) ⊆ No
43	28, 42	sstri 3921	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑅 ⊆ No
44	43, 29	sselid 3910	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑧 ∈ No)
45	39, 44	mulscld 28533	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) ·s 𝑧) ∈ No)
46		mulsasslem3.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ No)
47	46	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝐴 ∈ No)
48		leftssno 28271	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (L‘𝐵) ⊆ No
49		rightssno 28272	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (R‘𝐵) ⊆ No
50	48, 49	unssi 4191	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((L‘𝐵) ∪ (R‘𝐵)) ⊆ No
51	18, 50	sstri 3921	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑄 ⊆ No
52	51, 19	sselid 3910	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝑦 ∈ No)
53	47, 52	mulscld 28533	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s 𝑦) ∈ No)
54	53, 44	mulscld 28533	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝑦) ·s 𝑧) ∈ No)
55	45, 54	addscomd 28365	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) = (((𝐴 ·s 𝑦) ·s 𝑧) +s ((𝑥 ·s 𝐵) ·s 𝑧)))
56	55	oveq1d 7442	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) −s ((𝑥 ·s 𝑦) ·s 𝑧)) = ((((𝐴 ·s 𝑦) ·s 𝑧) +s ((𝑥 ·s 𝐵) ·s 𝑧)) −s ((𝑥 ·s 𝑦) ·s 𝑧)))
57	36, 52	mulscld 28533	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s 𝑦) ∈ No)
58	57, 44	mulscld 28533	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝑦) ·s 𝑧) ∈ No)
59	54, 45, 58	addsubsassd 28479	. . . . . . . . . . . . . . 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 7442	. . . . . . . . . . . . 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 28461	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) −s ((𝑥 ·s 𝑦) ·s 𝑧)) ∈ No)
63		mulsasslem3.3	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ No)
64	63	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → 𝐶 ∈ No)
65	57, 64	mulscld 28533	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝑦) ·s 𝐶) ∈ No)
66	54, 62, 65	addsassd 28404	. . . . . . . . . . . . 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 7442	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑂 = 𝑦 → ((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = ((𝐴 ·s 𝑦) ·s 𝑧𝑂))
68		oveq1 7434	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦𝑂 = 𝑦 → (𝑦𝑂 ·s 𝑧𝑂) = (𝑦 ·s 𝑧𝑂))
69	68	oveq2d 7443	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑂 = 𝑦 → (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)) = (𝐴 ·s (𝑦 ·s 𝑧𝑂)))
70	67, 69	eqeq12d 2779	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑂 = 𝑦 → (((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)) ↔ ((𝐴 ·s 𝑦) ·s 𝑧𝑂) = (𝐴 ·s (𝑦 ·s 𝑧𝑂))))
71		oveq2 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝑧𝑂 = 𝑧 → ((𝐴 ·s 𝑦) ·s 𝑧𝑂) = ((𝐴 ·s 𝑦) ·s 𝑧))
72		oveq2 7435	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧𝑂 = 𝑧 → (𝑦 ·s 𝑧𝑂) = (𝑦 ·s 𝑧))
73	72	oveq2d 7443	. . . . . . . . . . . . . . . 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 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑦𝑂 ∈ ((L‘𝐵) ∪ (R‘𝐵))∀𝑧𝑂 ∈ ((L‘𝐶) ∪ (R‘𝐶))((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)))
77	70, 74, 76, 20, 30	rspc2dv 3593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝑦) ·s 𝑧) = (𝐴 ·s (𝑦 ·s 𝑧)))
78	45, 65, 58	addsubsd 28480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝑥 ·s 𝑦) ·s 𝐶)) −s ((𝑥 ·s 𝑦) ·s 𝑧)) = ((((𝑥 ·s 𝐵) ·s 𝑧) −s ((𝑥 ·s 𝑦) ·s 𝑧)) +s ((𝑥 ·s 𝑦) ·s 𝐶)))
79	1	oveq1d 7442	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = ((𝑥 ·s 𝐵) ·s 𝑧𝑂))
80		oveq1 7434	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)) = (𝑥 ·s (𝐵 ·s 𝑧𝑂)))
81	79, 80	eqeq12d 2779	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝐵) ·s 𝑧𝑂) = (𝑥 ·s (𝐵 ·s 𝑧𝑂))))
82		oveq2 7435	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧𝑂 = 𝑧 → ((𝑥 ·s 𝐵) ·s 𝑧𝑂) = ((𝑥 ·s 𝐵) ·s 𝑧))
83	23	oveq2d 7443	. . . . . . . . . . . . . . . . . . . 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 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑥𝑂 ∈ ((L‘𝐴) ∪ (R‘𝐴))∀𝑧𝑂 ∈ ((L‘𝐶) ∪ (R‘𝐶))((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)))
87	81, 84, 86, 9, 30	rspc2dv 3593	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) ·s 𝑧) = (𝑥 ·s (𝐵 ·s 𝑧)))
88		oveq1 7434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s 𝑦𝑂) = (𝑥 ·s 𝑦𝑂))
89	88	oveq1d 7442	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = ((𝑥 ·s 𝑦𝑂) ·s 𝐶))
90		oveq1 7434	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)) = (𝑥 ·s (𝑦𝑂 ·s 𝐶)))
91	89, 90	eqeq12d 2779	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)) ↔ ((𝑥 ·s 𝑦𝑂) ·s 𝐶) = (𝑥 ·s (𝑦𝑂 ·s 𝐶))))
92		oveq2 7435	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦𝑂 = 𝑦 → (𝑥 ·s 𝑦𝑂) = (𝑥 ·s 𝑦))
93	92	oveq1d 7442	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦𝑂 = 𝑦 → ((𝑥 ·s 𝑦𝑂) ·s 𝐶) = ((𝑥 ·s 𝑦) ·s 𝐶))
94	13	oveq2d 7443	. . . . . . . . . . . . . . . . . . . 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 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑥𝑂 ∈ ((L‘𝐴) ∪ (R‘𝐴))∀𝑦𝑂 ∈ ((L‘𝐵) ∪ (R‘𝐵))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)))
98	91, 95, 97, 9, 20	rspc2dv 3593	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝑦) ·s 𝐶) = (𝑥 ·s (𝑦 ·s 𝐶)))
99	87, 98	oveq12d 7445	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝑥 ·s 𝑦) ·s 𝐶)) = ((𝑥 ·s (𝐵 ·s 𝑧)) +s (𝑥 ·s (𝑦 ·s 𝐶))))
100	38, 44	mulscld 28533	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐵 ·s 𝑧) ∈ No)
101	36, 100	mulscld 28533	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (𝐵 ·s 𝑧)) ∈ No)
102	52, 64	mulscld 28533	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑦 ·s 𝐶) ∈ No)
103	36, 102	mulscld 28533	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (𝑦 ·s 𝐶)) ∈ No)
104	101, 103	addscomd 28365	. . . . . . . . . . . . . . . . 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 7442	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑂 = 𝑥 → ((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = ((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂))
107		oveq1 7434	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑂 = 𝑥 → (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)) = (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂)))
108	106, 107	eqeq12d 2779	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑂 = 𝑥 → (((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂))))
109	92	oveq1d 7442	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦𝑂 = 𝑦 → ((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂) = ((𝑥 ·s 𝑦) ·s 𝑧𝑂))
110	68	oveq2d 7443	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦𝑂 = 𝑦 → (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂)) = (𝑥 ·s (𝑦 ·s 𝑧𝑂)))
111	109, 110	eqeq12d 2779	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦𝑂 = 𝑦 → (((𝑥 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥 ·s (𝑦𝑂 ·s 𝑧𝑂)) ↔ ((𝑥 ·s 𝑦) ·s 𝑧𝑂) = (𝑥 ·s (𝑦 ·s 𝑧𝑂))))
112		oveq2 7435	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧𝑂 = 𝑧 → ((𝑥 ·s 𝑦) ·s 𝑧𝑂) = ((𝑥 ·s 𝑦) ·s 𝑧))
113	72	oveq2d 7443	. . . . . . . . . . . . . . . . . 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 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ∀𝑥𝑂 ∈ ((L‘𝐴) ∪ (R‘𝐴))∀𝑦𝑂 ∈ ((L‘𝐵) ∪ (R‘𝐵))∀𝑧𝑂 ∈ ((L‘𝐶) ∪ (R‘𝐶))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)))
117	108, 111, 114, 116, 9, 20, 30	rspc3dv 3597	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝑦) ·s 𝑧) = (𝑥 ·s (𝑦 ·s 𝑧)))
118	105, 117	oveq12d 7445	. . . . . . . . . . . . . . 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 7445	. . . . . . . . . . . . 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 7445	. . . . . . . . . . 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 28533	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s 𝐵) ∈ No)
124	123, 44	mulscld 28533	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝐵) ·s 𝑧) ∈ No)
125	45, 54	addscld 28378	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) ∈ No)
126	125, 58	subscld 28461	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) −s ((𝑥 ·s 𝑦) ·s 𝑧)) ∈ No)
127	124, 126, 65	subsubs4d 28492	. . . . . . . . . . 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 28533	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (𝐵 ·s 𝑧)) ∈ No)
129	52, 44	mulscld 28533	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑦 ·s 𝑧) ∈ No)
130	47, 129	mulscld 28533	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (𝑦 ·s 𝑧)) ∈ No)
131	103, 101	addscld 28378	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) ∈ No)
132	36, 129	mulscld 28533	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (𝑦 ·s 𝑧)) ∈ No)
133	131, 132	subscld 28461	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))) −s (𝑥 ·s (𝑦 ·s 𝑧))) ∈ No)
134	128, 130, 133	subsubs4d 28492	. . . . . . . . . . 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 7445	. . . . . . . . 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 28533	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s 𝑦) ·s 𝐶) ∈ No)
138	124, 126	subscld 28461	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s 𝐵) ·s 𝑧) −s ((((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)) −s ((𝑥 ·s 𝑦) ·s 𝑧))) ∈ No)
139	137, 138, 65	addsubsd 28480	. . . . . . . . . 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 28479	. . . . . . . . . 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 28533	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (𝑦 ·s 𝐶)) ∈ No)
143	142, 128, 130	addsubsassd 28479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) −s (𝐴 ·s (𝑦 ·s 𝑧))) = ((𝐴 ·s (𝑦 ·s 𝐶)) +s ((𝐴 ·s (𝐵 ·s 𝑧)) −s (𝐴 ·s (𝑦 ·s 𝑧)))))
144	143	oveq1d 7442	. . . . . . . . . 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 28461	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s (𝐵 ·s 𝑧)) −s (𝐴 ·s (𝑦 ·s 𝑧))) ∈ No)
146	142, 145, 133	addsubsassd 28479	. . . . . . . . . 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 7445	. . . . . . 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 28533	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) ·s 𝐶) ∈ No)
151	150, 137	addscld 28378	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) ∈ No)
152	151, 65	subscld 28461	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) −s ((𝑥 ·s 𝑦) ·s 𝐶)) ∈ No)
153	152, 124, 126	addsubsassd 28479	. . . . . . . 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 28479	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)) −s ((𝑥 ·s 𝑦) ·s 𝐶)) = (((𝑥 ·s 𝐵) ·s 𝐶) +s (((𝐴 ·s 𝑦) ·s 𝐶) −s ((𝑥 ·s 𝑦) ·s 𝐶))))
155	154	oveq1d 7442	. . . . . . . 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 28461	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s 𝑦) ·s 𝐶) −s ((𝑥 ·s 𝑦) ·s 𝐶)) ∈ No)
157	150, 156, 138	addsassd 28404	. . . . . . . 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 28533	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐵 ·s 𝐶) ∈ No)
160	36, 159	mulscld 28533	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (𝐵 ·s 𝐶)) ∈ No)
161	142, 128	addscld 28378	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) ∈ No)
162	161, 130	subscld 28461	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))) −s (𝐴 ·s (𝑦 ·s 𝑧))) ∈ No)
163	160, 162, 133	addsubsassd 28479	. . . . . . 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 28378	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ∈ No)
166	165, 57, 64	subsdird 28557	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) −s (𝑥 ·s 𝑦)) ·s 𝐶) = ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝐶) −s ((𝑥 ·s 𝑦) ·s 𝐶)))
167	39, 53, 64	addsdird 28555	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝐶) = (((𝑥 ·s 𝐵) ·s 𝐶) +s ((𝐴 ·s 𝑦) ·s 𝐶)))
168	167	oveq1d 7442	. . . . . . . . 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 7442	. . . . . . 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 28557	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) −s (𝑥 ·s 𝑦)) ·s 𝑧) = ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝑧) −s ((𝑥 ·s 𝑦) ·s 𝑧)))
172	39, 53, 44	addsdird 28555	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) ·s 𝑧) = (((𝑥 ·s 𝐵) ·s 𝑧) +s ((𝐴 ·s 𝑦) ·s 𝑧)))
173	172	oveq1d 7442	. . . . . . . 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 7445	. . . . . 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 28378	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) ∈ No)
177	47, 176, 129	subsdid 28556	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) −s (𝑦 ·s 𝑧))) = ((𝐴 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) −s (𝐴 ·s (𝑦 ·s 𝑧))))
178	47, 102, 100	addsdid 28554	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝐴 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) = ((𝐴 ·s (𝑦 ·s 𝐶)) +s (𝐴 ·s (𝐵 ·s 𝑧))))
179	178	oveq1d 7442	. . . . . . . . 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 7443	. . . . . . 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 28556	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) −s (𝑦 ·s 𝑧))) = ((𝑥 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) −s (𝑥 ·s (𝑦 ·s 𝑧))))
183	36, 102, 100	addsdid 28554	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑄) ∧ 𝑧 ∈ 𝑅)) → (𝑥 ·s ((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧))) = ((𝑥 ·s (𝑦 ·s 𝐶)) +s (𝑥 ·s (𝐵 ·s 𝑧))))
184	183	oveq1d 7442	. . . . . . . 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 7445	. . . . . 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 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 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 𝑧))))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2146  ∀wral 3079  ∃wrex 3089   ⊆ wss 3899   ∪ cun 4151  ‘cfv 6546  (class class class)co 7427  Nocsur 28009  Lcleft 28223  Rcright 28224   +_s cadds 28357   −_s csubs 28418   ·_s cmuls 28504

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

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

This theorem is used by:  mulsass  28564