Metamath Proof Explorer

Theorem addsasslem2

Description: Lemma for addition associativity. Expand the other form of the triple sum. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Hypotheses addsasslem.1 
|- ( ph -> A e. No )
addsasslem.2 
|- ( ph -> B e. No )
addsasslem.3 
|- ( ph -> C e. No )
Assertion addsasslem2 
|- ( ph -> ( A +s ( B +s C ) ) = ( ( ( { y | E. l e. ( _Left ` A ) y = ( l +s ( B +s C ) ) } u. { z | E. m e. ( _Left ` B ) z = ( A +s ( m +s C ) ) } ) u. { w | E. n e. ( _Left ` C ) w = ( A +s ( B +s n ) ) } ) |s ( ( { a | E. p e. ( _Right ` A ) a = ( p +s ( B +s C ) ) } u. { b | E. q e. ( _Right ` B ) b = ( A +s ( q +s C ) ) } ) u. { c | E. r e. ( _Right ` C ) c = ( A +s ( B +s r ) ) } ) ) )

Proof

Step Hyp Ref Expression
1 addsasslem.1 
 |-  ( ph -> A e. No )
2 addsasslem.2 
 |-  ( ph -> B e. No )
3 addsasslem.3 
 |-  ( ph -> C e. No )
4 lltropt 
 |-  ( _Left ` A ) <
5 4 a1i 
 |-  ( ph -> ( _Left ` A ) <
6 2 3 addscut 
 |-  ( ph -> ( ( B +s C ) e. No /\ ( { d | E. m e. ( _Left ` B ) d = ( m +s C ) } u. { e | E. n e. ( _Left ` C ) e = ( B +s n ) } ) <
7 6 simp2d 
 |-  ( ph -> ( { d | E. m e. ( _Left ` B ) d = ( m +s C ) } u. { e | E. n e. ( _Left ` C ) e = ( B +s n ) } ) <
8 6 simp3d 
 |-  ( ph -> { ( B +s C ) } <
9 ovex 
 |-  ( B +s C ) e. _V
10 9 snnz 
 |-  { ( B +s C ) } =/= (/)
11 sslttr 
 |-  ( ( ( { d | E. m e. ( _Left ` B ) d = ( m +s C ) } u. { e | E. n e. ( _Left ` C ) e = ( B +s n ) } ) < ( { d | E. m e. ( _Left ` B ) d = ( m +s C ) } u. { e | E. n e. ( _Left ` C ) e = ( B +s n ) } ) <
12 10 11 mp3an3 
 |-  ( ( ( { d | E. m e. ( _Left ` B ) d = ( m +s C ) } u. { e | E. n e. ( _Left ` C ) e = ( B +s n ) } ) < ( { d | E. m e. ( _Left ` B ) d = ( m +s C ) } u. { e | E. n e. ( _Left ` C ) e = ( B +s n ) } ) <
13 7 8 12 syl2anc 
 |-  ( ph -> ( { d | E. m e. ( _Left ` B ) d = ( m +s C ) } u. { e | E. n e. ( _Left ` C ) e = ( B +s n ) } ) <
14 lrcut 
 |-  ( A e. No -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A )
15 1 14 syl 
 |-  ( ph -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A )
16 15 eqcomd 
 |-  ( ph -> A = ( ( _Left ` A ) |s ( _Right ` A ) ) )
17 addsval2 
 |-  ( ( B e. No /\ C e. No ) -> ( B +s C ) = ( ( { d | E. m e. ( _Left ` B ) d = ( m +s C ) } u. { e | E. n e. ( _Left ` C ) e = ( B +s n ) } ) |s ( { f | E. q e. ( _Right ` B ) f = ( q +s C ) } u. { g | E. r e. ( _Right ` C ) g = ( B +s r ) } ) ) )
18 2 3 17 syl2anc 
 |-  ( ph -> ( B +s C ) = ( ( { d | E. m e. ( _Left ` B ) d = ( m +s C ) } u. { e | E. n e. ( _Left ` C ) e = ( B +s n ) } ) |s ( { f | E. q e. ( _Right ` B ) f = ( q +s C ) } u. { g | E. r e. ( _Right ` C ) g = ( B +s r ) } ) ) )
19 5 13 16 18 addsunif 
 |-  ( ph -> ( A +s ( B +s C ) ) = ( ( { y | E. l e. ( _Left ` A ) y = ( l +s ( B +s C ) ) } u. { z | E. h e. ( { d | E. m e. ( _Left ` B ) d = ( m +s C ) } u. { e | E. n e. ( _Left ` C ) e = ( B +s n ) } ) z = ( A +s h ) } ) |s ( { a | E. p e. ( _Right ` A ) a = ( p +s ( B +s C ) ) } u. { b | E. i e. ( { f | E. q e. ( _Right ` B ) f = ( q +s C ) } u. { g | E. r e. ( _Right ` C ) g = ( B +s r ) } ) b = ( A +s i ) } ) ) )
20 rexun 
 |-  ( E. h e. ( { d | E. m e. ( _Left ` B ) d = ( m +s C ) } u. { e | E. n e. ( _Left ` C ) e = ( B +s n ) } ) z = ( A +s h ) <-> ( E. h e. { d | E. m e. ( _Left ` B ) d = ( m +s C ) } z = ( A +s h ) \/ E. h e. { e | E. n e. ( _Left ` C ) e = ( B +s n ) } z = ( A +s h ) ) )
21 eqeq1 
 |-  ( d = h -> ( d = ( m +s C ) <-> h = ( m +s C ) ) )
22 21 rexbidv 
 |-  ( d = h -> ( E. m e. ( _Left ` B ) d = ( m +s C ) <-> E. m e. ( _Left ` B ) h = ( m +s C ) ) )
23 22 rexab 
 |-  ( E. h e. { d | E. m e. ( _Left ` B ) d = ( m +s C ) } z = ( A +s h ) <-> E. h ( E. m e. ( _Left ` B ) h = ( m +s C ) /\ z = ( A +s h ) ) )
24 rexcom4 
 |-  ( E. m e. ( _Left ` B ) E. h ( h = ( m +s C ) /\ z = ( A +s h ) ) <-> E. h E. m e. ( _Left ` B ) ( h = ( m +s C ) /\ z = ( A +s h ) ) )
25 ovex 
 |-  ( m +s C ) e. _V
26 oveq2 
 |-  ( h = ( m +s C ) -> ( A +s h ) = ( A +s ( m +s C ) ) )
27 26 eqeq2d 
 |-  ( h = ( m +s C ) -> ( z = ( A +s h ) <-> z = ( A +s ( m +s C ) ) ) )
28 25 27 ceqsexv 
 |-  ( E. h ( h = ( m +s C ) /\ z = ( A +s h ) ) <-> z = ( A +s ( m +s C ) ) )
29 28 rexbii 
 |-  ( E. m e. ( _Left ` B ) E. h ( h = ( m +s C ) /\ z = ( A +s h ) ) <-> E. m e. ( _Left ` B ) z = ( A +s ( m +s C ) ) )
30 r19.41v 
 |-  ( E. m e. ( _Left ` B ) ( h = ( m +s C ) /\ z = ( A +s h ) ) <-> ( E. m e. ( _Left ` B ) h = ( m +s C ) /\ z = ( A +s h ) ) )
31 30 exbii 
 |-  ( E. h E. m e. ( _Left ` B ) ( h = ( m +s C ) /\ z = ( A +s h ) ) <-> E. h ( E. m e. ( _Left ` B ) h = ( m +s C ) /\ z = ( A +s h ) ) )
32 24 29 31 3bitr3ri 
 |-  ( E. h ( E. m e. ( _Left ` B ) h = ( m +s C ) /\ z = ( A +s h ) ) <-> E. m e. ( _Left ` B ) z = ( A +s ( m +s C ) ) )
33 23 32 bitri 
 |-  ( E. h e. { d | E. m e. ( _Left ` B ) d = ( m +s C ) } z = ( A +s h ) <-> E. m e. ( _Left ` B ) z = ( A +s ( m +s C ) ) )
34 eqeq1 
 |-  ( e = h -> ( e = ( B +s n ) <-> h = ( B +s n ) ) )
35 34 rexbidv 
 |-  ( e = h -> ( E. n e. ( _Left ` C ) e = ( B +s n ) <-> E. n e. ( _Left ` C ) h = ( B +s n ) ) )
36 35 rexab 
 |-  ( E. h e. { e | E. n e. ( _Left ` C ) e = ( B +s n ) } z = ( A +s h ) <-> E. h ( E. n e. ( _Left ` C ) h = ( B +s n ) /\ z = ( A +s h ) ) )
37 rexcom4 
 |-  ( E. n e. ( _Left ` C ) E. h ( h = ( B +s n ) /\ z = ( A +s h ) ) <-> E. h E. n e. ( _Left ` C ) ( h = ( B +s n ) /\ z = ( A +s h ) ) )
38 ovex 
 |-  ( B +s n ) e. _V
39 oveq2 
 |-  ( h = ( B +s n ) -> ( A +s h ) = ( A +s ( B +s n ) ) )
40 39 eqeq2d 
 |-  ( h = ( B +s n ) -> ( z = ( A +s h ) <-> z = ( A +s ( B +s n ) ) ) )
41 38 40 ceqsexv 
 |-  ( E. h ( h = ( B +s n ) /\ z = ( A +s h ) ) <-> z = ( A +s ( B +s n ) ) )
42 41 rexbii 
 |-  ( E. n e. ( _Left ` C ) E. h ( h = ( B +s n ) /\ z = ( A +s h ) ) <-> E. n e. ( _Left ` C ) z = ( A +s ( B +s n ) ) )
43 r19.41v 
 |-  ( E. n e. ( _Left ` C ) ( h = ( B +s n ) /\ z = ( A +s h ) ) <-> ( E. n e. ( _Left ` C ) h = ( B +s n ) /\ z = ( A +s h ) ) )
44 43 exbii 
 |-  ( E. h E. n e. ( _Left ` C ) ( h = ( B +s n ) /\ z = ( A +s h ) ) <-> E. h ( E. n e. ( _Left ` C ) h = ( B +s n ) /\ z = ( A +s h ) ) )
45 37 42 44 3bitr3ri 
 |-  ( E. h ( E. n e. ( _Left ` C ) h = ( B +s n ) /\ z = ( A +s h ) ) <-> E. n e. ( _Left ` C ) z = ( A +s ( B +s n ) ) )
46 36 45 bitri 
 |-  ( E. h e. { e | E. n e. ( _Left ` C ) e = ( B +s n ) } z = ( A +s h ) <-> E. n e. ( _Left ` C ) z = ( A +s ( B +s n ) ) )
47 33 46 orbi12i 
 |-  ( ( E. h e. { d | E. m e. ( _Left ` B ) d = ( m +s C ) } z = ( A +s h ) \/ E. h e. { e | E. n e. ( _Left ` C ) e = ( B +s n ) } z = ( A +s h ) ) <-> ( E. m e. ( _Left ` B ) z = ( A +s ( m +s C ) ) \/ E. n e. ( _Left ` C ) z = ( A +s ( B +s n ) ) ) )
48 20 47 bitri 
 |-  ( E. h e. ( { d | E. m e. ( _Left ` B ) d = ( m +s C ) } u. { e | E. n e. ( _Left ` C ) e = ( B +s n ) } ) z = ( A +s h ) <-> ( E. m e. ( _Left ` B ) z = ( A +s ( m +s C ) ) \/ E. n e. ( _Left ` C ) z = ( A +s ( B +s n ) ) ) )
49 48 abbii 
 |-  { z | E. h e. ( { d | E. m e. ( _Left ` B ) d = ( m +s C ) } u. { e | E. n e. ( _Left ` C ) e = ( B +s n ) } ) z = ( A +s h ) } = { z | ( E. m e. ( _Left ` B ) z = ( A +s ( m +s C ) ) \/ E. n e. ( _Left ` C ) z = ( A +s ( B +s n ) ) ) }
50 unab 
 |-  ( { z | E. m e. ( _Left ` B ) z = ( A +s ( m +s C ) ) } u. { z | E. n e. ( _Left ` C ) z = ( A +s ( B +s n ) ) } ) = { z | ( E. m e. ( _Left ` B ) z = ( A +s ( m +s C ) ) \/ E. n e. ( _Left ` C ) z = ( A +s ( B +s n ) ) ) }
51 eqeq1 
 |-  ( z = w -> ( z = ( A +s ( B +s n ) ) <-> w = ( A +s ( B +s n ) ) ) )
52 51 rexbidv 
 |-  ( z = w -> ( E. n e. ( _Left ` C ) z = ( A +s ( B +s n ) ) <-> E. n e. ( _Left ` C ) w = ( A +s ( B +s n ) ) ) )
53 52 cbvabv 
 |-  { z | E. n e. ( _Left ` C ) z = ( A +s ( B +s n ) ) } = { w | E. n e. ( _Left ` C ) w = ( A +s ( B +s n ) ) }
54 53 uneq2i 
 |-  ( { z | E. m e. ( _Left ` B ) z = ( A +s ( m +s C ) ) } u. { z | E. n e. ( _Left ` C ) z = ( A +s ( B +s n ) ) } ) = ( { z | E. m e. ( _Left ` B ) z = ( A +s ( m +s C ) ) } u. { w | E. n e. ( _Left ` C ) w = ( A +s ( B +s n ) ) } )
55 49 50 54 3eqtr2i 
 |-  { z | E. h e. ( { d | E. m e. ( _Left ` B ) d = ( m +s C ) } u. { e | E. n e. ( _Left ` C ) e = ( B +s n ) } ) z = ( A +s h ) } = ( { z | E. m e. ( _Left ` B ) z = ( A +s ( m +s C ) ) } u. { w | E. n e. ( _Left ` C ) w = ( A +s ( B +s n ) ) } )
56 55 uneq2i 
 |-  ( { y | E. l e. ( _Left ` A ) y = ( l +s ( B +s C ) ) } u. { z | E. h e. ( { d | E. m e. ( _Left ` B ) d = ( m +s C ) } u. { e | E. n e. ( _Left ` C ) e = ( B +s n ) } ) z = ( A +s h ) } ) = ( { y | E. l e. ( _Left ` A ) y = ( l +s ( B +s C ) ) } u. ( { z | E. m e. ( _Left ` B ) z = ( A +s ( m +s C ) ) } u. { w | E. n e. ( _Left ` C ) w = ( A +s ( B +s n ) ) } ) )
57 unass 
 |-  ( ( { y | E. l e. ( _Left ` A ) y = ( l +s ( B +s C ) ) } u. { z | E. m e. ( _Left ` B ) z = ( A +s ( m +s C ) ) } ) u. { w | E. n e. ( _Left ` C ) w = ( A +s ( B +s n ) ) } ) = ( { y | E. l e. ( _Left ` A ) y = ( l +s ( B +s C ) ) } u. ( { z | E. m e. ( _Left ` B ) z = ( A +s ( m +s C ) ) } u. { w | E. n e. ( _Left ` C ) w = ( A +s ( B +s n ) ) } ) )
58 56 57 eqtr4i 
 |-  ( { y | E. l e. ( _Left ` A ) y = ( l +s ( B +s C ) ) } u. { z | E. h e. ( { d | E. m e. ( _Left ` B ) d = ( m +s C ) } u. { e | E. n e. ( _Left ` C ) e = ( B +s n ) } ) z = ( A +s h ) } ) = ( ( { y | E. l e. ( _Left ` A ) y = ( l +s ( B +s C ) ) } u. { z | E. m e. ( _Left ` B ) z = ( A +s ( m +s C ) ) } ) u. { w | E. n e. ( _Left ` C ) w = ( A +s ( B +s n ) ) } )
59 rexun 
 |-  ( E. i e. ( { f | E. q e. ( _Right ` B ) f = ( q +s C ) } u. { g | E. r e. ( _Right ` C ) g = ( B +s r ) } ) b = ( A +s i ) <-> ( E. i e. { f | E. q e. ( _Right ` B ) f = ( q +s C ) } b = ( A +s i ) \/ E. i e. { g | E. r e. ( _Right ` C ) g = ( B +s r ) } b = ( A +s i ) ) )
60 eqeq1 
 |-  ( f = i -> ( f = ( q +s C ) <-> i = ( q +s C ) ) )
61 60 rexbidv 
 |-  ( f = i -> ( E. q e. ( _Right ` B ) f = ( q +s C ) <-> E. q e. ( _Right ` B ) i = ( q +s C ) ) )
62 61 rexab 
 |-  ( E. i e. { f | E. q e. ( _Right ` B ) f = ( q +s C ) } b = ( A +s i ) <-> E. i ( E. q e. ( _Right ` B ) i = ( q +s C ) /\ b = ( A +s i ) ) )
63 rexcom4 
 |-  ( E. q e. ( _Right ` B ) E. i ( i = ( q +s C ) /\ b = ( A +s i ) ) <-> E. i E. q e. ( _Right ` B ) ( i = ( q +s C ) /\ b = ( A +s i ) ) )
64 ovex 
 |-  ( q +s C ) e. _V
65 oveq2 
 |-  ( i = ( q +s C ) -> ( A +s i ) = ( A +s ( q +s C ) ) )
66 65 eqeq2d 
 |-  ( i = ( q +s C ) -> ( b = ( A +s i ) <-> b = ( A +s ( q +s C ) ) ) )
67 64 66 ceqsexv 
 |-  ( E. i ( i = ( q +s C ) /\ b = ( A +s i ) ) <-> b = ( A +s ( q +s C ) ) )
68 67 rexbii 
 |-  ( E. q e. ( _Right ` B ) E. i ( i = ( q +s C ) /\ b = ( A +s i ) ) <-> E. q e. ( _Right ` B ) b = ( A +s ( q +s C ) ) )
69 r19.41v 
 |-  ( E. q e. ( _Right ` B ) ( i = ( q +s C ) /\ b = ( A +s i ) ) <-> ( E. q e. ( _Right ` B ) i = ( q +s C ) /\ b = ( A +s i ) ) )
70 69 exbii 
 |-  ( E. i E. q e. ( _Right ` B ) ( i = ( q +s C ) /\ b = ( A +s i ) ) <-> E. i ( E. q e. ( _Right ` B ) i = ( q +s C ) /\ b = ( A +s i ) ) )
71 63 68 70 3bitr3ri 
 |-  ( E. i ( E. q e. ( _Right ` B ) i = ( q +s C ) /\ b = ( A +s i ) ) <-> E. q e. ( _Right ` B ) b = ( A +s ( q +s C ) ) )
72 62 71 bitri 
 |-  ( E. i e. { f | E. q e. ( _Right ` B ) f = ( q +s C ) } b = ( A +s i ) <-> E. q e. ( _Right ` B ) b = ( A +s ( q +s C ) ) )
73 eqeq1 
 |-  ( g = i -> ( g = ( B +s r ) <-> i = ( B +s r ) ) )
74 73 rexbidv 
 |-  ( g = i -> ( E. r e. ( _Right ` C ) g = ( B +s r ) <-> E. r e. ( _Right ` C ) i = ( B +s r ) ) )
75 74 rexab 
 |-  ( E. i e. { g | E. r e. ( _Right ` C ) g = ( B +s r ) } b = ( A +s i ) <-> E. i ( E. r e. ( _Right ` C ) i = ( B +s r ) /\ b = ( A +s i ) ) )
76 rexcom4 
 |-  ( E. r e. ( _Right ` C ) E. i ( i = ( B +s r ) /\ b = ( A +s i ) ) <-> E. i E. r e. ( _Right ` C ) ( i = ( B +s r ) /\ b = ( A +s i ) ) )
77 ovex 
 |-  ( B +s r ) e. _V
78 oveq2 
 |-  ( i = ( B +s r ) -> ( A +s i ) = ( A +s ( B +s r ) ) )
79 78 eqeq2d 
 |-  ( i = ( B +s r ) -> ( b = ( A +s i ) <-> b = ( A +s ( B +s r ) ) ) )
80 77 79 ceqsexv 
 |-  ( E. i ( i = ( B +s r ) /\ b = ( A +s i ) ) <-> b = ( A +s ( B +s r ) ) )
81 80 rexbii 
 |-  ( E. r e. ( _Right ` C ) E. i ( i = ( B +s r ) /\ b = ( A +s i ) ) <-> E. r e. ( _Right ` C ) b = ( A +s ( B +s r ) ) )
82 r19.41v 
 |-  ( E. r e. ( _Right ` C ) ( i = ( B +s r ) /\ b = ( A +s i ) ) <-> ( E. r e. ( _Right ` C ) i = ( B +s r ) /\ b = ( A +s i ) ) )
83 82 exbii 
 |-  ( E. i E. r e. ( _Right ` C ) ( i = ( B +s r ) /\ b = ( A +s i ) ) <-> E. i ( E. r e. ( _Right ` C ) i = ( B +s r ) /\ b = ( A +s i ) ) )
84 76 81 83 3bitr3ri 
 |-  ( E. i ( E. r e. ( _Right ` C ) i = ( B +s r ) /\ b = ( A +s i ) ) <-> E. r e. ( _Right ` C ) b = ( A +s ( B +s r ) ) )
85 75 84 bitri 
 |-  ( E. i e. { g | E. r e. ( _Right ` C ) g = ( B +s r ) } b = ( A +s i ) <-> E. r e. ( _Right ` C ) b = ( A +s ( B +s r ) ) )
86 72 85 orbi12i 
 |-  ( ( E. i e. { f | E. q e. ( _Right ` B ) f = ( q +s C ) } b = ( A +s i ) \/ E. i e. { g | E. r e. ( _Right ` C ) g = ( B +s r ) } b = ( A +s i ) ) <-> ( E. q e. ( _Right ` B ) b = ( A +s ( q +s C ) ) \/ E. r e. ( _Right ` C ) b = ( A +s ( B +s r ) ) ) )
87 59 86 bitri 
 |-  ( E. i e. ( { f | E. q e. ( _Right ` B ) f = ( q +s C ) } u. { g | E. r e. ( _Right ` C ) g = ( B +s r ) } ) b = ( A +s i ) <-> ( E. q e. ( _Right ` B ) b = ( A +s ( q +s C ) ) \/ E. r e. ( _Right ` C ) b = ( A +s ( B +s r ) ) ) )
88 87 abbii 
 |-  { b | E. i e. ( { f | E. q e. ( _Right ` B ) f = ( q +s C ) } u. { g | E. r e. ( _Right ` C ) g = ( B +s r ) } ) b = ( A +s i ) } = { b | ( E. q e. ( _Right ` B ) b = ( A +s ( q +s C ) ) \/ E. r e. ( _Right ` C ) b = ( A +s ( B +s r ) ) ) }
89 unab 
 |-  ( { b | E. q e. ( _Right ` B ) b = ( A +s ( q +s C ) ) } u. { b | E. r e. ( _Right ` C ) b = ( A +s ( B +s r ) ) } ) = { b | ( E. q e. ( _Right ` B ) b = ( A +s ( q +s C ) ) \/ E. r e. ( _Right ` C ) b = ( A +s ( B +s r ) ) ) }
90 eqeq1 
 |-  ( b = c -> ( b = ( A +s ( B +s r ) ) <-> c = ( A +s ( B +s r ) ) ) )
91 90 rexbidv 
 |-  ( b = c -> ( E. r e. ( _Right ` C ) b = ( A +s ( B +s r ) ) <-> E. r e. ( _Right ` C ) c = ( A +s ( B +s r ) ) ) )
92 91 cbvabv 
 |-  { b | E. r e. ( _Right ` C ) b = ( A +s ( B +s r ) ) } = { c | E. r e. ( _Right ` C ) c = ( A +s ( B +s r ) ) }
93 92 uneq2i 
 |-  ( { b | E. q e. ( _Right ` B ) b = ( A +s ( q +s C ) ) } u. { b | E. r e. ( _Right ` C ) b = ( A +s ( B +s r ) ) } ) = ( { b | E. q e. ( _Right ` B ) b = ( A +s ( q +s C ) ) } u. { c | E. r e. ( _Right ` C ) c = ( A +s ( B +s r ) ) } )
94 88 89 93 3eqtr2i 
 |-  { b | E. i e. ( { f | E. q e. ( _Right ` B ) f = ( q +s C ) } u. { g | E. r e. ( _Right ` C ) g = ( B +s r ) } ) b = ( A +s i ) } = ( { b | E. q e. ( _Right ` B ) b = ( A +s ( q +s C ) ) } u. { c | E. r e. ( _Right ` C ) c = ( A +s ( B +s r ) ) } )
95 94 uneq2i 
 |-  ( { a | E. p e. ( _Right ` A ) a = ( p +s ( B +s C ) ) } u. { b | E. i e. ( { f | E. q e. ( _Right ` B ) f = ( q +s C ) } u. { g | E. r e. ( _Right ` C ) g = ( B +s r ) } ) b = ( A +s i ) } ) = ( { a | E. p e. ( _Right ` A ) a = ( p +s ( B +s C ) ) } u. ( { b | E. q e. ( _Right ` B ) b = ( A +s ( q +s C ) ) } u. { c | E. r e. ( _Right ` C ) c = ( A +s ( B +s r ) ) } ) )
96 unass 
 |-  ( ( { a | E. p e. ( _Right ` A ) a = ( p +s ( B +s C ) ) } u. { b | E. q e. ( _Right ` B ) b = ( A +s ( q +s C ) ) } ) u. { c | E. r e. ( _Right ` C ) c = ( A +s ( B +s r ) ) } ) = ( { a | E. p e. ( _Right ` A ) a = ( p +s ( B +s C ) ) } u. ( { b | E. q e. ( _Right ` B ) b = ( A +s ( q +s C ) ) } u. { c | E. r e. ( _Right ` C ) c = ( A +s ( B +s r ) ) } ) )
97 95 96 eqtr4i 
 |-  ( { a | E. p e. ( _Right ` A ) a = ( p +s ( B +s C ) ) } u. { b | E. i e. ( { f | E. q e. ( _Right ` B ) f = ( q +s C ) } u. { g | E. r e. ( _Right ` C ) g = ( B +s r ) } ) b = ( A +s i ) } ) = ( ( { a | E. p e. ( _Right ` A ) a = ( p +s ( B +s C ) ) } u. { b | E. q e. ( _Right ` B ) b = ( A +s ( q +s C ) ) } ) u. { c | E. r e. ( _Right ` C ) c = ( A +s ( B +s r ) ) } )
98 58 97 oveq12i 
 |-  ( ( { y | E. l e. ( _Left ` A ) y = ( l +s ( B +s C ) ) } u. { z | E. h e. ( { d | E. m e. ( _Left ` B ) d = ( m +s C ) } u. { e | E. n e. ( _Left ` C ) e = ( B +s n ) } ) z = ( A +s h ) } ) |s ( { a | E. p e. ( _Right ` A ) a = ( p +s ( B +s C ) ) } u. { b | E. i e. ( { f | E. q e. ( _Right ` B ) f = ( q +s C ) } u. { g | E. r e. ( _Right ` C ) g = ( B +s r ) } ) b = ( A +s i ) } ) ) = ( ( ( { y | E. l e. ( _Left ` A ) y = ( l +s ( B +s C ) ) } u. { z | E. m e. ( _Left ` B ) z = ( A +s ( m +s C ) ) } ) u. { w | E. n e. ( _Left ` C ) w = ( A +s ( B +s n ) ) } ) |s ( ( { a | E. p e. ( _Right ` A ) a = ( p +s ( B +s C ) ) } u. { b | E. q e. ( _Right ` B ) b = ( A +s ( q +s C ) ) } ) u. { c | E. r e. ( _Right ` C ) c = ( A +s ( B +s r ) ) } ) )
99 19 98 eqtrdi 
 |-  ( ph -> ( A +s ( B +s C ) ) = ( ( ( { y | E. l e. ( _Left ` A ) y = ( l +s ( B +s C ) ) } u. { z | E. m e. ( _Left ` B ) z = ( A +s ( m +s C ) ) } ) u. { w | E. n e. ( _Left ` C ) w = ( A +s ( B +s n ) ) } ) |s ( ( { a | E. p e. ( _Right ` A ) a = ( p +s ( B +s C ) ) } u. { b | E. q e. ( _Right ` B ) b = ( A +s ( q +s C ) ) } ) u. { c | E. r e. ( _Right ` C ) c = ( A +s ( B +s r ) ) } ) ) )