Metamath Proof Explorer

Theorem mulsasslem1

Description: Lemma for mulsass . Expand the left 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 mulsasslem1 
|- ( 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 ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) x.s C ) +s ( ( A x.s B ) x.s zL ) ) -s ( ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) E. zL e. ( _Left ` C ) a = ( ( ( ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) x.s C ) +s ( ( A x.s B ) x.s zL ) ) -s ( ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) 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 ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) x.s C ) +s ( ( A x.s B ) x.s zR ) ) -s ( ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.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 ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) x.s C ) +s ( ( A x.s B ) x.s zR ) ) -s ( ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) x.s zR ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) E. zR e. ( _Right ` C ) a = ( ( ( ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) x.s C ) +s ( ( A x.s B ) x.s zR ) ) -s ( ( ( ( xL x.s B ) +s ( A x.s yL ) ) -s ( xL x.s yL ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) E. zR e. ( _Right ` C ) a = ( ( ( ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) x.s C ) +s ( ( A x.s B ) x.s zR ) ) -s ( ( ( ( xR x.s B ) +s ( A x.s yR ) ) -s ( xR x.s yR ) ) 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 ) +s ( A x.s yR ) ) -s ( xL x.s yR ) ) x.s C ) +s ( ( A x.s B ) x.s zL ) ) -s ( ( ( ( xL x.s B ) +s ( A x.s yR ) ) -s ( xL x.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 ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) x.s C ) +s ( ( A x.s B ) x.s zL ) ) -s ( ( ( ( xR x.s B ) +s ( A x.s yL ) ) -s ( xR x.s yL ) ) x.s zL ) ) } ) ) ) )

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