Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  addsass Structured version   Visualization version   GIF version

Theorem addsass 34303
Description: Surreal addition is associative. Part of theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 22-Jan-2025.)
Assertion
Ref Expression
addsass ((𝐴 No 𝐵 No 𝐶 No ) → ((𝐴 +s 𝐵) +s 𝐶) = (𝐴 +s (𝐵 +s 𝐶)))

Proof of Theorem addsass
Dummy variables 𝑥 𝑦 𝑧 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑥O 𝑦O 𝑧O 𝑥L 𝑦L 𝑧L 𝑥R 𝑦R 𝑧R are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 7358 . . . 4 (𝑥 = 𝑥O → (𝑥 +s 𝑦) = (𝑥O +s 𝑦))
21oveq1d 7366 . . 3 (𝑥 = 𝑥O → ((𝑥 +s 𝑦) +s 𝑧) = ((𝑥O +s 𝑦) +s 𝑧))
3 oveq1 7358 . . 3 (𝑥 = 𝑥O → (𝑥 +s (𝑦 +s 𝑧)) = (𝑥O +s (𝑦 +s 𝑧)))
42, 3eqeq12d 2753 . 2 (𝑥 = 𝑥O → (((𝑥 +s 𝑦) +s 𝑧) = (𝑥 +s (𝑦 +s 𝑧)) ↔ ((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧))))
5 oveq2 7359 . . . 4 (𝑦 = 𝑦O → (𝑥O +s 𝑦) = (𝑥O +s 𝑦O))
65oveq1d 7366 . . 3 (𝑦 = 𝑦O → ((𝑥O +s 𝑦) +s 𝑧) = ((𝑥O +s 𝑦O) +s 𝑧))
7 oveq1 7358 . . . 4 (𝑦 = 𝑦O → (𝑦 +s 𝑧) = (𝑦O +s 𝑧))
87oveq2d 7367 . . 3 (𝑦 = 𝑦O → (𝑥O +s (𝑦 +s 𝑧)) = (𝑥O +s (𝑦O +s 𝑧)))
96, 8eqeq12d 2753 . 2 (𝑦 = 𝑦O → (((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ↔ ((𝑥O +s 𝑦O) +s 𝑧) = (𝑥O +s (𝑦O +s 𝑧))))
10 oveq2 7359 . . 3 (𝑧 = 𝑧O → ((𝑥O +s 𝑦O) +s 𝑧) = ((𝑥O +s 𝑦O) +s 𝑧O))
11 oveq2 7359 . . . 4 (𝑧 = 𝑧O → (𝑦O +s 𝑧) = (𝑦O +s 𝑧O))
1211oveq2d 7367 . . 3 (𝑧 = 𝑧O → (𝑥O +s (𝑦O +s 𝑧)) = (𝑥O +s (𝑦O +s 𝑧O)))
1310, 12eqeq12d 2753 . 2 (𝑧 = 𝑧O → (((𝑥O +s 𝑦O) +s 𝑧) = (𝑥O +s (𝑦O +s 𝑧)) ↔ ((𝑥O +s 𝑦O) +s 𝑧O) = (𝑥O +s (𝑦O +s 𝑧O))))
14 oveq1 7358 . . . 4 (𝑥 = 𝑥O → (𝑥 +s 𝑦O) = (𝑥O +s 𝑦O))
1514oveq1d 7366 . . 3 (𝑥 = 𝑥O → ((𝑥 +s 𝑦O) +s 𝑧O) = ((𝑥O +s 𝑦O) +s 𝑧O))
16 oveq1 7358 . . 3 (𝑥 = 𝑥O → (𝑥 +s (𝑦O +s 𝑧O)) = (𝑥O +s (𝑦O +s 𝑧O)))
1715, 16eqeq12d 2753 . 2 (𝑥 = 𝑥O → (((𝑥 +s 𝑦O) +s 𝑧O) = (𝑥 +s (𝑦O +s 𝑧O)) ↔ ((𝑥O +s 𝑦O) +s 𝑧O) = (𝑥O +s (𝑦O +s 𝑧O))))
18 oveq2 7359 . . . 4 (𝑦 = 𝑦O → (𝑥 +s 𝑦) = (𝑥 +s 𝑦O))
1918oveq1d 7366 . . 3 (𝑦 = 𝑦O → ((𝑥 +s 𝑦) +s 𝑧O) = ((𝑥 +s 𝑦O) +s 𝑧O))
20 oveq1 7358 . . . 4 (𝑦 = 𝑦O → (𝑦 +s 𝑧O) = (𝑦O +s 𝑧O))
2120oveq2d 7367 . . 3 (𝑦 = 𝑦O → (𝑥 +s (𝑦 +s 𝑧O)) = (𝑥 +s (𝑦O +s 𝑧O)))
2219, 21eqeq12d 2753 . 2 (𝑦 = 𝑦O → (((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)) ↔ ((𝑥 +s 𝑦O) +s 𝑧O) = (𝑥 +s (𝑦O +s 𝑧O))))
235oveq1d 7366 . . 3 (𝑦 = 𝑦O → ((𝑥O +s 𝑦) +s 𝑧O) = ((𝑥O +s 𝑦O) +s 𝑧O))
2420oveq2d 7367 . . 3 (𝑦 = 𝑦O → (𝑥O +s (𝑦 +s 𝑧O)) = (𝑥O +s (𝑦O +s 𝑧O)))
2523, 24eqeq12d 2753 . 2 (𝑦 = 𝑦O → (((𝑥O +s 𝑦) +s 𝑧O) = (𝑥O +s (𝑦 +s 𝑧O)) ↔ ((𝑥O +s 𝑦O) +s 𝑧O) = (𝑥O +s (𝑦O +s 𝑧O))))
26 oveq2 7359 . . 3 (𝑧 = 𝑧O → ((𝑥 +s 𝑦O) +s 𝑧) = ((𝑥 +s 𝑦O) +s 𝑧O))
2711oveq2d 7367 . . 3 (𝑧 = 𝑧O → (𝑥 +s (𝑦O +s 𝑧)) = (𝑥 +s (𝑦O +s 𝑧O)))
2826, 27eqeq12d 2753 . 2 (𝑧 = 𝑧O → (((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ↔ ((𝑥 +s 𝑦O) +s 𝑧O) = (𝑥 +s (𝑦O +s 𝑧O))))
29 oveq1 7358 . . . 4 (𝑥 = 𝐴 → (𝑥 +s 𝑦) = (𝐴 +s 𝑦))
3029oveq1d 7366 . . 3 (𝑥 = 𝐴 → ((𝑥 +s 𝑦) +s 𝑧) = ((𝐴 +s 𝑦) +s 𝑧))
31 oveq1 7358 . . 3 (𝑥 = 𝐴 → (𝑥 +s (𝑦 +s 𝑧)) = (𝐴 +s (𝑦 +s 𝑧)))
3230, 31eqeq12d 2753 . 2 (𝑥 = 𝐴 → (((𝑥 +s 𝑦) +s 𝑧) = (𝑥 +s (𝑦 +s 𝑧)) ↔ ((𝐴 +s 𝑦) +s 𝑧) = (𝐴 +s (𝑦 +s 𝑧))))
33 oveq2 7359 . . . 4 (𝑦 = 𝐵 → (𝐴 +s 𝑦) = (𝐴 +s 𝐵))
3433oveq1d 7366 . . 3 (𝑦 = 𝐵 → ((𝐴 +s 𝑦) +s 𝑧) = ((𝐴 +s 𝐵) +s 𝑧))
35 oveq1 7358 . . . 4 (𝑦 = 𝐵 → (𝑦 +s 𝑧) = (𝐵 +s 𝑧))
3635oveq2d 7367 . . 3 (𝑦 = 𝐵 → (𝐴 +s (𝑦 +s 𝑧)) = (𝐴 +s (𝐵 +s 𝑧)))
3734, 36eqeq12d 2753 . 2 (𝑦 = 𝐵 → (((𝐴 +s 𝑦) +s 𝑧) = (𝐴 +s (𝑦 +s 𝑧)) ↔ ((𝐴 +s 𝐵) +s 𝑧) = (𝐴 +s (𝐵 +s 𝑧))))
38 oveq2 7359 . . 3 (𝑧 = 𝐶 → ((𝐴 +s 𝐵) +s 𝑧) = ((𝐴 +s 𝐵) +s 𝐶))
39 oveq2 7359 . . . 4 (𝑧 = 𝐶 → (𝐵 +s 𝑧) = (𝐵 +s 𝐶))
4039oveq2d 7367 . . 3 (𝑧 = 𝐶 → (𝐴 +s (𝐵 +s 𝑧)) = (𝐴 +s (𝐵 +s 𝐶)))
4138, 40eqeq12d 2753 . 2 (𝑧 = 𝐶 → (((𝐴 +s 𝐵) +s 𝑧) = (𝐴 +s (𝐵 +s 𝑧)) ↔ ((𝐴 +s 𝐵) +s 𝐶) = (𝐴 +s (𝐵 +s 𝐶))))
42 simp21 1206 . . . 4 (((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥O +s 𝑦O) +s 𝑧O) = (𝑥O +s (𝑦O +s 𝑧O)) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥O +s 𝑦O) +s 𝑧) = (𝑥O +s (𝑦O +s 𝑧)) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥O +s 𝑦) +s 𝑧O) = (𝑥O +s (𝑦 +s 𝑧O))) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦O) +s 𝑧O) = (𝑥 +s (𝑦O +s 𝑧O)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧))) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O))) → ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)))
43 simp23 1208 . . . 4 (((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥O +s 𝑦O) +s 𝑧O) = (𝑥O +s (𝑦O +s 𝑧O)) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥O +s 𝑦O) +s 𝑧) = (𝑥O +s (𝑦O +s 𝑧)) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥O +s 𝑦) +s 𝑧O) = (𝑥O +s (𝑦 +s 𝑧O))) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦O) +s 𝑧O) = (𝑥 +s (𝑦O +s 𝑧O)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧))) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O))) → ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)))
44 simp3 1138 . . . 4 (((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥O +s 𝑦O) +s 𝑧O) = (𝑥O +s (𝑦O +s 𝑧O)) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥O +s 𝑦O) +s 𝑧) = (𝑥O +s (𝑦O +s 𝑧)) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥O +s 𝑦) +s 𝑧O) = (𝑥O +s (𝑦 +s 𝑧O))) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦O) +s 𝑧O) = (𝑥 +s (𝑦O +s 𝑧O)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧))) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O))) → ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))
4542, 43, 443jca 1128 . . 3 (((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥O +s 𝑦O) +s 𝑧O) = (𝑥O +s (𝑦O +s 𝑧O)) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥O +s 𝑦O) +s 𝑧) = (𝑥O +s (𝑦O +s 𝑧)) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥O +s 𝑦) +s 𝑧O) = (𝑥O +s (𝑦 +s 𝑧O))) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦O) +s 𝑧O) = (𝑥 +s (𝑦O +s 𝑧O)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧))) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O))) → (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O))))
46 oveq1 7358 . . . . . . . . . . . . . 14 (𝑥O = 𝑥L → (𝑥O +s 𝑦) = (𝑥L +s 𝑦))
4746oveq1d 7366 . . . . . . . . . . . . 13 (𝑥O = 𝑥L → ((𝑥O +s 𝑦) +s 𝑧) = ((𝑥L +s 𝑦) +s 𝑧))
48 oveq1 7358 . . . . . . . . . . . . 13 (𝑥O = 𝑥L → (𝑥O +s (𝑦 +s 𝑧)) = (𝑥L +s (𝑦 +s 𝑧)))
4947, 48eqeq12d 2753 . . . . . . . . . . . 12 (𝑥O = 𝑥L → (((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ↔ ((𝑥L +s 𝑦) +s 𝑧) = (𝑥L +s (𝑦 +s 𝑧))))
50 simplr1 1215 . . . . . . . . . . . 12 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑥L ∈ ( L ‘𝑥)) → ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)))
51 elun1 4134 . . . . . . . . . . . . 13 (𝑥L ∈ ( L ‘𝑥) → 𝑥L ∈ (( L ‘𝑥) ∪ ( R ‘𝑥)))
5251adantl 482 . . . . . . . . . . . 12 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑥L ∈ ( L ‘𝑥)) → 𝑥L ∈ (( L ‘𝑥) ∪ ( R ‘𝑥)))
5349, 50, 52rspcdva 3580 . . . . . . . . . . 11 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑥L ∈ ( L ‘𝑥)) → ((𝑥L +s 𝑦) +s 𝑧) = (𝑥L +s (𝑦 +s 𝑧)))
5453eqeq2d 2748 . . . . . . . . . 10 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑥L ∈ ( L ‘𝑥)) → (𝑎 = ((𝑥L +s 𝑦) +s 𝑧) ↔ 𝑎 = (𝑥L +s (𝑦 +s 𝑧))))
5554rexbidva 3171 . . . . . . . . 9 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → (∃𝑥L ∈ ( L ‘𝑥)𝑎 = ((𝑥L +s 𝑦) +s 𝑧) ↔ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s (𝑦 +s 𝑧))))
5655abbidv 2806 . . . . . . . 8 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → {𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = ((𝑥L +s 𝑦) +s 𝑧)} = {𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s (𝑦 +s 𝑧))})
57 oveq2 7359 . . . . . . . . . . . . . 14 (𝑦O = 𝑦L → (𝑥 +s 𝑦O) = (𝑥 +s 𝑦L))
5857oveq1d 7366 . . . . . . . . . . . . 13 (𝑦O = 𝑦L → ((𝑥 +s 𝑦O) +s 𝑧) = ((𝑥 +s 𝑦L) +s 𝑧))
59 oveq1 7358 . . . . . . . . . . . . . 14 (𝑦O = 𝑦L → (𝑦O +s 𝑧) = (𝑦L +s 𝑧))
6059oveq2d 7367 . . . . . . . . . . . . 13 (𝑦O = 𝑦L → (𝑥 +s (𝑦O +s 𝑧)) = (𝑥 +s (𝑦L +s 𝑧)))
6158, 60eqeq12d 2753 . . . . . . . . . . . 12 (𝑦O = 𝑦L → (((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ↔ ((𝑥 +s 𝑦L) +s 𝑧) = (𝑥 +s (𝑦L +s 𝑧))))
62 simplr2 1216 . . . . . . . . . . . 12 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑦L ∈ ( L ‘𝑦)) → ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)))
63 elun1 4134 . . . . . . . . . . . . 13 (𝑦L ∈ ( L ‘𝑦) → 𝑦L ∈ (( L ‘𝑦) ∪ ( R ‘𝑦)))
6463adantl 482 . . . . . . . . . . . 12 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑦L ∈ ( L ‘𝑦)) → 𝑦L ∈ (( L ‘𝑦) ∪ ( R ‘𝑦)))
6561, 62, 64rspcdva 3580 . . . . . . . . . . 11 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑦L ∈ ( L ‘𝑦)) → ((𝑥 +s 𝑦L) +s 𝑧) = (𝑥 +s (𝑦L +s 𝑧)))
6665eqeq2d 2748 . . . . . . . . . 10 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑦L ∈ ( L ‘𝑦)) → (𝑏 = ((𝑥 +s 𝑦L) +s 𝑧) ↔ 𝑏 = (𝑥 +s (𝑦L +s 𝑧))))
6766rexbidva 3171 . . . . . . . . 9 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → (∃𝑦L ∈ ( L ‘𝑦)𝑏 = ((𝑥 +s 𝑦L) +s 𝑧) ↔ ∃𝑦L ∈ ( L ‘𝑦)𝑏 = (𝑥 +s (𝑦L +s 𝑧))))
6867abbidv 2806 . . . . . . . 8 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → {𝑏 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑏 = ((𝑥 +s 𝑦L) +s 𝑧)} = {𝑏 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑏 = (𝑥 +s (𝑦L +s 𝑧))})
6956, 68uneq12d 4122 . . . . . . 7 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = ((𝑥L +s 𝑦) +s 𝑧)} ∪ {𝑏 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑏 = ((𝑥 +s 𝑦L) +s 𝑧)}) = ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s (𝑦 +s 𝑧))} ∪ {𝑏 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑏 = (𝑥 +s (𝑦L +s 𝑧))}))
70 oveq2 7359 . . . . . . . . . . . 12 (𝑧O = 𝑧L → ((𝑥 +s 𝑦) +s 𝑧O) = ((𝑥 +s 𝑦) +s 𝑧L))
71 oveq2 7359 . . . . . . . . . . . . 13 (𝑧O = 𝑧L → (𝑦 +s 𝑧O) = (𝑦 +s 𝑧L))
7271oveq2d 7367 . . . . . . . . . . . 12 (𝑧O = 𝑧L → (𝑥 +s (𝑦 +s 𝑧O)) = (𝑥 +s (𝑦 +s 𝑧L)))
7370, 72eqeq12d 2753 . . . . . . . . . . 11 (𝑧O = 𝑧L → (((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)) ↔ ((𝑥 +s 𝑦) +s 𝑧L) = (𝑥 +s (𝑦 +s 𝑧L))))
74 simplr3 1217 . . . . . . . . . . 11 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑧L ∈ ( L ‘𝑧)) → ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))
75 elun1 4134 . . . . . . . . . . . 12 (𝑧L ∈ ( L ‘𝑧) → 𝑧L ∈ (( L ‘𝑧) ∪ ( R ‘𝑧)))
7675adantl 482 . . . . . . . . . . 11 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑧L ∈ ( L ‘𝑧)) → 𝑧L ∈ (( L ‘𝑧) ∪ ( R ‘𝑧)))
7773, 74, 76rspcdva 3580 . . . . . . . . . 10 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑧L ∈ ( L ‘𝑧)) → ((𝑥 +s 𝑦) +s 𝑧L) = (𝑥 +s (𝑦 +s 𝑧L)))
7877eqeq2d 2748 . . . . . . . . 9 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑧L ∈ ( L ‘𝑧)) → (𝑐 = ((𝑥 +s 𝑦) +s 𝑧L) ↔ 𝑐 = (𝑥 +s (𝑦 +s 𝑧L))))
7978rexbidva 3171 . . . . . . . 8 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → (∃𝑧L ∈ ( L ‘𝑧)𝑐 = ((𝑥 +s 𝑦) +s 𝑧L) ↔ ∃𝑧L ∈ ( L ‘𝑧)𝑐 = (𝑥 +s (𝑦 +s 𝑧L))))
8079abbidv 2806 . . . . . . 7 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → {𝑐 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑐 = ((𝑥 +s 𝑦) +s 𝑧L)} = {𝑐 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑐 = (𝑥 +s (𝑦 +s 𝑧L))})
8169, 80uneq12d 4122 . . . . . 6 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → (({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = ((𝑥L +s 𝑦) +s 𝑧)} ∪ {𝑏 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑏 = ((𝑥 +s 𝑦L) +s 𝑧)}) ∪ {𝑐 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑐 = ((𝑥 +s 𝑦) +s 𝑧L)}) = (({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s (𝑦 +s 𝑧))} ∪ {𝑏 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑏 = (𝑥 +s (𝑦L +s 𝑧))}) ∪ {𝑐 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑐 = (𝑥 +s (𝑦 +s 𝑧L))}))
82 oveq1 7358 . . . . . . . . . . . . . 14 (𝑥O = 𝑥R → (𝑥O +s 𝑦) = (𝑥R +s 𝑦))
8382oveq1d 7366 . . . . . . . . . . . . 13 (𝑥O = 𝑥R → ((𝑥O +s 𝑦) +s 𝑧) = ((𝑥R +s 𝑦) +s 𝑧))
84 oveq1 7358 . . . . . . . . . . . . 13 (𝑥O = 𝑥R → (𝑥O +s (𝑦 +s 𝑧)) = (𝑥R +s (𝑦 +s 𝑧)))
8583, 84eqeq12d 2753 . . . . . . . . . . . 12 (𝑥O = 𝑥R → (((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ↔ ((𝑥R +s 𝑦) +s 𝑧) = (𝑥R +s (𝑦 +s 𝑧))))
86 simplr1 1215 . . . . . . . . . . . 12 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑥R ∈ ( R ‘𝑥)) → ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)))
87 elun2 4135 . . . . . . . . . . . . 13 (𝑥R ∈ ( R ‘𝑥) → 𝑥R ∈ (( L ‘𝑥) ∪ ( R ‘𝑥)))
8887adantl 482 . . . . . . . . . . . 12 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑥R ∈ ( R ‘𝑥)) → 𝑥R ∈ (( L ‘𝑥) ∪ ( R ‘𝑥)))
8985, 86, 88rspcdva 3580 . . . . . . . . . . 11 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑥R ∈ ( R ‘𝑥)) → ((𝑥R +s 𝑦) +s 𝑧) = (𝑥R +s (𝑦 +s 𝑧)))
9089eqeq2d 2748 . . . . . . . . . 10 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑥R ∈ ( R ‘𝑥)) → (𝑑 = ((𝑥R +s 𝑦) +s 𝑧) ↔ 𝑑 = (𝑥R +s (𝑦 +s 𝑧))))
9190rexbidva 3171 . . . . . . . . 9 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → (∃𝑥R ∈ ( R ‘𝑥)𝑑 = ((𝑥R +s 𝑦) +s 𝑧) ↔ ∃𝑥R ∈ ( R ‘𝑥)𝑑 = (𝑥R +s (𝑦 +s 𝑧))))
9291abbidv 2806 . . . . . . . 8 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → {𝑑 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑑 = ((𝑥R +s 𝑦) +s 𝑧)} = {𝑑 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑑 = (𝑥R +s (𝑦 +s 𝑧))})
93 oveq2 7359 . . . . . . . . . . . . . 14 (𝑦O = 𝑦R → (𝑥 +s 𝑦O) = (𝑥 +s 𝑦R))
9493oveq1d 7366 . . . . . . . . . . . . 13 (𝑦O = 𝑦R → ((𝑥 +s 𝑦O) +s 𝑧) = ((𝑥 +s 𝑦R) +s 𝑧))
95 oveq1 7358 . . . . . . . . . . . . . 14 (𝑦O = 𝑦R → (𝑦O +s 𝑧) = (𝑦R +s 𝑧))
9695oveq2d 7367 . . . . . . . . . . . . 13 (𝑦O = 𝑦R → (𝑥 +s (𝑦O +s 𝑧)) = (𝑥 +s (𝑦R +s 𝑧)))
9794, 96eqeq12d 2753 . . . . . . . . . . . 12 (𝑦O = 𝑦R → (((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ↔ ((𝑥 +s 𝑦R) +s 𝑧) = (𝑥 +s (𝑦R +s 𝑧))))
98 simplr2 1216 . . . . . . . . . . . 12 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑦R ∈ ( R ‘𝑦)) → ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)))
99 elun2 4135 . . . . . . . . . . . . 13 (𝑦R ∈ ( R ‘𝑦) → 𝑦R ∈ (( L ‘𝑦) ∪ ( R ‘𝑦)))
10099adantl 482 . . . . . . . . . . . 12 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑦R ∈ ( R ‘𝑦)) → 𝑦R ∈ (( L ‘𝑦) ∪ ( R ‘𝑦)))
10197, 98, 100rspcdva 3580 . . . . . . . . . . 11 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑦R ∈ ( R ‘𝑦)) → ((𝑥 +s 𝑦R) +s 𝑧) = (𝑥 +s (𝑦R +s 𝑧)))
102101eqeq2d 2748 . . . . . . . . . 10 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑦R ∈ ( R ‘𝑦)) → (𝑒 = ((𝑥 +s 𝑦R) +s 𝑧) ↔ 𝑒 = (𝑥 +s (𝑦R +s 𝑧))))
103102rexbidva 3171 . . . . . . . . 9 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → (∃𝑦R ∈ ( R ‘𝑦)𝑒 = ((𝑥 +s 𝑦R) +s 𝑧) ↔ ∃𝑦R ∈ ( R ‘𝑦)𝑒 = (𝑥 +s (𝑦R +s 𝑧))))
104103abbidv 2806 . . . . . . . 8 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → {𝑒 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑒 = ((𝑥 +s 𝑦R) +s 𝑧)} = {𝑒 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑒 = (𝑥 +s (𝑦R +s 𝑧))})
10592, 104uneq12d 4122 . . . . . . 7 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → ({𝑑 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑑 = ((𝑥R +s 𝑦) +s 𝑧)} ∪ {𝑒 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑒 = ((𝑥 +s 𝑦R) +s 𝑧)}) = ({𝑑 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑑 = (𝑥R +s (𝑦 +s 𝑧))} ∪ {𝑒 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑒 = (𝑥 +s (𝑦R +s 𝑧))}))
106 oveq2 7359 . . . . . . . . . . . 12 (𝑧O = 𝑧R → ((𝑥 +s 𝑦) +s 𝑧O) = ((𝑥 +s 𝑦) +s 𝑧R))
107 oveq2 7359 . . . . . . . . . . . . 13 (𝑧O = 𝑧R → (𝑦 +s 𝑧O) = (𝑦 +s 𝑧R))
108107oveq2d 7367 . . . . . . . . . . . 12 (𝑧O = 𝑧R → (𝑥 +s (𝑦 +s 𝑧O)) = (𝑥 +s (𝑦 +s 𝑧R)))
109106, 108eqeq12d 2753 . . . . . . . . . . 11 (𝑧O = 𝑧R → (((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)) ↔ ((𝑥 +s 𝑦) +s 𝑧R) = (𝑥 +s (𝑦 +s 𝑧R))))
110 simplr3 1217 . . . . . . . . . . 11 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑧R ∈ ( R ‘𝑧)) → ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))
111 elun2 4135 . . . . . . . . . . . 12 (𝑧R ∈ ( R ‘𝑧) → 𝑧R ∈ (( L ‘𝑧) ∪ ( R ‘𝑧)))
112111adantl 482 . . . . . . . . . . 11 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑧R ∈ ( R ‘𝑧)) → 𝑧R ∈ (( L ‘𝑧) ∪ ( R ‘𝑧)))
113109, 110, 112rspcdva 3580 . . . . . . . . . 10 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑧R ∈ ( R ‘𝑧)) → ((𝑥 +s 𝑦) +s 𝑧R) = (𝑥 +s (𝑦 +s 𝑧R)))
114113eqeq2d 2748 . . . . . . . . 9 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) ∧ 𝑧R ∈ ( R ‘𝑧)) → (𝑓 = ((𝑥 +s 𝑦) +s 𝑧R) ↔ 𝑓 = (𝑥 +s (𝑦 +s 𝑧R))))
115114rexbidva 3171 . . . . . . . 8 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → (∃𝑧R ∈ ( R ‘𝑧)𝑓 = ((𝑥 +s 𝑦) +s 𝑧R) ↔ ∃𝑧R ∈ ( R ‘𝑧)𝑓 = (𝑥 +s (𝑦 +s 𝑧R))))
116115abbidv 2806 . . . . . . 7 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → {𝑓 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑓 = ((𝑥 +s 𝑦) +s 𝑧R)} = {𝑓 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑓 = (𝑥 +s (𝑦 +s 𝑧R))})
117105, 116uneq12d 4122 . . . . . 6 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → (({𝑑 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑑 = ((𝑥R +s 𝑦) +s 𝑧)} ∪ {𝑒 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑒 = ((𝑥 +s 𝑦R) +s 𝑧)}) ∪ {𝑓 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑓 = ((𝑥 +s 𝑦) +s 𝑧R)}) = (({𝑑 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑑 = (𝑥R +s (𝑦 +s 𝑧))} ∪ {𝑒 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑒 = (𝑥 +s (𝑦R +s 𝑧))}) ∪ {𝑓 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑓 = (𝑥 +s (𝑦 +s 𝑧R))}))
11881, 117oveq12d 7369 . . . . 5 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → ((({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = ((𝑥L +s 𝑦) +s 𝑧)} ∪ {𝑏 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑏 = ((𝑥 +s 𝑦L) +s 𝑧)}) ∪ {𝑐 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑐 = ((𝑥 +s 𝑦) +s 𝑧L)}) |s (({𝑑 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑑 = ((𝑥R +s 𝑦) +s 𝑧)} ∪ {𝑒 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑒 = ((𝑥 +s 𝑦R) +s 𝑧)}) ∪ {𝑓 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑓 = ((𝑥 +s 𝑦) +s 𝑧R)})) = ((({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s (𝑦 +s 𝑧))} ∪ {𝑏 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑏 = (𝑥 +s (𝑦L +s 𝑧))}) ∪ {𝑐 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑐 = (𝑥 +s (𝑦 +s 𝑧L))}) |s (({𝑑 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑑 = (𝑥R +s (𝑦 +s 𝑧))} ∪ {𝑒 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑒 = (𝑥 +s (𝑦R +s 𝑧))}) ∪ {𝑓 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑓 = (𝑥 +s (𝑦 +s 𝑧R))})))
119 simpl1 1191 . . . . . 6 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → 𝑥 No )
120 simpl2 1192 . . . . . 6 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → 𝑦 No )
121 simpl3 1193 . . . . . 6 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → 𝑧 No )
122119, 120, 121addsasslem1 34301 . . . . 5 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → ((𝑥 +s 𝑦) +s 𝑧) = ((({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = ((𝑥L +s 𝑦) +s 𝑧)} ∪ {𝑏 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑏 = ((𝑥 +s 𝑦L) +s 𝑧)}) ∪ {𝑐 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑐 = ((𝑥 +s 𝑦) +s 𝑧L)}) |s (({𝑑 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑑 = ((𝑥R +s 𝑦) +s 𝑧)} ∪ {𝑒 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑒 = ((𝑥 +s 𝑦R) +s 𝑧)}) ∪ {𝑓 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑓 = ((𝑥 +s 𝑦) +s 𝑧R)})))
123119, 120, 121addsasslem2 34302 . . . . 5 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → (𝑥 +s (𝑦 +s 𝑧)) = ((({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s (𝑦 +s 𝑧))} ∪ {𝑏 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑏 = (𝑥 +s (𝑦L +s 𝑧))}) ∪ {𝑐 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑐 = (𝑥 +s (𝑦 +s 𝑧L))}) |s (({𝑑 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑑 = (𝑥R +s (𝑦 +s 𝑧))} ∪ {𝑒 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑒 = (𝑥 +s (𝑦R +s 𝑧))}) ∪ {𝑓 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑓 = (𝑥 +s (𝑦 +s 𝑧R))})))
124118, 122, 1233eqtr4d 2787 . . . 4 (((𝑥 No 𝑦 No 𝑧 No ) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O)))) → ((𝑥 +s 𝑦) +s 𝑧) = (𝑥 +s (𝑦 +s 𝑧)))
125124ex 413 . . 3 ((𝑥 No 𝑦 No 𝑧 No ) → ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O))) → ((𝑥 +s 𝑦) +s 𝑧) = (𝑥 +s (𝑦 +s 𝑧))))
12645, 125syl5 34 . 2 ((𝑥 No 𝑦 No 𝑧 No ) → (((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥O +s 𝑦O) +s 𝑧O) = (𝑥O +s (𝑦O +s 𝑧O)) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥O +s 𝑦O) +s 𝑧) = (𝑥O +s (𝑦O +s 𝑧)) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥O +s 𝑦) +s 𝑧O) = (𝑥O +s (𝑦 +s 𝑧O))) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥O +s 𝑦) +s 𝑧) = (𝑥O +s (𝑦 +s 𝑧)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦O) +s 𝑧O) = (𝑥 +s (𝑦O +s 𝑧O)) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑥 +s 𝑦O) +s 𝑧) = (𝑥 +s (𝑦O +s 𝑧))) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧O) = (𝑥 +s (𝑦 +s 𝑧O))) → ((𝑥 +s 𝑦) +s 𝑧) = (𝑥 +s (𝑦 +s 𝑧))))
1274, 9, 13, 17, 22, 25, 28, 32, 37, 41, 126no3inds 34266 1 ((𝐴 No 𝐵 No 𝐶 No ) → ((𝐴 +s 𝐵) +s 𝐶) = (𝐴 +s (𝐵 +s 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087   = wceq 1541  wcel 2106  {cab 2714  wral 3062  wrex 3071  cun 3906  cfv 6493  (class class class)co 7351   No csur 26939   |s cscut 27073   L cleft 27126   R cright 27127   +s cadds 34267
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7664
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-ot 4593  df-uni 4864  df-int 4906  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-ord 6318  df-on 6319  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7307  df-ov 7354  df-oprab 7355  df-mpo 7356  df-1st 7913  df-2nd 7914  df-frecs 8204  df-wrecs 8235  df-recs 8309  df-1o 8404  df-2o 8405  df-no 26942  df-slt 26943  df-bday 26944  df-sle 27044  df-sslt 27072  df-scut 27074  df-0s 27114  df-made 27128  df-old 27129  df-left 27131  df-right 27132  df-nadd 34215  df-norec2 34257  df-adds 34268
This theorem is referenced by:  addsassd  34304
  Copyright terms: Public domain W3C validator