Metamath Proof Explorer


Theorem addsasslem1

Description: Lemma for addition associativity. Expand one 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 addsasslem1 φ 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 1 2 addscut φ A + s B No d | l L A d = l + s B e | m L B e = A + s m s A + s B A + s B s f | p R A f = p + s B g | q R B g = A + s q
5 4 simp2d φ d | l L A d = l + s B e | m L B e = A + s m s A + s B
6 4 simp3d φ A + s B s f | p R A f = p + s B g | q R B g = A + s q
7 ovex A + s B V
8 7 snnz A + s B
9 sslttr d | l L A d = l + s B e | m L B e = A + s m s A + s B A + s B s f | p R A f = p + s B g | q R B g = A + s q A + s B d | l L A d = l + s B e | m L B e = A + s m s f | p R A f = p + s B g | q R B g = A + s q
10 8 9 mp3an3 d | l L A d = l + s B e | m L B e = A + s m s A + s B A + s B s f | p R A f = p + s B g | q R B g = A + s q d | l L A d = l + s B e | m L B e = A + s m s f | p R A f = p + s B g | q R B g = A + s q
11 5 6 10 syl2anc φ d | l L A d = l + s B e | m L B e = A + s m s f | p R A f = p + s B g | q R B g = A + s q
12 lltropt L C s R C
13 12 a1i φ L C s R C
14 addsval2 A No B No A + s B = d | l L A d = l + s B e | m L B e = A + s m | s f | p R A f = p + s B g | q R B g = A + s q
15 1 2 14 syl2anc φ A + s B = d | l L A d = l + s B e | m L B e = A + s m | s f | p R A f = p + s B g | q R B g = A + s q
16 lrcut C No L C | s R C = C
17 3 16 syl φ L C | s R C = C
18 17 eqcomd φ C = L C | s R C
19 11 13 15 18 addsunif φ A + s B + s C = y | h d | l L A d = l + s B e | m L B e = A + s m y = h + s C w | n L C w = A + s B + s n | s a | i f | p R A f = p + s B g | q R B g = A + s q a = i + s C c | r R C c = A + s B + s r
20 unab y | l L A y = l + s B + s C y | m L B y = A + s m + s C = y | l L A y = l + s B + s C m L B y = A + s m + s C
21 eqeq1 z = y z = A + s m + s C y = A + s m + s C
22 21 rexbidv z = y m L B z = A + s m + s C m L B y = A + s m + s C
23 22 cbvabv z | m L B z = A + s m + s C = y | m L B y = A + s m + s C
24 23 uneq2i y | l L A y = l + s B + s C z | m L B z = A + s m + s C = y | l L A y = l + s B + s C y | m L B y = A + s m + s C
25 rexun h d | l L A d = l + s B e | m L B e = A + s m y = h + s C h d | l L A d = l + s B y = h + s C h e | m L B e = A + s m y = h + s C
26 eqeq1 d = h d = l + s B h = l + s B
27 26 rexbidv d = h l L A d = l + s B l L A h = l + s B
28 27 rexab h d | l L A d = l + s B y = h + s C h l L A h = l + s B y = h + s C
29 rexcom4 l L A h h = l + s B y = h + s C h l L A h = l + s B y = h + s C
30 ovex l + s B V
31 oveq1 h = l + s B h + s C = l + s B + s C
32 31 eqeq2d h = l + s B y = h + s C y = l + s B + s C
33 30 32 ceqsexv h h = l + s B y = h + s C y = l + s B + s C
34 33 rexbii l L A h h = l + s B y = h + s C l L A y = l + s B + s C
35 r19.41v l L A h = l + s B y = h + s C l L A h = l + s B y = h + s C
36 35 exbii h l L A h = l + s B y = h + s C h l L A h = l + s B y = h + s C
37 29 34 36 3bitr3ri h l L A h = l + s B y = h + s C l L A y = l + s B + s C
38 28 37 bitri h d | l L A d = l + s B y = h + s C l L A y = l + s B + s C
39 eqeq1 e = h e = A + s m h = A + s m
40 39 rexbidv e = h m L B e = A + s m m L B h = A + s m
41 40 rexab h e | m L B e = A + s m y = h + s C h m L B h = A + s m y = h + s C
42 rexcom4 m L B h h = A + s m y = h + s C h m L B h = A + s m y = h + s C
43 ovex A + s m V
44 oveq1 h = A + s m h + s C = A + s m + s C
45 44 eqeq2d h = A + s m y = h + s C y = A + s m + s C
46 43 45 ceqsexv h h = A + s m y = h + s C y = A + s m + s C
47 46 rexbii m L B h h = A + s m y = h + s C m L B y = A + s m + s C
48 r19.41v m L B h = A + s m y = h + s C m L B h = A + s m y = h + s C
49 48 exbii h m L B h = A + s m y = h + s C h m L B h = A + s m y = h + s C
50 42 47 49 3bitr3ri h m L B h = A + s m y = h + s C m L B y = A + s m + s C
51 41 50 bitri h e | m L B e = A + s m y = h + s C m L B y = A + s m + s C
52 38 51 orbi12i h d | l L A d = l + s B y = h + s C h e | m L B e = A + s m y = h + s C l L A y = l + s B + s C m L B y = A + s m + s C
53 25 52 bitri h d | l L A d = l + s B e | m L B e = A + s m y = h + s C l L A y = l + s B + s C m L B y = A + s m + s C
54 53 abbii y | h d | l L A d = l + s B e | m L B e = A + s m y = h + s C = y | l L A y = l + s B + s C m L B y = A + s m + s C
55 20 24 54 3eqtr4ri y | h d | l L A d = l + s B e | m L B e = A + s m y = h + s C = y | l L A y = l + s B + s C z | m L B z = A + s m + s C
56 55 uneq1i y | h d | l L A d = l + s B e | m L B e = A + s m y = h + 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
57 unab a | p R A a = p + s B + s C a | q R B a = A + s q + s C = a | p R A a = p + s B + s C q R B a = A + s q + s C
58 eqeq1 b = a b = A + s q + s C a = A + s q + s C
59 58 rexbidv b = a q R B b = A + s q + s C q R B a = A + s q + s C
60 59 cbvabv b | q R B b = A + s q + s C = a | q R B a = A + s q + s C
61 60 uneq2i a | p R A a = p + s B + s C b | q R B b = A + s q + s C = a | p R A a = p + s B + s C a | q R B a = A + s q + s C
62 rexun i f | p R A f = p + s B g | q R B g = A + s q a = i + s C i f | p R A f = p + s B a = i + s C i g | q R B g = A + s q a = i + s C
63 eqeq1 f = i f = p + s B i = p + s B
64 63 rexbidv f = i p R A f = p + s B p R A i = p + s B
65 64 rexab i f | p R A f = p + s B a = i + s C i p R A i = p + s B a = i + s C
66 rexcom4 p R A i i = p + s B a = i + s C i p R A i = p + s B a = i + s C
67 ovex p + s B V
68 oveq1 i = p + s B i + s C = p + s B + s C
69 68 eqeq2d i = p + s B a = i + s C a = p + s B + s C
70 67 69 ceqsexv i i = p + s B a = i + s C a = p + s B + s C
71 70 rexbii p R A i i = p + s B a = i + s C p R A a = p + s B + s C
72 r19.41v p R A i = p + s B a = i + s C p R A i = p + s B a = i + s C
73 72 exbii i p R A i = p + s B a = i + s C i p R A i = p + s B a = i + s C
74 66 71 73 3bitr3ri i p R A i = p + s B a = i + s C p R A a = p + s B + s C
75 65 74 bitri i f | p R A f = p + s B a = i + s C p R A a = p + s B + s C
76 eqeq1 g = i g = A + s q i = A + s q
77 76 rexbidv g = i q R B g = A + s q q R B i = A + s q
78 77 rexab i g | q R B g = A + s q a = i + s C i q R B i = A + s q a = i + s C
79 rexcom4 q R B i i = A + s q a = i + s C i q R B i = A + s q a = i + s C
80 ovex A + s q V
81 oveq1 i = A + s q i + s C = A + s q + s C
82 81 eqeq2d i = A + s q a = i + s C a = A + s q + s C
83 80 82 ceqsexv i i = A + s q a = i + s C a = A + s q + s C
84 83 rexbii q R B i i = A + s q a = i + s C q R B a = A + s q + s C
85 r19.41v q R B i = A + s q a = i + s C q R B i = A + s q a = i + s C
86 85 exbii i q R B i = A + s q a = i + s C i q R B i = A + s q a = i + s C
87 79 84 86 3bitr3ri i q R B i = A + s q a = i + s C q R B a = A + s q + s C
88 78 87 bitri i g | q R B g = A + s q a = i + s C q R B a = A + s q + s C
89 75 88 orbi12i i f | p R A f = p + s B a = i + s C i g | q R B g = A + s q a = i + s C p R A a = p + s B + s C q R B a = A + s q + s C
90 62 89 bitri i f | p R A f = p + s B g | q R B g = A + s q a = i + s C p R A a = p + s B + s C q R B a = A + s q + s C
91 90 abbii a | i f | p R A f = p + s B g | q R B g = A + s q a = i + s C = a | p R A a = p + s B + s C q R B a = A + s q + s C
92 57 61 91 3eqtr4ri a | i f | p R A f = p + s B g | q R B g = A + s q a = i + s C = a | p R A a = p + s B + s C b | q R B b = A + s q + s C
93 92 uneq1i a | i f | p R A f = p + s B g | q R B g = A + s q a = i + 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
94 56 93 oveq12i y | h d | l L A d = l + s B e | m L B e = A + s m y = h + s C w | n L C w = A + s B + s n | s a | i f | p R A f = p + s B g | q R B g = A + s q a = i + s C c | r R C c = A + s B + s r = 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
95 19 94 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