Metamath Proof Explorer

Theorem addsdi

Description: Distributive law for surreal numbers. Commuted form of part of theorem 7 of Conway p. 19. (Contributed by Scott Fenton, 9-Mar-2025)

Ref Expression
Assertion addsdi 
|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( A x.s ( B +s C ) ) = ( ( A x.s B ) +s ( A x.s C ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( x = xO -> ( x x.s ( y +s z ) ) = ( xO x.s ( y +s z ) ) )
2 oveq1 
 |-  ( x = xO -> ( x x.s y ) = ( xO x.s y ) )
3 oveq1 
 |-  ( x = xO -> ( x x.s z ) = ( xO x.s z ) )
4 2 3 oveq12d 
 |-  ( x = xO -> ( ( x x.s y ) +s ( x x.s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) )
5 1 4 eqeq12d 
 |-  ( x = xO -> ( ( x x.s ( y +s z ) ) = ( ( x x.s y ) +s ( x x.s z ) ) <-> ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) ) )
6 oveq1 
 |-  ( y = yO -> ( y +s z ) = ( yO +s z ) )
7 6 oveq2d 
 |-  ( y = yO -> ( xO x.s ( y +s z ) ) = ( xO x.s ( yO +s z ) ) )
8 oveq2 
 |-  ( y = yO -> ( xO x.s y ) = ( xO x.s yO ) )
9 8 oveq1d 
 |-  ( y = yO -> ( ( xO x.s y ) +s ( xO x.s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) )
10 7 9 eqeq12d 
 |-  ( y = yO -> ( ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) <-> ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) ) )
11 oveq2 
 |-  ( z = zO -> ( yO +s z ) = ( yO +s zO ) )
12 11 oveq2d 
 |-  ( z = zO -> ( xO x.s ( yO +s z ) ) = ( xO x.s ( yO +s zO ) ) )
13 oveq2 
 |-  ( z = zO -> ( xO x.s z ) = ( xO x.s zO ) )
14 13 oveq2d 
 |-  ( z = zO -> ( ( xO x.s yO ) +s ( xO x.s z ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) )
15 12 14 eqeq12d 
 |-  ( z = zO -> ( ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) <-> ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) ) )
16 oveq1 
 |-  ( x = xO -> ( x x.s ( yO +s zO ) ) = ( xO x.s ( yO +s zO ) ) )
17 oveq1 
 |-  ( x = xO -> ( x x.s yO ) = ( xO x.s yO ) )
18 oveq1 
 |-  ( x = xO -> ( x x.s zO ) = ( xO x.s zO ) )
19 17 18 oveq12d 
 |-  ( x = xO -> ( ( x x.s yO ) +s ( x x.s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) )
20 16 19 eqeq12d 
 |-  ( x = xO -> ( ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) <-> ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) ) )
21 oveq1 
 |-  ( y = yO -> ( y +s zO ) = ( yO +s zO ) )
22 21 oveq2d 
 |-  ( y = yO -> ( x x.s ( y +s zO ) ) = ( x x.s ( yO +s zO ) ) )
23 oveq2 
 |-  ( y = yO -> ( x x.s y ) = ( x x.s yO ) )
24 23 oveq1d 
 |-  ( y = yO -> ( ( x x.s y ) +s ( x x.s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) )
25 22 24 eqeq12d 
 |-  ( y = yO -> ( ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) <-> ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) ) )
26 21 oveq2d 
 |-  ( y = yO -> ( xO x.s ( y +s zO ) ) = ( xO x.s ( yO +s zO ) ) )
27 8 oveq1d 
 |-  ( y = yO -> ( ( xO x.s y ) +s ( xO x.s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) )
28 26 27 eqeq12d 
 |-  ( y = yO -> ( ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) <-> ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) ) )
29 11 oveq2d 
 |-  ( z = zO -> ( x x.s ( yO +s z ) ) = ( x x.s ( yO +s zO ) ) )
30 oveq2 
 |-  ( z = zO -> ( x x.s z ) = ( x x.s zO ) )
31 30 oveq2d 
 |-  ( z = zO -> ( ( x x.s yO ) +s ( x x.s z ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) )
32 29 31 eqeq12d 
 |-  ( z = zO -> ( ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) <-> ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) ) )
33 oveq1 
 |-  ( x = A -> ( x x.s ( y +s z ) ) = ( A x.s ( y +s z ) ) )
34 oveq1 
 |-  ( x = A -> ( x x.s y ) = ( A x.s y ) )
35 oveq1 
 |-  ( x = A -> ( x x.s z ) = ( A x.s z ) )
36 34 35 oveq12d 
 |-  ( x = A -> ( ( x x.s y ) +s ( x x.s z ) ) = ( ( A x.s y ) +s ( A x.s z ) ) )
37 33 36 eqeq12d 
 |-  ( x = A -> ( ( x x.s ( y +s z ) ) = ( ( x x.s y ) +s ( x x.s z ) ) <-> ( A x.s ( y +s z ) ) = ( ( A x.s y ) +s ( A x.s z ) ) ) )
38 oveq1 
 |-  ( y = B -> ( y +s z ) = ( B +s z ) )
39 38 oveq2d 
 |-  ( y = B -> ( A x.s ( y +s z ) ) = ( A x.s ( B +s z ) ) )
40 oveq2 
 |-  ( y = B -> ( A x.s y ) = ( A x.s B ) )
41 40 oveq1d 
 |-  ( y = B -> ( ( A x.s y ) +s ( A x.s z ) ) = ( ( A x.s B ) +s ( A x.s z ) ) )
42 39 41 eqeq12d 
 |-  ( y = B -> ( ( A x.s ( y +s z ) ) = ( ( A x.s y ) +s ( A x.s z ) ) <-> ( A x.s ( B +s z ) ) = ( ( A x.s B ) +s ( A x.s z ) ) ) )
43 oveq2 
 |-  ( z = C -> ( B +s z ) = ( B +s C ) )
44 43 oveq2d 
 |-  ( z = C -> ( A x.s ( B +s z ) ) = ( A x.s ( B +s C ) ) )
45 oveq2 
 |-  ( z = C -> ( A x.s z ) = ( A x.s C ) )
46 45 oveq2d 
 |-  ( z = C -> ( ( A x.s B ) +s ( A x.s z ) ) = ( ( A x.s B ) +s ( A x.s C ) ) )
47 44 46 eqeq12d 
 |-  ( z = C -> ( ( A x.s ( B +s z ) ) = ( ( A x.s B ) +s ( A x.s z ) ) <-> ( A x.s ( B +s C ) ) = ( ( A x.s B ) +s ( A x.s C ) ) ) )
48 simpl1 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> x e. No )
49 simpl2 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> y e. No )
50 simpl3 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> z e. No )
51 simpr21 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) )
52 simpr23 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) )
53 simpr12 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) )
54 elun1 
 |-  ( xL e. ( _Left ` x ) -> xL e. ( ( _Left ` x ) u. ( _Right ` x ) ) )
55 54 adantr 
 |-  ( ( xL e. ( _Left ` x ) /\ yL e. ( _Left ` y ) ) -> xL e. ( ( _Left ` x ) u. ( _Right ` x ) ) )
56 elun1 
 |-  ( yL e. ( _Left ` y ) -> yL e. ( ( _Left ` y ) u. ( _Right ` y ) ) )
57 56 adantl 
 |-  ( ( xL e. ( _Left ` x ) /\ yL e. ( _Left ` y ) ) -> yL e. ( ( _Left ` y ) u. ( _Right ` y ) ) )
58 48 49 50 51 52 53 55 57 addsdilem3 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ yL e. ( _Left ` y ) ) ) -> ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) )
59 58 eqeq2d 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ yL e. ( _Left ` y ) ) ) -> ( a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) <-> a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) ) )
60 59 2rexbidva 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) <-> E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) ) )
61 60 abbidv 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) } = { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } )
62 simpr3 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) )
63 simpr13 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) )
64 54 adantr 
 |-  ( ( xL e. ( _Left ` x ) /\ zL e. ( _Left ` z ) ) -> xL e. ( ( _Left ` x ) u. ( _Right ` x ) ) )
65 elun1 
 |-  ( zL e. ( _Left ` z ) -> zL e. ( ( _Left ` z ) u. ( _Right ` z ) ) )
66 65 adantl 
 |-  ( ( xL e. ( _Left ` x ) /\ zL e. ( _Left ` z ) ) -> zL e. ( ( _Left ` z ) u. ( _Right ` z ) ) )
67 48 49 50 51 62 63 64 66 addsdilem4 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ zL e. ( _Left ` z ) ) ) -> ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) )
68 67 eqeq2d 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ zL e. ( _Left ` z ) ) ) -> ( a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) <-> a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) ) )
69 68 2rexbidva 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) <-> E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) ) )
70 69 abbidv 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) } = { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } )
71 61 70 uneq12d 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) } ) = ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } ) )
72 elun2 
 |-  ( xR e. ( _Right ` x ) -> xR e. ( ( _Left ` x ) u. ( _Right ` x ) ) )
73 72 adantr 
 |-  ( ( xR e. ( _Right ` x ) /\ yR e. ( _Right ` y ) ) -> xR e. ( ( _Left ` x ) u. ( _Right ` x ) ) )
74 elun2 
 |-  ( yR e. ( _Right ` y ) -> yR e. ( ( _Left ` y ) u. ( _Right ` y ) ) )
75 74 adantl 
 |-  ( ( xR e. ( _Right ` x ) /\ yR e. ( _Right ` y ) ) -> yR e. ( ( _Left ` y ) u. ( _Right ` y ) ) )
76 48 49 50 51 52 53 73 75 addsdilem3 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ yR e. ( _Right ` y ) ) ) -> ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) )
77 76 eqeq2d 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ yR e. ( _Right ` y ) ) ) -> ( a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) <-> a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) ) )
78 77 2rexbidva 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) <-> E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) ) )
79 78 abbidv 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) } = { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } )
80 72 adantr 
 |-  ( ( xR e. ( _Right ` x ) /\ zR e. ( _Right ` z ) ) -> xR e. ( ( _Left ` x ) u. ( _Right ` x ) ) )
81 elun2 
 |-  ( zR e. ( _Right ` z ) -> zR e. ( ( _Left ` z ) u. ( _Right ` z ) ) )
82 81 adantl 
 |-  ( ( xR e. ( _Right ` x ) /\ zR e. ( _Right ` z ) ) -> zR e. ( ( _Left ` z ) u. ( _Right ` z ) ) )
83 48 49 50 51 62 63 80 82 addsdilem4 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ zR e. ( _Right ` z ) ) ) -> ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) )
84 83 eqeq2d 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ zR e. ( _Right ` z ) ) ) -> ( a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) <-> a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) ) )
85 84 2rexbidva 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) <-> E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) ) )
86 85 abbidv 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) } = { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } )
87 79 86 uneq12d 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) } ) = ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) )
88 71 87 uneq12d 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) )
89 un4 
 |-  ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) )
90 88 89 eqtrdi 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) )
91 54 adantr 
 |-  ( ( xL e. ( _Left ` x ) /\ yR e. ( _Right ` y ) ) -> xL e. ( ( _Left ` x ) u. ( _Right ` x ) ) )
92 74 adantl 
 |-  ( ( xL e. ( _Left ` x ) /\ yR e. ( _Right ` y ) ) -> yR e. ( ( _Left ` y ) u. ( _Right ` y ) ) )
93 48 49 50 51 52 53 91 92 addsdilem3 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ yR e. ( _Right ` y ) ) ) -> ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) )
94 93 eqeq2d 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ yR e. ( _Right ` y ) ) ) -> ( a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) <-> a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) ) )
95 94 2rexbidva 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) <-> E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) ) )
96 95 abbidv 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) } = { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } )
97 54 adantr 
 |-  ( ( xL e. ( _Left ` x ) /\ zR e. ( _Right ` z ) ) -> xL e. ( ( _Left ` x ) u. ( _Right ` x ) ) )
98 81 adantl 
 |-  ( ( xL e. ( _Left ` x ) /\ zR e. ( _Right ` z ) ) -> zR e. ( ( _Left ` z ) u. ( _Right ` z ) ) )
99 48 49 50 51 62 63 97 98 addsdilem4 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ zR e. ( _Right ` z ) ) ) -> ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) )
100 99 eqeq2d 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ zR e. ( _Right ` z ) ) ) -> ( a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) <-> a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) ) )
101 100 2rexbidva 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) <-> E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) ) )
102 101 abbidv 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) } = { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } )
103 96 102 uneq12d 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) } ) = ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } ) )
104 72 adantr 
 |-  ( ( xR e. ( _Right ` x ) /\ yL e. ( _Left ` y ) ) -> xR e. ( ( _Left ` x ) u. ( _Right ` x ) ) )
105 56 adantl 
 |-  ( ( xR e. ( _Right ` x ) /\ yL e. ( _Left ` y ) ) -> yL e. ( ( _Left ` y ) u. ( _Right ` y ) ) )
106 48 49 50 51 52 53 104 105 addsdilem3 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ yL e. ( _Left ` y ) ) ) -> ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) )
107 106 eqeq2d 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ yL e. ( _Left ` y ) ) ) -> ( a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) <-> a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) ) )
108 107 2rexbidva 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) <-> E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) ) )
109 108 abbidv 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) } = { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } )
110 72 adantr 
 |-  ( ( xR e. ( _Right ` x ) /\ zL e. ( _Left ` z ) ) -> xR e. ( ( _Left ` x ) u. ( _Right ` x ) ) )
111 65 adantl 
 |-  ( ( xR e. ( _Right ` x ) /\ zL e. ( _Left ` z ) ) -> zL e. ( ( _Left ` z ) u. ( _Right ` z ) ) )
112 48 49 50 51 62 63 110 111 addsdilem4 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ zL e. ( _Left ` z ) ) ) -> ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) )
113 112 eqeq2d 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ zL e. ( _Left ` z ) ) ) -> ( a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) <-> a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) ) )
114 113 2rexbidva 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) <-> E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) ) )
115 114 abbidv 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) } = { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } )
116 109 115 uneq12d 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) } ) = ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) )
117 103 116 uneq12d 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) )
118 un4 
 |-  ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) )
119 117 118 eqtrdi 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) )
120 90 119 oveq12d 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) } ) ) ) = ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) ) )
121 48 49 50 addsdilem1 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( x x.s ( y +s z ) ) = ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) } ) ) ) )
122 48 49 50 addsdilem2 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( ( x x.s y ) +s ( x x.s z ) ) = ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) ) )
123 120 121 122 3eqtr4d 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( x x.s ( y +s z ) ) = ( ( x x.s y ) +s ( x x.s z ) ) )
124 123 ex 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) -> ( x x.s ( y +s z ) ) = ( ( x x.s y ) +s ( x x.s z ) ) ) )
125 5 10 15 20 25 28 32 37 42 47 124 no3inds 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( A x.s ( B +s C ) ) = ( ( A x.s B ) +s ( A x.s C ) ) )