Metamath Proof Explorer

Theorem addsdilem2

Description: Lemma for surreal distribution. Expand the right hand side of the main expression. (Contributed by Scott Fenton, 8-Mar-2025)

Ref Expression
Hypotheses addsdilem.1 
|- ( ph -> A e. No )
addsdilem.2 
|- ( ph -> B e. No )
addsdilem.3 
|- ( ph -> C e. No )
Assertion addsdilem2 
|- ( ph -> ( ( A x.s B ) +s ( A x.s C ) ) = ( ( ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) +s ( A x.s C ) ) } u. { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) +s ( A x.s C ) ) } ) u. ( { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) +s ( A x.s C ) ) } u. { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) +s ( A x.s C ) ) } ) u. ( { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) ) )

Proof

Step Hyp Ref Expression
1 addsdilem.1 
 |-  ( ph -> A e. No )
2 addsdilem.2 
 |-  ( ph -> B e. No )
3 addsdilem.3 
 |-  ( ph -> C e. No )
4 1 2 mulscut2 
 |-  ( ph -> ( { b | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) } u. { b | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) } ) <
5 1 3 mulscut2 
 |-  ( ph -> ( { b | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) } u. { b | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) } ) <
6 mulsval2 
 |-  ( ( A e. No /\ B e. No ) -> ( A x.s B ) = ( ( { b | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) } u. { b | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) } ) |s ( { b | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) } u. { b | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) } ) ) )
7 1 2 6 syl2anc 
 |-  ( ph -> ( A x.s B ) = ( ( { b | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) } u. { b | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) } ) |s ( { b | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) } u. { b | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) } ) ) )
8 mulsval2 
 |-  ( ( A e. No /\ C e. No ) -> ( A x.s C ) = ( ( { b | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) } u. { b | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) } ) |s ( { b | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) } u. { b | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) } ) ) )
9 1 3 8 syl2anc 
 |-  ( ph -> ( A x.s C ) = ( ( { b | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) } u. { b | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) } ) |s ( { b | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) } u. { b | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) } ) ) )
10 4 5 7 9 addsunif 
 |-  ( ph -> ( ( A x.s B ) +s ( A x.s C ) ) = ( ( { a | E. t e. ( { b | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) } u. { b | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) } ) a = ( t +s ( A x.s C ) ) } u. { a | E. t e. ( { b | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) } u. { b | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) } ) a = ( ( A x.s B ) +s t ) } ) |s ( { a | E. t e. ( { b | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) } u. { b | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) } ) a = ( t +s ( A x.s C ) ) } u. { a | E. t e. ( { b | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) } u. { b | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) } ) a = ( ( A x.s B ) +s t ) } ) ) )
11 unab 
 |-  ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) +s ( A x.s C ) ) } u. { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) +s ( A x.s C ) ) } ) = { a | ( E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) +s ( A x.s C ) ) \/ E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) +s ( A x.s C ) ) ) }
12 rexun 
 |-  ( E. t e. ( { b | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) } u. { b | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) } ) a = ( t +s ( A x.s C ) ) <-> ( E. t e. { b | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) } a = ( t +s ( A x.s C ) ) \/ E. t e. { b | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) } a = ( t +s ( A x.s C ) ) ) )
13 eqeq1 
 |-  ( b = t -> ( b = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) <-> t = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) ) )
14 13 2rexbidv 
 |-  ( b = t -> ( E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) <-> E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) t = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) ) )
15 14 rexab 
 |-  ( E. t e. { b | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) } a = ( t +s ( A x.s C ) ) <-> E. t ( E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) t = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) )
16 rexcom4 
 |-  ( E. xL e. ( _Left ` A ) E. t E. yL e. ( _Left ` B ) ( t = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. t E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) ( t = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) )
17 rexcom4 
 |-  ( E. yL e. ( _Left ` B ) E. t ( t = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. t E. yL e. ( _Left ` B ) ( t = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) )
18 ovex 
 |-  ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) e. _V
19 oveq1 
 |-  ( t = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) -> ( t +s ( A x.s C ) ) = ( ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) +s ( A x.s C ) ) )
20 19 eqeq2d 
 |-  ( t = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) -> ( a = ( t +s ( A x.s C ) ) <-> a = ( ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) +s ( A x.s C ) ) ) )
21 18 20 ceqsexv 
 |-  ( E. t ( t = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> a = ( ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) +s ( A x.s C ) ) )
22 21 rexbii 
 |-  ( E. yL e. ( _Left ` B ) E. t ( t = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. yL e. ( _Left ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) +s ( A x.s C ) ) )
23 17 22 bitr3i 
 |-  ( E. t E. yL e. ( _Left ` B ) ( t = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. yL e. ( _Left ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) +s ( A x.s C ) ) )
24 23 rexbii 
 |-  ( E. xL e. ( _Left ` A ) E. t E. yL e. ( _Left ` B ) ( t = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) +s ( A x.s C ) ) )
25 r19.41vv 
 |-  ( E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) ( t = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> ( E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) t = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) )
26 25 exbii 
 |-  ( E. t E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) ( t = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. t ( E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) t = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) )
27 16 24 26 3bitr3ri 
 |-  ( E. t ( E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) t = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) +s ( A x.s C ) ) )
28 15 27 bitri 
 |-  ( E. t e. { b | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) } a = ( t +s ( A x.s C ) ) <-> E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) +s ( A x.s C ) ) )
29 eqeq1 
 |-  ( b = t -> ( b = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) <-> t = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) ) )
30 29 2rexbidv 
 |-  ( b = t -> ( E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) <-> E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) t = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) ) )
31 30 rexab 
 |-  ( E. t e. { b | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) } a = ( t +s ( A x.s C ) ) <-> E. t ( E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) t = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) )
32 rexcom4 
 |-  ( E. xR e. ( _Right ` A ) E. t E. yR e. ( _Right ` B ) ( t = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. t E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) ( t = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) )
33 rexcom4 
 |-  ( E. yR e. ( _Right ` B ) E. t ( t = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. t E. yR e. ( _Right ` B ) ( t = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) )
34 ovex 
 |-  ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) e. _V
35 oveq1 
 |-  ( t = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) -> ( t +s ( A x.s C ) ) = ( ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) +s ( A x.s C ) ) )
36 35 eqeq2d 
 |-  ( t = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) -> ( a = ( t +s ( A x.s C ) ) <-> a = ( ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) +s ( A x.s C ) ) ) )
37 34 36 ceqsexv 
 |-  ( E. t ( t = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> a = ( ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) +s ( A x.s C ) ) )
38 37 rexbii 
 |-  ( E. yR e. ( _Right ` B ) E. t ( t = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. yR e. ( _Right ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) +s ( A x.s C ) ) )
39 33 38 bitr3i 
 |-  ( E. t E. yR e. ( _Right ` B ) ( t = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. yR e. ( _Right ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) +s ( A x.s C ) ) )
40 39 rexbii 
 |-  ( E. xR e. ( _Right ` A ) E. t E. yR e. ( _Right ` B ) ( t = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) +s ( A x.s C ) ) )
41 r19.41vv 
 |-  ( E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) ( t = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> ( E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) t = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) )
42 41 exbii 
 |-  ( E. t E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) ( t = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. t ( E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) t = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) )
43 32 40 42 3bitr3ri 
 |-  ( E. t ( E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) t = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) +s ( A x.s C ) ) )
44 31 43 bitri 
 |-  ( E. t e. { b | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) } a = ( t +s ( A x.s C ) ) <-> E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) +s ( A x.s C ) ) )
45 28 44 orbi12i 
 |-  ( ( E. t e. { b | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) } a = ( t +s ( A x.s C ) ) \/ E. t e. { b | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) } a = ( t +s ( A x.s C ) ) ) <-> ( E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) +s ( A x.s C ) ) \/ E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) +s ( A x.s C ) ) ) )
46 12 45 bitr2i 
 |-  ( ( E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) +s ( A x.s C ) ) \/ E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) +s ( A x.s C ) ) ) <-> E. t e. ( { b | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) } u. { b | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) } ) a = ( t +s ( A x.s C ) ) )
47 46 abbii 
 |-  { a | ( E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) +s ( A x.s C ) ) \/ E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) +s ( A x.s C ) ) ) } = { a | E. t e. ( { b | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) } u. { b | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) } ) a = ( t +s ( A x.s C ) ) }
48 11 47 eqtri 
 |-  ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) +s ( A x.s C ) ) } u. { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) +s ( A x.s C ) ) } ) = { a | E. t e. ( { b | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) } u. { b | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) } ) a = ( t +s ( A x.s C ) ) }
49 unab 
 |-  ( { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) ) } ) = { a | ( E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) ) \/ E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) ) ) }
50 rexun 
 |-  ( E. t e. ( { b | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) } u. { b | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) } ) a = ( ( A x.s B ) +s t ) <-> ( E. t e. { b | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) } a = ( ( A x.s B ) +s t ) \/ E. t e. { b | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) } a = ( ( A x.s B ) +s t ) ) )
51 eqeq1 
 |-  ( b = t -> ( b = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) <-> t = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) ) )
52 51 2rexbidv 
 |-  ( b = t -> ( E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) <-> E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) t = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) ) )
53 52 rexab 
 |-  ( E. t e. { b | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) } a = ( ( A x.s B ) +s t ) <-> E. t ( E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) t = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) )
54 rexcom4 
 |-  ( E. xL e. ( _Left ` A ) E. t E. zL e. ( _Left ` C ) ( t = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. t E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) ( t = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) )
55 rexcom4 
 |-  ( E. zL e. ( _Left ` C ) E. t ( t = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. t E. zL e. ( _Left ` C ) ( t = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) )
56 ovex 
 |-  ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) e. _V
57 oveq2 
 |-  ( t = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) -> ( ( A x.s B ) +s t ) = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) ) )
58 57 eqeq2d 
 |-  ( t = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) -> ( a = ( ( A x.s B ) +s t ) <-> a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) ) ) )
59 56 58 ceqsexv 
 |-  ( E. t ( t = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) ) )
60 59 rexbii 
 |-  ( E. zL e. ( _Left ` C ) E. t ( t = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) ) )
61 55 60 bitr3i 
 |-  ( E. t E. zL e. ( _Left ` C ) ( t = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) ) )
62 61 rexbii 
 |-  ( E. xL e. ( _Left ` A ) E. t E. zL e. ( _Left ` C ) ( t = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) ) )
63 r19.41vv 
 |-  ( E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) ( t = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> ( E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) t = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) )
64 63 exbii 
 |-  ( E. t E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) ( t = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. t ( E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) t = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) )
65 54 62 64 3bitr3ri 
 |-  ( E. t ( E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) t = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) ) )
66 53 65 bitri 
 |-  ( E. t e. { b | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) } a = ( ( A x.s B ) +s t ) <-> E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) ) )
67 eqeq1 
 |-  ( b = t -> ( b = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) <-> t = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) ) )
68 67 2rexbidv 
 |-  ( b = t -> ( E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) <-> E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) t = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) ) )
69 68 rexab 
 |-  ( E. t e. { b | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) } a = ( ( A x.s B ) +s t ) <-> E. t ( E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) t = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) )
70 rexcom4 
 |-  ( E. xR e. ( _Right ` A ) E. t E. zR e. ( _Right ` C ) ( t = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. t E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) ( t = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) )
71 rexcom4 
 |-  ( E. zR e. ( _Right ` C ) E. t ( t = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. t E. zR e. ( _Right ` C ) ( t = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) )
72 ovex 
 |-  ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) e. _V
73 oveq2 
 |-  ( t = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) -> ( ( A x.s B ) +s t ) = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) ) )
74 73 eqeq2d 
 |-  ( t = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) -> ( a = ( ( A x.s B ) +s t ) <-> a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) ) ) )
75 72 74 ceqsexv 
 |-  ( E. t ( t = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) ) )
76 75 rexbii 
 |-  ( E. zR e. ( _Right ` C ) E. t ( t = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) ) )
77 71 76 bitr3i 
 |-  ( E. t E. zR e. ( _Right ` C ) ( t = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) ) )
78 77 rexbii 
 |-  ( E. xR e. ( _Right ` A ) E. t E. zR e. ( _Right ` C ) ( t = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) ) )
79 r19.41vv 
 |-  ( E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) ( t = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> ( E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) t = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) )
80 79 exbii 
 |-  ( E. t E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) ( t = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. t ( E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) t = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) )
81 70 78 80 3bitr3ri 
 |-  ( E. t ( E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) t = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) ) )
82 69 81 bitri 
 |-  ( E. t e. { b | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) } a = ( ( A x.s B ) +s t ) <-> E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) ) )
83 66 82 orbi12i 
 |-  ( ( E. t e. { b | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) } a = ( ( A x.s B ) +s t ) \/ E. t e. { b | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) } a = ( ( A x.s B ) +s t ) ) <-> ( E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) ) \/ E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) ) ) )
84 50 83 bitr2i 
 |-  ( ( E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) ) \/ E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) ) ) <-> E. t e. ( { b | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) } u. { b | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) } ) a = ( ( A x.s B ) +s t ) )
85 84 abbii 
 |-  { a | ( E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) ) \/ E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) ) ) } = { a | E. t e. ( { b | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) } u. { b | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) } ) a = ( ( A x.s B ) +s t ) }
86 49 85 eqtri 
 |-  ( { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) ) } ) = { a | E. t e. ( { b | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) } u. { b | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) } ) a = ( ( A x.s B ) +s t ) }
87 48 86 uneq12i 
 |-  ( ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) +s ( A x.s C ) ) } u. { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) +s ( A x.s C ) ) } ) u. ( { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) = ( { a | E. t e. ( { b | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) } u. { b | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) } ) a = ( t +s ( A x.s C ) ) } u. { a | E. t e. ( { b | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) } u. { b | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) } ) a = ( ( A x.s B ) +s t ) } )
88 unab 
 |-  ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) +s ( A x.s C ) ) } u. { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) +s ( A x.s C ) ) } ) = { a | ( E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) +s ( A x.s C ) ) \/ E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) +s ( A x.s C ) ) ) }
89 rexun 
 |-  ( E. t e. ( { b | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) } u. { b | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) } ) a = ( t +s ( A x.s C ) ) <-> ( E. t e. { b | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) } a = ( t +s ( A x.s C ) ) \/ E. t e. { b | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) } a = ( t +s ( A x.s C ) ) ) )
90 eqeq1 
 |-  ( b = t -> ( b = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) <-> t = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) ) )
91 90 2rexbidv 
 |-  ( b = t -> ( E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) <-> E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) t = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) ) )
92 91 rexab 
 |-  ( E. t e. { b | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) } a = ( t +s ( A x.s C ) ) <-> E. t ( E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) t = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) )
93 rexcom4 
 |-  ( E. xL e. ( _Left ` A ) E. t E. yR e. ( _Right ` B ) ( t = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. t E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) ( t = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) )
94 rexcom4 
 |-  ( E. yR e. ( _Right ` B ) E. t ( t = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. t E. yR e. ( _Right ` B ) ( t = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) )
95 ovex 
 |-  ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) e. _V
96 oveq1 
 |-  ( t = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) -> ( t +s ( A x.s C ) ) = ( ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) +s ( A x.s C ) ) )
97 96 eqeq2d 
 |-  ( t = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) -> ( a = ( t +s ( A x.s C ) ) <-> a = ( ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) +s ( A x.s C ) ) ) )
98 95 97 ceqsexv 
 |-  ( E. t ( t = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> a = ( ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) +s ( A x.s C ) ) )
99 98 rexbii 
 |-  ( E. yR e. ( _Right ` B ) E. t ( t = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. yR e. ( _Right ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) +s ( A x.s C ) ) )
100 94 99 bitr3i 
 |-  ( E. t E. yR e. ( _Right ` B ) ( t = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. yR e. ( _Right ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) +s ( A x.s C ) ) )
101 100 rexbii 
 |-  ( E. xL e. ( _Left ` A ) E. t E. yR e. ( _Right ` B ) ( t = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) +s ( A x.s C ) ) )
102 r19.41vv 
 |-  ( E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) ( t = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> ( E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) t = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) )
103 102 exbii 
 |-  ( E. t E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) ( t = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. t ( E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) t = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) )
104 93 101 103 3bitr3ri 
 |-  ( E. t ( E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) t = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) +s ( A x.s C ) ) )
105 92 104 bitri 
 |-  ( E. t e. { b | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) } a = ( t +s ( A x.s C ) ) <-> E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) +s ( A x.s C ) ) )
106 eqeq1 
 |-  ( b = t -> ( b = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) <-> t = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) ) )
107 106 2rexbidv 
 |-  ( b = t -> ( E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) <-> E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) t = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) ) )
108 107 rexab 
 |-  ( E. t e. { b | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) } a = ( t +s ( A x.s C ) ) <-> E. t ( E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) t = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) )
109 rexcom4 
 |-  ( E. xR e. ( _Right ` A ) E. t E. yL e. ( _Left ` B ) ( t = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. t E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) ( t = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) )
110 rexcom4 
 |-  ( E. yL e. ( _Left ` B ) E. t ( t = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. t E. yL e. ( _Left ` B ) ( t = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) )
111 ovex 
 |-  ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) e. _V
112 oveq1 
 |-  ( t = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) -> ( t +s ( A x.s C ) ) = ( ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) +s ( A x.s C ) ) )
113 112 eqeq2d 
 |-  ( t = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) -> ( a = ( t +s ( A x.s C ) ) <-> a = ( ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) +s ( A x.s C ) ) ) )
114 111 113 ceqsexv 
 |-  ( E. t ( t = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> a = ( ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) +s ( A x.s C ) ) )
115 114 rexbii 
 |-  ( E. yL e. ( _Left ` B ) E. t ( t = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. yL e. ( _Left ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) +s ( A x.s C ) ) )
116 110 115 bitr3i 
 |-  ( E. t E. yL e. ( _Left ` B ) ( t = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. yL e. ( _Left ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) +s ( A x.s C ) ) )
117 116 rexbii 
 |-  ( E. xR e. ( _Right ` A ) E. t E. yL e. ( _Left ` B ) ( t = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) +s ( A x.s C ) ) )
118 r19.41vv 
 |-  ( E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) ( t = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> ( E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) t = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) )
119 118 exbii 
 |-  ( E. t E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) ( t = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. t ( E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) t = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) )
120 109 117 119 3bitr3ri 
 |-  ( E. t ( E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) t = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) /\ a = ( t +s ( A x.s C ) ) ) <-> E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) +s ( A x.s C ) ) )
121 108 120 bitri 
 |-  ( E. t e. { b | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) } a = ( t +s ( A x.s C ) ) <-> E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) +s ( A x.s C ) ) )
122 105 121 orbi12i 
 |-  ( ( E. t e. { b | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) } a = ( t +s ( A x.s C ) ) \/ E. t e. { b | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) } a = ( t +s ( A x.s C ) ) ) <-> ( E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) +s ( A x.s C ) ) \/ E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) +s ( A x.s C ) ) ) )
123 89 122 bitr2i 
 |-  ( ( E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) +s ( A x.s C ) ) \/ E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) +s ( A x.s C ) ) ) <-> E. t e. ( { b | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) } u. { b | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) } ) a = ( t +s ( A x.s C ) ) )
124 123 abbii 
 |-  { a | ( E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) +s ( A x.s C ) ) \/ E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) +s ( A x.s C ) ) ) } = { a | E. t e. ( { b | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) } u. { b | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) } ) a = ( t +s ( A x.s C ) ) }
125 88 124 eqtri 
 |-  ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) +s ( A x.s C ) ) } u. { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) +s ( A x.s C ) ) } ) = { a | E. t e. ( { b | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) } u. { b | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) } ) a = ( t +s ( A x.s C ) ) }
126 unab 
 |-  ( { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) ) } ) = { a | ( E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) ) \/ E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) ) ) }
127 rexun 
 |-  ( E. t e. ( { b | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) } u. { b | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) } ) a = ( ( A x.s B ) +s t ) <-> ( E. t e. { b | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) } a = ( ( A x.s B ) +s t ) \/ E. t e. { b | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) } a = ( ( A x.s B ) +s t ) ) )
128 eqeq1 
 |-  ( b = t -> ( b = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) <-> t = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) ) )
129 128 2rexbidv 
 |-  ( b = t -> ( E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) <-> E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) t = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) ) )
130 129 rexab 
 |-  ( E. t e. { b | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) } a = ( ( A x.s B ) +s t ) <-> E. t ( E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) t = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) )
131 rexcom4 
 |-  ( E. xL e. ( _Left ` A ) E. t E. zR e. ( _Right ` C ) ( t = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. t E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) ( t = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) )
132 rexcom4 
 |-  ( E. zR e. ( _Right ` C ) E. t ( t = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. t E. zR e. ( _Right ` C ) ( t = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) )
133 ovex 
 |-  ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) e. _V
134 oveq2 
 |-  ( t = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) -> ( ( A x.s B ) +s t ) = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) ) )
135 134 eqeq2d 
 |-  ( t = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) -> ( a = ( ( A x.s B ) +s t ) <-> a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) ) ) )
136 133 135 ceqsexv 
 |-  ( E. t ( t = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) ) )
137 136 rexbii 
 |-  ( E. zR e. ( _Right ` C ) E. t ( t = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) ) )
138 132 137 bitr3i 
 |-  ( E. t E. zR e. ( _Right ` C ) ( t = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) ) )
139 138 rexbii 
 |-  ( E. xL e. ( _Left ` A ) E. t E. zR e. ( _Right ` C ) ( t = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) ) )
140 r19.41vv 
 |-  ( E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) ( t = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> ( E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) t = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) )
141 140 exbii 
 |-  ( E. t E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) ( t = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. t ( E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) t = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) )
142 131 139 141 3bitr3ri 
 |-  ( E. t ( E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) t = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) ) )
143 130 142 bitri 
 |-  ( E. t e. { b | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) } a = ( ( A x.s B ) +s t ) <-> E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) ) )
144 eqeq1 
 |-  ( b = t -> ( b = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) <-> t = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) ) )
145 144 2rexbidv 
 |-  ( b = t -> ( E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) <-> E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) t = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) ) )
146 145 rexab 
 |-  ( E. t e. { b | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) } a = ( ( A x.s B ) +s t ) <-> E. t ( E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) t = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) )
147 rexcom4 
 |-  ( E. xR e. ( _Right ` A ) E. t E. zL e. ( _Left ` C ) ( t = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. t E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) ( t = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) )
148 rexcom4 
 |-  ( E. zL e. ( _Left ` C ) E. t ( t = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. t E. zL e. ( _Left ` C ) ( t = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) )
149 ovex 
 |-  ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) e. _V
150 oveq2 
 |-  ( t = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) -> ( ( A x.s B ) +s t ) = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) ) )
151 150 eqeq2d 
 |-  ( t = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) -> ( a = ( ( A x.s B ) +s t ) <-> a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) ) ) )
152 149 151 ceqsexv 
 |-  ( E. t ( t = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) ) )
153 152 rexbii 
 |-  ( E. zL e. ( _Left ` C ) E. t ( t = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) ) )
154 148 153 bitr3i 
 |-  ( E. t E. zL e. ( _Left ` C ) ( t = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) ) )
155 154 rexbii 
 |-  ( E. xR e. ( _Right ` A ) E. t E. zL e. ( _Left ` C ) ( t = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) ) )
156 r19.41vv 
 |-  ( E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) ( t = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> ( E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) t = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) )
157 156 exbii 
 |-  ( E. t E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) ( t = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. t ( E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) t = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) )
158 147 155 157 3bitr3ri 
 |-  ( E. t ( E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) t = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) /\ a = ( ( A x.s B ) +s t ) ) <-> E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) ) )
159 146 158 bitri 
 |-  ( E. t e. { b | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) } a = ( ( A x.s B ) +s t ) <-> E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) ) )
160 143 159 orbi12i 
 |-  ( ( E. t e. { b | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) } a = ( ( A x.s B ) +s t ) \/ E. t e. { b | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) } a = ( ( A x.s B ) +s t ) ) <-> ( E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) ) \/ E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) ) ) )
161 127 160 bitr2i 
 |-  ( ( E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) ) \/ E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) ) ) <-> E. t e. ( { b | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) } u. { b | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) } ) a = ( ( A x.s B ) +s t ) )
162 161 abbii 
 |-  { a | ( E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) ) \/ E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) ) ) } = { a | E. t e. ( { b | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) } u. { b | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) } ) a = ( ( A x.s B ) +s t ) }
163 126 162 eqtri 
 |-  ( { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) ) } ) = { a | E. t e. ( { b | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) } u. { b | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) } ) a = ( ( A x.s B ) +s t ) }
164 125 163 uneq12i 
 |-  ( ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) +s ( A x.s C ) ) } u. { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) +s ( A x.s C ) ) } ) u. ( { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) = ( { a | E. t e. ( { b | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) } u. { b | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) } ) a = ( t +s ( A x.s C ) ) } u. { a | E. t e. ( { b | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) } u. { b | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) } ) a = ( ( A x.s B ) +s t ) } )
165 87 164 oveq12i 
 |-  ( ( ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) +s ( A x.s C ) ) } u. { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) +s ( A x.s C ) ) } ) u. ( { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) +s ( A x.s C ) ) } u. { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) +s ( A x.s C ) ) } ) u. ( { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) ) = ( ( { a | E. t e. ( { b | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) } u. { b | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) } ) a = ( t +s ( A x.s C ) ) } u. { a | E. t e. ( { b | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) } u. { b | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) } ) a = ( ( A x.s B ) +s t ) } ) |s ( { a | E. t e. ( { b | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) b = ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) } u. { b | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) b = ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) } ) a = ( t +s ( A x.s C ) ) } u. { a | E. t e. ( { b | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) b = ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) } u. { b | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) b = ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) } ) a = ( ( A x.s B ) +s t ) } ) )
166 10 165 eqtr4di 
 |-  ( ph -> ( ( A x.s B ) +s ( A x.s C ) ) = ( ( ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) +s ( A x.s C ) ) } u. { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) +s ( A x.s C ) ) } ) u. ( { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zL ) ) -s ( xL x.s zL ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) +s ( A x.s C ) ) } u. { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) +s ( A x.s C ) ) } ) u. ( { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( A x.s B ) +s ( ( ( xL x.s C ) +s ( A x.s zR ) ) -s ( xL x.s zR ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( A x.s B ) +s ( ( ( xR x.s C ) +s ( A x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) ) )