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	No typesetting found for |- ( ps -> X e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode |-
	addsdilem3.8	No typesetting found for |- ( ps -> Y e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) with typecode |-
Assertion	addsdilem3	Could not format assertion : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( X x.s ( B +s C ) ) +s ( A x.s ( Y +s C ) ) ) -s ( X x.s ( Y +s C ) ) ) = ( ( ( ( X x.s B ) +s ( A x.s Y ) ) -s ( X x.s Y ) ) +s ( A x.s C ) ) ) with typecode |-

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	Could not format ( ps -> X e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) : No typesetting found for |- ( ps -> X e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode |-
8		addsdilem3.8	Could not format ( ps -> Y e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) : No typesetting found for |- ( ps -> Y e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) with typecode |-
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	Could not format ( ( ph /\ ps ) -> X e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> X e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode |-
16	13 14 15	rspcdva	Could not format ( ( ph /\ ps ) -> ( X x.s ( B +s C ) ) = ( ( X x.s B ) +s ( X x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( X x.s ( B +s C ) ) = ( ( X x.s B ) +s ( X x.s C ) ) ) with typecode |-
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	Could not format ( ( ph /\ ps ) -> Y e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> Y e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) with typecode |-
24	21 22 23	rspcdva	Could not format ( ( ph /\ ps ) -> ( A x.s ( Y +s C ) ) = ( ( A x.s Y ) +s ( A x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( A x.s ( Y +s C ) ) = ( ( A x.s Y ) +s ( A x.s C ) ) ) with typecode |-
25	16 24	oveq12d	Could not format ( ( ph /\ ps ) -> ( ( X x.s ( B +s C ) ) +s ( A x.s ( Y +s C ) ) ) = ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( X x.s ( B +s C ) ) +s ( A x.s ( Y +s C ) ) ) = ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) ) with typecode |-
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	Could not format ( ( ph /\ ps ) -> ( X x.s ( Y +s C ) ) = ( ( X x.s Y ) +s ( X x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( X x.s ( Y +s C ) ) = ( ( X x.s Y ) +s ( X x.s C ) ) ) with typecode |-
36	25 35	oveq12d	Could not format ( ( ph /\ ps ) -> ( ( ( X x.s ( B +s C ) ) +s ( A x.s ( Y +s C ) ) ) -s ( X x.s ( Y +s C ) ) ) = ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) -s ( ( X x.s Y ) +s ( X x.s C ) ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( X x.s ( B +s C ) ) +s ( A x.s ( Y +s C ) ) ) -s ( X x.s ( Y +s C ) ) ) = ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) -s ( ( X x.s Y ) +s ( X x.s C ) ) ) ) with typecode |-
37		leftssno	Could not format ( _Left ` A ) C_ No : No typesetting found for |- ( _Left ` A ) C_ No with typecode |-
38		rightssno	Could not format ( _Right ` A ) C_ No : No typesetting found for |- ( _Right ` A ) C_ No with typecode |-
39	37 38	unssi	Could not format ( ( _Left ` A ) u. ( _Right ` A ) ) C_ No : No typesetting found for |- ( ( _Left ` A ) u. ( _Right ` A ) ) C_ No with typecode |-
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	Could not format ( ( ph /\ ps ) -> ( X x.s B ) e. No ) : No typesetting found for |- ( ( ph /\ ps ) -> ( X x.s B ) e. No ) with typecode |-
44	3	adantr	$$⊢\left(\phi \wedge \psi \right)\to C\in \mathrm{No}$$
45	41 44	mulscld	Could not format ( ( ph /\ ps ) -> ( X x.s C ) e. No ) : No typesetting found for |- ( ( ph /\ ps ) -> ( X x.s C ) e. No ) with typecode |-
46		pncans	Could not format ( ( ( X x.s B ) e. No /\ ( X x.s C ) e. No ) -> ( ( ( X x.s B ) +s ( X x.s C ) ) -s ( X x.s C ) ) = ( X x.s B ) ) : No typesetting found for |- ( ( ( X x.s B ) e. No /\ ( X x.s C ) e. No ) -> ( ( ( X x.s B ) +s ( X x.s C ) ) -s ( X x.s C ) ) = ( X x.s B ) ) with typecode |-
47	43 45 46	syl2anc	Could not format ( ( ph /\ ps ) -> ( ( ( X x.s B ) +s ( X x.s C ) ) -s ( X x.s C ) ) = ( X x.s B ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( X x.s B ) +s ( X x.s C ) ) -s ( X x.s C ) ) = ( X x.s B ) ) with typecode |-
48	47	oveq1d	Could not format ( ( ph /\ ps ) -> ( ( ( ( X x.s B ) +s ( X x.s C ) ) -s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) = ( ( X x.s B ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( ( X x.s B ) +s ( X x.s C ) ) -s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) = ( ( X x.s B ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) ) with typecode |-
49	43 45	addscld	Could not format ( ( ph /\ ps ) -> ( ( X x.s B ) +s ( X x.s C ) ) e. No ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( X x.s B ) +s ( X x.s C ) ) e. No ) with typecode |-
50	1	adantr	$$⊢\left(\phi \wedge \psi \right)\to A\in \mathrm{No}$$
51		leftssno	Could not format ( _Left ` B ) C_ No : No typesetting found for |- ( _Left ` B ) C_ No with typecode |-
52		rightssno	Could not format ( _Right ` B ) C_ No : No typesetting found for |- ( _Right ` B ) C_ No with typecode |-
53	51 52	unssi	Could not format ( ( _Left ` B ) u. ( _Right ` B ) ) C_ No : No typesetting found for |- ( ( _Left ` B ) u. ( _Right ` B ) ) C_ No with typecode |-
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	Could not format ( ( ph /\ ps ) -> ( A x.s Y ) e. No ) : No typesetting found for |- ( ( ph /\ ps ) -> ( A x.s Y ) e. No ) with typecode |-
57	1 3	mulscld	Could not format ( ph -> ( A x.s C ) e. No ) : No typesetting found for |- ( ph -> ( A x.s C ) e. No ) with typecode |-
58	57	adantr	Could not format ( ( ph /\ ps ) -> ( A x.s C ) e. No ) : No typesetting found for |- ( ( ph /\ ps ) -> ( A x.s C ) e. No ) with typecode |-
59	56 58	addscld	Could not format ( ( ph /\ ps ) -> ( ( A x.s Y ) +s ( A x.s C ) ) e. No ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( A x.s Y ) +s ( A x.s C ) ) e. No ) with typecode |-
60	49 59 45	addsubsd	Could not format ( ( ph /\ ps ) -> ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) -s ( X x.s C ) ) = ( ( ( ( X x.s B ) +s ( X x.s C ) ) -s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) -s ( X x.s C ) ) = ( ( ( ( X x.s B ) +s ( X x.s C ) ) -s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) ) with typecode |-
61	43 56 58	addsassd	Could not format ( ( ph /\ ps ) -> ( ( ( X x.s B ) +s ( A x.s Y ) ) +s ( A x.s C ) ) = ( ( X x.s B ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( X x.s B ) +s ( A x.s Y ) ) +s ( A x.s C ) ) = ( ( X x.s B ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) ) with typecode |-
62	48 60 61	3eqtr4d	Could not format ( ( ph /\ ps ) -> ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) -s ( X x.s C ) ) = ( ( ( X x.s B ) +s ( A x.s Y ) ) +s ( A x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) -s ( X x.s C ) ) = ( ( ( X x.s B ) +s ( A x.s Y ) ) +s ( A x.s C ) ) ) with typecode |-
63	62	oveq1d	Could not format ( ( ph /\ ps ) -> ( ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) -s ( X x.s C ) ) -s ( X x.s Y ) ) = ( ( ( ( X x.s B ) +s ( A x.s Y ) ) +s ( A x.s C ) ) -s ( X x.s Y ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) -s ( X x.s C ) ) -s ( X x.s Y ) ) = ( ( ( ( X x.s B ) +s ( A x.s Y ) ) +s ( A x.s C ) ) -s ( X x.s Y ) ) ) with typecode |-
64	49 59	addscld	Could not format ( ( ph /\ ps ) -> ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) e. No ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) e. No ) with typecode |-
65	40 54	mulscld	Could not format ( ps -> ( X x.s Y ) e. No ) : No typesetting found for |- ( ps -> ( X x.s Y ) e. No ) with typecode |-
66	65	adantl	Could not format ( ( ph /\ ps ) -> ( X x.s Y ) e. No ) : No typesetting found for |- ( ( ph /\ ps ) -> ( X x.s Y ) e. No ) with typecode |-
67	64 45 66	subsubs4d	Could not format ( ( ph /\ ps ) -> ( ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) -s ( X x.s C ) ) -s ( X x.s Y ) ) = ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) -s ( ( X x.s C ) +s ( X x.s Y ) ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) -s ( X x.s C ) ) -s ( X x.s Y ) ) = ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) -s ( ( X x.s C ) +s ( X x.s Y ) ) ) ) with typecode |-
68	45 66	addscomd	Could not format ( ( ph /\ ps ) -> ( ( X x.s C ) +s ( X x.s Y ) ) = ( ( X x.s Y ) +s ( X x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( X x.s C ) +s ( X x.s Y ) ) = ( ( X x.s Y ) +s ( X x.s C ) ) ) with typecode |-
69	68	oveq2d	Could not format ( ( ph /\ ps ) -> ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) -s ( ( X x.s C ) +s ( X x.s Y ) ) ) = ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) -s ( ( X x.s Y ) +s ( X x.s C ) ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) -s ( ( X x.s C ) +s ( X x.s Y ) ) ) = ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) -s ( ( X x.s Y ) +s ( X x.s C ) ) ) ) with typecode |-
70	67 69	eqtrd	Could not format ( ( ph /\ ps ) -> ( ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) -s ( X x.s C ) ) -s ( X x.s Y ) ) = ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) -s ( ( X x.s Y ) +s ( X x.s C ) ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) -s ( X x.s C ) ) -s ( X x.s Y ) ) = ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) -s ( ( X x.s Y ) +s ( X x.s C ) ) ) ) with typecode |-
71	43 56	addscld	Could not format ( ( ph /\ ps ) -> ( ( X x.s B ) +s ( A x.s Y ) ) e. No ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( X x.s B ) +s ( A x.s Y ) ) e. No ) with typecode |-
72	71 58 66	addsubsd	Could not format ( ( ph /\ ps ) -> ( ( ( ( X x.s B ) +s ( A x.s Y ) ) +s ( A x.s C ) ) -s ( X x.s Y ) ) = ( ( ( ( X x.s B ) +s ( A x.s Y ) ) -s ( X x.s Y ) ) +s ( A x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( ( X x.s B ) +s ( A x.s Y ) ) +s ( A x.s C ) ) -s ( X x.s Y ) ) = ( ( ( ( X x.s B ) +s ( A x.s Y ) ) -s ( X x.s Y ) ) +s ( A x.s C ) ) ) with typecode |-
73	63 70 72	3eqtr3d	Could not format ( ( ph /\ ps ) -> ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) -s ( ( X x.s Y ) +s ( X x.s C ) ) ) = ( ( ( ( X x.s B ) +s ( A x.s Y ) ) -s ( X x.s Y ) ) +s ( A x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s Y ) +s ( A x.s C ) ) ) -s ( ( X x.s Y ) +s ( X x.s C ) ) ) = ( ( ( ( X x.s B ) +s ( A x.s Y ) ) -s ( X x.s Y ) ) +s ( A x.s C ) ) ) with typecode |-
74	36 73	eqtrd	Could not format ( ( ph /\ ps ) -> ( ( ( X x.s ( B +s C ) ) +s ( A x.s ( Y +s C ) ) ) -s ( X x.s ( Y +s C ) ) ) = ( ( ( ( X x.s B ) +s ( A x.s Y ) ) -s ( X x.s Y ) ) +s ( A x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( X x.s ( B +s C ) ) +s ( A x.s ( Y +s C ) ) ) -s ( X x.s ( Y +s C ) ) ) = ( ( ( ( X x.s B ) +s ( A x.s Y ) ) -s ( X x.s Y ) ) +s ( A x.s C ) ) ) with typecode |-