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