Metamath Proof Explorer


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 A No B No A s B = B 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 x s y = A s y
11 oveq2 x = A y s x = y s A
12 10 11 eqeq12d x = A x s y = y s x A s y = y s A
13 oveq2 y = B A s y = A s B
14 oveq1 y = B y s A = B s A
15 13 14 eqeq12d y = B A s y = y s A A s B = B s A
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 L x p L x R x
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 L y q L y R y
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 leftssno L x No
35 34 20 sselid 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 |-
36 33 35 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 |-
37 leftssno L y No
38 37 28 sselid 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 |-
39 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 |-
40 38 39 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 |-
41 36 40 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 |-
42 32 41 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 |-
43 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 |-
44 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 |-
45 43 44 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 |-
46 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 |-
47 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 |-
48 46 47 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 |-
49 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 |-
50 45 48 49 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 |-
51 42 50 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 |-
52 51 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 |-
53 52 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 |-
54 rexcom p L x q L y a = q s x + s y s p - s q s p q L y p L x a = q s x + s y s p - s q s p
55 53 54 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 |-
56 55 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 |-
57 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 |-
58 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 |-
59 57 58 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 |-
60 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 |-
61 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 |-
62 elun2 r R x r L x R x
63 61 62 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 |-
64 59 60 63 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 |-
65 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 |-
66 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 |-
67 65 66 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 |-
68 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 |-
69 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 |-
70 elun2 s R y s L y R y
71 69 70 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 |-
72 67 68 71 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 |-
73 64 72 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 |-
74 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 |-
75 rightssno R x No
76 75 61 sselid 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 |-
77 74 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 ) ) ) -> ( 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 |-
78 rightssno R y No
79 78 69 sselid 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 |-
80 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 |-
81 79 80 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 |-
82 77 81 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 |-
83 73 82 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 |-
84 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 |-
85 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 |-
86 84 85 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 |-
87 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 |-
88 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 |-
89 87 88 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 |-
90 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 |-
91 86 89 90 63 71 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 |-
92 83 91 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 |-
93 92 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 |-
94 93 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 |-
95 rexcom r R x s R y b = s s x + s y s r - s s s r s R y r R x b = s s x + s y s r - s s s r
96 94 95 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 |-
97 96 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 |-
98 56 97 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 |-
99 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 |-
100 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 |-
101 99 100 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 |-
102 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 |-
103 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 |-
104 elun1 t L x t L x R x
105 103 104 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 |-
106 101 102 105 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 |-
107 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 |-
108 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 |-
109 107 108 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 |-
110 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 |-
111 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 |-
112 elun2 u R y u L y R y
113 111 112 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 |-
114 109 110 113 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 |-
115 106 114 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 |-
116 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 |-
117 34 103 sselid 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 |-
118 116 117 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 |-
119 78 111 sselid 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 |-
120 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 |-
121 119 120 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 |-
122 118 121 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 |-
123 115 122 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 |-
124 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 |-
125 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 |-
126 124 125 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 |-
127 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 |-
128 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 |-
129 127 128 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 |-
130 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 |-
131 126 129 130 105 113 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 |-
132 123 131 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 |-
133 132 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 |-
134 133 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 |-
135 rexcom t L x u R y c = u s x + s y s t - s u s t u R y t L x c = u s x + s y s t - s u s t
136 134 135 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 |-
137 136 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 |-
138 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 |-
139 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 |-
140 138 139 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 |-
141 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 |-
142 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 |-
143 elun2 v R x v L x R x
144 142 143 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 |-
145 140 141 144 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 |-
146 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 |-
147 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 |-
148 146 147 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 |-
149 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 |-
150 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 |-
151 elun1 w L y w L y R y
152 150 151 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 |-
153 148 149 152 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 |-
154 145 153 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 |-
155 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 |-
156 75 142 sselid 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 |-
157 155 156 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 |-
158 37 150 sselid 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 |-
159 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 |-
160 158 159 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 |-
161 157 160 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 |-
162 154 161 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 |-
163 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 |-
164 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 |-
165 163 164 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 |-
166 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 |-
167 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 |-
168 166 167 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 |-
169 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 |-
170 165 168 169 144 152 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 |-
171 162 170 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 |-
172 171 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 |-
173 172 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 |-
174 rexcom v R x w L y d = w s x + s y s v - s w s v w L y v R x d = w s x + s y s v - s w s v
175 173 174 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 |-
176 175 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 |-
177 137 176 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 |-
178 uncom c | u R y t L x c = u s x + s y s t - s u s t d | w L y v R x d = w s x + s y s v - s w s v = d | w L y v R x d = w s x + s y s v - s w s v c | u R y t L x c = u s x + s y s t - s u s t
179 177 178 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 |-
180 98 179 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 |-
181 mulsval x No y No x s y = a | p L x q L y a = p s y + s x s q - s p s q b | r R x s R y b = r s y + s x s s - s r s s | s c | t L x u R y c = t s y + s x s u - s t s u d | v R x w L y d = v s y + s x s w - s v s w
182 181 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 |-
183 mulsval y No x No y s x = a | q L y p L x a = q s x + s y s p - s q s p b | s R y r R x b = s s x + s y s r - s s s r | s d | w L y v R x d = w s x + s y s v - s w s v c | u R y t L x c = u s x + s y s t - s u s t
184 183 ancoms x No y No y s x = a | q L y p L x a = q s x + s y s p - s q s p b | s R y r R x b = s s x + s y s r - s s s r | s d | w L y v R x d = w s x + s y s v - s w s v c | u R y t L x c = u s x + s y s t - s u s t
185 184 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 |-
186 180 182 185 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 |-
187 186 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 |-
188 3 6 9 12 15 187 no2inds A No B No A s B = B s A