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 e. No /\ B e. No ) -> ( A x.s B ) = ( B x.s A ) )

Proof

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