Metamath Proof Explorer

Theorem mulsasslem2

Description: Lemma for mulsass . Expand the right hand side of the formula. (Contributed by Scott Fenton, 9-Mar-2025)

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

Proof

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