Theorem addsdilem4

Description: Lemma for addsdi . Show one of the equalities involved in the final expression. (Contributed by Scott Fenton, 9-Mar-2025)

	Ref	Expression
Hypotheses	addsdilem4.1	$$⊢\phi \to A\in \mathrm{No}$$
	addsdilem4.2	$$⊢\phi \to B\in \mathrm{No}$$
	addsdilem4.3	$$⊢\phi \to C\in \mathrm{No}$$
	addsdilem4.4	No typesetting found for |- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( xO x.s ( B +s C ) ) = ( ( xO x.s B ) +s ( xO x.s C ) ) ) with typecode |-
	addsdilem4.5	No typesetting found for |- ( ph -> A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( A x.s ( B +s zO ) ) = ( ( A x.s B ) +s ( A x.s zO ) ) ) with typecode |-
	addsdilem4.6	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 +s zO ) ) = ( ( xO x.s B ) +s ( xO x.s zO ) ) ) with typecode |-
	addsdilem4.7	$$⊢\psi \to X\in \left(L\left(A\right)\cup R\left(A\right)\right)$$
	addsdilem4.8	$$⊢\psi \to Z\in \left(L\left(C\right)\cup R\left(C\right)\right)$$
Assertion	addsdilem4	$$⊢\left(\phi \wedge \psi \right)\to \left(\left(X{\cdot }_s\left(B{+}_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(B{+}_{s}Z\right)\right)\right){-}_s\left(X{\cdot }_s\left(B{+}_{s}Z\right)\right)=\left(A{\cdot }_{s}B\right){+}_s\left(\left(\left(X{\cdot }_{s}C\right){+}_s\left(A{\cdot }_{s}Z\right)\right){-}_s\left(X{\cdot }_{s}Z\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		addsdilem4.1	$$⊢\phi \to A\in \mathrm{No}$$
2		addsdilem4.2	$$⊢\phi \to B\in \mathrm{No}$$
3		addsdilem4.3	$$⊢\phi \to C\in \mathrm{No}$$
4		addsdilem4.4	Could not format ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( xO x.s ( B +s C ) ) = ( ( xO x.s B ) +s ( xO x.s C ) ) ) : No typesetting found for |- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( xO x.s ( B +s C ) ) = ( ( xO x.s B ) +s ( xO x.s C ) ) ) with typecode |-
5		addsdilem4.5	Could not format ( ph -> A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( A x.s ( B +s zO ) ) = ( ( A x.s B ) +s ( A x.s zO ) ) ) : No typesetting found for |- ( ph -> A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( A x.s ( B +s zO ) ) = ( ( A x.s B ) +s ( A x.s zO ) ) ) with typecode |-
6		addsdilem4.6	Could not format ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( xO x.s ( B +s zO ) ) = ( ( xO x.s B ) +s ( xO 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 +s zO ) ) = ( ( xO x.s B ) +s ( xO x.s zO ) ) ) with typecode |-
7		addsdilem4.7	$$⊢\psi \to X\in \left(L\left(A\right)\cup R\left(A\right)\right)$$
8		addsdilem4.8	$$⊢\psi \to Z\in \left(L\left(C\right)\cup R\left(C\right)\right)$$
9		oveq1	Could not format ( xO = X -> ( xO x.s ( B +s C ) ) = ( X x.s ( B +s C ) ) ) : No typesetting found for |- ( xO = X -> ( xO x.s ( B +s C ) ) = ( X x.s ( B +s C ) ) ) with typecode |-
10		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 |-
11		oveq1	Could not format ( xO = X -> ( xO x.s C ) = ( X x.s C ) ) : No typesetting found for |- ( xO = X -> ( xO x.s C ) = ( X x.s C ) ) with typecode |-
12	10 11	oveq12d	Could not format ( xO = X -> ( ( xO x.s B ) +s ( xO x.s C ) ) = ( ( X x.s B ) +s ( X x.s C ) ) ) : No typesetting found for |- ( xO = X -> ( ( xO x.s B ) +s ( xO x.s C ) ) = ( ( X x.s B ) +s ( X x.s C ) ) ) with typecode |-
13	9 12	eqeq12d	Could not format ( xO = X -> ( ( xO x.s ( B +s C ) ) = ( ( xO x.s B ) +s ( xO x.s C ) ) <-> ( X x.s ( B +s C ) ) = ( ( X x.s B ) +s ( X x.s C ) ) ) ) : No typesetting found for |- ( xO = X -> ( ( xO x.s ( B +s C ) ) = ( ( xO x.s B ) +s ( xO x.s C ) ) <-> ( X x.s ( B +s C ) ) = ( ( X x.s B ) +s ( X x.s C ) ) ) ) with typecode |-
14	4	adantr	Could not format ( ( ph /\ ps ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( xO x.s ( B +s C ) ) = ( ( xO x.s B ) +s ( xO x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( xO x.s ( B +s C ) ) = ( ( xO x.s B ) +s ( xO x.s C ) ) ) with typecode |-
15	7	adantl	$$⊢\left(\phi \wedge \psi \right)\to X\in \left(L\left(A\right)\cup R\left(A\right)\right)$$
16	13 14 15	rspcdva	$$⊢\left(\phi \wedge \psi \right)\to X{\cdot }_s\left(B{+}_{s}C\right)=\left(X{\cdot }_{s}B\right){+}_s\left(X{\cdot }_{s}C\right)$$
17		oveq2	Could not format ( zO = Z -> ( B +s zO ) = ( B +s Z ) ) : No typesetting found for |- ( zO = Z -> ( B +s zO ) = ( B +s Z ) ) with typecode |-
18	17	oveq2d	Could not format ( zO = Z -> ( A x.s ( B +s zO ) ) = ( A x.s ( B +s Z ) ) ) : No typesetting found for |- ( zO = Z -> ( A x.s ( B +s zO ) ) = ( A x.s ( B +s Z ) ) ) with typecode |-
19		oveq2	Could not format ( zO = Z -> ( A x.s zO ) = ( A x.s Z ) ) : No typesetting found for |- ( zO = Z -> ( A x.s zO ) = ( A x.s Z ) ) with typecode |-
20	19	oveq2d	Could not format ( zO = Z -> ( ( A x.s B ) +s ( A x.s zO ) ) = ( ( A x.s B ) +s ( A x.s Z ) ) ) : No typesetting found for |- ( zO = Z -> ( ( A x.s B ) +s ( A x.s zO ) ) = ( ( A x.s B ) +s ( A x.s Z ) ) ) with typecode |-
21	18 20	eqeq12d	Could not format ( zO = Z -> ( ( A x.s ( B +s zO ) ) = ( ( A x.s B ) +s ( A x.s zO ) ) <-> ( A x.s ( B +s Z ) ) = ( ( A x.s B ) +s ( A x.s Z ) ) ) ) : No typesetting found for |- ( zO = Z -> ( ( A x.s ( B +s zO ) ) = ( ( A x.s B ) +s ( A x.s zO ) ) <-> ( A x.s ( B +s Z ) ) = ( ( A x.s B ) +s ( A x.s Z ) ) ) ) with typecode |-
22	5	adantr	Could not format ( ( ph /\ ps ) -> A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( A x.s ( B +s zO ) ) = ( ( A x.s B ) +s ( A x.s zO ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( A x.s ( B +s zO ) ) = ( ( A x.s B ) +s ( A x.s zO ) ) ) with typecode |-
23	8	adantl	$$⊢\left(\phi \wedge \psi \right)\to Z\in \left(L\left(C\right)\cup R\left(C\right)\right)$$
24	21 22 23	rspcdva	$$⊢\left(\phi \wedge \psi \right)\to A{\cdot }_s\left(B{+}_{s}Z\right)=\left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}Z\right)$$
25	16 24	oveq12d	$$⊢\left(\phi \wedge \psi \right)\to \left(X{\cdot }_s\left(B{+}_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(B{+}_{s}Z\right)\right)=\left(\left(X{\cdot }_{s}B\right){+}_s\left(X{\cdot }_{s}C\right)\right){+}_s\left(\left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}Z\right)\right)$$
26		oveq1	Could not format ( xO = X -> ( xO x.s ( B +s zO ) ) = ( X x.s ( B +s zO ) ) ) : No typesetting found for |- ( xO = X -> ( xO x.s ( B +s zO ) ) = ( X x.s ( B +s zO ) ) ) with typecode |-
27		oveq1	Could not format ( xO = X -> ( xO x.s zO ) = ( X x.s zO ) ) : No typesetting found for |- ( xO = X -> ( xO x.s zO ) = ( X x.s zO ) ) with typecode |-
28	10 27	oveq12d	Could not format ( xO = X -> ( ( xO x.s B ) +s ( xO x.s zO ) ) = ( ( X x.s B ) +s ( X x.s zO ) ) ) : No typesetting found for |- ( xO = X -> ( ( xO x.s B ) +s ( xO x.s zO ) ) = ( ( X x.s B ) +s ( X x.s zO ) ) ) with typecode |-
29	26 28	eqeq12d	Could not format ( xO = X -> ( ( xO x.s ( B +s zO ) ) = ( ( xO x.s B ) +s ( xO x.s zO ) ) <-> ( X x.s ( B +s zO ) ) = ( ( X x.s B ) +s ( X x.s zO ) ) ) ) : No typesetting found for |- ( xO = X -> ( ( xO x.s ( B +s zO ) ) = ( ( xO x.s B ) +s ( xO x.s zO ) ) <-> ( X x.s ( B +s zO ) ) = ( ( X x.s B ) +s ( X x.s zO ) ) ) ) with typecode |-
30	17	oveq2d	Could not format ( zO = Z -> ( X x.s ( B +s zO ) ) = ( X x.s ( B +s Z ) ) ) : No typesetting found for |- ( zO = Z -> ( X x.s ( B +s zO ) ) = ( X x.s ( B +s Z ) ) ) with typecode |-
31		oveq2	Could not format ( zO = Z -> ( X x.s zO ) = ( X x.s Z ) ) : No typesetting found for |- ( zO = Z -> ( X x.s zO ) = ( X x.s Z ) ) with typecode |-
32	31	oveq2d	Could not format ( zO = Z -> ( ( X x.s B ) +s ( X x.s zO ) ) = ( ( X x.s B ) +s ( X x.s Z ) ) ) : No typesetting found for |- ( zO = Z -> ( ( X x.s B ) +s ( X x.s zO ) ) = ( ( X x.s B ) +s ( X x.s Z ) ) ) with typecode |-
33	30 32	eqeq12d	Could not format ( zO = Z -> ( ( X x.s ( B +s zO ) ) = ( ( X x.s B ) +s ( X x.s zO ) ) <-> ( X x.s ( B +s Z ) ) = ( ( X x.s B ) +s ( X x.s Z ) ) ) ) : No typesetting found for |- ( zO = Z -> ( ( X x.s ( B +s zO ) ) = ( ( X x.s B ) +s ( X x.s zO ) ) <-> ( X x.s ( B +s Z ) ) = ( ( X x.s B ) +s ( X x.s Z ) ) ) ) with typecode |-
34	6	adantr	Could not format ( ( ph /\ ps ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( xO x.s ( B +s zO ) ) = ( ( xO x.s B ) +s ( xO x.s zO ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( xO x.s ( B +s zO ) ) = ( ( xO x.s B ) +s ( xO x.s zO ) ) ) with typecode |-
35	29 33 34 15 23	rspc2dv	$$⊢\left(\phi \wedge \psi \right)\to X{\cdot }_s\left(B{+}_{s}Z\right)=\left(X{\cdot }_{s}B\right){+}_s\left(X{\cdot }_{s}Z\right)$$
36	25 35	oveq12d	$$⊢\left(\phi \wedge \psi \right)\to \left(\left(X{\cdot }_s\left(B{+}_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(B{+}_{s}Z\right)\right)\right){-}_s\left(X{\cdot }_s\left(B{+}_{s}Z\right)\right)=\left(\left(\left(X{\cdot }_{s}B\right){+}_s\left(X{\cdot }_{s}C\right)\right){+}_s\left(\left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}Z\right)\right)\right){-}_s\left(\left(X{\cdot }_{s}B\right){+}_s\left(X{\cdot }_{s}Z\right)\right)$$
37		leftssno	$$⊢L\left(A\right)\subseteq \mathrm{No}$$
38		rightssno	$$⊢R\left(A\right)\subseteq \mathrm{No}$$
39	37 38	unssi	$$⊢L\left(A\right)\cup R\left(A\right)\subseteq \mathrm{No}$$
40	39 7	sselid	$$⊢\psi \to X\in \mathrm{No}$$
41	40	adantl	$$⊢\left(\phi \wedge \psi \right)\to X\in \mathrm{No}$$
42	2	adantr	$$⊢\left(\phi \wedge \psi \right)\to B\in \mathrm{No}$$
43	41 42	mulscld	$$⊢\left(\phi \wedge \psi \right)\to X{\cdot }_{s}B\in \mathrm{No}$$
44	3	adantr	$$⊢\left(\phi \wedge \psi \right)\to C\in \mathrm{No}$$
45	41 44	mulscld	$$⊢\left(\phi \wedge \psi \right)\to X{\cdot }_{s}C\in \mathrm{No}$$
46	43 45	addscld	$$⊢\left(\phi \wedge \psi \right)\to \left(X{\cdot }_{s}B\right){+}_s\left(X{\cdot }_{s}C\right)\in \mathrm{No}$$
47	1 2	mulscld	$$⊢\phi \to A{\cdot }_{s}B\in \mathrm{No}$$
48	47	adantr	$$⊢\left(\phi \wedge \psi \right)\to A{\cdot }_{s}B\in \mathrm{No}$$
49	1	adantr	$$⊢\left(\phi \wedge \psi \right)\to A\in \mathrm{No}$$
50		leftssno	$$⊢L\left(C\right)\subseteq \mathrm{No}$$
51		rightssno	$$⊢R\left(C\right)\subseteq \mathrm{No}$$
52	50 51	unssi	$$⊢L\left(C\right)\cup R\left(C\right)\subseteq \mathrm{No}$$
53	52 8	sselid	$$⊢\psi \to Z\in \mathrm{No}$$
54	53	adantl	$$⊢\left(\phi \wedge \psi \right)\to Z\in \mathrm{No}$$
55	49 54	mulscld	$$⊢\left(\phi \wedge \psi \right)\to A{\cdot }_{s}Z\in \mathrm{No}$$
56	48 55	addscld	$$⊢\left(\phi \wedge \psi \right)\to \left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}Z\right)\in \mathrm{No}$$
57	46 56	addscld	$$⊢\left(\phi \wedge \psi \right)\to \left(\left(X{\cdot }_{s}B\right){+}_s\left(X{\cdot }_{s}C\right)\right){+}_s\left(\left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}Z\right)\right)\in \mathrm{No}$$
58	41 54	mulscld	$$⊢\left(\phi \wedge \psi \right)\to X{\cdot }_{s}Z\in \mathrm{No}$$
59	57 43 58	subsubs4d	$$⊢\left(\phi \wedge \psi \right)\to \left(\left(\left(\left(X{\cdot }_{s}B\right){+}_s\left(X{\cdot }_{s}C\right)\right){+}_s\left(\left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}Z\right)\right)\right){-}_s\left(X{\cdot }_{s}B\right)\right){-}_s\left(X{\cdot }_{s}Z\right)=\left(\left(\left(X{\cdot }_{s}B\right){+}_s\left(X{\cdot }_{s}C\right)\right){+}_s\left(\left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}Z\right)\right)\right){-}_s\left(\left(X{\cdot }_{s}B\right){+}_s\left(X{\cdot }_{s}Z\right)\right)$$
60	46 56 43	addsubsd	$$⊢\left(\phi \wedge \psi \right)\to \left(\left(\left(X{\cdot }_{s}B\right){+}_s\left(X{\cdot }_{s}C\right)\right){+}_s\left(\left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}Z\right)\right)\right){-}_s\left(X{\cdot }_{s}B\right)=\left(\left(\left(X{\cdot }_{s}B\right){+}_s\left(X{\cdot }_{s}C\right)\right){-}_s\left(X{\cdot }_{s}B\right)\right){+}_s\left(\left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}Z\right)\right)$$
61	43 45	addscomd	$$⊢\left(\phi \wedge \psi \right)\to \left(X{\cdot }_{s}B\right){+}_s\left(X{\cdot }_{s}C\right)=\left(X{\cdot }_{s}C\right){+}_s\left(X{\cdot }_{s}B\right)$$
62	61	oveq1d	$$⊢\left(\phi \wedge \psi \right)\to \left(\left(X{\cdot }_{s}B\right){+}_s\left(X{\cdot }_{s}C\right)\right){-}_s\left(X{\cdot }_{s}B\right)=\left(\left(X{\cdot }_{s}C\right){+}_s\left(X{\cdot }_{s}B\right)\right){-}_s\left(X{\cdot }_{s}B\right)$$
63		pncans	$$⊢\left(X{\cdot }_{s}C\in \mathrm{No}\wedge X{\cdot }_{s}B\in \mathrm{No}\right)\to \left(\left(X{\cdot }_{s}C\right){+}_s\left(X{\cdot }_{s}B\right)\right){-}_s\left(X{\cdot }_{s}B\right)=X{\cdot }_{s}C$$
64	45 43 63	syl2anc	$$⊢\left(\phi \wedge \psi \right)\to \left(\left(X{\cdot }_{s}C\right){+}_s\left(X{\cdot }_{s}B\right)\right){-}_s\left(X{\cdot }_{s}B\right)=X{\cdot }_{s}C$$
65	62 64	eqtrd	$$⊢\left(\phi \wedge \psi \right)\to \left(\left(X{\cdot }_{s}B\right){+}_s\left(X{\cdot }_{s}C\right)\right){-}_s\left(X{\cdot }_{s}B\right)=X{\cdot }_{s}C$$
66	65	oveq1d	$$⊢\left(\phi \wedge \psi \right)\to \left(\left(\left(X{\cdot }_{s}B\right){+}_s\left(X{\cdot }_{s}C\right)\right){-}_s\left(X{\cdot }_{s}B\right)\right){+}_s\left(\left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}Z\right)\right)=\left(X{\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}Z\right)\right)$$
67	45 48 55	adds12d	$$⊢\left(\phi \wedge \psi \right)\to \left(X{\cdot }_{s}C\right){+}_s\left(\left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}Z\right)\right)=\left(A{\cdot }_{s}B\right){+}_s\left(\left(X{\cdot }_{s}C\right){+}_s\left(A{\cdot }_{s}Z\right)\right)$$
68	60 66 67	3eqtrd	$$⊢\left(\phi \wedge \psi \right)\to \left(\left(\left(X{\cdot }_{s}B\right){+}_s\left(X{\cdot }_{s}C\right)\right){+}_s\left(\left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}Z\right)\right)\right){-}_s\left(X{\cdot }_{s}B\right)=\left(A{\cdot }_{s}B\right){+}_s\left(\left(X{\cdot }_{s}C\right){+}_s\left(A{\cdot }_{s}Z\right)\right)$$
69	68	oveq1d	$$⊢\left(\phi \wedge \psi \right)\to \left(\left(\left(\left(X{\cdot }_{s}B\right){+}_s\left(X{\cdot }_{s}C\right)\right){+}_s\left(\left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}Z\right)\right)\right){-}_s\left(X{\cdot }_{s}B\right)\right){-}_s\left(X{\cdot }_{s}Z\right)=\left(\left(A{\cdot }_{s}B\right){+}_s\left(\left(X{\cdot }_{s}C\right){+}_s\left(A{\cdot }_{s}Z\right)\right)\right){-}_s\left(X{\cdot }_{s}Z\right)$$
70	45 55	addscld	$$⊢\left(\phi \wedge \psi \right)\to \left(X{\cdot }_{s}C\right){+}_s\left(A{\cdot }_{s}Z\right)\in \mathrm{No}$$
71	48 70 58	addsubsassd	$$⊢\left(\phi \wedge \psi \right)\to \left(\left(A{\cdot }_{s}B\right){+}_s\left(\left(X{\cdot }_{s}C\right){+}_s\left(A{\cdot }_{s}Z\right)\right)\right){-}_s\left(X{\cdot }_{s}Z\right)=\left(A{\cdot }_{s}B\right){+}_s\left(\left(\left(X{\cdot }_{s}C\right){+}_s\left(A{\cdot }_{s}Z\right)\right){-}_s\left(X{\cdot }_{s}Z\right)\right)$$
72	69 71	eqtrd	$$⊢\left(\phi \wedge \psi \right)\to \left(\left(\left(\left(X{\cdot }_{s}B\right){+}_s\left(X{\cdot }_{s}C\right)\right){+}_s\left(\left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}Z\right)\right)\right){-}_s\left(X{\cdot }_{s}B\right)\right){-}_s\left(X{\cdot }_{s}Z\right)=\left(A{\cdot }_{s}B\right){+}_s\left(\left(\left(X{\cdot }_{s}C\right){+}_s\left(A{\cdot }_{s}Z\right)\right){-}_s\left(X{\cdot }_{s}Z\right)\right)$$
73	36 59 72	3eqtr2d	$$⊢\left(\phi \wedge \psi \right)\to \left(\left(X{\cdot }_s\left(B{+}_{s}C\right)\right){+}_s\left(A{\cdot }_s\left(B{+}_{s}Z\right)\right)\right){-}_s\left(X{\cdot }_s\left(B{+}_{s}Z\right)\right)=\left(A{\cdot }_{s}B\right){+}_s\left(\left(\left(X{\cdot }_{s}C\right){+}_s\left(A{\cdot }_{s}Z\right)\right){-}_s\left(X{\cdot }_{s}Z\right)\right)$$