| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq1 7438 | . . 3
⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s (𝑦 +s 𝑧)) = (𝑥𝑂 ·s
(𝑦 +s 𝑧))) | 
| 2 |  | oveq1 7438 | . . . 4
⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s 𝑦) = (𝑥𝑂 ·s
𝑦)) | 
| 3 |  | oveq1 7438 | . . . 4
⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s 𝑧) = (𝑥𝑂 ·s
𝑧)) | 
| 4 | 2, 3 | oveq12d 7449 | . . 3
⊢ (𝑥 = 𝑥𝑂 → ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))) | 
| 5 | 1, 4 | eqeq12d 2753 | . 2
⊢ (𝑥 = 𝑥𝑂 → ((𝑥 ·s (𝑦 +s 𝑧)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧)) ↔ (𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧)))) | 
| 6 |  | oveq1 7438 | . . . 4
⊢ (𝑦 = 𝑦𝑂 → (𝑦 +s 𝑧) = (𝑦𝑂 +s 𝑧)) | 
| 7 | 6 | oveq2d 7447 | . . 3
⊢ (𝑦 = 𝑦𝑂 → (𝑥𝑂
·s (𝑦
+s 𝑧)) = (𝑥𝑂
·s (𝑦𝑂 +s 𝑧))) | 
| 8 |  | oveq2 7439 | . . . 4
⊢ (𝑦 = 𝑦𝑂 → (𝑥𝑂
·s 𝑦) =
(𝑥𝑂
·s 𝑦𝑂)) | 
| 9 | 8 | oveq1d 7446 | . . 3
⊢ (𝑦 = 𝑦𝑂 → ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧))) | 
| 10 | 7, 9 | eqeq12d 2753 | . 2
⊢ (𝑦 = 𝑦𝑂 → ((𝑥𝑂
·s (𝑦
+s 𝑧)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧)) ↔ (𝑥𝑂
·s (𝑦𝑂 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧)))) | 
| 11 |  | oveq2 7439 | . . . 4
⊢ (𝑧 = 𝑧𝑂 → (𝑦𝑂
+s 𝑧) = (𝑦𝑂
+s 𝑧𝑂)) | 
| 12 | 11 | oveq2d 7447 | . . 3
⊢ (𝑧 = 𝑧𝑂 → (𝑥𝑂
·s (𝑦𝑂 +s 𝑧)) = (𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂))) | 
| 13 |  | oveq2 7439 | . . . 4
⊢ (𝑧 = 𝑧𝑂 → (𝑥𝑂
·s 𝑧) =
(𝑥𝑂
·s 𝑧𝑂)) | 
| 14 | 13 | oveq2d 7447 | . . 3
⊢ (𝑧 = 𝑧𝑂 → ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧)) =
((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧𝑂))) | 
| 15 | 12, 14 | eqeq12d 2753 | . 2
⊢ (𝑧 = 𝑧𝑂 → ((𝑥𝑂
·s (𝑦𝑂 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧)) ↔ (𝑥𝑂
·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧𝑂)))) | 
| 16 |  | oveq1 7438 | . . 3
⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s (𝑦𝑂
+s 𝑧𝑂)) = (𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂))) | 
| 17 |  | oveq1 7438 | . . . 4
⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s 𝑦𝑂) = (𝑥𝑂
·s 𝑦𝑂)) | 
| 18 |  | oveq1 7438 | . . . 4
⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s 𝑧𝑂) = (𝑥𝑂
·s 𝑧𝑂)) | 
| 19 | 17, 18 | oveq12d 7449 | . . 3
⊢ (𝑥 = 𝑥𝑂 → ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))) | 
| 20 | 16, 19 | eqeq12d 2753 | . 2
⊢ (𝑥 = 𝑥𝑂 → ((𝑥 ·s (𝑦𝑂
+s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂) +s (𝑥 ·s 𝑧𝑂)) ↔
(𝑥𝑂
·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧𝑂)))) | 
| 21 |  | oveq1 7438 | . . . 4
⊢ (𝑦 = 𝑦𝑂 → (𝑦 +s 𝑧𝑂) = (𝑦𝑂
+s 𝑧𝑂)) | 
| 22 | 21 | oveq2d 7447 | . . 3
⊢ (𝑦 = 𝑦𝑂 → (𝑥 ·s (𝑦 +s 𝑧𝑂)) = (𝑥 ·s (𝑦𝑂
+s 𝑧𝑂))) | 
| 23 |  | oveq2 7439 | . . . 4
⊢ (𝑦 = 𝑦𝑂 → (𝑥 ·s 𝑦) = (𝑥 ·s 𝑦𝑂)) | 
| 24 | 23 | oveq1d 7446 | . . 3
⊢ (𝑦 = 𝑦𝑂 → ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂))) | 
| 25 | 22, 24 | eqeq12d 2753 | . 2
⊢ (𝑦 = 𝑦𝑂 → ((𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)) ↔
(𝑥 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂) +s (𝑥 ·s 𝑧𝑂)))) | 
| 26 | 21 | oveq2d 7447 | . . 3
⊢ (𝑦 = 𝑦𝑂 → (𝑥𝑂
·s (𝑦
+s 𝑧𝑂)) = (𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂))) | 
| 27 | 8 | oveq1d 7446 | . . 3
⊢ (𝑦 = 𝑦𝑂 → ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)) =
((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧𝑂))) | 
| 28 | 26, 27 | eqeq12d 2753 | . 2
⊢ (𝑦 = 𝑦𝑂 → ((𝑥𝑂
·s (𝑦
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧𝑂)) ↔ (𝑥𝑂
·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧𝑂)))) | 
| 29 | 11 | oveq2d 7447 | . . 3
⊢ (𝑧 = 𝑧𝑂 → (𝑥 ·s (𝑦𝑂
+s 𝑧)) = (𝑥 ·s (𝑦𝑂
+s 𝑧𝑂))) | 
| 30 |  | oveq2 7439 | . . . 4
⊢ (𝑧 = 𝑧𝑂 → (𝑥 ·s 𝑧) = (𝑥 ·s 𝑧𝑂)) | 
| 31 | 30 | oveq2d 7447 | . . 3
⊢ (𝑧 = 𝑧𝑂 → ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)) =
((𝑥 ·s
𝑦𝑂)
+s (𝑥
·s 𝑧𝑂))) | 
| 32 | 29, 31 | eqeq12d 2753 | . 2
⊢ (𝑧 = 𝑧𝑂 → ((𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧))
↔ (𝑥
·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)))) | 
| 33 |  | oveq1 7438 | . . 3
⊢ (𝑥 = 𝐴 → (𝑥 ·s (𝑦 +s 𝑧)) = (𝐴 ·s (𝑦 +s 𝑧))) | 
| 34 |  | oveq1 7438 | . . . 4
⊢ (𝑥 = 𝐴 → (𝑥 ·s 𝑦) = (𝐴 ·s 𝑦)) | 
| 35 |  | oveq1 7438 | . . . 4
⊢ (𝑥 = 𝐴 → (𝑥 ·s 𝑧) = (𝐴 ·s 𝑧)) | 
| 36 | 34, 35 | oveq12d 7449 | . . 3
⊢ (𝑥 = 𝐴 → ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧)) = ((𝐴 ·s 𝑦) +s (𝐴 ·s 𝑧))) | 
| 37 | 33, 36 | eqeq12d 2753 | . 2
⊢ (𝑥 = 𝐴 → ((𝑥 ·s (𝑦 +s 𝑧)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧)) ↔ (𝐴 ·s (𝑦 +s 𝑧)) = ((𝐴 ·s 𝑦) +s (𝐴 ·s 𝑧)))) | 
| 38 |  | oveq1 7438 | . . . 4
⊢ (𝑦 = 𝐵 → (𝑦 +s 𝑧) = (𝐵 +s 𝑧)) | 
| 39 | 38 | oveq2d 7447 | . . 3
⊢ (𝑦 = 𝐵 → (𝐴 ·s (𝑦 +s 𝑧)) = (𝐴 ·s (𝐵 +s 𝑧))) | 
| 40 |  | oveq2 7439 | . . . 4
⊢ (𝑦 = 𝐵 → (𝐴 ·s 𝑦) = (𝐴 ·s 𝐵)) | 
| 41 | 40 | oveq1d 7446 | . . 3
⊢ (𝑦 = 𝐵 → ((𝐴 ·s 𝑦) +s (𝐴 ·s 𝑧)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑧))) | 
| 42 | 39, 41 | eqeq12d 2753 | . 2
⊢ (𝑦 = 𝐵 → ((𝐴 ·s (𝑦 +s 𝑧)) = ((𝐴 ·s 𝑦) +s (𝐴 ·s 𝑧)) ↔ (𝐴 ·s (𝐵 +s 𝑧)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑧)))) | 
| 43 |  | oveq2 7439 | . . . 4
⊢ (𝑧 = 𝐶 → (𝐵 +s 𝑧) = (𝐵 +s 𝐶)) | 
| 44 | 43 | oveq2d 7447 | . . 3
⊢ (𝑧 = 𝐶 → (𝐴 ·s (𝐵 +s 𝑧)) = (𝐴 ·s (𝐵 +s 𝐶))) | 
| 45 |  | oveq2 7439 | . . . 4
⊢ (𝑧 = 𝐶 → (𝐴 ·s 𝑧) = (𝐴 ·s 𝐶)) | 
| 46 | 45 | oveq2d 7447 | . . 3
⊢ (𝑧 = 𝐶 → ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑧)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝐶))) | 
| 47 | 44, 46 | eqeq12d 2753 | . 2
⊢ (𝑧 = 𝐶 → ((𝐴 ·s (𝐵 +s 𝑧)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑧)) ↔ (𝐴 ·s (𝐵 +s 𝐶)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝐶)))) | 
| 48 |  | simpl1 1192 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → 𝑥 ∈ 
No ) | 
| 49 |  | simpl2 1193 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → 𝑦 ∈ 
No ) | 
| 50 |  | simpl3 1194 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → 𝑧 ∈ 
No ) | 
| 51 |  | simpr21 1261 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s (𝑦
+s 𝑧)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧))) | 
| 52 |  | simpr23 1263 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧))) | 
| 53 |  | simpr12 1259 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥𝑂
·s (𝑦𝑂 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧))) | 
| 54 |  | elun1 4182 | . . . . . . . . . . . . 13
⊢ (𝑥𝐿 ∈ ( L
‘𝑥) → 𝑥𝐿 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) | 
| 55 | 54 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑦𝐿 ∈ ( L
‘𝑦)) → 𝑥𝐿 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) | 
| 56 |  | elun1 4182 | . . . . . . . . . . . . 13
⊢ (𝑦𝐿 ∈ ( L
‘𝑦) → 𝑦𝐿 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))) | 
| 57 | 56 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑦𝐿 ∈ ( L
‘𝑦)) → 𝑦𝐿 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))) | 
| 58 | 48, 49, 50, 51, 52, 53, 55, 57 | addsdilem3 28179 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑦𝐿 ∈ ( L
‘𝑦))) → (((𝑥𝐿
·s (𝑦
+s 𝑧))
+s (𝑥
·s (𝑦𝐿 +s 𝑧))) -s (𝑥𝐿
·s (𝑦𝐿 +s 𝑧))) = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))) | 
| 59 | 58 | eqeq2d 2748 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑦𝐿 ∈ ( L
‘𝑦))) → (𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝐿
+s 𝑧))) ↔
𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧)))) | 
| 60 | 59 | 2rexbidva 3220 | . . . . . . . . 9
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝐿
+s 𝑧))) ↔
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧)))) | 
| 61 | 60 | abbidv 2808 | . . . . . . . 8
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝐿
+s 𝑧)))} =
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}) | 
| 62 |  | simpr3 1197 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → ∀𝑧𝑂 ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂))) | 
| 63 |  | simpr13 1260 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))∀𝑧𝑂 ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))(𝑥𝑂
·s (𝑦
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧𝑂))) | 
| 64 | 54 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑧𝐿 ∈ ( L
‘𝑧)) → 𝑥𝐿 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) | 
| 65 |  | elun1 4182 | . . . . . . . . . . . . 13
⊢ (𝑧𝐿 ∈ ( L
‘𝑧) → 𝑧𝐿 ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))) | 
| 66 | 65 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑧𝐿 ∈ ( L
‘𝑧)) → 𝑧𝐿 ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))) | 
| 67 | 48, 49, 50, 51, 62, 63, 64, 66 | addsdilem4 28180 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑧𝐿 ∈ ( L
‘𝑧))) → (((𝑥𝐿
·s (𝑦
+s 𝑧))
+s (𝑥
·s (𝑦
+s 𝑧𝐿))) -s (𝑥𝐿
·s (𝑦
+s 𝑧𝐿))) = ((𝑥 ·s 𝑦) +s (((𝑥𝐿
·s 𝑧)
+s (𝑥
·s 𝑧𝐿)) -s (𝑥𝐿
·s 𝑧𝐿)))) | 
| 68 | 67 | eqeq2d 2748 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑧𝐿 ∈ ( L
‘𝑧))) → (𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝐿))) ↔
𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝐿 ·s
𝑧𝐿))))) | 
| 69 | 68 | 2rexbidva 3220 | . . . . . . . . 9
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝐿))) ↔
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝐿 ·s
𝑧𝐿))))) | 
| 70 | 69 | abbidv 2808 | . . . . . . . 8
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝐿)))} =
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝐿 ·s
𝑧𝐿)))}) | 
| 71 | 61, 70 | uneq12d 4169 | . . . . . . 7
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝐿
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝐿)))}) =
({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝐿 ·s
𝑧𝐿)))})) | 
| 72 |  | elun2 4183 | . . . . . . . . . . . . 13
⊢ (𝑥𝑅 ∈ ( R
‘𝑥) → 𝑥𝑅 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) | 
| 73 | 72 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑦𝑅 ∈ ( R
‘𝑦)) → 𝑥𝑅 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) | 
| 74 |  | elun2 4183 | . . . . . . . . . . . . 13
⊢ (𝑦𝑅 ∈ ( R
‘𝑦) → 𝑦𝑅 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))) | 
| 75 | 74 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑦𝑅 ∈ ( R
‘𝑦)) → 𝑦𝑅 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))) | 
| 76 | 48, 49, 50, 51, 52, 53, 73, 75 | addsdilem3 28179 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑦𝑅 ∈ ( R
‘𝑦))) → (((𝑥𝑅
·s (𝑦
+s 𝑧))
+s (𝑥
·s (𝑦𝑅 +s 𝑧))) -s (𝑥𝑅
·s (𝑦𝑅 +s 𝑧))) = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))) | 
| 77 | 76 | eqeq2d 2748 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑦𝑅 ∈ ( R
‘𝑦))) → (𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝑅
+s 𝑧))) ↔
𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧)))) | 
| 78 | 77 | 2rexbidva 3220 | . . . . . . . . 9
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝑅
+s 𝑧))) ↔
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧)))) | 
| 79 | 78 | abbidv 2808 | . . . . . . . 8
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝑅
+s 𝑧)))} =
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}) | 
| 80 | 72 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑧𝑅 ∈ ( R
‘𝑧)) → 𝑥𝑅 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) | 
| 81 |  | elun2 4183 | . . . . . . . . . . . . 13
⊢ (𝑧𝑅 ∈ ( R
‘𝑧) → 𝑧𝑅 ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))) | 
| 82 | 81 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑧𝑅 ∈ ( R
‘𝑧)) → 𝑧𝑅 ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))) | 
| 83 | 48, 49, 50, 51, 62, 63, 80, 82 | addsdilem4 28180 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑧𝑅 ∈ ( R
‘𝑧))) → (((𝑥𝑅
·s (𝑦
+s 𝑧))
+s (𝑥
·s (𝑦
+s 𝑧𝑅))) -s (𝑥𝑅
·s (𝑦
+s 𝑧𝑅))) = ((𝑥 ·s 𝑦) +s (((𝑥𝑅
·s 𝑧)
+s (𝑥
·s 𝑧𝑅)) -s (𝑥𝑅
·s 𝑧𝑅)))) | 
| 84 | 83 | eqeq2d 2748 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑧𝑅 ∈ ( R
‘𝑧))) → (𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝑅))) ↔
𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝑅 ·s
𝑧𝑅))))) | 
| 85 | 84 | 2rexbidva 3220 | . . . . . . . . 9
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝑅))) ↔
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝑅 ·s
𝑧𝑅))))) | 
| 86 | 85 | abbidv 2808 | . . . . . . . 8
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝑅)))} =
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝑅 ·s
𝑧𝑅)))}) | 
| 87 | 79, 86 | uneq12d 4169 | . . . . . . 7
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝑅
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝑅)))}) =
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝑅 ·s
𝑧𝑅)))})) | 
| 88 | 71, 87 | uneq12d 4169 | . . . . . 6
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝐿
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝐿)))}) ∪
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝑅
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝑅)))})) =
(({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝐿 ·s
𝑧𝐿)))})
∪ ({𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝑅 ·s
𝑧𝑅)))}))) | 
| 89 |  | un4 4175 | . . . . . 6
⊢ (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝐿 ·s
𝑧𝐿)))})
∪ ({𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝑅 ·s
𝑧𝑅)))}))
= (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝐿 ·s
𝑧𝐿)))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝑅 ·s
𝑧𝑅)))})) | 
| 90 | 88, 89 | eqtrdi 2793 | . . . . 5
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝐿
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝐿)))}) ∪
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝑅
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝑅)))})) =
(({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝐿 ·s
𝑧𝐿)))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝑅 ·s
𝑧𝑅)))}))) | 
| 91 | 54 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑦𝑅 ∈ ( R
‘𝑦)) → 𝑥𝐿 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) | 
| 92 | 74 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑦𝑅 ∈ ( R
‘𝑦)) → 𝑦𝑅 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))) | 
| 93 | 48, 49, 50, 51, 52, 53, 91, 92 | addsdilem3 28179 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑦𝑅 ∈ ( R
‘𝑦))) → (((𝑥𝐿
·s (𝑦
+s 𝑧))
+s (𝑥
·s (𝑦𝑅 +s 𝑧))) -s (𝑥𝐿
·s (𝑦𝑅 +s 𝑧))) = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))) | 
| 94 | 93 | eqeq2d 2748 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑦𝑅 ∈ ( R
‘𝑦))) → (𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝑅
+s 𝑧))) ↔
𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧)))) | 
| 95 | 94 | 2rexbidva 3220 | . . . . . . . . 9
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝑅
+s 𝑧))) ↔
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧)))) | 
| 96 | 95 | abbidv 2808 | . . . . . . . 8
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝑅
+s 𝑧)))} =
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}) | 
| 97 | 54 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑧𝑅 ∈ ( R
‘𝑧)) → 𝑥𝐿 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) | 
| 98 | 81 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑧𝑅 ∈ ( R
‘𝑧)) → 𝑧𝑅 ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))) | 
| 99 | 48, 49, 50, 51, 62, 63, 97, 98 | addsdilem4 28180 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑧𝑅 ∈ ( R
‘𝑧))) → (((𝑥𝐿
·s (𝑦
+s 𝑧))
+s (𝑥
·s (𝑦
+s 𝑧𝑅))) -s (𝑥𝐿
·s (𝑦
+s 𝑧𝑅))) = ((𝑥 ·s 𝑦) +s (((𝑥𝐿
·s 𝑧)
+s (𝑥
·s 𝑧𝑅)) -s (𝑥𝐿
·s 𝑧𝑅)))) | 
| 100 | 99 | eqeq2d 2748 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝐿 ∈ ( L
‘𝑥) ∧ 𝑧𝑅 ∈ ( R
‘𝑧))) → (𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝑅))) ↔
𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝐿 ·s
𝑧𝑅))))) | 
| 101 | 100 | 2rexbidva 3220 | . . . . . . . . 9
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝑅))) ↔
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝐿 ·s
𝑧𝑅))))) | 
| 102 | 101 | abbidv 2808 | . . . . . . . 8
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝑅)))} =
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝐿 ·s
𝑧𝑅)))}) | 
| 103 | 96, 102 | uneq12d 4169 | . . . . . . 7
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝑅
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝑅)))}) =
({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝐿 ·s
𝑧𝑅)))})) | 
| 104 | 72 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑦𝐿 ∈ ( L
‘𝑦)) → 𝑥𝑅 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) | 
| 105 | 56 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑦𝐿 ∈ ( L
‘𝑦)) → 𝑦𝐿 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))) | 
| 106 | 48, 49, 50, 51, 52, 53, 104, 105 | addsdilem3 28179 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑦𝐿 ∈ ( L
‘𝑦))) → (((𝑥𝑅
·s (𝑦
+s 𝑧))
+s (𝑥
·s (𝑦𝐿 +s 𝑧))) -s (𝑥𝑅
·s (𝑦𝐿 +s 𝑧))) = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))) | 
| 107 | 106 | eqeq2d 2748 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑦𝐿 ∈ ( L
‘𝑦))) → (𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝐿
+s 𝑧))) ↔
𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧)))) | 
| 108 | 107 | 2rexbidva 3220 | . . . . . . . . 9
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝐿
+s 𝑧))) ↔
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧)))) | 
| 109 | 108 | abbidv 2808 | . . . . . . . 8
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝐿
+s 𝑧)))} =
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}) | 
| 110 | 72 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑧𝐿 ∈ ( L
‘𝑧)) → 𝑥𝑅 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) | 
| 111 | 65 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑧𝐿 ∈ ( L
‘𝑧)) → 𝑧𝐿 ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))) | 
| 112 | 48, 49, 50, 51, 62, 63, 110, 111 | addsdilem4 28180 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑧𝐿 ∈ ( L
‘𝑧))) → (((𝑥𝑅
·s (𝑦
+s 𝑧))
+s (𝑥
·s (𝑦
+s 𝑧𝐿))) -s (𝑥𝑅
·s (𝑦
+s 𝑧𝐿))) = ((𝑥 ·s 𝑦) +s (((𝑥𝑅
·s 𝑧)
+s (𝑥
·s 𝑧𝐿)) -s (𝑥𝑅
·s 𝑧𝐿)))) | 
| 113 | 112 | eqeq2d 2748 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) ∧ (𝑥𝑅 ∈ ( R
‘𝑥) ∧ 𝑧𝐿 ∈ ( L
‘𝑧))) → (𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝐿))) ↔
𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝑅 ·s
𝑧𝐿))))) | 
| 114 | 113 | 2rexbidva 3220 | . . . . . . . . 9
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝐿))) ↔
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝑅 ·s
𝑧𝐿))))) | 
| 115 | 114 | abbidv 2808 | . . . . . . . 8
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → {𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝐿)))} =
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝑅 ·s
𝑧𝐿)))}) | 
| 116 | 109, 115 | uneq12d 4169 | . . . . . . 7
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝐿
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝐿)))}) =
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝑅 ·s
𝑧𝐿)))})) | 
| 117 | 103, 116 | uneq12d 4169 | . . . . . 6
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝑅
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝑅)))}) ∪
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝐿
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝐿)))})) =
(({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝐿 ·s
𝑧𝑅)))})
∪ ({𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝑅 ·s
𝑧𝐿)))}))) | 
| 118 |  | un4 4175 | . . . . . 6
⊢ (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝐿 ·s
𝑧𝑅)))})
∪ ({𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝑅 ·s
𝑧𝐿)))}))
= (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝐿 ·s
𝑧𝑅)))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝑅 ·s
𝑧𝐿)))})) | 
| 119 | 117, 118 | eqtrdi 2793 | . . . . 5
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝑅
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝑅)))}) ∪
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝐿
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝐿)))})) =
(({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝐿 ·s
𝑧𝑅)))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝑅 ·s
𝑧𝐿)))}))) | 
| 120 | 90, 119 | oveq12d 7449 | . . . 4
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → ((({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝐿
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝐿)))}) ∪
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝑅
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝑅)))})) |s
(({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝑅
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝑅)))}) ∪
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝐿
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝐿)))}))) =
((({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝐿 ·s
𝑧𝐿)))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝑅 ·s
𝑧𝑅)))}))
|s (({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝐿 ·s
𝑧𝑅)))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝑅 ·s
𝑧𝐿)))})))) | 
| 121 | 48, 49, 50 | addsdilem1 28177 | . . . 4
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (𝑥 ·s (𝑦 +s 𝑧)) = ((({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝐿
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝐿)))}) ∪
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝑅
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝑅)))})) |s
(({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑦𝑅 ∈ ( R
‘𝑦)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝑅
+s 𝑧)))
-s (𝑥𝐿 ·s
(𝑦𝑅
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)∃𝑧𝑅 ∈ ( R
‘𝑧)𝑎 = (((𝑥𝐿 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝑅)))
-s (𝑥𝐿 ·s
(𝑦 +s 𝑧𝑅)))}) ∪
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑦𝐿 ∈ ( L
‘𝑦)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦𝐿
+s 𝑧)))
-s (𝑥𝑅 ·s
(𝑦𝐿
+s 𝑧)))} ∪
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)∃𝑧𝐿 ∈ ( L
‘𝑧)𝑎 = (((𝑥𝑅 ·s
(𝑦 +s 𝑧)) +s (𝑥 ·s (𝑦 +s 𝑧𝐿)))
-s (𝑥𝑅 ·s
(𝑦 +s 𝑧𝐿)))})))) | 
| 122 | 48, 49, 50 | addsdilem2 28178 | . . . 4
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧)) = ((({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝐿 ·s
𝑧𝐿)))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝑅 ·s
𝑧𝑅)))}))
|s (({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑦𝑅 ∈ ( R ‘𝑦)𝑎 = ((((𝑥𝐿 ·s
𝑦) +s (𝑥 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
+s (𝑥
·s 𝑧))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = ((((𝑥𝑅 ·s
𝑦) +s (𝑥 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
+s (𝑥
·s 𝑧))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑧𝑅 ∈ ( R ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝐿 ·s
𝑧) +s (𝑥 ·s 𝑧𝑅))
-s (𝑥𝐿 ·s
𝑧𝑅)))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)∃𝑧𝐿 ∈ ( L ‘𝑧)𝑎 = ((𝑥 ·s 𝑦) +s (((𝑥𝑅 ·s
𝑧) +s (𝑥 ·s 𝑧𝐿))
-s (𝑥𝑅 ·s
𝑧𝐿)))})))) | 
| 123 | 120, 121,
122 | 3eqtr4d 2787 | . . 3
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂)))) → (𝑥 ·s (𝑦 +s 𝑧)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧))) | 
| 124 | 123 | ex 412 | . 2
⊢ ((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
→ (((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧𝑂)) = ((𝑥𝑂 ·s
𝑦𝑂)
+s (𝑥𝑂 ·s
𝑧𝑂))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 ·s
(𝑦𝑂
+s 𝑧)) = ((𝑥𝑂
·s 𝑦𝑂) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥𝑂 ·s
(𝑦 +s 𝑧𝑂)) = ((𝑥𝑂
·s 𝑦)
+s (𝑥𝑂 ·s
𝑧𝑂)))
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
(𝑦 +s 𝑧)) = ((𝑥𝑂 ·s
𝑦) +s (𝑥𝑂
·s 𝑧))
∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦𝑂 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧𝑂)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 ·s (𝑦𝑂
+s 𝑧)) = ((𝑥 ·s 𝑦𝑂)
+s (𝑥
·s 𝑧)))
∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))(𝑥 ·s (𝑦 +s 𝑧𝑂)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧𝑂))) → (𝑥 ·s (𝑦 +s 𝑧)) = ((𝑥 ·s 𝑦) +s (𝑥 ·s 𝑧)))) | 
| 125 | 5, 10, 15, 20, 25, 28, 32, 37, 42, 47, 124 | no3inds 27991 | 1
⊢ ((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝐶 ∈  No )
→ (𝐴
·s (𝐵
+s 𝐶)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝐶))) |