Theorem mulscom

Description: Surreal multiplication commutes. Part of theorem 7 of Conway p. 19. (Contributed by Scott Fenton, 6-Mar-2025)

	Ref	Expression
Assertion	mulscom	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A{\cdot }_{s}B=B{\cdot }_{s}A$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	Could not format ( x = xO -> ( x x.s y ) = ( xO x.s y ) ) : No typesetting found for |- ( x = xO -> ( x x.s y ) = ( xO x.s y ) ) with typecode |-
2		oveq2	Could not format ( x = xO -> ( y x.s x ) = ( y x.s xO ) ) : No typesetting found for |- ( x = xO -> ( y x.s x ) = ( y x.s xO ) ) with typecode |-
3	1 2	eqeq12d	Could not format ( x = xO -> ( ( x x.s y ) = ( y x.s x ) <-> ( xO x.s y ) = ( y x.s xO ) ) ) : No typesetting found for |- ( x = xO -> ( ( x x.s y ) = ( y x.s x ) <-> ( xO x.s y ) = ( y x.s xO ) ) ) with typecode |-
4		oveq2	Could not format ( y = yO -> ( xO x.s y ) = ( xO x.s yO ) ) : No typesetting found for |- ( y = yO -> ( xO x.s y ) = ( xO x.s yO ) ) with typecode |-
5		oveq1	Could not format ( y = yO -> ( y x.s xO ) = ( yO x.s xO ) ) : No typesetting found for |- ( y = yO -> ( y x.s xO ) = ( yO x.s xO ) ) with typecode |-
6	4 5	eqeq12d	Could not format ( y = yO -> ( ( xO x.s y ) = ( y x.s xO ) <-> ( xO x.s yO ) = ( yO x.s xO ) ) ) : No typesetting found for |- ( y = yO -> ( ( xO x.s y ) = ( y x.s xO ) <-> ( xO x.s yO ) = ( yO x.s xO ) ) ) with typecode |-
7		oveq1	Could not format ( x = xO -> ( x x.s yO ) = ( xO x.s yO ) ) : No typesetting found for |- ( x = xO -> ( x x.s yO ) = ( xO x.s yO ) ) with typecode |-
8		oveq2	Could not format ( x = xO -> ( yO x.s x ) = ( yO x.s xO ) ) : No typesetting found for |- ( x = xO -> ( yO x.s x ) = ( yO x.s xO ) ) with typecode |-
9	7 8	eqeq12d	Could not format ( x = xO -> ( ( x x.s yO ) = ( yO x.s x ) <-> ( xO x.s yO ) = ( yO x.s xO ) ) ) : No typesetting found for |- ( x = xO -> ( ( x x.s yO ) = ( yO x.s x ) <-> ( xO x.s yO ) = ( yO x.s xO ) ) ) with typecode |-
10		oveq1	$$⊢x=A\to x{\cdot }_{s}y=A{\cdot }_{s}y$$
11		oveq2	$$⊢x=A\to y{\cdot }_{s}x=y{\cdot }_{s}A$$
12	10 11	eqeq12d	$$⊢x=A\to \left(x{\cdot }_{s}y=y{\cdot }_{s}x\leftrightarrow A{\cdot }_{s}y=y{\cdot }_{s}A\right)$$
13		oveq2	$$⊢y=B\to A{\cdot }_{s}y=A{\cdot }_{s}B$$
14		oveq1	$$⊢y=B\to y{\cdot }_{s}A=B{\cdot }_{s}A$$
15	13 14	eqeq12d	$$⊢y=B\to \left(A{\cdot }_{s}y=y{\cdot }_{s}A\leftrightarrow A{\cdot }_{s}B=B{\cdot }_{s}A\right)$$
16		oveq1	Could not format ( xO = p -> ( xO x.s y ) = ( p x.s y ) ) : No typesetting found for |- ( xO = p -> ( xO x.s y ) = ( p x.s y ) ) with typecode |-
17		oveq2	Could not format ( xO = p -> ( y x.s xO ) = ( y x.s p ) ) : No typesetting found for |- ( xO = p -> ( y x.s xO ) = ( y x.s p ) ) with typecode |-
18	16 17	eqeq12d	Could not format ( xO = p -> ( ( xO x.s y ) = ( y x.s xO ) <-> ( p x.s y ) = ( y x.s p ) ) ) : No typesetting found for |- ( xO = p -> ( ( xO x.s y ) = ( y x.s xO ) <-> ( p x.s y ) = ( y x.s p ) ) ) with typecode |-
19		simplr2	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) ) with typecode |-
20		simprl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> p e. ( _Left ` x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> p e. ( _Left ` x ) ) with typecode |-
21		elun1	$$⊢p\in L\left(x\right)\to p\in \left(L\left(x\right)\cup R\left(x\right)\right)$$
22	20 21	syl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> p e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> p e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
23	18 19 22	rspcdva	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( p x.s y ) = ( y x.s p ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( p x.s y ) = ( y x.s p ) ) with typecode |-
24		oveq2	Could not format ( yO = q -> ( x x.s yO ) = ( x x.s q ) ) : No typesetting found for |- ( yO = q -> ( x x.s yO ) = ( x x.s q ) ) with typecode |-
25		oveq1	Could not format ( yO = q -> ( yO x.s x ) = ( q x.s x ) ) : No typesetting found for |- ( yO = q -> ( yO x.s x ) = ( q x.s x ) ) with typecode |-
26	24 25	eqeq12d	Could not format ( yO = q -> ( ( x x.s yO ) = ( yO x.s x ) <-> ( x x.s q ) = ( q x.s x ) ) ) : No typesetting found for |- ( yO = q -> ( ( x x.s yO ) = ( yO x.s x ) <-> ( x x.s q ) = ( q x.s x ) ) ) with typecode |-
27		simplr3	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) with typecode |-
28		simprr	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> q e. ( _Left ` y ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> q e. ( _Left ` y ) ) with typecode |-
29		elun1	$$⊢q\in L\left(y\right)\to q\in \left(L\left(y\right)\cup R\left(y\right)\right)$$
30	28 29	syl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> q e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> q e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) with typecode |-
31	26 27 30	rspcdva	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( x x.s q ) = ( q x.s x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( x x.s q ) = ( q x.s x ) ) with typecode |-
32	23 31	oveq12d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( ( p x.s y ) +s ( x x.s q ) ) = ( ( y x.s p ) +s ( q x.s x ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( ( p x.s y ) +s ( x x.s q ) ) = ( ( y x.s p ) +s ( q x.s x ) ) ) with typecode |-
33		simpllr	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> y e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> y e. No ) with typecode |-
34	20	leftnod	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> p e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> p e. No ) with typecode |-
35	33 34	mulscld	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( y x.s p ) e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( y x.s p ) e. No ) with typecode |-
36	28	leftnod	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> q e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> q e. No ) with typecode |-
37		simplll	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> x e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> x e. No ) with typecode |-
38	36 37	mulscld	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( q x.s x ) e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( q x.s x ) e. No ) with typecode |-
39	35 38	addscomd	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( ( y x.s p ) +s ( q x.s x ) ) = ( ( q x.s x ) +s ( y x.s p ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( ( y x.s p ) +s ( q x.s x ) ) = ( ( q x.s x ) +s ( y x.s p ) ) ) with typecode |-
40	32 39	eqtrd	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( ( p x.s y ) +s ( x x.s q ) ) = ( ( q x.s x ) +s ( y x.s p ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( ( p x.s y ) +s ( x x.s q ) ) = ( ( q x.s x ) +s ( y x.s p ) ) ) with typecode |-
41		oveq1	Could not format ( xO = p -> ( xO x.s yO ) = ( p x.s yO ) ) : No typesetting found for |- ( xO = p -> ( xO x.s yO ) = ( p x.s yO ) ) with typecode |-
42		oveq2	Could not format ( xO = p -> ( yO x.s xO ) = ( yO x.s p ) ) : No typesetting found for |- ( xO = p -> ( yO x.s xO ) = ( yO x.s p ) ) with typecode |-
43	41 42	eqeq12d	Could not format ( xO = p -> ( ( xO x.s yO ) = ( yO x.s xO ) <-> ( p x.s yO ) = ( yO x.s p ) ) ) : No typesetting found for |- ( xO = p -> ( ( xO x.s yO ) = ( yO x.s xO ) <-> ( p x.s yO ) = ( yO x.s p ) ) ) with typecode |-
44		oveq2	Could not format ( yO = q -> ( p x.s yO ) = ( p x.s q ) ) : No typesetting found for |- ( yO = q -> ( p x.s yO ) = ( p x.s q ) ) with typecode |-
45		oveq1	Could not format ( yO = q -> ( yO x.s p ) = ( q x.s p ) ) : No typesetting found for |- ( yO = q -> ( yO x.s p ) = ( q x.s p ) ) with typecode |-
46	44 45	eqeq12d	Could not format ( yO = q -> ( ( p x.s yO ) = ( yO x.s p ) <-> ( p x.s q ) = ( q x.s p ) ) ) : No typesetting found for |- ( yO = q -> ( ( p x.s yO ) = ( yO x.s p ) <-> ( p x.s q ) = ( q x.s p ) ) ) with typecode |-
47		simplr1	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) ) with typecode |-
48	43 46 47 22 30	rspc2dv	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( p x.s q ) = ( q x.s p ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( p x.s q ) = ( q x.s p ) ) with typecode |-
49	40 48	oveq12d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) ) with typecode |-
50	49	eqeq2d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) ) ) with typecode |-
51	50	2rexbidva	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) ) ) with typecode |-
52		rexcom	$$⊢\exists p\in L\left(x\right)\exists q\in L\left(y\right)a=\left(\left(q{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}p\right)\right){-}_s\left(q{\cdot }_{s}p\right)\leftrightarrow \exists q\in L\left(y\right)\exists p\in L\left(x\right)a=\left(\left(q{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}p\right)\right){-}_s\left(q{\cdot }_{s}p\right)$$
53	51 52	bitrdi	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> E. q e. ( _Left ` y ) E. p e. ( _Left ` x ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> E. q e. ( _Left ` y ) E. p e. ( _Left ` x ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) ) ) with typecode |-
54	53	abbidv	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) } = { a | E. q e. ( _Left ` y ) E. p e. ( _Left ` x ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) } = { a | E. q e. ( _Left ` y ) E. p e. ( _Left ` x ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) } ) with typecode |-
55		oveq1	Could not format ( xO = r -> ( xO x.s y ) = ( r x.s y ) ) : No typesetting found for |- ( xO = r -> ( xO x.s y ) = ( r x.s y ) ) with typecode |-
56		oveq2	Could not format ( xO = r -> ( y x.s xO ) = ( y x.s r ) ) : No typesetting found for |- ( xO = r -> ( y x.s xO ) = ( y x.s r ) ) with typecode |-
57	55 56	eqeq12d	Could not format ( xO = r -> ( ( xO x.s y ) = ( y x.s xO ) <-> ( r x.s y ) = ( y x.s r ) ) ) : No typesetting found for |- ( xO = r -> ( ( xO x.s y ) = ( y x.s xO ) <-> ( r x.s y ) = ( y x.s r ) ) ) with typecode |-
58		simplr2	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) ) with typecode |-
59		simprl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> r e. ( _Right ` x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> r e. ( _Right ` x ) ) with typecode |-
60		elun2	$$⊢r\in R\left(x\right)\to r\in \left(L\left(x\right)\cup R\left(x\right)\right)$$
61	59 60	syl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> r e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> r e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
62	57 58 61	rspcdva	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( r x.s y ) = ( y x.s r ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( r x.s y ) = ( y x.s r ) ) with typecode |-
63		oveq2	Could not format ( yO = s -> ( x x.s yO ) = ( x x.s s ) ) : No typesetting found for |- ( yO = s -> ( x x.s yO ) = ( x x.s s ) ) with typecode |-
64		oveq1	Could not format ( yO = s -> ( yO x.s x ) = ( s x.s x ) ) : No typesetting found for |- ( yO = s -> ( yO x.s x ) = ( s x.s x ) ) with typecode |-
65	63 64	eqeq12d	Could not format ( yO = s -> ( ( x x.s yO ) = ( yO x.s x ) <-> ( x x.s s ) = ( s x.s x ) ) ) : No typesetting found for |- ( yO = s -> ( ( x x.s yO ) = ( yO x.s x ) <-> ( x x.s s ) = ( s x.s x ) ) ) with typecode |-
66		simplr3	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) with typecode |-
67		simprr	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> s e. ( _Right ` y ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> s e. ( _Right ` y ) ) with typecode |-
68		elun2	$$⊢s\in R\left(y\right)\to s\in \left(L\left(y\right)\cup R\left(y\right)\right)$$
69	67 68	syl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> s e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> s e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) with typecode |-
70	65 66 69	rspcdva	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( x x.s s ) = ( s x.s x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( x x.s s ) = ( s x.s x ) ) with typecode |-
71	62 70	oveq12d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( ( r x.s y ) +s ( x x.s s ) ) = ( ( y x.s r ) +s ( s x.s x ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( ( r x.s y ) +s ( x x.s s ) ) = ( ( y x.s r ) +s ( s x.s x ) ) ) with typecode |-
72		simpllr	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> y e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> y e. No ) with typecode |-
73	59	rightnod	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> r e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> r e. No ) with typecode |-
74	72 73	mulscld	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( y x.s r ) e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( y x.s r ) e. No ) with typecode |-
75	67	rightnod	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> s e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> s e. No ) with typecode |-
76		simplll	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> x e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> x e. No ) with typecode |-
77	75 76	mulscld	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( s x.s x ) e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( s x.s x ) e. No ) with typecode |-
78	74 77	addscomd	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( ( y x.s r ) +s ( s x.s x ) ) = ( ( s x.s x ) +s ( y x.s r ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( ( y x.s r ) +s ( s x.s x ) ) = ( ( s x.s x ) +s ( y x.s r ) ) ) with typecode |-
79	71 78	eqtrd	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( ( r x.s y ) +s ( x x.s s ) ) = ( ( s x.s x ) +s ( y x.s r ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( ( r x.s y ) +s ( x x.s s ) ) = ( ( s x.s x ) +s ( y x.s r ) ) ) with typecode |-
80		oveq1	Could not format ( xO = r -> ( xO x.s yO ) = ( r x.s yO ) ) : No typesetting found for |- ( xO = r -> ( xO x.s yO ) = ( r x.s yO ) ) with typecode |-
81		oveq2	Could not format ( xO = r -> ( yO x.s xO ) = ( yO x.s r ) ) : No typesetting found for |- ( xO = r -> ( yO x.s xO ) = ( yO x.s r ) ) with typecode |-
82	80 81	eqeq12d	Could not format ( xO = r -> ( ( xO x.s yO ) = ( yO x.s xO ) <-> ( r x.s yO ) = ( yO x.s r ) ) ) : No typesetting found for |- ( xO = r -> ( ( xO x.s yO ) = ( yO x.s xO ) <-> ( r x.s yO ) = ( yO x.s r ) ) ) with typecode |-
83		oveq2	Could not format ( yO = s -> ( r x.s yO ) = ( r x.s s ) ) : No typesetting found for |- ( yO = s -> ( r x.s yO ) = ( r x.s s ) ) with typecode |-
84		oveq1	Could not format ( yO = s -> ( yO x.s r ) = ( s x.s r ) ) : No typesetting found for |- ( yO = s -> ( yO x.s r ) = ( s x.s r ) ) with typecode |-
85	83 84	eqeq12d	Could not format ( yO = s -> ( ( r x.s yO ) = ( yO x.s r ) <-> ( r x.s s ) = ( s x.s r ) ) ) : No typesetting found for |- ( yO = s -> ( ( r x.s yO ) = ( yO x.s r ) <-> ( r x.s s ) = ( s x.s r ) ) ) with typecode |-
86		simplr1	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) ) with typecode |-
87	82 85 86 61 69	rspc2dv	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( r x.s s ) = ( s x.s r ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( r x.s s ) = ( s x.s r ) ) with typecode |-
88	79 87	oveq12d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) ) with typecode |-
89	88	eqeq2d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) <-> b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) <-> b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) ) ) with typecode |-
90	89	2rexbidva	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) <-> E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) <-> E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) ) ) with typecode |-
91		rexcom	$$⊢\exists r\in R\left(x\right)\exists s\in R\left(y\right)b=\left(\left(s{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}r\right)\right){-}_s\left(s{\cdot }_{s}r\right)\leftrightarrow \exists s\in R\left(y\right)\exists r\in R\left(x\right)b=\left(\left(s{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}r\right)\right){-}_s\left(s{\cdot }_{s}r\right)$$
92	90 91	bitrdi	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) <-> E. s e. ( _Right ` y ) E. r e. ( _Right ` x ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) <-> E. s e. ( _Right ` y ) E. r e. ( _Right ` x ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) ) ) with typecode |-
93	92	abbidv	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) } = { b | E. s e. ( _Right ` y ) E. r e. ( _Right ` x ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) } = { b | E. s e. ( _Right ` y ) E. r e. ( _Right ` x ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) } ) with typecode |-
94	54 93	uneq12d	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) = ( { a | E. q e. ( _Left ` y ) E. p e. ( _Left ` x ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) } u. { b | E. s e. ( _Right ` y ) E. r e. ( _Right ` x ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) } ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) = ( { a | E. q e. ( _Left ` y ) E. p e. ( _Left ` x ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) } u. { b | E. s e. ( _Right ` y ) E. r e. ( _Right ` x ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) } ) ) with typecode |-
95		oveq1	Could not format ( xO = t -> ( xO x.s y ) = ( t x.s y ) ) : No typesetting found for |- ( xO = t -> ( xO x.s y ) = ( t x.s y ) ) with typecode |-
96		oveq2	Could not format ( xO = t -> ( y x.s xO ) = ( y x.s t ) ) : No typesetting found for |- ( xO = t -> ( y x.s xO ) = ( y x.s t ) ) with typecode |-
97	95 96	eqeq12d	Could not format ( xO = t -> ( ( xO x.s y ) = ( y x.s xO ) <-> ( t x.s y ) = ( y x.s t ) ) ) : No typesetting found for |- ( xO = t -> ( ( xO x.s y ) = ( y x.s xO ) <-> ( t x.s y ) = ( y x.s t ) ) ) with typecode |-
98		simplr2	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) ) with typecode |-
99		simprl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> t e. ( _Left ` x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> t e. ( _Left ` x ) ) with typecode |-
100		elun1	$$⊢t\in L\left(x\right)\to t\in \left(L\left(x\right)\cup R\left(x\right)\right)$$
101	99 100	syl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> t e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> t e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
102	97 98 101	rspcdva	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( t x.s y ) = ( y x.s t ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( t x.s y ) = ( y x.s t ) ) with typecode |-
103		oveq2	Could not format ( yO = u -> ( x x.s yO ) = ( x x.s u ) ) : No typesetting found for |- ( yO = u -> ( x x.s yO ) = ( x x.s u ) ) with typecode |-
104		oveq1	Could not format ( yO = u -> ( yO x.s x ) = ( u x.s x ) ) : No typesetting found for |- ( yO = u -> ( yO x.s x ) = ( u x.s x ) ) with typecode |-
105	103 104	eqeq12d	Could not format ( yO = u -> ( ( x x.s yO ) = ( yO x.s x ) <-> ( x x.s u ) = ( u x.s x ) ) ) : No typesetting found for |- ( yO = u -> ( ( x x.s yO ) = ( yO x.s x ) <-> ( x x.s u ) = ( u x.s x ) ) ) with typecode |-
106		simplr3	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) with typecode |-
107		simprr	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> u e. ( _Right ` y ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> u e. ( _Right ` y ) ) with typecode |-
108		elun2	$$⊢u\in R\left(y\right)\to u\in \left(L\left(y\right)\cup R\left(y\right)\right)$$
109	107 108	syl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> u e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> u e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) with typecode |-
110	105 106 109	rspcdva	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( x x.s u ) = ( u x.s x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( x x.s u ) = ( u x.s x ) ) with typecode |-
111	102 110	oveq12d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( ( t x.s y ) +s ( x x.s u ) ) = ( ( y x.s t ) +s ( u x.s x ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( ( t x.s y ) +s ( x x.s u ) ) = ( ( y x.s t ) +s ( u x.s x ) ) ) with typecode |-
112		simpllr	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> y e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> y e. No ) with typecode |-
113	99	leftnod	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> t e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> t e. No ) with typecode |-
114	112 113	mulscld	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( y x.s t ) e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( y x.s t ) e. No ) with typecode |-
115	107	rightnod	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> u e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> u e. No ) with typecode |-
116		simplll	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> x e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> x e. No ) with typecode |-
117	115 116	mulscld	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( u x.s x ) e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( u x.s x ) e. No ) with typecode |-
118	114 117	addscomd	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( ( y x.s t ) +s ( u x.s x ) ) = ( ( u x.s x ) +s ( y x.s t ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( ( y x.s t ) +s ( u x.s x ) ) = ( ( u x.s x ) +s ( y x.s t ) ) ) with typecode |-
119	111 118	eqtrd	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( ( t x.s y ) +s ( x x.s u ) ) = ( ( u x.s x ) +s ( y x.s t ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( ( t x.s y ) +s ( x x.s u ) ) = ( ( u x.s x ) +s ( y x.s t ) ) ) with typecode |-
120		oveq1	Could not format ( xO = t -> ( xO x.s yO ) = ( t x.s yO ) ) : No typesetting found for |- ( xO = t -> ( xO x.s yO ) = ( t x.s yO ) ) with typecode |-
121		oveq2	Could not format ( xO = t -> ( yO x.s xO ) = ( yO x.s t ) ) : No typesetting found for |- ( xO = t -> ( yO x.s xO ) = ( yO x.s t ) ) with typecode |-
122	120 121	eqeq12d	Could not format ( xO = t -> ( ( xO x.s yO ) = ( yO x.s xO ) <-> ( t x.s yO ) = ( yO x.s t ) ) ) : No typesetting found for |- ( xO = t -> ( ( xO x.s yO ) = ( yO x.s xO ) <-> ( t x.s yO ) = ( yO x.s t ) ) ) with typecode |-
123		oveq2	Could not format ( yO = u -> ( t x.s yO ) = ( t x.s u ) ) : No typesetting found for |- ( yO = u -> ( t x.s yO ) = ( t x.s u ) ) with typecode |-
124		oveq1	Could not format ( yO = u -> ( yO x.s t ) = ( u x.s t ) ) : No typesetting found for |- ( yO = u -> ( yO x.s t ) = ( u x.s t ) ) with typecode |-
125	123 124	eqeq12d	Could not format ( yO = u -> ( ( t x.s yO ) = ( yO x.s t ) <-> ( t x.s u ) = ( u x.s t ) ) ) : No typesetting found for |- ( yO = u -> ( ( t x.s yO ) = ( yO x.s t ) <-> ( t x.s u ) = ( u x.s t ) ) ) with typecode |-
126		simplr1	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) ) with typecode |-
127	122 125 126 101 109	rspc2dv	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( t x.s u ) = ( u x.s t ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( t x.s u ) = ( u x.s t ) ) with typecode |-
128	119 127	oveq12d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) ) with typecode |-
129	128	eqeq2d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) <-> c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) <-> c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) ) ) with typecode |-
130	129	2rexbidva	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) <-> E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) <-> E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) ) ) with typecode |-
131		rexcom	$$⊢\exists t\in L\left(x\right)\exists u\in R\left(y\right)c=\left(\left(u{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}t\right)\right){-}_s\left(u{\cdot }_{s}t\right)\leftrightarrow \exists u\in R\left(y\right)\exists t\in L\left(x\right)c=\left(\left(u{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}t\right)\right){-}_s\left(u{\cdot }_{s}t\right)$$
132	130 131	bitrdi	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) <-> E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) <-> E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) ) ) with typecode |-
133	132	abbidv	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) } = { c | E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) } = { c | E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) } ) with typecode |-
134		oveq1	Could not format ( xO = v -> ( xO x.s y ) = ( v x.s y ) ) : No typesetting found for |- ( xO = v -> ( xO x.s y ) = ( v x.s y ) ) with typecode |-
135		oveq2	Could not format ( xO = v -> ( y x.s xO ) = ( y x.s v ) ) : No typesetting found for |- ( xO = v -> ( y x.s xO ) = ( y x.s v ) ) with typecode |-
136	134 135	eqeq12d	Could not format ( xO = v -> ( ( xO x.s y ) = ( y x.s xO ) <-> ( v x.s y ) = ( y x.s v ) ) ) : No typesetting found for |- ( xO = v -> ( ( xO x.s y ) = ( y x.s xO ) <-> ( v x.s y ) = ( y x.s v ) ) ) with typecode |-
137		simplr2	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) ) with typecode |-
138		simprl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> v e. ( _Right ` x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> v e. ( _Right ` x ) ) with typecode |-
139		elun2	$$⊢v\in R\left(x\right)\to v\in \left(L\left(x\right)\cup R\left(x\right)\right)$$
140	138 139	syl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> v e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> v e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
141	136 137 140	rspcdva	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( v x.s y ) = ( y x.s v ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( v x.s y ) = ( y x.s v ) ) with typecode |-
142		oveq2	Could not format ( yO = w -> ( x x.s yO ) = ( x x.s w ) ) : No typesetting found for |- ( yO = w -> ( x x.s yO ) = ( x x.s w ) ) with typecode |-
143		oveq1	Could not format ( yO = w -> ( yO x.s x ) = ( w x.s x ) ) : No typesetting found for |- ( yO = w -> ( yO x.s x ) = ( w x.s x ) ) with typecode |-
144	142 143	eqeq12d	Could not format ( yO = w -> ( ( x x.s yO ) = ( yO x.s x ) <-> ( x x.s w ) = ( w x.s x ) ) ) : No typesetting found for |- ( yO = w -> ( ( x x.s yO ) = ( yO x.s x ) <-> ( x x.s w ) = ( w x.s x ) ) ) with typecode |-
145		simplr3	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) with typecode |-
146		simprr	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> w e. ( _Left ` y ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> w e. ( _Left ` y ) ) with typecode |-
147		elun1	$$⊢w\in L\left(y\right)\to w\in \left(L\left(y\right)\cup R\left(y\right)\right)$$
148	146 147	syl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> w e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> w e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) with typecode |-
149	144 145 148	rspcdva	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( x x.s w ) = ( w x.s x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( x x.s w ) = ( w x.s x ) ) with typecode |-
150	141 149	oveq12d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( ( v x.s y ) +s ( x x.s w ) ) = ( ( y x.s v ) +s ( w x.s x ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( ( v x.s y ) +s ( x x.s w ) ) = ( ( y x.s v ) +s ( w x.s x ) ) ) with typecode |-
151		simpllr	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> y e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> y e. No ) with typecode |-
152	138	rightnod	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> v e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> v e. No ) with typecode |-
153	151 152	mulscld	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( y x.s v ) e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( y x.s v ) e. No ) with typecode |-
154	146	leftnod	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> w e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> w e. No ) with typecode |-
155		simplll	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> x e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> x e. No ) with typecode |-
156	154 155	mulscld	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( w x.s x ) e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( w x.s x ) e. No ) with typecode |-
157	153 156	addscomd	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( ( y x.s v ) +s ( w x.s x ) ) = ( ( w x.s x ) +s ( y x.s v ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( ( y x.s v ) +s ( w x.s x ) ) = ( ( w x.s x ) +s ( y x.s v ) ) ) with typecode |-
158	150 157	eqtrd	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( ( v x.s y ) +s ( x x.s w ) ) = ( ( w x.s x ) +s ( y x.s v ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( ( v x.s y ) +s ( x x.s w ) ) = ( ( w x.s x ) +s ( y x.s v ) ) ) with typecode |-
159		oveq1	Could not format ( xO = v -> ( xO x.s yO ) = ( v x.s yO ) ) : No typesetting found for |- ( xO = v -> ( xO x.s yO ) = ( v x.s yO ) ) with typecode |-
160		oveq2	Could not format ( xO = v -> ( yO x.s xO ) = ( yO x.s v ) ) : No typesetting found for |- ( xO = v -> ( yO x.s xO ) = ( yO x.s v ) ) with typecode |-
161	159 160	eqeq12d	Could not format ( xO = v -> ( ( xO x.s yO ) = ( yO x.s xO ) <-> ( v x.s yO ) = ( yO x.s v ) ) ) : No typesetting found for |- ( xO = v -> ( ( xO x.s yO ) = ( yO x.s xO ) <-> ( v x.s yO ) = ( yO x.s v ) ) ) with typecode |-
162		oveq2	Could not format ( yO = w -> ( v x.s yO ) = ( v x.s w ) ) : No typesetting found for |- ( yO = w -> ( v x.s yO ) = ( v x.s w ) ) with typecode |-
163		oveq1	Could not format ( yO = w -> ( yO x.s v ) = ( w x.s v ) ) : No typesetting found for |- ( yO = w -> ( yO x.s v ) = ( w x.s v ) ) with typecode |-
164	162 163	eqeq12d	Could not format ( yO = w -> ( ( v x.s yO ) = ( yO x.s v ) <-> ( v x.s w ) = ( w x.s v ) ) ) : No typesetting found for |- ( yO = w -> ( ( v x.s yO ) = ( yO x.s v ) <-> ( v x.s w ) = ( w x.s v ) ) ) with typecode |-
165		simplr1	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) ) with typecode |-
166	161 164 165 140 148	rspc2dv	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( v x.s w ) = ( w x.s v ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( v x.s w ) = ( w x.s v ) ) with typecode |-
167	158 166	oveq12d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) ) with typecode |-
168	167	eqeq2d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) ) ) with typecode |-
169	168	2rexbidva	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) ) ) with typecode |-
170		rexcom	$$⊢\exists v\in R\left(x\right)\exists w\in L\left(y\right)d=\left(\left(w{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}v\right)\right){-}_s\left(w{\cdot }_{s}v\right)\leftrightarrow \exists w\in L\left(y\right)\exists v\in R\left(x\right)d=\left(\left(w{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}v\right)\right){-}_s\left(w{\cdot }_{s}v\right)$$
171	169 170	bitrdi	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) ) ) with typecode |-
172	171	abbidv	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) } = { d | E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) } = { d | E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) } ) with typecode |-
173	133 172	uneq12d	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) = ( { c | E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) } u. { d | E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) } ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) = ( { c | E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) } u. { d | E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) } ) ) with typecode |-
174		uncom	$$⊢\left\{c|\exists u\in R\left(y\right)\exists t\in L\left(x\right)c=\left(\left(u{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}t\right)\right){-}_s\left(u{\cdot }_{s}t\right)\right\}\cup \left\{d|\exists w\in L\left(y\right)\exists v\in R\left(x\right)d=\left(\left(w{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}v\right)\right){-}_s\left(w{\cdot }_{s}v\right)\right\}=\left\{d|\exists w\in L\left(y\right)\exists v\in R\left(x\right)d=\left(\left(w{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}v\right)\right){-}_s\left(w{\cdot }_{s}v\right)\right\}\cup \left\{c|\exists u\in R\left(y\right)\exists t\in L\left(x\right)c=\left(\left(u{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}t\right)\right){-}_s\left(u{\cdot }_{s}t\right)\right\}$$
175	173 174	eqtrdi	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) = ( { d | E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) } u. { c | E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) } ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) = ( { d | E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) } u. { c | E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) } ) ) with typecode |-
176	94 175	oveq12d	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) = ( ( { a | E. q e. ( _Left ` y ) E. p e. ( _Left ` x ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) } u. { b | E. s e. ( _Right ` y ) E. r e. ( _Right ` x ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) } ) |s ( { d | E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) } u. { c | E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) } ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) = ( ( { a | E. q e. ( _Left ` y ) E. p e. ( _Left ` x ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) } u. { b | E. s e. ( _Right ` y ) E. r e. ( _Right ` x ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) } ) |s ( { d | E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) } u. { c | E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) } ) ) ) with typecode |-
177		mulsval	$$⊢\left(x\in \mathrm{No}\wedge y\in \mathrm{No}\right)\to x{\cdot }_{s}y=\left(\left\{a|\exists p\in L\left(x\right)\exists q\in L\left(y\right)a=\left(\left(p{\cdot }_{s}y\right){+}_s\left(x{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)\right\}\cup \left\{b|\exists r\in R\left(x\right)\exists s\in R\left(y\right)b=\left(\left(r{\cdot }_{s}y\right){+}_s\left(x{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)\right\}\right){|}_s\left(\left\{c|\exists t\in L\left(x\right)\exists u\in R\left(y\right)c=\left(\left(t{\cdot }_{s}y\right){+}_s\left(x{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)\right\}\cup \left\{d|\exists v\in R\left(x\right)\exists w\in L\left(y\right)d=\left(\left(v{\cdot }_{s}y\right){+}_s\left(x{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)\right\}\right)$$
178	177	adantr	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( x x.s y ) = ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( x x.s y ) = ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) ) with typecode |-
179		mulsval	$$⊢\left(y\in \mathrm{No}\wedge x\in \mathrm{No}\right)\to y{\cdot }_{s}x=\left(\left\{a|\exists q\in L\left(y\right)\exists p\in L\left(x\right)a=\left(\left(q{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}p\right)\right){-}_s\left(q{\cdot }_{s}p\right)\right\}\cup \left\{b|\exists s\in R\left(y\right)\exists r\in R\left(x\right)b=\left(\left(s{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}r\right)\right){-}_s\left(s{\cdot }_{s}r\right)\right\}\right){|}_s\left(\left\{d|\exists w\in L\left(y\right)\exists v\in R\left(x\right)d=\left(\left(w{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}v\right)\right){-}_s\left(w{\cdot }_{s}v\right)\right\}\cup \left\{c|\exists u\in R\left(y\right)\exists t\in L\left(x\right)c=\left(\left(u{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}t\right)\right){-}_s\left(u{\cdot }_{s}t\right)\right\}\right)$$
180	179	ancoms	$$⊢\left(x\in \mathrm{No}\wedge y\in \mathrm{No}\right)\to y{\cdot }_{s}x=\left(\left\{a|\exists q\in L\left(y\right)\exists p\in L\left(x\right)a=\left(\left(q{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}p\right)\right){-}_s\left(q{\cdot }_{s}p\right)\right\}\cup \left\{b|\exists s\in R\left(y\right)\exists r\in R\left(x\right)b=\left(\left(s{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}r\right)\right){-}_s\left(s{\cdot }_{s}r\right)\right\}\right){|}_s\left(\left\{d|\exists w\in L\left(y\right)\exists v\in R\left(x\right)d=\left(\left(w{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}v\right)\right){-}_s\left(w{\cdot }_{s}v\right)\right\}\cup \left\{c|\exists u\in R\left(y\right)\exists t\in L\left(x\right)c=\left(\left(u{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}t\right)\right){-}_s\left(u{\cdot }_{s}t\right)\right\}\right)$$
181	180	adantr	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( y x.s x ) = ( ( { a | E. q e. ( _Left ` y ) E. p e. ( _Left ` x ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) } u. { b | E. s e. ( _Right ` y ) E. r e. ( _Right ` x ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) } ) |s ( { d | E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) } u. { c | E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) } ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( y x.s x ) = ( ( { a | E. q e. ( _Left ` y ) E. p e. ( _Left ` x ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) } u. { b | E. s e. ( _Right ` y ) E. r e. ( _Right ` x ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) } ) |s ( { d | E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) } u. { c | E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) } ) ) ) with typecode |-
182	176 178 181	3eqtr4d	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( x x.s y ) = ( y x.s x ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( x x.s y ) = ( y x.s x ) ) with typecode |-
183	182	ex	Could not format ( ( x e. No /\ y e. No ) -> ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) -> ( x x.s y ) = ( y x.s x ) ) ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) -> ( x x.s y ) = ( y x.s x ) ) ) with typecode |-
184	3 6 9 12 15 183	no2inds	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A{\cdot }_{s}B=B{\cdot }_{s}A$$