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 φ A No
addsasslem.2 φ B No
addsasslem.3 φ C No
Assertion addsasslem2 φ A + s B + s C = y | l L A y = l + s B + s C z | m L B z = A + s m + s C w | n L C w = A + s B + s n | s a | p R A a = p + s B + s C b | q R B b = A + s q + s C c | r R C c = A + s B + s r

Proof

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