Theorem mulsasslem3

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

	Ref	Expression
Hypotheses	mulsasslem3.1	$$⊢\phi \to A\in \mathrm{No}$$
	mulsasslem3.2	$$⊢\phi \to B\in \mathrm{No}$$
	mulsasslem3.3	$$⊢\phi \to C\in \mathrm{No}$$
	mulsasslem3.4	$$⊢P\subseteq L\left(A\right)\cup R\left(A\right)$$
	mulsasslem3.5	$$⊢Q\subseteq L\left(B\right)\cup R\left(B\right)$$
	mulsasslem3.6	$$⊢R\subseteq L\left(C\right)\cup R\left(C\right)$$
	mulsasslem3.7	No typesetting found for |- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( xO x.s yO ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) ) with typecode |-
	mulsasslem3.8	No typesetting found for |- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( ( xO x.s yO ) x.s C ) = ( xO x.s ( yO x.s C ) ) ) with typecode |-
	mulsasslem3.9	No typesetting found for |- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( xO x.s B ) x.s zO ) = ( xO x.s ( B x.s zO ) ) ) with typecode |-
	mulsasslem3.10	No typesetting found for |- ( ph -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( A x.s yO ) x.s zO ) = ( A x.s ( yO x.s zO ) ) ) with typecode |-
	mulsasslem3.11	No typesetting found for |- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( ( xO x.s B ) x.s C ) = ( xO x.s ( B x.s C ) ) ) with typecode |-
	mulsasslem3.12	No typesetting found for |- ( ph -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( ( A x.s yO ) x.s C ) = ( A x.s ( yO x.s C ) ) ) with typecode |-
	mulsasslem3.13	No typesetting found for |- ( ph -> A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( A x.s B ) x.s zO ) = ( A x.s ( B x.s zO ) ) ) with typecode |-
Assertion	mulsasslem3	$$⊢\phi \to \left(\exists x\in P\exists y\in Q\exists z\in Ra=\left(\left(\left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){-}_s\left(x{\cdot }_{s}y\right)\right){\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right)\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){-}_s\left(x{\cdot }_{s}y\right)\right){\cdot }_{s}z\right)\leftrightarrow \exists x\in P\exists y\in Q\exists z\in Ra=\left(\left(x{\cdot }_s\left(B{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(y{\cdot }_{s}z\right)\right)\right)\right){-}_s\left(x{\cdot }_s\left(\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(y{\cdot }_{s}z\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mulsasslem3.1	$$⊢\phi \to A\in \mathrm{No}$$
2		mulsasslem3.2	$$⊢\phi \to B\in \mathrm{No}$$
3		mulsasslem3.3	$$⊢\phi \to C\in \mathrm{No}$$
4		mulsasslem3.4	$$⊢P\subseteq L\left(A\right)\cup R\left(A\right)$$
5		mulsasslem3.5	$$⊢Q\subseteq L\left(B\right)\cup R\left(B\right)$$
6		mulsasslem3.6	$$⊢R\subseteq L\left(C\right)\cup R\left(C\right)$$
7		mulsasslem3.7	Could not format ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( xO x.s yO ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) ) : No typesetting found for |- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( xO x.s yO ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) ) with typecode |-
8		mulsasslem3.8	Could not format ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( ( xO x.s yO ) x.s C ) = ( xO x.s ( yO x.s C ) ) ) : No typesetting found for |- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( ( xO x.s yO ) x.s C ) = ( xO x.s ( yO x.s C ) ) ) with typecode |-
9		mulsasslem3.9	Could not format ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( xO x.s B ) x.s zO ) = ( xO x.s ( B x.s zO ) ) ) : No typesetting found for |- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( xO x.s B ) x.s zO ) = ( xO x.s ( B x.s zO ) ) ) with typecode |-
10		mulsasslem3.10	Could not format ( ph -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( A x.s yO ) x.s zO ) = ( A x.s ( yO x.s zO ) ) ) : No typesetting found for |- ( ph -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( A x.s yO ) x.s zO ) = ( A x.s ( yO x.s zO ) ) ) with typecode |-
11		mulsasslem3.11	Could not format ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( ( xO x.s B ) x.s C ) = ( xO x.s ( B x.s C ) ) ) : No typesetting found for |- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( ( xO x.s B ) x.s C ) = ( xO x.s ( B x.s C ) ) ) with typecode |-
12		mulsasslem3.12	Could not format ( ph -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( ( A x.s yO ) x.s C ) = ( A x.s ( yO x.s C ) ) ) : No typesetting found for |- ( ph -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( ( A x.s yO ) x.s C ) = ( A x.s ( yO x.s C ) ) ) with typecode |-
13		mulsasslem3.13	Could not format ( ph -> A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( A x.s B ) x.s zO ) = ( A x.s ( B x.s zO ) ) ) : No typesetting found for |- ( ph -> A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( A x.s B ) x.s zO ) = ( A x.s ( B x.s zO ) ) ) with typecode |-
14		oveq1	Could not format ( xO = x -> ( xO x.s B ) = ( x x.s B ) ) : No typesetting found for |- ( xO = x -> ( xO x.s B ) = ( x x.s B ) ) with typecode |-
15	14	oveq1d	Could not format ( xO = x -> ( ( xO x.s B ) x.s C ) = ( ( x x.s B ) x.s C ) ) : No typesetting found for |- ( xO = x -> ( ( xO x.s B ) x.s C ) = ( ( x x.s B ) x.s C ) ) with typecode |-
16		oveq1	Could not format ( xO = x -> ( xO x.s ( B x.s C ) ) = ( x x.s ( B x.s C ) ) ) : No typesetting found for |- ( xO = x -> ( xO x.s ( B x.s C ) ) = ( x x.s ( B x.s C ) ) ) with typecode |-
17	15 16	eqeq12d	Could not format ( xO = x -> ( ( ( xO x.s B ) x.s C ) = ( xO x.s ( B x.s C ) ) <-> ( ( x x.s B ) x.s C ) = ( x x.s ( B x.s C ) ) ) ) : No typesetting found for |- ( xO = x -> ( ( ( xO x.s B ) x.s C ) = ( xO x.s ( B x.s C ) ) <-> ( ( x x.s B ) x.s C ) = ( x x.s ( B x.s C ) ) ) ) with typecode |-
18	11	adantr	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( ( xO x.s B ) x.s C ) = ( xO x.s ( B x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( ( xO x.s B ) x.s C ) = ( xO x.s ( B x.s C ) ) ) with typecode |-
19		simprll	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to x\in P$$
20	4 19	sselid	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to x\in \left(L\left(A\right)\cup R\left(A\right)\right)$$
21	17 18 20	rspcdva	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(x{\cdot }_{s}B\right){\cdot }_{s}C=x{\cdot }_s\left(B{\cdot }_{s}C\right)$$
22		oveq2	Could not format ( yO = y -> ( A x.s yO ) = ( A x.s y ) ) : No typesetting found for |- ( yO = y -> ( A x.s yO ) = ( A x.s y ) ) with typecode |-
23	22	oveq1d	Could not format ( yO = y -> ( ( A x.s yO ) x.s C ) = ( ( A x.s y ) x.s C ) ) : No typesetting found for |- ( yO = y -> ( ( A x.s yO ) x.s C ) = ( ( A x.s y ) x.s C ) ) with typecode |-
24		oveq1	Could not format ( yO = y -> ( yO x.s C ) = ( y x.s C ) ) : No typesetting found for |- ( yO = y -> ( yO x.s C ) = ( y x.s C ) ) with typecode |-
25	24	oveq2d	Could not format ( yO = y -> ( A x.s ( yO x.s C ) ) = ( A x.s ( y x.s C ) ) ) : No typesetting found for |- ( yO = y -> ( A x.s ( yO x.s C ) ) = ( A x.s ( y x.s C ) ) ) with typecode |-
26	23 25	eqeq12d	Could not format ( yO = y -> ( ( ( A x.s yO ) x.s C ) = ( A x.s ( yO x.s C ) ) <-> ( ( A x.s y ) x.s C ) = ( A x.s ( y x.s C ) ) ) ) : No typesetting found for |- ( yO = y -> ( ( ( A x.s yO ) x.s C ) = ( A x.s ( yO x.s C ) ) <-> ( ( A x.s y ) x.s C ) = ( A x.s ( y x.s C ) ) ) ) with typecode |-
27	12	adantr	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( ( A x.s yO ) x.s C ) = ( A x.s ( yO x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( ( A x.s yO ) x.s C ) = ( A x.s ( yO x.s C ) ) ) with typecode |-
28		simprlr	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to y\in Q$$
29	5 28	sselid	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to y\in \left(L\left(B\right)\cup R\left(B\right)\right)$$
30	26 27 29	rspcdva	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(A{\cdot }_{s}y\right){\cdot }_{s}C=A{\cdot }_s\left(y{\cdot }_{s}C\right)$$
31		oveq2	Could not format ( zO = z -> ( ( A x.s B ) x.s zO ) = ( ( A x.s B ) x.s z ) ) : No typesetting found for |- ( zO = z -> ( ( A x.s B ) x.s zO ) = ( ( A x.s B ) x.s z ) ) with typecode |-
32		oveq2	Could not format ( zO = z -> ( B x.s zO ) = ( B x.s z ) ) : No typesetting found for |- ( zO = z -> ( B x.s zO ) = ( B x.s z ) ) with typecode |-
33	32	oveq2d	Could not format ( zO = z -> ( A x.s ( B x.s zO ) ) = ( A x.s ( B x.s z ) ) ) : No typesetting found for |- ( zO = z -> ( A x.s ( B x.s zO ) ) = ( A x.s ( B x.s z ) ) ) with typecode |-
34	31 33	eqeq12d	Could not format ( zO = z -> ( ( ( A x.s B ) x.s zO ) = ( A x.s ( B x.s zO ) ) <-> ( ( A x.s B ) x.s z ) = ( A x.s ( B x.s z ) ) ) ) : No typesetting found for |- ( zO = z -> ( ( ( A x.s B ) x.s zO ) = ( A x.s ( B x.s zO ) ) <-> ( ( A x.s B ) x.s z ) = ( A x.s ( B x.s z ) ) ) ) with typecode |-
35	13	adantr	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( A x.s B ) x.s zO ) = ( A x.s ( B x.s zO ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( A x.s B ) x.s zO ) = ( A x.s ( B x.s zO ) ) ) with typecode |-
36		simprr	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to z\in R$$
37	6 36	sselid	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to z\in \left(L\left(C\right)\cup R\left(C\right)\right)$$
38	34 35 37	rspcdva	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(A{\cdot }_{s}B\right){\cdot }_{s}z=A{\cdot }_s\left(B{\cdot }_{s}z\right)$$
39		leftssno	$$⊢L\left(A\right)\subseteq \mathrm{No}$$
40		rightssno	$$⊢R\left(A\right)\subseteq \mathrm{No}$$
41	39 40	unssi	$$⊢L\left(A\right)\cup R\left(A\right)\subseteq \mathrm{No}$$
42	4 41	sstri	$$⊢P\subseteq \mathrm{No}$$
43	42 19	sselid	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to x\in \mathrm{No}$$
44	2	adantr	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to B\in \mathrm{No}$$
45	43 44	mulscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to x{\cdot }_{s}B\in \mathrm{No}$$
46		leftssno	$$⊢L\left(C\right)\subseteq \mathrm{No}$$
47		rightssno	$$⊢R\left(C\right)\subseteq \mathrm{No}$$
48	46 47	unssi	$$⊢L\left(C\right)\cup R\left(C\right)\subseteq \mathrm{No}$$
49	6 48	sstri	$$⊢R\subseteq \mathrm{No}$$
50	49 36	sselid	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to z\in \mathrm{No}$$
51	45 50	mulscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(x{\cdot }_{s}B\right){\cdot }_{s}z\in \mathrm{No}$$
52	1	adantr	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to A\in \mathrm{No}$$
53		leftssno	$$⊢L\left(B\right)\subseteq \mathrm{No}$$
54		rightssno	$$⊢R\left(B\right)\subseteq \mathrm{No}$$
55	53 54	unssi	$$⊢L\left(B\right)\cup R\left(B\right)\subseteq \mathrm{No}$$
56	5 55	sstri	$$⊢Q\subseteq \mathrm{No}$$
57	56 28	sselid	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to y\in \mathrm{No}$$
58	52 57	mulscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to A{\cdot }_{s}y\in \mathrm{No}$$
59	58 50	mulscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(A{\cdot }_{s}y\right){\cdot }_{s}z\in \mathrm{No}$$
60	51 59	addscomd	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)=\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right){+}_s\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right)$$
61	60	oveq1d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)=\left(\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right){+}_s\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)$$
62	43 57	mulscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to x{\cdot }_{s}y\in \mathrm{No}$$
63	62 50	mulscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(x{\cdot }_{s}y\right){\cdot }_{s}z\in \mathrm{No}$$
64	59 51 63	addsubsassd	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right){+}_s\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)=\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right){+}_s\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)$$
65	61 64	eqtrd	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)=\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right){+}_s\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)$$
66	65	oveq1d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){+}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)=\left(\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right){+}_s\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)\right){+}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)$$
67	51 63	subscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\in \mathrm{No}$$
68	3	adantr	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to C\in \mathrm{No}$$
69	62 68	mulscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(x{\cdot }_{s}y\right){\cdot }_{s}C\in \mathrm{No}$$
70	59 67 69	addsassd	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right){+}_s\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)\right){+}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)=\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right){+}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){+}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right)$$
71	22	oveq1d	Could not format ( yO = y -> ( ( A x.s yO ) x.s zO ) = ( ( A x.s y ) x.s zO ) ) : No typesetting found for |- ( yO = y -> ( ( A x.s yO ) x.s zO ) = ( ( A x.s y ) x.s zO ) ) with typecode |-
72		oveq1	Could not format ( yO = y -> ( yO x.s zO ) = ( y x.s zO ) ) : No typesetting found for |- ( yO = y -> ( yO x.s zO ) = ( y x.s zO ) ) with typecode |-
73	72	oveq2d	Could not format ( yO = y -> ( A x.s ( yO x.s zO ) ) = ( A x.s ( y x.s zO ) ) ) : No typesetting found for |- ( yO = y -> ( A x.s ( yO x.s zO ) ) = ( A x.s ( y x.s zO ) ) ) with typecode |-
74	71 73	eqeq12d	Could not format ( yO = y -> ( ( ( A x.s yO ) x.s zO ) = ( A x.s ( yO x.s zO ) ) <-> ( ( A x.s y ) x.s zO ) = ( A x.s ( y x.s zO ) ) ) ) : No typesetting found for |- ( yO = y -> ( ( ( A x.s yO ) x.s zO ) = ( A x.s ( yO x.s zO ) ) <-> ( ( A x.s y ) x.s zO ) = ( A x.s ( y x.s zO ) ) ) ) with typecode |-
75		oveq2	Could not format ( zO = z -> ( ( A x.s y ) x.s zO ) = ( ( A x.s y ) x.s z ) ) : No typesetting found for |- ( zO = z -> ( ( A x.s y ) x.s zO ) = ( ( A x.s y ) x.s z ) ) with typecode |-
76		oveq2	Could not format ( zO = z -> ( y x.s zO ) = ( y x.s z ) ) : No typesetting found for |- ( zO = z -> ( y x.s zO ) = ( y x.s z ) ) with typecode |-
77	76	oveq2d	Could not format ( zO = z -> ( A x.s ( y x.s zO ) ) = ( A x.s ( y x.s z ) ) ) : No typesetting found for |- ( zO = z -> ( A x.s ( y x.s zO ) ) = ( A x.s ( y x.s z ) ) ) with typecode |-
78	75 77	eqeq12d	Could not format ( zO = z -> ( ( ( A x.s y ) x.s zO ) = ( A x.s ( y x.s zO ) ) <-> ( ( A x.s y ) x.s z ) = ( A x.s ( y x.s z ) ) ) ) : No typesetting found for |- ( zO = z -> ( ( ( A x.s y ) x.s zO ) = ( A x.s ( y x.s zO ) ) <-> ( ( A x.s y ) x.s z ) = ( A x.s ( y x.s z ) ) ) ) with typecode |-
79	10	adantr	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( A x.s yO ) x.s zO ) = ( A x.s ( yO x.s zO ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( A x.s yO ) x.s zO ) = ( A x.s ( yO x.s zO ) ) ) with typecode |-
80	74 78 79 29 37	rspc2dv	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(A{\cdot }_{s}y\right){\cdot }_{s}z=A{\cdot }_s\left(y{\cdot }_{s}z\right)$$
81	51 69 63	addsubsd	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)=\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){+}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)$$
82	14	oveq1d	Could not format ( xO = x -> ( ( xO x.s B ) x.s zO ) = ( ( x x.s B ) x.s zO ) ) : No typesetting found for |- ( xO = x -> ( ( xO x.s B ) x.s zO ) = ( ( x x.s B ) x.s zO ) ) with typecode |-
83		oveq1	Could not format ( xO = x -> ( xO x.s ( B x.s zO ) ) = ( x x.s ( B x.s zO ) ) ) : No typesetting found for |- ( xO = x -> ( xO x.s ( B x.s zO ) ) = ( x x.s ( B x.s zO ) ) ) with typecode |-
84	82 83	eqeq12d	Could not format ( xO = x -> ( ( ( xO x.s B ) x.s zO ) = ( xO x.s ( B x.s zO ) ) <-> ( ( x x.s B ) x.s zO ) = ( x x.s ( B x.s zO ) ) ) ) : No typesetting found for |- ( xO = x -> ( ( ( xO x.s B ) x.s zO ) = ( xO x.s ( B x.s zO ) ) <-> ( ( x x.s B ) x.s zO ) = ( x x.s ( B x.s zO ) ) ) ) with typecode |-
85		oveq2	Could not format ( zO = z -> ( ( x x.s B ) x.s zO ) = ( ( x x.s B ) x.s z ) ) : No typesetting found for |- ( zO = z -> ( ( x x.s B ) x.s zO ) = ( ( x x.s B ) x.s z ) ) with typecode |-
86	32	oveq2d	Could not format ( zO = z -> ( x x.s ( B x.s zO ) ) = ( x x.s ( B x.s z ) ) ) : No typesetting found for |- ( zO = z -> ( x x.s ( B x.s zO ) ) = ( x x.s ( B x.s z ) ) ) with typecode |-
87	85 86	eqeq12d	Could not format ( zO = z -> ( ( ( x x.s B ) x.s zO ) = ( x x.s ( B x.s zO ) ) <-> ( ( x x.s B ) x.s z ) = ( x x.s ( B x.s z ) ) ) ) : No typesetting found for |- ( zO = z -> ( ( ( x x.s B ) x.s zO ) = ( x x.s ( B x.s zO ) ) <-> ( ( x x.s B ) x.s z ) = ( x x.s ( B x.s z ) ) ) ) with typecode |-
88	9	adantr	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( xO x.s B ) x.s zO ) = ( xO x.s ( B x.s zO ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( xO x.s B ) x.s zO ) = ( xO x.s ( B x.s zO ) ) ) with typecode |-
89	84 87 88 20 37	rspc2dv	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(x{\cdot }_{s}B\right){\cdot }_{s}z=x{\cdot }_s\left(B{\cdot }_{s}z\right)$$
90		oveq1	Could not format ( xO = x -> ( xO x.s yO ) = ( x x.s yO ) ) : No typesetting found for |- ( xO = x -> ( xO x.s yO ) = ( x x.s yO ) ) with typecode |-
91	90	oveq1d	Could not format ( xO = x -> ( ( xO x.s yO ) x.s C ) = ( ( x x.s yO ) x.s C ) ) : No typesetting found for |- ( xO = x -> ( ( xO x.s yO ) x.s C ) = ( ( x x.s yO ) x.s C ) ) with typecode |-
92		oveq1	Could not format ( xO = x -> ( xO x.s ( yO x.s C ) ) = ( x x.s ( yO x.s C ) ) ) : No typesetting found for |- ( xO = x -> ( xO x.s ( yO x.s C ) ) = ( x x.s ( yO x.s C ) ) ) with typecode |-
93	91 92	eqeq12d	Could not format ( xO = x -> ( ( ( xO x.s yO ) x.s C ) = ( xO x.s ( yO x.s C ) ) <-> ( ( x x.s yO ) x.s C ) = ( x x.s ( yO x.s C ) ) ) ) : No typesetting found for |- ( xO = x -> ( ( ( xO x.s yO ) x.s C ) = ( xO x.s ( yO x.s C ) ) <-> ( ( x x.s yO ) x.s C ) = ( x x.s ( yO x.s C ) ) ) ) with typecode |-
94		oveq2	Could not format ( yO = y -> ( x x.s yO ) = ( x x.s y ) ) : No typesetting found for |- ( yO = y -> ( x x.s yO ) = ( x x.s y ) ) with typecode |-
95	94	oveq1d	Could not format ( yO = y -> ( ( x x.s yO ) x.s C ) = ( ( x x.s y ) x.s C ) ) : No typesetting found for |- ( yO = y -> ( ( x x.s yO ) x.s C ) = ( ( x x.s y ) x.s C ) ) with typecode |-
96	24	oveq2d	Could not format ( yO = y -> ( x x.s ( yO x.s C ) ) = ( x x.s ( y x.s C ) ) ) : No typesetting found for |- ( yO = y -> ( x x.s ( yO x.s C ) ) = ( x x.s ( y x.s C ) ) ) with typecode |-
97	95 96	eqeq12d	Could not format ( yO = y -> ( ( ( x x.s yO ) x.s C ) = ( x x.s ( yO x.s C ) ) <-> ( ( x x.s y ) x.s C ) = ( x x.s ( y x.s C ) ) ) ) : No typesetting found for |- ( yO = y -> ( ( ( x x.s yO ) x.s C ) = ( x x.s ( yO x.s C ) ) <-> ( ( x x.s y ) x.s C ) = ( x x.s ( y x.s C ) ) ) ) with typecode |-
98	8	adantr	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( ( xO x.s yO ) x.s C ) = ( xO x.s ( yO x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( ( xO x.s yO ) x.s C ) = ( xO x.s ( yO x.s C ) ) ) with typecode |-
99	93 97 98 20 29	rspc2dv	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(x{\cdot }_{s}y\right){\cdot }_{s}C=x{\cdot }_s\left(y{\cdot }_{s}C\right)$$
100	89 99	oveq12d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)=\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right){+}_s\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right)$$
101	44 50	mulscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to B{\cdot }_{s}z\in \mathrm{No}$$
102	43 101	mulscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to x{\cdot }_s\left(B{\cdot }_{s}z\right)\in \mathrm{No}$$
103	57 68	mulscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to y{\cdot }_{s}C\in \mathrm{No}$$
104	43 103	mulscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to x{\cdot }_s\left(y{\cdot }_{s}C\right)\in \mathrm{No}$$
105	102 104	addscomd	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right){+}_s\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right)=\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)$$
106	100 105	eqtrd	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)=\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)$$
107	90	oveq1d	Could not format ( xO = x -> ( ( xO x.s yO ) x.s zO ) = ( ( x x.s yO ) x.s zO ) ) : No typesetting found for |- ( xO = x -> ( ( xO x.s yO ) x.s zO ) = ( ( x x.s yO ) x.s zO ) ) with typecode |-
108		oveq1	Could not format ( xO = x -> ( xO x.s ( yO x.s zO ) ) = ( x x.s ( yO x.s zO ) ) ) : No typesetting found for |- ( xO = x -> ( xO x.s ( yO x.s zO ) ) = ( x x.s ( yO x.s zO ) ) ) with typecode |-
109	107 108	eqeq12d	Could not format ( xO = x -> ( ( ( xO x.s yO ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) <-> ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) ) ) : No typesetting found for |- ( xO = x -> ( ( ( xO x.s yO ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) <-> ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) ) ) with typecode |-
110	94	oveq1d	Could not format ( yO = y -> ( ( x x.s yO ) x.s zO ) = ( ( x x.s y ) x.s zO ) ) : No typesetting found for |- ( yO = y -> ( ( x x.s yO ) x.s zO ) = ( ( x x.s y ) x.s zO ) ) with typecode |-
111	72	oveq2d	Could not format ( yO = y -> ( x x.s ( yO x.s zO ) ) = ( x x.s ( y x.s zO ) ) ) : No typesetting found for |- ( yO = y -> ( x x.s ( yO x.s zO ) ) = ( x x.s ( y x.s zO ) ) ) with typecode |-
112	110 111	eqeq12d	Could not format ( yO = y -> ( ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) <-> ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) : No typesetting found for |- ( yO = y -> ( ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) <-> ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) with typecode |-
113		oveq2	Could not format ( zO = z -> ( ( x x.s y ) x.s zO ) = ( ( x x.s y ) x.s z ) ) : No typesetting found for |- ( zO = z -> ( ( x x.s y ) x.s zO ) = ( ( x x.s y ) x.s z ) ) with typecode |-
114	76	oveq2d	Could not format ( zO = z -> ( x x.s ( y x.s zO ) ) = ( x x.s ( y x.s z ) ) ) : No typesetting found for |- ( zO = z -> ( x x.s ( y x.s zO ) ) = ( x x.s ( y x.s z ) ) ) with typecode |-
115	113 114	eqeq12d	Could not format ( zO = z -> ( ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) <-> ( ( x x.s y ) x.s z ) = ( x x.s ( y x.s z ) ) ) ) : No typesetting found for |- ( zO = z -> ( ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) <-> ( ( x x.s y ) x.s z ) = ( x x.s ( y x.s z ) ) ) ) with typecode |-
116	7	adantr	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( xO x.s yO ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( ( xO x.s yO ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) ) with typecode |-
117	109 112 115 116 20 29 37	rspc3dv	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(x{\cdot }_{s}y\right){\cdot }_{s}z=x{\cdot }_s\left(y{\cdot }_{s}z\right)$$
118	106 117	oveq12d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)=\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)$$
119	81 118	eqtr3d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){+}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)=\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)$$
120	80 119	oveq12d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right){+}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){+}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right)=\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right){+}_s\left(\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)$$
121	66 70 120	3eqtrd	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){+}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)=\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right){+}_s\left(\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)$$
122	38 121	oveq12d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){+}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right)=\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right){+}_s\left(\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)\right)$$
123	52 44	mulscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to A{\cdot }_{s}B\in \mathrm{No}$$
124	123 50	mulscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(A{\cdot }_{s}B\right){\cdot }_{s}z\in \mathrm{No}$$
125	51 59	addscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\in \mathrm{No}$$
126	125 63	subscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\in \mathrm{No}$$
127	124 126 69	subsubs4d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)=\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){+}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right)$$
128	52 101	mulscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to A{\cdot }_s\left(B{\cdot }_{s}z\right)\in \mathrm{No}$$
129	57 50	mulscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to y{\cdot }_{s}z\in \mathrm{No}$$
130	52 129	mulscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to A{\cdot }_s\left(y{\cdot }_{s}z\right)\in \mathrm{No}$$
131	104 102	addscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\in \mathrm{No}$$
132	43 129	mulscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to x{\cdot }_s\left(y{\cdot }_{s}z\right)\in \mathrm{No}$$
133	131 132	subscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\in \mathrm{No}$$
134	128 130 133	subsubs4d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right){-}_s\left(\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)=\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right){+}_s\left(\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)\right)$$
135	122 127 134	3eqtr4d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)=\left(\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right){-}_s\left(\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)$$
136	30 135	oveq12d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right){+}_s\left(\left(\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right)=\left(A{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(\left(\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right){-}_s\left(\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)\right)$$
137	58 68	mulscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(A{\cdot }_{s}y\right){\cdot }_{s}C\in \mathrm{No}$$
138	124 126	subscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)\in \mathrm{No}$$
139	137 138 69	addsubsd	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right){+}_s\left(\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)=\left(\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){+}_s\left(\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)\right)$$
140	137 138 69	addsubsassd	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right){+}_s\left(\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)=\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right){+}_s\left(\left(\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right)$$
141	139 140	eqtr3d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){+}_s\left(\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)\right)=\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right){+}_s\left(\left(\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right)$$
142	52 103	mulscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to A{\cdot }_s\left(y{\cdot }_{s}C\right)\in \mathrm{No}$$
143	142 128 130	addsubsassd	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(A{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)=\left(A{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)$$
144	143	oveq1d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(A{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right){-}_s\left(\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)=\left(\left(A{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)\right){-}_s\left(\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)$$
145	128 130	subscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\in \mathrm{No}$$
146	142 145 133	addsubsassd	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(A{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)\right){-}_s\left(\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)=\left(A{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(\left(\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right){-}_s\left(\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)\right)$$
147	144 146	eqtrd	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(A{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right){-}_s\left(\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)=\left(A{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(\left(\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right){-}_s\left(\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)\right)$$
148	136 141 147	3eqtr4d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){+}_s\left(\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)\right)=\left(\left(\left(A{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right){-}_s\left(\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)$$
149	21 148	oveq12d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(x{\cdot }_{s}B\right){\cdot }_{s}C\right){+}_s\left(\left(\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){+}_s\left(\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)\right)\right)=\left(x{\cdot }_s\left(B{\cdot }_{s}C\right)\right){+}_s\left(\left(\left(\left(A{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right){-}_s\left(\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)\right)$$
150	45 68	mulscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(x{\cdot }_{s}B\right){\cdot }_{s}C\in \mathrm{No}$$
151	150 137	addscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(x{\cdot }_{s}B\right){\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right)\in \mathrm{No}$$
152	151 69	subscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\in \mathrm{No}$$
153	152 124 126	addsubsassd	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){+}_s\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right)\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)=\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){+}_s\left(\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)\right)$$
154	150 137 69	addsubsassd	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)=\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}C\right){+}_s\left(\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right)$$
155	154	oveq1d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){+}_s\left(\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)\right)=\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}C\right){+}_s\left(\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right)\right){+}_s\left(\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)\right)$$
156	137 69	subscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\in \mathrm{No}$$
157	150 156 138	addsassd	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}C\right){+}_s\left(\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right)\right){+}_s\left(\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)\right)=\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}C\right){+}_s\left(\left(\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){+}_s\left(\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)\right)\right)$$
158	153 155 157	3eqtrd	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){+}_s\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right)\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)=\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}C\right){+}_s\left(\left(\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){+}_s\left(\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)\right)\right)$$
159	44 68	mulscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to B{\cdot }_{s}C\in \mathrm{No}$$
160	43 159	mulscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to x{\cdot }_s\left(B{\cdot }_{s}C\right)\in \mathrm{No}$$
161	142 128	addscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(A{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\in \mathrm{No}$$
162	161 130	subscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(A{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\in \mathrm{No}$$
163	160 162 133	addsubsassd	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(x{\cdot }_s\left(B{\cdot }_{s}C\right)\right){+}_s\left(\left(\left(A{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)\right){-}_s\left(\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)=\left(x{\cdot }_s\left(B{\cdot }_{s}C\right)\right){+}_s\left(\left(\left(\left(A{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right){-}_s\left(\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)\right)$$
164	149 158 163	3eqtr4d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){+}_s\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right)\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)=\left(\left(x{\cdot }_s\left(B{\cdot }_{s}C\right)\right){+}_s\left(\left(\left(A{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)\right){-}_s\left(\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)$$
165	45 58	addscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\in \mathrm{No}$$
166	165 62 68	subsdird	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){-}_s\left(x{\cdot }_{s}y\right)\right){\cdot }_{s}C=\left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){\cdot }_{s}C\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)$$
167	45 58 68	addsdird	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){\cdot }_{s}C=\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right)$$
168	167	oveq1d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){\cdot }_{s}C\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)=\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)$$
169	166 168	eqtrd	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){-}_s\left(x{\cdot }_{s}y\right)\right){\cdot }_{s}C=\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)$$
170	169	oveq1d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){-}_s\left(x{\cdot }_{s}y\right)\right){\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right)=\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){+}_s\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right)$$
171	165 62 50	subsdird	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){-}_s\left(x{\cdot }_{s}y\right)\right){\cdot }_{s}z=\left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){\cdot }_{s}z\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)$$
172	45 58 50	addsdird	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){\cdot }_{s}z=\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)$$
173	172	oveq1d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){\cdot }_{s}z\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)=\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)$$
174	171 173	eqtrd	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){-}_s\left(x{\cdot }_{s}y\right)\right){\cdot }_{s}z=\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)$$
175	170 174	oveq12d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){-}_s\left(x{\cdot }_{s}y\right)\right){\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right)\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){-}_s\left(x{\cdot }_{s}y\right)\right){\cdot }_{s}z\right)=\left(\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}C\right)\right){+}_s\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right)\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){\cdot }_{s}z\right){+}_s\left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z\right)\right)$$
176	103 101	addscld	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\in \mathrm{No}$$
177	52 176 129	subsdid	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to A{\cdot }_s\left(\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(y{\cdot }_{s}z\right)\right)=\left(A{\cdot }_s\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)$$
178	52 103 101	addsdid	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to A{\cdot }_s\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right)=\left(A{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right)$$
179	178	oveq1d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(A{\cdot }_s\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)=\left(\left(A{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)$$
180	177 179	eqtrd	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to A{\cdot }_s\left(\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(y{\cdot }_{s}z\right)\right)=\left(\left(A{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)$$
181	180	oveq2d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(x{\cdot }_s\left(B{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(y{\cdot }_{s}z\right)\right)\right)=\left(x{\cdot }_s\left(B{\cdot }_{s}C\right)\right){+}_s\left(\left(\left(A{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)$$
182	43 176 129	subsdid	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to x{\cdot }_s\left(\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(y{\cdot }_{s}z\right)\right)=\left(x{\cdot }_s\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)$$
183	43 103 101	addsdid	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to x{\cdot }_s\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right)=\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)$$
184	183	oveq1d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(x{\cdot }_s\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)=\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)$$
185	182 184	eqtrd	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to x{\cdot }_s\left(\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(y{\cdot }_{s}z\right)\right)=\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)$$
186	181 185	oveq12d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(x{\cdot }_s\left(B{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(y{\cdot }_{s}z\right)\right)\right)\right){-}_s\left(x{\cdot }_s\left(\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(y{\cdot }_{s}z\right)\right)\right)=\left(\left(x{\cdot }_s\left(B{\cdot }_{s}C\right)\right){+}_s\left(\left(\left(A{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)\right){-}_s\left(\left(\left(x{\cdot }_s\left(y{\cdot }_{s}C\right)\right){+}_s\left(x{\cdot }_s\left(B{\cdot }_{s}z\right)\right)\right){-}_s\left(x{\cdot }_s\left(y{\cdot }_{s}z\right)\right)\right)$$
187	164 175 186	3eqtr4d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(\left(\left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){-}_s\left(x{\cdot }_{s}y\right)\right){\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right)\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){-}_s\left(x{\cdot }_{s}y\right)\right){\cdot }_{s}z\right)=\left(\left(x{\cdot }_s\left(B{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(y{\cdot }_{s}z\right)\right)\right)\right){-}_s\left(x{\cdot }_s\left(\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(y{\cdot }_{s}z\right)\right)\right)$$
188	187	eqeq2d	$$⊢\left(\phi \wedge \left(\left(x\in P\wedge y\in Q\right)\wedge z\in R\right)\right)\to \left(a=\left(\left(\left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){-}_s\left(x{\cdot }_{s}y\right)\right){\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right)\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){-}_s\left(x{\cdot }_{s}y\right)\right){\cdot }_{s}z\right)\leftrightarrow a=\left(\left(x{\cdot }_s\left(B{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(y{\cdot }_{s}z\right)\right)\right)\right){-}_s\left(x{\cdot }_s\left(\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(y{\cdot }_{s}z\right)\right)\right)\right)$$
189	188	anassrs	$$⊢\left(\left(\phi \wedge \left(x\in P\wedge y\in Q\right)\right)\wedge z\in R\right)\to \left(a=\left(\left(\left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){-}_s\left(x{\cdot }_{s}y\right)\right){\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right)\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){-}_s\left(x{\cdot }_{s}y\right)\right){\cdot }_{s}z\right)\leftrightarrow a=\left(\left(x{\cdot }_s\left(B{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(y{\cdot }_{s}z\right)\right)\right)\right){-}_s\left(x{\cdot }_s\left(\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(y{\cdot }_{s}z\right)\right)\right)\right)$$
190	189	rexbidva	$$⊢\left(\phi \wedge \left(x\in P\wedge y\in Q\right)\right)\to \left(\exists z\in Ra=\left(\left(\left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){-}_s\left(x{\cdot }_{s}y\right)\right){\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right)\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){-}_s\left(x{\cdot }_{s}y\right)\right){\cdot }_{s}z\right)\leftrightarrow \exists z\in Ra=\left(\left(x{\cdot }_s\left(B{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(y{\cdot }_{s}z\right)\right)\right)\right){-}_s\left(x{\cdot }_s\left(\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(y{\cdot }_{s}z\right)\right)\right)\right)$$
191	190	2rexbidva	$$⊢\phi \to \left(\exists x\in P\exists y\in Q\exists z\in Ra=\left(\left(\left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){-}_s\left(x{\cdot }_{s}y\right)\right){\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z\right)\right){-}_s\left(\left(\left(\left(x{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}y\right)\right){-}_s\left(x{\cdot }_{s}y\right)\right){\cdot }_{s}z\right)\leftrightarrow \exists x\in P\exists y\in Q\exists z\in Ra=\left(\left(x{\cdot }_s\left(B{\cdot }_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(y{\cdot }_{s}z\right)\right)\right)\right){-}_s\left(x{\cdot }_s\left(\left(\left(y{\cdot }_{s}C\right){+}_s\left(B{\cdot }_{s}z\right)\right){-}_s\left(y{\cdot }_{s}z\right)\right)\right)\right)$$