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