Metamath Proof Explorer

Theorem mulsass

Description: Associative law for surreal multiplication. Part of theorem 7 of Conway p. 19. Much like the case for additive groups, this theorem together with mulscom , addsdi , mulsgt0 , and the addition theorems would make the surreals into an ordered ring except that they are a proper class. (Contributed by Scott Fenton, 10-Mar-2025)

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

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( x = xO -> ( x x.s y ) = ( xO x.s y ) )
2 1 oveq1d 
 |-  ( x = xO -> ( ( x x.s y ) x.s z ) = ( ( xO x.s y ) x.s z ) )
3 oveq1 
 |-  ( x = xO -> ( x x.s ( y x.s z ) ) = ( xO x.s ( y x.s z ) ) )
4 2 3 eqeq12d 
 |-  ( x = xO -> ( ( ( x x.s y ) x.s z ) = ( x x.s ( y x.s z ) ) <-> ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) ) )
5 oveq2 
 |-  ( y = yO -> ( xO x.s y ) = ( xO x.s yO ) )
6 5 oveq1d 
 |-  ( y = yO -> ( ( xO x.s y ) x.s z ) = ( ( xO x.s yO ) x.s z ) )
7 oveq1 
 |-  ( y = yO -> ( y x.s z ) = ( yO x.s z ) )
8 7 oveq2d 
 |-  ( y = yO -> ( xO x.s ( y x.s z ) ) = ( xO x.s ( yO x.s z ) ) )
9 6 8 eqeq12d 
 |-  ( y = yO -> ( ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) <-> ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) ) )
10 oveq2 
 |-  ( z = zO -> ( ( xO x.s yO ) x.s z ) = ( ( xO x.s yO ) x.s zO ) )
11 oveq2 
 |-  ( z = zO -> ( yO x.s z ) = ( yO x.s zO ) )
12 11 oveq2d 
 |-  ( z = zO -> ( xO x.s ( yO x.s z ) ) = ( xO x.s ( yO x.s zO ) ) )
13 10 12 eqeq12d 
 |-  ( z = zO -> ( ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) <-> ( ( xO x.s yO ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) ) )
14 oveq1 
 |-  ( x = xO -> ( x x.s yO ) = ( xO x.s yO ) )
15 14 oveq1d 
 |-  ( x = xO -> ( ( x x.s yO ) x.s zO ) = ( ( xO x.s yO ) x.s zO ) )
16 oveq1 
 |-  ( x = xO -> ( x x.s ( yO x.s zO ) ) = ( xO x.s ( yO x.s zO ) ) )
17 15 16 eqeq12d 
 |-  ( x = xO -> ( ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) <-> ( ( xO x.s yO ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) ) )
18 oveq2 
 |-  ( y = yO -> ( x x.s y ) = ( x x.s yO ) )
19 18 oveq1d 
 |-  ( y = yO -> ( ( x x.s y ) x.s zO ) = ( ( x x.s yO ) x.s zO ) )
20 oveq1 
 |-  ( y = yO -> ( y x.s zO ) = ( yO x.s zO ) )
21 20 oveq2d 
 |-  ( y = yO -> ( x x.s ( y x.s zO ) ) = ( x x.s ( yO x.s zO ) ) )
22 19 21 eqeq12d 
 |-  ( y = yO -> ( ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) <-> ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) ) )
23 5 oveq1d 
 |-  ( y = yO -> ( ( xO x.s y ) x.s zO ) = ( ( xO x.s yO ) x.s zO ) )
24 20 oveq2d 
 |-  ( y = yO -> ( xO x.s ( y x.s zO ) ) = ( xO x.s ( yO x.s zO ) ) )
25 23 24 eqeq12d 
 |-  ( y = yO -> ( ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) <-> ( ( xO x.s yO ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) ) )
26 oveq2 
 |-  ( z = zO -> ( ( x x.s yO ) x.s z ) = ( ( x x.s yO ) x.s zO ) )
27 11 oveq2d 
 |-  ( z = zO -> ( x x.s ( yO x.s z ) ) = ( x x.s ( yO x.s zO ) ) )
28 26 27 eqeq12d 
 |-  ( z = zO -> ( ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) <-> ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) ) )
29 oveq1 
 |-  ( x = A -> ( x x.s y ) = ( A x.s y ) )
30 29 oveq1d 
 |-  ( x = A -> ( ( x x.s y ) x.s z ) = ( ( A x.s y ) x.s z ) )
31 oveq1 
 |-  ( x = A -> ( x x.s ( y x.s z ) ) = ( A x.s ( y x.s z ) ) )
32 30 31 eqeq12d 
 |-  ( x = A -> ( ( ( x x.s y ) x.s z ) = ( x x.s ( y x.s z ) ) <-> ( ( A x.s y ) x.s z ) = ( A x.s ( y x.s z ) ) ) )
33 oveq2 
 |-  ( y = B -> ( A x.s y ) = ( A x.s B ) )
34 33 oveq1d 
 |-  ( y = B -> ( ( A x.s y ) x.s z ) = ( ( A x.s B ) x.s z ) )
35 oveq1 
 |-  ( y = B -> ( y x.s z ) = ( B x.s z ) )
36 35 oveq2d 
 |-  ( y = B -> ( A x.s ( y x.s z ) ) = ( A x.s ( B x.s z ) ) )
37 34 36 eqeq12d 
 |-  ( y = B -> ( ( ( A x.s y ) x.s z ) = ( A x.s ( y x.s z ) ) <-> ( ( A x.s B ) x.s z ) = ( A x.s ( B x.s z ) ) ) )
38 oveq2 
 |-  ( z = C -> ( ( A x.s B ) x.s z ) = ( ( A x.s B ) x.s C ) )
39 oveq2 
 |-  ( z = C -> ( B x.s z ) = ( B x.s C ) )
40 39 oveq2d 
 |-  ( z = C -> ( A x.s ( B x.s z ) ) = ( A x.s ( B x.s C ) ) )
41 38 40 eqeq12d 
 |-  ( z = C -> ( ( ( A x.s B ) x.s z ) = ( A x.s ( B x.s z ) ) <-> ( ( A x.s B ) x.s C ) = ( A x.s ( B x.s C ) ) ) )
42 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> x e. No )
43 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> y e. No )
44 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> z e. No )
45 ssun1 
 |-  ( _Left ` x ) C_ ( ( _Left ` x ) u. ( _Right ` x ) )
46 ssun1 
 |-  ( _Left ` y ) C_ ( ( _Left ` y ) u. ( _Right ` y ) )
47 ssun1 
 |-  ( _Left ` z ) C_ ( ( _Left ` z ) u. ( _Right ` z ) )
48 simpr11 
 |-  ( ( ( 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) )
49 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) )
50 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) )
51 simpr22 
 |-  ( ( ( 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) )
52 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) )
53 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) )
54 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) )
55 42 43 44 45 46 47 48 49 50 51 52 53 54 mulsasslem3 
 |-  ( ( ( 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zL ) ) <-> E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) ) )
56 55 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zL ) ) } = { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } )
57 ssun2 
 |-  ( _Right ` x ) C_ ( ( _Left ` x ) u. ( _Right ` x ) )
58 ssun2 
 |-  ( _Right ` y ) C_ ( ( _Left ` y ) u. ( _Right ` y ) )
59 42 43 44 57 58 47 48 49 50 51 52 53 54 mulsasslem3 
 |-  ( ( ( 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zL ) ) <-> E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) ) )
60 59 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zL ) ) } = { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } )
61 56 60 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zL ) ) } ) = ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) )
62 ssun2 
 |-  ( _Right ` z ) C_ ( ( _Left ` z ) u. ( _Right ` z ) )
63 42 43 44 45 58 62 48 49 50 51 52 53 54 mulsasslem3 
 |-  ( ( ( 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zR ) ) <-> E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) ) )
64 63 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zR ) ) } = { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } )
65 42 43 44 57 46 62 48 49 50 51 52 53 54 mulsasslem3 
 |-  ( ( ( 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zR ) ) <-> E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) ) )
66 65 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zR ) ) } = { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } )
67 64 66 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zR ) ) } ) = ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } ) )
68 61 67 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zL ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zR ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } ) ) )
69 un4 
 |-  ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } ) )
70 uncom 
 |-  ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } ) = ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } )
71 70 uneq2i 
 |-  ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) )
72 69 71 eqtri 
 |-  ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) )
73 68 72 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zL ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zR ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) ) )
74 42 43 44 45 46 62 48 49 50 51 52 53 54 mulsasslem3 
 |-  ( ( ( 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zR ) ) <-> E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) ) )
75 74 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zR ) ) } = { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } )
76 42 43 44 57 58 62 48 49 50 51 52 53 54 mulsasslem3 
 |-  ( ( ( 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zR ) ) <-> E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) ) )
77 76 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zR ) ) } = { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } )
78 75 77 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zR ) ) } ) = ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) )
79 42 43 44 45 58 47 48 49 50 51 52 53 54 mulsasslem3 
 |-  ( ( ( 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zL ) ) <-> E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) ) )
80 79 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zL ) ) } = { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } )
81 42 43 44 57 46 47 48 49 50 51 52 53 54 mulsasslem3 
 |-  ( ( ( 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zL ) ) <-> E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) ) )
82 81 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zL ) ) } = { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } )
83 80 82 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zL ) ) } ) = ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } ) )
84 78 83 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zR ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zL ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } ) ) )
85 un4 
 |-  ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } ) )
86 uncom 
 |-  ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } ) = ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } )
87 86 uneq2i 
 |-  ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) )
88 85 87 eqtri 
 |-  ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) )
89 84 88 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zR ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zL ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) ) )
90 73 89 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zL ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zR ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zR ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zL ) ) } ) ) ) = ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) ) ) )
91 42 43 44 mulsasslem1 
 |-  ( ( ( 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( ( x x.s y ) x.s z ) = ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zL ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zR ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zR ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zL ) ) } ) ) ) )
92 42 43 44 mulsasslem2 
 |-  ( ( ( 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( x x.s ( y x.s z ) ) = ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) ) ) )
93 90 91 92 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( ( x x.s y ) x.s z ) = ( x x.s ( y x.s z ) ) )
94 93 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) -> ( ( x x.s y ) x.s z ) = ( x x.s ( y x.s z ) ) ) )
95 4 9 13 17 22 25 28 32 37 41 94 no3inds 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A x.s B ) x.s C ) = ( A x.s ( B x.s C ) ) )