Theorem addsdilem3

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

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

Proof

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