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	No typesetting found for |- P C_ ( ( _Left ` A ) u. ( _Right ` A ) ) with typecode |-
	mulsasslem3.5	No typesetting found for |- Q C_ ( ( _Left ` B ) u. ( _Right ` B ) ) with typecode |-
	mulsasslem3.6	No typesetting found for |- R C_ ( ( _Left ` C ) u. ( _Right ` C ) ) with typecode |-
	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	Could not format assertion : No typesetting found for |- ( ph -> ( E. x e. P E. y e. Q E. z e. R a = ( ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) ) <-> E. x e. P E. y e. Q E. z e. R a = ( ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) -s ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) ) ) with typecode |-

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	Could not format P C_ ( ( _Left ` A ) u. ( _Right ` A ) ) : No typesetting found for |- P C_ ( ( _Left ` A ) u. ( _Right ` A ) ) with typecode |-
5		mulsasslem3.5	Could not format Q C_ ( ( _Left ` B ) u. ( _Right ` B ) ) : No typesetting found for |- Q C_ ( ( _Left ` B ) u. ( _Right ` B ) ) with typecode |-
6		mulsasslem3.6	Could not format R C_ ( ( _Left ` C ) u. ( _Right ` C ) ) : No typesetting found for |- R C_ ( ( _Left ` C ) u. ( _Right ` C ) ) with typecode |-
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	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> x e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> x e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode |-
21	17 18 20	rspcdva	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s B ) x.s C ) = ( x x.s ( B x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s B ) x.s C ) = ( x x.s ( B x.s C ) ) ) with typecode |-
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	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> y e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> y e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) with typecode |-
30	26 27 29	rspcdva	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s y ) x.s C ) = ( A x.s ( y x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s y ) x.s C ) = ( A x.s ( y x.s C ) ) ) with typecode |-
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	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> z e. ( ( _Left ` C ) u. ( _Right ` C ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> z e. ( ( _Left ` C ) u. ( _Right ` C ) ) ) with typecode |-
38	34 35 37	rspcdva	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s B ) x.s z ) = ( A x.s ( B x.s z ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s B ) x.s z ) = ( A x.s ( B x.s z ) ) ) with typecode |-
39		leftssno	Could not format ( _Left ` A ) C_ No : No typesetting found for |- ( _Left ` A ) C_ No with typecode |-
40		rightssno	Could not format ( _Right ` A ) C_ No : No typesetting found for |- ( _Right ` A ) C_ No with typecode |-
41	39 40	unssi	Could not format ( ( _Left ` A ) u. ( _Right ` A ) ) C_ No : No typesetting found for |- ( ( _Left ` A ) u. ( _Right ` A ) ) C_ No with typecode |-
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	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s B ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s B ) e. No ) with typecode |-
46		leftssno	Could not format ( _Left ` C ) C_ No : No typesetting found for |- ( _Left ` C ) C_ No with typecode |-
47		rightssno	Could not format ( _Right ` C ) C_ No : No typesetting found for |- ( _Right ` C ) C_ No with typecode |-
48	46 47	unssi	Could not format ( ( _Left ` C ) u. ( _Right ` C ) ) C_ No : No typesetting found for |- ( ( _Left ` C ) u. ( _Right ` C ) ) C_ No with typecode |-
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	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s B ) x.s z ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s B ) x.s z ) e. No ) with typecode |-
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	Could not format ( _Left ` B ) C_ No : No typesetting found for |- ( _Left ` B ) C_ No with typecode |-
54		rightssno	Could not format ( _Right ` B ) C_ No : No typesetting found for |- ( _Right ` B ) C_ No with typecode |-
55	53 54	unssi	Could not format ( ( _Left ` B ) u. ( _Right ` B ) ) C_ No : No typesetting found for |- ( ( _Left ` B ) u. ( _Right ` B ) ) C_ No with typecode |-
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	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s y ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s y ) e. No ) with typecode |-
59	58 50	mulscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s y ) x.s z ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s y ) x.s z ) e. No ) with typecode |-
60	51 59	addscomd	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) = ( ( ( A x.s y ) x.s z ) +s ( ( x x.s B ) x.s z ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) = ( ( ( A x.s y ) x.s z ) +s ( ( x x.s B ) x.s z ) ) ) with typecode |-
61	60	oveq1d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) = ( ( ( ( A x.s y ) x.s z ) +s ( ( x x.s B ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) = ( ( ( ( A x.s y ) x.s z ) +s ( ( x x.s B ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) with typecode |-
62	43 57	mulscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s y ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s y ) e. No ) with typecode |-
63	62 50	mulscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s y ) x.s z ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s y ) x.s z ) e. No ) with typecode |-
64	59 51 63	addsubsassd	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s y ) x.s z ) +s ( ( x x.s B ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) = ( ( ( A x.s y ) x.s z ) +s ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s y ) x.s z ) +s ( ( x x.s B ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) = ( ( ( A x.s y ) x.s z ) +s ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) ) ) with typecode |-
65	61 64	eqtrd	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) = ( ( ( A x.s y ) x.s z ) +s ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) = ( ( ( A x.s y ) x.s z ) +s ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) ) ) with typecode |-
66	65	oveq1d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) = ( ( ( ( A x.s y ) x.s z ) +s ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) ) +s ( ( x x.s y ) x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) = ( ( ( ( A x.s y ) x.s z ) +s ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) ) +s ( ( x x.s y ) x.s C ) ) ) with typecode |-
67	51 63	subscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) e. No ) with typecode |-
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	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s y ) x.s C ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s y ) x.s C ) e. No ) with typecode |-
70	59 67 69	addsassd	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s y ) x.s z ) +s ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) ) +s ( ( x x.s y ) x.s C ) ) = ( ( ( A x.s y ) x.s z ) +s ( ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s y ) x.s z ) +s ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) ) +s ( ( x x.s y ) x.s C ) ) = ( ( ( A x.s y ) x.s z ) +s ( ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) ) ) with typecode |-
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	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s y ) x.s z ) = ( A x.s ( y x.s z ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s y ) x.s z ) = ( A x.s ( y x.s z ) ) ) with typecode |-
81	51 69 63	addsubsd	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s z ) +s ( ( x x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s z ) ) = ( ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s z ) +s ( ( x x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s z ) ) = ( ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) ) with typecode |-
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	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s B ) x.s z ) = ( x x.s ( B x.s z ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s B ) x.s z ) = ( x x.s ( B x.s z ) ) ) with typecode |-
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	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s y ) x.s C ) = ( x x.s ( y x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s y ) x.s C ) = ( x x.s ( y x.s C ) ) ) with typecode |-
100	89 99	oveq12d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) x.s z ) +s ( ( x x.s y ) x.s C ) ) = ( ( x x.s ( B x.s z ) ) +s ( x x.s ( y x.s C ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) x.s z ) +s ( ( x x.s y ) x.s C ) ) = ( ( x x.s ( B x.s z ) ) +s ( x x.s ( y x.s C ) ) ) ) with typecode |-
101	44 50	mulscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( B x.s z ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( B x.s z ) e. No ) with typecode |-
102	43 101	mulscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s ( B x.s z ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s ( B x.s z ) ) e. No ) with typecode |-
103	57 68	mulscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( y x.s C ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( y x.s C ) e. No ) with typecode |-
104	43 103	mulscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s ( y x.s C ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s ( y x.s C ) ) e. No ) with typecode |-
105	102 104	addscomd	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s ( B x.s z ) ) +s ( x x.s ( y x.s C ) ) ) = ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s ( B x.s z ) ) +s ( x x.s ( y x.s C ) ) ) = ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) ) with typecode |-
106	100 105	eqtrd	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) x.s z ) +s ( ( x x.s y ) x.s C ) ) = ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) x.s z ) +s ( ( x x.s y ) x.s C ) ) = ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) ) with typecode |-
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	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s y ) x.s z ) = ( x x.s ( y x.s z ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s y ) x.s z ) = ( x x.s ( y x.s z ) ) ) with typecode |-
118	106 117	oveq12d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s z ) +s ( ( x x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s z ) ) = ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s z ) +s ( ( x x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s z ) ) = ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) with typecode |-
119	81 118	eqtr3d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) = ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) = ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) with typecode |-
120	80 119	oveq12d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s y ) x.s z ) +s ( ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) ) = ( ( A x.s ( y x.s z ) ) +s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s y ) x.s z ) +s ( ( ( ( x x.s B ) x.s z ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) ) = ( ( A x.s ( y x.s z ) ) +s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) with typecode |-
121	66 70 120	3eqtrd	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) = ( ( A x.s ( y x.s z ) ) +s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) = ( ( A x.s ( y x.s z ) ) +s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) with typecode |-
122	38 121	oveq12d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s B ) x.s z ) -s ( ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) ) = ( ( A x.s ( B x.s z ) ) -s ( ( A x.s ( y x.s z ) ) +s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s B ) x.s z ) -s ( ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) ) = ( ( A x.s ( B x.s z ) ) -s ( ( A x.s ( y x.s z ) ) +s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) ) with typecode |-
123	52 44	mulscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s B ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s B ) e. No ) with typecode |-
124	123 50	mulscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s B ) x.s z ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s B ) x.s z ) e. No ) with typecode |-
125	51 59	addscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) e. No ) with typecode |-
126	125 63	subscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) e. No ) with typecode |-
127	124 126 69	subsubs4d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) -s ( ( x x.s y ) x.s C ) ) = ( ( ( A x.s B ) x.s z ) -s ( ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) -s ( ( x x.s y ) x.s C ) ) = ( ( ( A x.s B ) x.s z ) -s ( ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) +s ( ( x x.s y ) x.s C ) ) ) ) with typecode |-
128	52 101	mulscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s ( B x.s z ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s ( B x.s z ) ) e. No ) with typecode |-
129	57 50	mulscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( y x.s z ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( y x.s z ) e. No ) with typecode |-
130	52 129	mulscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s ( y x.s z ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s ( y x.s z ) ) e. No ) with typecode |-
131	104 102	addscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) e. No ) with typecode |-
132	43 129	mulscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s ( y x.s z ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s ( y x.s z ) ) e. No ) with typecode |-
133	131 132	subscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) e. No ) with typecode |-
134	128 130 133	subsubs4d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) = ( ( A x.s ( B x.s z ) ) -s ( ( A x.s ( y x.s z ) ) +s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) = ( ( A x.s ( B x.s z ) ) -s ( ( A x.s ( y x.s z ) ) +s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) ) with typecode |-
135	122 127 134	3eqtr4d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) -s ( ( x x.s y ) x.s C ) ) = ( ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) -s ( ( x x.s y ) x.s C ) ) = ( ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) with typecode |-
136	30 135	oveq12d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s y ) x.s C ) +s ( ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) -s ( ( x x.s y ) x.s C ) ) ) = ( ( A x.s ( y x.s C ) ) +s ( ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s y ) x.s C ) +s ( ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) -s ( ( x x.s y ) x.s C ) ) ) = ( ( A x.s ( y x.s C ) ) +s ( ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) ) with typecode |-
137	58 68	mulscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s y ) x.s C ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s y ) x.s C ) e. No ) with typecode |-
138	124 126	subscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) e. No ) with typecode |-
139	137 138 69	addsubsd	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s y ) x.s C ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) -s ( ( x x.s y ) x.s C ) ) = ( ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s y ) x.s C ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) -s ( ( x x.s y ) x.s C ) ) = ( ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) ) with typecode |-
140	137 138 69	addsubsassd	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s y ) x.s C ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) -s ( ( x x.s y ) x.s C ) ) = ( ( ( A x.s y ) x.s C ) +s ( ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) -s ( ( x x.s y ) x.s C ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s y ) x.s C ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) -s ( ( x x.s y ) x.s C ) ) = ( ( ( A x.s y ) x.s C ) +s ( ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) -s ( ( x x.s y ) x.s C ) ) ) ) with typecode |-
141	139 140	eqtr3d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) = ( ( ( A x.s y ) x.s C ) +s ( ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) -s ( ( x x.s y ) x.s C ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) = ( ( ( A x.s y ) x.s C ) +s ( ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) -s ( ( x x.s y ) x.s C ) ) ) ) with typecode |-
142	52 103	mulscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s ( y x.s C ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s ( y x.s C ) ) e. No ) with typecode |-
143	142 128 130	addsubsassd	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) = ( ( A x.s ( y x.s C ) ) +s ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) = ( ( A x.s ( y x.s C ) ) +s ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) ) ) with typecode |-
144	143	oveq1d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) = ( ( ( A x.s ( y x.s C ) ) +s ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) = ( ( ( A x.s ( y x.s C ) ) +s ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) with typecode |-
145	128 130	subscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) e. No ) with typecode |-
146	142 145 133	addsubsassd	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s ( y x.s C ) ) +s ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) = ( ( A x.s ( y x.s C ) ) +s ( ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s ( y x.s C ) ) +s ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) = ( ( A x.s ( y x.s C ) ) +s ( ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) ) with typecode |-
147	144 146	eqtrd	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) = ( ( A x.s ( y x.s C ) ) +s ( ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) = ( ( A x.s ( y x.s C ) ) +s ( ( ( A x.s ( B x.s z ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) ) with typecode |-
148	136 141 147	3eqtr4d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) = ( ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) = ( ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) with typecode |-
149	21 148	oveq12d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) x.s C ) +s ( ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) ) = ( ( x x.s ( B x.s C ) ) +s ( ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) x.s C ) +s ( ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) ) = ( ( x x.s ( B x.s C ) ) +s ( ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) ) with typecode |-
150	45 68	mulscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s B ) x.s C ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s B ) x.s C ) e. No ) with typecode |-
151	150 137	addscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) e. No ) with typecode |-
152	151 69	subscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) e. No ) with typecode |-
153	152 124 126	addsubsassd	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) = ( ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) = ( ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) ) with typecode |-
154	150 137 69	addsubsassd	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) = ( ( ( x x.s B ) x.s C ) +s ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) = ( ( ( x x.s B ) x.s C ) +s ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) ) ) with typecode |-
155	154	oveq1d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) = ( ( ( ( x x.s B ) x.s C ) +s ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) = ( ( ( ( x x.s B ) x.s C ) +s ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) ) with typecode |-
156	137 69	subscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) e. No ) with typecode |-
157	150 156 138	addsassd	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s C ) +s ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) = ( ( ( x x.s B ) x.s C ) +s ( ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) x.s C ) +s ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) = ( ( ( x x.s B ) x.s C ) +s ( ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) ) ) with typecode |-
158	153 155 157	3eqtrd	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) = ( ( ( x x.s B ) x.s C ) +s ( ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) = ( ( ( x x.s B ) x.s C ) +s ( ( ( ( A x.s y ) x.s C ) -s ( ( x x.s y ) x.s C ) ) +s ( ( ( A x.s B ) x.s z ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) ) ) with typecode |-
159	44 68	mulscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( B x.s C ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( B x.s C ) e. No ) with typecode |-
160	43 159	mulscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s ( B x.s C ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s ( B x.s C ) ) e. No ) with typecode |-
161	142 128	addscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) e. No ) with typecode |-
162	161 130	subscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) e. No ) with typecode |-
163	160 162 133	addsubsassd	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s ( B x.s C ) ) +s ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) = ( ( x x.s ( B x.s C ) ) +s ( ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s ( B x.s C ) ) +s ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) = ( ( x x.s ( B x.s C ) ) +s ( ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) ) with typecode |-
164	149 158 163	3eqtr4d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) = ( ( ( x x.s ( B x.s C ) ) +s ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) = ( ( ( x x.s ( B x.s C ) ) +s ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) with typecode |-
165	45 58	addscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s B ) +s ( A x.s y ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s B ) +s ( A x.s y ) ) e. No ) with typecode |-
166	165 62 68	subsdird	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) = ( ( ( ( x x.s B ) +s ( A x.s y ) ) x.s C ) -s ( ( x x.s y ) x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) = ( ( ( ( x x.s B ) +s ( A x.s y ) ) x.s C ) -s ( ( x x.s y ) x.s C ) ) ) with typecode |-
167	45 58 68	addsdird	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) +s ( A x.s y ) ) x.s C ) = ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) +s ( A x.s y ) ) x.s C ) = ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) ) with typecode |-
168	167	oveq1d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) +s ( A x.s y ) ) x.s C ) -s ( ( x x.s y ) x.s C ) ) = ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) +s ( A x.s y ) ) x.s C ) -s ( ( x x.s y ) x.s C ) ) = ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) ) with typecode |-
169	166 168	eqtrd	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) = ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) = ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) ) with typecode |-
170	169	oveq1d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) = ( ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) +s ( ( A x.s B ) x.s z ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) = ( ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) +s ( ( A x.s B ) x.s z ) ) ) with typecode |-
171	165 62 50	subsdird	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) = ( ( ( ( x x.s B ) +s ( A x.s y ) ) x.s z ) -s ( ( x x.s y ) x.s z ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) = ( ( ( ( x x.s B ) +s ( A x.s y ) ) x.s z ) -s ( ( x x.s y ) x.s z ) ) ) with typecode |-
172	45 58 50	addsdird	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) +s ( A x.s y ) ) x.s z ) = ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s B ) +s ( A x.s y ) ) x.s z ) = ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) ) with typecode |-
173	172	oveq1d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) +s ( A x.s y ) ) x.s z ) -s ( ( x x.s y ) x.s z ) ) = ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) +s ( A x.s y ) ) x.s z ) -s ( ( x x.s y ) x.s z ) ) = ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) with typecode |-
174	171 173	eqtrd	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) = ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) = ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) with typecode |-
175	170 174	oveq12d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) ) = ( ( ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) ) = ( ( ( ( ( ( x x.s B ) x.s C ) +s ( ( A x.s y ) x.s C ) ) -s ( ( x x.s y ) x.s C ) ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) x.s z ) +s ( ( A x.s y ) x.s z ) ) -s ( ( x x.s y ) x.s z ) ) ) ) with typecode |-
176	103 101	addscld	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( y x.s C ) +s ( B x.s z ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( y x.s C ) +s ( B x.s z ) ) e. No ) with typecode |-
177	52 176 129	subsdid	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) = ( ( A x.s ( ( y x.s C ) +s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) = ( ( A x.s ( ( y x.s C ) +s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) ) with typecode |-
178	52 103 101	addsdid	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s ( ( y x.s C ) +s ( B x.s z ) ) ) = ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s ( ( y x.s C ) +s ( B x.s z ) ) ) = ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) ) with typecode |-
179	178	oveq1d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s ( ( y x.s C ) +s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) = ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( A x.s ( ( y x.s C ) +s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) = ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) ) with typecode |-
180	177 179	eqtrd	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) = ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) = ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) ) with typecode |-
181	180	oveq2d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) = ( ( x x.s ( B x.s C ) ) +s ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) = ( ( x x.s ( B x.s C ) ) +s ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) ) ) with typecode |-
182	43 176 129	subsdid	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) = ( ( x x.s ( ( y x.s C ) +s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) = ( ( x x.s ( ( y x.s C ) +s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) with typecode |-
183	43 103 101	addsdid	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s ( ( y x.s C ) +s ( B x.s z ) ) ) = ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s ( ( y x.s C ) +s ( B x.s z ) ) ) = ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) ) with typecode |-
184	183	oveq1d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s ( ( y x.s C ) +s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) = ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( x x.s ( ( y x.s C ) +s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) = ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) with typecode |-
185	182 184	eqtrd	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) = ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) = ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) with typecode |-
186	181 185	oveq12d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) -s ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) = ( ( ( x x.s ( B x.s C ) ) +s ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) -s ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) = ( ( ( x x.s ( B x.s C ) ) +s ( ( ( A x.s ( y x.s C ) ) +s ( A x.s ( B x.s z ) ) ) -s ( A x.s ( y x.s z ) ) ) ) -s ( ( ( x x.s ( y x.s C ) ) +s ( x x.s ( B x.s z ) ) ) -s ( x x.s ( y x.s z ) ) ) ) ) with typecode |-
187	164 175 186	3eqtr4d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) ) = ( ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) -s ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) ) = ( ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) -s ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) ) with typecode |-
188	187	eqeq2d	Could not format ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( a = ( ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) ) <-> a = ( ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) -s ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( x e. P /\ y e. Q ) /\ z e. R ) ) -> ( a = ( ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) ) <-> a = ( ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) -s ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) ) ) with typecode |-
189	188	anassrs	Could not format ( ( ( ph /\ ( x e. P /\ y e. Q ) ) /\ z e. R ) -> ( a = ( ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) ) <-> a = ( ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) -s ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) ) ) : No typesetting found for |- ( ( ( ph /\ ( x e. P /\ y e. Q ) ) /\ z e. R ) -> ( a = ( ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) ) <-> a = ( ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) -s ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) ) ) with typecode |-
190	189	rexbidva	Could not format ( ( ph /\ ( x e. P /\ y e. Q ) ) -> ( E. z e. R a = ( ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) ) <-> E. z e. R a = ( ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) -s ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( x e. P /\ y e. Q ) ) -> ( E. z e. R a = ( ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) ) <-> E. z e. R a = ( ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) -s ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) ) ) with typecode |-
191	190	2rexbidva	Could not format ( ph -> ( E. x e. P E. y e. Q E. z e. R a = ( ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) ) <-> E. x e. P E. y e. Q E. z e. R a = ( ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) -s ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( E. x e. P E. y e. Q E. z e. R a = ( ( ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s C ) +s ( ( A x.s B ) x.s z ) ) -s ( ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) x.s z ) ) <-> E. x e. P E. y e. Q E. z e. R a = ( ( ( x x.s ( B x.s C ) ) +s ( A x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) -s ( x x.s ( ( ( y x.s C ) +s ( B x.s z ) ) -s ( y x.s z ) ) ) ) ) ) with typecode |-