Metamath Proof Explorer

Theorem addsass

Description: Surreal addition is associative. Part of theorem 3 of Conway p. 17. (Contributed by Scott Fenton, 22-Jan-2025)

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

Proof

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